Using XBDDs and ZBDDs in points‐to analysis

Binary decision diagrams (BDDs) have recently become widely accepted as a space‐efficient method of representing relations in points‐to or reference analyses. When BDDs are used to represent relations, each element of a domain is assigned a bit pattern to represent it, but not every bit pattern represents an element. The circuit design, model checking, and verification communities have achieved significant reductions in BDD sizes using several techniques to reduce the overhead of these don't‐care bit patterns. We adapt these techniques to BDD‐based program analysis, and we study their effect on the BDD size in this context. Specifically, we compare the effectiveness of Coudert and Madre's restrict operation and the use of zero‐suppressed BDDs (ZBDDs) to represent relations. Using don't‐care BDDs (XBDDs) and ZBDDs to reduce the size of the relations allows a compiler or other software analysis tools to analyze larger programs with greater precision. Our experimental evaluation considers both context‐insensitive and context‐sensitive program analyses. We also provide a metric that can be used to estimate whether ZBDDs will be more compact than BDDs for a given analysis. Copyright © 2008 John Wiley & Sons, Ltd.     

Reducing and manipulating complex trace data

In performance analysis of computer systems, trace-driven simulation techniques have the important advantage of credibility and accuracy. Unfortunately, traces are usually difficult to obtain, and little work has been done to provide efficient tools to help in the process of reducing and manipulating them. This paper presents TRAMP, a tool for the data reduction and data analysis phases of trace-driven simulation studies. TRAMP has three main advantages: it accepts a variety of common trace formats; it provides a programmable user interface in which many actions can be directly specified; and it is easy to extend. TRAMP is particularly helpful for reducing and analysing complex trace data, such as traces of file system or database activity. This paper presents the design principles and implementation techniques of TRAMP and provides a few concrete examples of the use of this tool.     

Abstract execution: A technique for efficiently tracing programs

Many areas of computer performance analysis require detailed traces of events that occur during a program's execution. Collecting traces is expensive. The additional code required to record events greatly slows a program's execution. In addition, the resulting trace files can grow unmanageably large. This paper describes a technique called abstract execution that alleviates both problems. Abstract execution records a small set of events during the traced program's execution. These events serve as input to an abstract version of the program that generates a full trace by re-executing selected portions of the original program. This process greatly reduces both the cost of tracing the original program and the size of the trace files. The cost of regenerating a trace is insignificant in comparison to the cost of applications that use it. This paper also describes a system called AE that implements Abstract Execution. The paper contains measurements that demonstrate that AE can efficiently trace large programs.     

BDD-based software verification

In software model checking, most successful symbolic approaches use predicates as representation of the state space, and SMT solvers for computations on the state space; BDDs are often used as auxiliary data structure. Although BDDs are applied with great success in hardware verification, BDD representations of software state spaces were not yet thoroughly investigated, mainly because not all operations that are needed in software verification are efficiently supported by BDDs. We evaluate the use of a pure BDD representation of integer values, and focus on a particular class of programs: event-condition-action (ECA) programs with limited operations. A symbolic representation using BDDs seems appropriate for ECA programs under certain conditions. We configure a program analysis based on BDDs and experimentally compare it to four approaches to verify reachability properties of ECA programs: an explicit-value analysis, a symbolic bounded-loops analysis, a predicate-abstraction analysis, and a predicate-impact analysis. The results show that BDDs are efficient for a restricted class of programs, which yields the insight that BDDs could be used selectively for variables that are restricted to certain program operations (according to the variable’s domain type), even in general software model checking. We show that even a naive portfolio approach, in which after a pre-analysis either a BDD-based analysis or a predicate-impact analysis is performed, outperforms all above-mentioned analyses.     

Compositional Analysis of C/C++ Programs with VeriSoft

