Dynamic model checking with property driven pruning to detect race conditions

Chao Wang, Yu Yang, Aarti Gupta, Ganesh Gopalakrishnan

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

19 Scopus citations

Abstract

We present a new property driven pruning algorithm in dynamic model checking to efficiently detect race conditions in multithreaded programs. The main idea is to use a lockset based analysis of observed executions to help prune the search space to be explored by the dynamic search. We assume that a stateless search algorithm is used to systematically execute the program in a depth-first search order. If our conservative lockset analysis shows that a search subspace is race-free, it can be pruned away by avoiding backtracks to certain states in the depth-first search. The new dynamic race detection algorithm is both sound and complete (as precise as the dynamic partial order reduction algorithm by Flanagan and Godefroid). The algorithm is also more efficient in practice, allowing it to scale much better to real-world multithreaded C programs.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings
Pages126-140
Number of pages15
Volume5311 LNCS
DOIs
StatePublished - Dec 1 2008
Externally publishedYes
Event6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008 - Seoul, Korea, Republic of
Duration: Oct 20 2008Oct 23 2008

Publication series

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

Other

Other6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008
CountryKorea, Republic of
CitySeoul
Period10/20/0810/23/08

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Dynamic model checking with property driven pruning to detect race conditions'. Together they form a unique fingerprint.

  • Cite this

    Wang, C., Yang, Y., Gupta, A., & Gopalakrishnan, G. (2008). Dynamic model checking with property driven pruning to detect race conditions. In Automated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings (Vol. 5311 LNCS, pp. 126-140). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5311 LNCS). https://doi.org/10.1007/978-3-540-88387-6-11