Sciweavers

Share
CAV
2005
Springer

Reasoning About Threads Communicating via Locks

10 years 1 months ago
Reasoning About Threads Communicating via Locks
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 [10]. 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 aptandard 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. Thus not only yields decidability but also avoids construction of the state space of the concurrent program at hand and thus bypasses the ...
Vineet Kahlon, Franjo Ivancic, Aarti Gupta
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CAV
Authors Vineet Kahlon, Franjo Ivancic, Aarti Gupta
Comments (0)
books