Arnab Sinha
	sinha@princeton.edu www.princeton.edu/~sinha Princeton University Advisor: Sharad Malik GSRC theme:  resiliency Expected graduation:  Jul, 2012

Research Overview:  Trace Based Verification of Concurrent Software

Runtime Checking of Serializability in Software Transactional Memory

Abstract for paper in IEEE International Parallel & Distributed Processing Symposium (IPDPS) 2010

Ensuring the correctness of complex implementations of software transactional memory (STM) is a daunting task. Attempts have been made to formally verify STMs, but these are limited in the scale of systems they can handle and generally verify only a model of the system, and not the actual system. In this work we present an alternate attack on checking the correctness of an STM implementation by verifying the execution runs of an STM using a checker that runs in parallel with the transaction memory system. With future many-core systems predicted to have hundreds and even thousands of cores, it is reasonable to utilize some of these cores for ensuring the correctness of the rest of the system. This will be needed anyway given the increasing likelihood of dynamic errors due to particle hits (soft errors) and increasing fragility of nanoscale devices. These errors can only be detected at runtime. An important correctness criterion that is the subject of verification is the serializability of transactions. While checking transaction serializability is NP-complete, practically useful subclasses such as interchange serializability (DSR) are efficiently computable. Checking DSR reduces to checking for cycles in a transaction ordering graph which captures the access order of objects shared between transaction instances. Doing this concurrent to the main transaction execution requires minimizing the overhead of capturing object accesses, and managing the size of the graph, which can be as large as the total number of dynamic transactions and object accesses. We discuss techniques for minimizing the overhead of access logging which includes timestamping, and present 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. We have implemented concurrent serializability checking in the Rochester Software Transactional Memory (RSTM) system. We present our practical experiences with this including results for the RSTM, STAMP and synthetic benchmarks. The overhead of concurrent checking is a strong function of the transaction length. For long transactions this is negligible. Thus the use of the proposed method for continuous runtime checking is acceptable. For very short transactions this can be significant. In this case we see the applicability of the proposed method for debugging.

Predictive Analysis for Detecting Serializability Errors through Trace Segmentation

Abstract for paper submitted to Verification, Model Checking, and Abstract Interpretation (VMCAI) 2011

We address the problem of detecting serializability errors in a concurrent program using predictive analysis, where an error is detected either in an observed trace or in an alternate interleaving of events in that trace. Under the widely used notion of conflict-serializability, checking whether a given execution is serializable can be done in polynomial time. However, when all possible interleavings are considered, the problem becomes intractable. We address this in practice through a graph-based method, which for a given atomic block and trace, derive a smaller segment of the trace, referred to as the Trace Atomicity Segment (TAS), for further systematic exploration. We use the observed read-write 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 almost view-preserving (AVP) interleavings. We show that the TAS is sufficient for finding serializability violations among all AVP interleavings. Further, the TAS enables a simple static check that can prove the absence of a violation. This check often succeeds in practice. If it fails, we perform a systematic exploration over events in the TAS, where we use dynamic partial order reduction with additional pruning to reduce the number of interleavings considered. 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. We report experimental results that demonstrate the effectiveness of our method on some Java and C/C++ programs.