This paper describes how the state space exploration ool VeriSoft can be used to analyze parallel C/C++ programs compositionally. VeriSoft is employed for two analyses: transition traceanalysis and assume/guarantee reasoning. Both analyses are compositional in the sense that the behaviour of a parallel program is determined in terms of the behaviour of its constituent processes. While both analyses have traditionally been carried out with “pencil and paper”, the paper demonstrates how VeriSoft can be used to automate them. In the context of transition trace analysis, the question whether a given program can exhibit a given trace is addressed with VeriSoft. To implement assume/guarantee reasoning, VeriSoft is used to determine whether a given program satisfies a given assume/guarantee specification. Since VeriSoft’s state space exploration is bounded and thus not complete in general, our proposed analyses are only meant to complement standard reasoning about parallel programs using traces or assume/guarantee specifications. For instance, a successful analysis does not always imply the general correctness of an assume/guarantee specification. However, it increases the confidence in the verification effort. On the other hand, an unsuccessful analysis always produces a counterexample which can be used to correct the specification or the program. VeriSoft’s optimization and visualization techniques make the analyses relatively efficient and effective.     

Modeling and simulation of circuits with shared structurally synthesized BDDs

Modeling and simulation are critical tools for the analysis of testability and verification of digital circuits. BDDs are a well-known model for manipulating Boolean functions. However, the traditional BDDs mainly address modeling the function of the digital circuits, and not the structural aspects that are important for testability analysis. We propose a new type of BDD in the form of Shared Structurally Synthesized BDD (S³BDD) for representing the structure and simulating the faults in digital circuits. The paper presents a method for synthesis of S³BDDs, offers a formula for calculating the minimal size of the model, and proposes a method for parallel pattern simulation with S³BDDs We demonstrate a considerable increase in the speed-up of simulation of digital circuits using S³BDDs.     

Accuracy of memory reference traces of parallel computations intrace-drive simulation

For given input the global trace generated by a parallel program in a shared memory multiprocessing environment may change as the memory architecture, and management policies change. A method is proposed for ensuring that a correct global trace is generated in the new environment. This method involves a new characterization of a parallel program that identifies its address change points and address affecting points. An extension of traditional process traces, called the intrinsic trace of each process, is developed. The intrinsic traces maximize the decoupling of program execution from simulation by describing the address flow graph and path expressions of each process program. At each point where an address is issued, the trace-driven simulator uses the intrinsic traces and the sequence of loads and stores before the current cycle, to determine the next address. The mapping between load and store sequences and next addresses to issue, sometimes, requires partial program reexecution. Programs that do not require partial program reexecution are called graph-traceable     

Exploiting traces in static program analysis: better model checking through {{\tt printf}}s

From operating systems and web browsers to spacecraft, many software systems maintain a log of events that provides a partial history of execution, supporting post-mortem (or post-reboot) analysis. Unfortunately, bandwidth, storage limitations, and privacy concerns limit the information content of logs, making it difficult to fully reconstruct execution from these traces. This paper presents a technique for modifying a program such that it can produce exactly those executions consistent with a given (partial) trace of events, enabling efficient analysis of the reduced program. Our method requires no additional history variables to track log events, and it can slice away code that does not execute in a given trace. We describe initial experiences with implementing our ideas by extending the CBMC bounded model checker for C programs. Applying our technique to a small, 400-line file system written in C, we get more than three orders of magnitude improvement in running time over a naïve approach based on adding history variables, along with fifty- to eighty-fold reductions in the sizes of the SAT problems solved.     

Cultural algorithm for minimization of binary decision diagram and its application in crosstalk fault detection

The binary decision diagrams (BDDs) can give canonical representation to Boolean functions; they have wide applications in the design and verification of digital systems. A new method based on cultural algorithms for minimizing the size of BDDs is presented in this paper. First of all, the coding of an individual representing a BDDs is given, and the fitness of an individual is defined. The population is built by a set of the individuals. Second, the implementations based on cultural algorithms for the minimization of BDDs, i.e., the designs of belief space and population space, and the designs of acceptance function and influence function, are given in detail. Third, the fault detection approaches using BDDs for digital circuits are studied. A new method for the detection of crosstalk faults by using BDDs is presented. Experimental results on a number of digital circuits show that the BDDs with small number of nodes can be obtained by the method proposed in this paper, and all test vectors of a fault in digital circuits can also be produced.     

