AbstractsComputer Science

Trace Based Analyses of Parallel Software

by Arnab Sinha




Institution: Princeton University
Department: Electrical Engineering
Degree: PhD
Year: 2012
Keywords: Computer engineering; Electrical engineering; Computer science
Record ID: 1955688
Full text PDF: http://arks.princeton.edu/ark:/88435/dsp01tt44pm906


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…