Symbolic predictive analysis for concurrent programs

Chao Wang, Sudipta Kundu, Malay Ganai, Aarti Gupta

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

46 Scopus citations

Abstract

Predictive analysis aims at detecting concurrency errors during runtime by monitoring a concrete execution trace of a concurrent program. In recent years, various models based on happens-before causality relations have been proposed for predictive analysis to improve the interleaving coverage while ensuring the absence of false alarms. However, these models are based on only the observed events, and typically do not utilize source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted execution traces often suffer from the interleaving explosion problem. In this paper, we introduce a new symbolic causal model based on source code and the observed events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events in the given execution trace. Rather than explicitly enumerating the interleavings, our algorithm conducts the verification using a novel encoding of the causal model and symbolic reasoning with a satisfiability modulo theory (SMT) solver. Our algorithm has a larger interleaving coverage than known causal models in the literature. We also propose a method to symbolically bound the number of context switches allowed in an interleaving, to further improve the scalability of the algorithm.

Original languageEnglish (US)
Title of host publicationFM 2009
Subtitle of host publicationFormal Methods - Second World Congress, Proceedings
Pages256-272
Number of pages17
DOIs
StatePublished - Dec 2 2009
Externally publishedYes
Event2nd World Congress on Formal Methods, FM 2009 - Eindhoven, Netherlands
Duration: Nov 2 2009Nov 6 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5850 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other2nd World Congress on Formal Methods, FM 2009
CountryNetherlands
CityEindhoven
Period11/2/0911/6/09

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Symbolic predictive analysis for concurrent programs'. Together they form a unique fingerprint.

  • Cite this

    Wang, C., Kundu, S., Ganai, M., & Gupta, A. (2009). Symbolic predictive analysis for concurrent programs. In FM 2009: Formal Methods - Second World Congress, Proceedings (pp. 256-272). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5850 LNCS). https://doi.org/10.1007/978-3-642-05089-3_17