Detection of strong unstable predicates in distributed programs

This paper discusses detection of global predicates in a distributed program. A run of a distributed program results in a set of sequential traces, one for each process. These traces may be combined to form many global sequences consistent with the single run of the program. A strong global predicate is true in a run if it is true for all global sequences consistent with the run. We present algorithms which detect if the given strong global predicate became true in a run of a distributed program. Our algorithms can be executed on line as well as off line. Moreover, our algorithms do not assume that underlying channels satisfy FIFO ordering     

TraceAnalyzer: a system for processing performance traces

The performance of a program often varies significantly over the course of the program's run. Thus, to understand the performance of a program it is valuable to look not just at end‐to‐end metrics (e.g. total number of cache misses) but also the time‐varying performance of the program. Unfortunately, analyzing time‐varying performance is both cumbersome and difficult. This paper makes three contributions, all geared toward helping others in working with traces. First, it describes a system, the TraceAnalyzer, designed specifically for working with performance traces; a performance trace captures the time‐varying performance of a program run. Second, it describes lessons that we have learned from many years of working with these traces. Finally, it uses a case study to demonstrate how we have used the TraceAnalyzer to understand a performance anomaly. Copyright © 2010 John Wiley & Sons, Ltd.     

Using passive testing based on symbolic execution and slicing techniques: Application to the validation of communication protocols

This paper presents a new approach to perform passive testing based on the analysis of the control and data part of the system under test. Passive testing techniques are based on the observation and verification of properties on the behaviour of a system without interfering with its normal operation. Many passive testing techniques consider only the control part of the system and neglect data, or are confronted with an overwhelming amount of data values to process. In our approach, we consider control and data parts by integrating the concepts of symbolic execution and we improve trace analysis by introducing trace slicing techniques. Properties are described using Input–Output Symbolic Transition Systems (IOSTSs) and we illustrate in the paper how they can be tested on real execution traces optimizing the trace analysis. These properties can be designed to test the functional conformance of a protocol as well as security properties.     

Grasp: Visualizing the behavior of hierarchical multiprocessor real-time systems

Trace visualization is a viable approach for gaining insight into the behavior of complex distributed real-time systems. Grasp is a versatile trace visualization toolset. Its flexible plugin infrastructure allows for easy extension with custom visualization and analysis techniques for automatic trace verification. This paper presents its visualization capabilities for hierarchical multiprocessor systems, including partitioned and global multiprocessor scheduling with migrating tasks and jobs, communication between jobs via shared memory and message passing, and hierarchical scheduling in combination with multiprocessor scheduling. For tracing distributed systems with asynchronous local clocks Grasp also supports the synchronization of traces from different processors during the visualization and analysis.     

Manipulating Wi‐Fi packet traces with WiPal: design and experience

Packet traces are important objects in networking, commonly used in a wide set of applications, including monitoring, troubleshooting, measurements, and validation, to cite a few. Many tools exist to produce and process such traces, but they are often too specific; using them as a basis for creating extended tools is then impractical. Some other tools are generic enough, but exhibit performance issues. This paper reports on our experience designing WiPal, a packet trace manipulation framework with a focus on IEEE 802.11. WiPal is designed for performance and re‐usability, while introducing several novel features compared to previous solutions. Besides presenting how WiPal's original design can benefit packet processing programs, we discuss a number of issues a program designer might encounter when writing packet trace processing software. An evaluation of WiPal shows that, albeit generic, it does not impact performance regarding execution speed. WiPal achieves performance levels observed only with specialized code and outperforms some well‐known packet processing programs. Copyright © 2011 John Wiley & Sons, Ltd.     

Asynchronous trace-matching automata

