Symbolic predictive analysis for concurrent programs

Chao Wang, Sudipta Kundu, Rhishikesh Limaye, Malay Ganai, Aarti Gupta

Research output: Contribution to journalArticle

7 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 the happens-before causality relations have been proposed for predictive analysis. However, these models often rely on only the observed runtime events and typically do not utilize the program source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted traces often suffer from the interleaving explosion problem. In this paper, we introduce a precise predictive model based on both the program source code and the observed execution events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events of the given trace. Rather than explicitly enumerating and checking the interleavings, our method conducts the search using a novel encoding and symbolic reasoning with a satisfiability modulo theory solver.We also propose a technique to bound the number of context switches allowed in the interleavings during the symbolic search, to further improve the scalability of the algorithm. BCS

Original languageEnglish (US)
Pages (from-to)781-805
Number of pages25
JournalFormal Aspects of Computing
Volume23
Issue number6
DOIs
StatePublished - Nov 1 2011
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Software
  • Theoretical Computer Science

Keywords

  • Concurrent trace program
  • Context bounding
  • Happens-before
  • Predictive analysis
  • SAT
  • SMT

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

  • Cite this