Trace-based symbolic analysis for atomicity violations

Chao Wang, Rhishikesh Limaye, Malay Ganai, Aarti Gupta

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

41 Scopus citations

Abstract

We propose a symbolic algorithm to accurately predict atomicity violations by analyzing a concrete execution trace of a concurrent program. We use both the execution trace and the program source code to construct a symbolic predictive model, which captures a large set of alternative interleavings of the events of the given trace. We use precise symbolic reasoning with a satisfiability modulo theory (SMT) solver to check the feasible interleavings for atomicity violations. Our algorithm differs from the existing methods in that all reported atomicity violations can appear in the actual program execution; and at the same time the feasible interleavings analyzed by our model are significantly more than other predictive models that guarantee the absence of false alarms.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.
Pages328-342
Number of pages15
DOIs
StatePublished - May 3 2010
Externally publishedYes
Event16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010 - Paphos, Cyprus
Duration: Mar 20 2010Mar 28 2010

Publication series

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

Other

Other16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010
CountryCyprus
CityPaphos
Period3/20/103/28/10

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Trace-based symbolic analysis for atomicity violations'. Together they form a unique fingerprint.

  • Cite this

    Wang, C., Limaye, R., Ganai, M., & Gupta, A. (2010). Trace-based symbolic analysis for atomicity violations. In Tools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc. (pp. 328-342). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6015 LNCS). https://doi.org/10.1007/978-3-642-12002-2_27