A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks
Nicholas Kidd, Peter Lammich, Tayssir Touili, and Thomas Reps
The problem of interest is to verify data consistency of a
concurrent Java program. In particular, we 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. Our previous work used only a semi-decision
procedure, and hence provides a definite answer only some of the
time. In this paper, we rectify this shortcoming by developing a
decision procedure for verifying data consistency, i.e., atomic-set
serializability, of an EML program. When coupled with the previous
work, it provides a decision procedure for verifying data
consistency of a concurrent Java program.
We implemented the decision procedure, and applied it to detect both
single-location and multi-location data races in models of
concurrent Java programs. Compared with the prior method based on a
semi-decision procedure, not only was the decision procedure 34
times faster overall, but the semi-decision procedure timed out on
about 50% of the queries, whereas the decision procedure timed out
on none of the queries.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)