Trace Based Analyses of Parallel Software

Abstract

A major challenge in the formal verification of parallel software is the large state space due to the numerous interleavings of events of interest across the concurrent threads. Trace-based verification/falsification addresses this by focusing on correctness criteria that depend on a single trace. Trace based <italic>monitoring</italic> validates the system behavior for the actual execution of this trace. Trace based <italic>predictive analysis</italic> goes a step further, by considering other interleavings that are related to the given trace and verifies the behavior for this set of interleavings. This dissertation presents both monitoring and predictive analysis techniques based on a single program trace for verifying consistency properties (such as serializability and determinism) for parallel software.

This dissertation explores an alternate direction in checking the serializability property of a state-of-the-art multi-threaded Software Transactional Memory (STM) implementation unlike existing model-based approaches. We propose the use of an independent serializability checker thread that runs in parallel to the main STM system and monitors it. <italic>Our approach minimizes the overhead of access logging and presents techniques for on-the-fly graph compaction that drastically reduce the size of the graph that needs to be maintained to be no larger than the number of threads.</italic>

Next, we address the problem of detecting serializability violations in a parallel program using predictive analysis, where a violation is detected either in an observed trace or in an alternate interleaving of events in that trace. The problem becomes intractable when all possible interleavings are considered. We address this in practice through a graph-based method, which for a given atomic block and trace, derives a smaller segment of the trace, referred to as the <italic>Trace Atomicity Segment (TAS)</italic>, for further systematic exploration. We use the observed write-read pairs of events in the given trace to consider a set of events that guarantee feasibility, i.e., each interleaving of these events corresponds to some real execution of the program. We call this set of interleavings the <italic>almost view-preserving (AVP)</italic> interleavings. <italic>We show that the TAS is sufficient for finding serializability violations among all AVP interleavings.</italic> Further, the TAS enables a simple static check that can prove the absence of a violation that often succeeds in practice. For the case where it fails, we propose a systematic exploration of event orders in the TAS, where we employ both explicit (Dynamic Partial Order Reduction) and implicit (Satisfiability Modulo Theory (SMT)-based) exploration techniques. The comparative experimental evaluation provides some insight into the characteristics of instances when one of these is superior to the other. This is useful for predicting the preferred technique for a given instance. Unlike previous efforts that are less precise, when our method reports a serializability violation, the reported interleaving is guaranteed to correspond to an actual execution of the program.

Further, we propose a predictive analysis technique to detect non-determinism in parallel programs. A parallel program is said to be deterministic if for a given input, different thread interleavings result in the same system state in the execution of the program. This, in turn, requires that different interleavings preserve the values read by each read operation. The key feature of our graph-based method is that it searches a reduced set of sufficient interleavings -- <italic>the average number of graphs analyzed (for checking cycles in them) is almost equal to the number of possible instances of non-determinism in practice.</italic>

In summary, this dissertation presents scalable techniques to catch or predict real violations in parallel software using execution traces.