Reasoning about Threads with Bounded Lock Chains

11 years 1 months ago
Reasoning about Threads with Bounded Lock Chains
The problem of model checking threads interacting purely via the standard synchronization primitives is key for many concurrent program analyses, particularly dataflow analysis. Unfortunately, it is undecidable even for the most commonly used synchronization primitive, i.e., mutex locks. Lock usage in concurrent programs can be characterized in terms of lock chains, where a sequence of mutex locks is said to be chained if the scopes of adjacent (non-nested) mutexes overlap. Although the model checking problem for fragments of Linear Temporal Logic (LTL) is known to be decidable for threads interacting via nested locks, i.e., chains of length one, these techniques don’t extend to programs with non-nested locks used in crucial applications like databases. We exploit the fact that lock usage patterns in real life programs do not produce unbounded lock chains. For such a framework, we show, by using the new concept of Lock Causality Automata (LCA), that pre∗ -closures of regular sets ...
Vineet Kahlon
Added 18 Dec 2011
Updated 18 Dec 2011
Type Journal
Year 2011
Authors Vineet Kahlon
Comments (0)