Predictive analysis for detecting serializability violations through Trace Segmentation

Arnab Sinha, Sharad Malik, Chao Wang, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

23 Scopus citations

Abstract

We address the problem of detecting serializability violations in a concurrent program using predictive analysis, where a violation 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, derives a smaller segment of the trace, referred to as the Trace Atomicity Segment (TAS), 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 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 in detecting serializability violations for Java and C/C benchmark programs.

Original languageEnglish (US)
Title of host publication9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011
Pages99-108
Number of pages10
DOIs
StatePublished - Sep 1 2011
Event9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011 - Cambridge, United Kingdom
Duration: Jul 11 2011Jul 13 2011

Publication series

Name9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011

Other

Other9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011
CountryUnited Kingdom
CityCambridge
Period7/11/117/13/11

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Modeling and Simulation

Fingerprint Dive into the research topics of 'Predictive analysis for detecting serializability violations through Trace Segmentation'. Together they form a unique fingerprint.

Cite this