This paper presents algorithms for solving several matching problems on Mazurkiewicz traces. The creation of the algorithms is reduced to the construction of automata that recognize corresponding rational trace languages. Such languages and their properties were studied by many authors. This paper considers trace languages used in solving concrete problems that have analogs in stringology.     

BIFER: a biphasic trace filter approach to scalable prediction of concurrency errors

Predictive trace analysis (PTA), a static trace analysis technique for concurrent programs, can offer powerful capability support for finding concurrency errors unseen in a previous program execution. Existing PTA techniques always face considerable challenges in scaling to large traces which contain numerous critical events. One main reason is that an analyzed trace includes not only redundant memory accessing events and threads that cannot contribute to discovering any additional errors different from the found candidate ones, but also many residual synchronization events which still affect PTA to check whether these candidate ones are feasible or not even after removing the redundant events. Removing them from the trace can significantly improve the scalability of PTA without affecting the quality of the PTA results. In this paper, we propose a biphasic trace filter approach, BIFER in short, to filter these redundant events and residual events for improving the scalability of PTA to expose general concurrency errors. In addition, we design a model which indicates the lock history and the happens-before history of each thread with two kinds of ways to achieve the efficient filtering. We implement a prototypical tool BIFER for Java programs on the basis of a predictive trace analysis framework. Experiments show that BIFER can improve the scalability of PTA during the process of analyzing all of the traces.     

A performance analysis exemplar: Parallel ray tracing

Among the many techniques in computer graphics, ray tracing is prized because it can render realistic images, albeit at great computational expense. Ray tracing's large computation requirements, coupled with its inherently parallel nature, make ray tracing algorithms attractive candidates for parallel implementation. In this paper we illustrate the utility and the importance of a suite of performance analysis tools when exploring the performance of several approaches to ray tracing on a distributed memory parallel system. These ray tracing algorithm variations introduce parallelism based on both ray and object partitions. Traditional timing analysis can quantify the performance effects of different algorithm choices (i.e. when an algorithm is best matched to a given problem), but it cannot identify the causes of these performance differences. We argue, by example, that a performance instrumentation system is needed that can trace the execution of distributed memory parallel programs by recording the occurrence of parallel program events. The resulting event traces can be used to compile summary stapistics that provide a global view of program performance. In addition, visualization tools permit the graphic display of event traces. Visual presentation of performance data is particularly useful, indeed, necessary for large-scale, parallel computations; assimilating the enormous volume of performance data mandates visual display.     

A declarative framework for stateful analysis of execution traces

With newer complex multi-core systems, it is important to understand an application’s runtime behavior to be able to debug its execution, detect possible problems and bottlenecks and finally identify potential root causes. Execution traces usually contain precise data about an application execution. Their analysis and abstraction at multiple levels can provide valuable information and insights about an application’s runtime behavior. However, with multiple abstraction levels, it becomes increasingly difficult to find the exact location of detected performance or security problems. Tracing tools provide various analysis views to help users to understand their application problems. However, these pre-defined views are often not sufficient to reveal all analysis aspects of the underlying application. A declarative approach that enables users to specify and build their own custom analysis and views based on their knowledge, requirements and problems can be more useful and effective. In this paper, we propose a generic declarative trace analysis framework to analyze, comprehend and visualize execution traces. This enhanced framework builds custom analyses based on a specified modeled state, extracted from a system execution trace and stored in a special purpose database. The proposed solution enables users to first define their different analysis models based on their application and requirements, then visualize these models in many alternate representations (Gantt chart, XY chart, etc.), and finally filter the data to get some highlights or detect some potential patterns. Several sample applications with different operating systems are shown, using trace events gathered from Linux and Windows, at the kernel and user-space levels.     

Forbidden traces and forbidden subtraces

The concepts of forbidden strings and forbidden subsequences are generalized to traces. This paper presents algorithms for constructing sets of minimal forbidden traces and minimal forbidden subtraces for a given trace.