Reasoning about threads communicating via locks

Vineet Kahlon, Franjo Ivančić, Aarti Gupta

Research output: Contribution to journalConference article

69 Scopus citations

Abstract

We propose a new technique for the static analysis of concurrent programs comprised of multiple threads. In general, the problem is known to be undecidable even for programs with only two threads but where the threads communicate using CCS-style pairwise rendezvous [11]. However, in practice, a large fraction of concurrent programs can either be directly modeled as threads communicating solely using locks or can be reduced to such systems either by applying standard abstract interpretation techniques or by exploiting separation of control from data. For such a framework, we show that for the commonly occurring case of threads with nested access to locks, the problem is efficiently decidable. Our technique involves reducing the analysis of a concurrent program with multiple threads to individually analyzing augmented versions of the given threads. This not only yields decidability but also avoids construction of the state space of the concurrent program at hand and thus bypasses the state explosion problem making our technique scalable. We go on to show that for programs with threads that have non-nested access to locks, the static analysis problem for programs with even two threads becomes undecidable even for reachability, thus sharpening the result of [11]. As a case study, we consider the Daisy file system [1] which is a benchmark for analyzing the efficacy of different methodologies for debugging concurrent programs and provide results for the detection of several bugs.

Original languageEnglish (US)
Pages (from-to)505-518
Number of pages14
JournalLECTURE NOTES IN COMPUTER SCIENCE
Volume3576
DOIs
StatePublished - Jan 1 2005
Externally publishedYes
Event17th International Conference on Computer Aided Verification, CAV 2005 - Edinburgh, Scotland, United Kingdom
Duration: Jul 6 2005Jul 10 2005

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Reasoning about threads communicating via locks'. Together they form a unique fingerprint.

  • Cite this