Semantic reduction of thread interleavings in concurrent programs

Vineet Kahlon, Sriram Sankaranarayanan, Aarti Gupta

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

20 Scopus citations

Abstract

We propose a static analysis framework for concurrent programs based on reduction of thread interleavings using sound invariants on the top of partial order techniques. Starting from a product graph that represents transactions, we iteratively refine the graph to remove statically unreachable nodes in the product graph using the results of these analyses. We use abstract interpretation to automatically derive program invariants, based on abstract domains of increasing precision. We demonstrate the benefits of this framework in an application to find data race bugs in concurrent programs, where our static analyses serve to reduce the number of false warnings captured by an initial lockset analysis. This framework also facilitates use of model checking on the remaining warnings to generate concrete error traces, where we leverage the preceding static analyses to generate small program slices and the derived invariants to improve scalability. We describe our experimental results on a suite of Linux device drivers.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 15th International Conference, TACAS 2009 - Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2009, Proc.
Pages124-138
Number of pages15
DOIs
StatePublished - Nov 9 2009
Externally publishedYes
Event15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009 - York, United Kingdom
Duration: Mar 22 2009Mar 29 2009

Publication series

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

Other

Other15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009
CountryUnited Kingdom
CityYork
Period3/22/093/29/09

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Semantic reduction of thread interleavings in concurrent programs'. Together they form a unique fingerprint.

  • Cite this

    Kahlon, V., Sankaranarayanan, S., & Gupta, A. (2009). Semantic reduction of thread interleavings in concurrent programs. In Tools and Algorithms for the Construction and Analysis of Systems - 15th International Conference, TACAS 2009 - Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2009, Proc. (pp. 124-138). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5505 LNCS). https://doi.org/10.1007/978-3-642-00768-2_12