A Decision Procedure for Detecting Atomicity Violations for Communicating Processes With Locks
The problem of interest is to verify data consistency of a concurrent Java program. In particular, the authors present a new decision procedure for verifying that a class of data races caused by inconsistent accesses on multiple fields of an object cannot occur (So-called atomic-set serializability). Atomic-set serializability generalizes the ordinary notion of a data race (i.e., Inconsistent coordination of accesses on a single memory location) to a broader class of races that involve accesses on multiple memory locations. Previous work by some of the authors presented a technique to abstract a concurrent Java program into an EML program, a modeling language based on pushdown systems and a finite set of reentrant locks.