12.00
Verifying Concurrent Programs against Sequential Specifications
Ahmed Bouajjani
LIAFA, Univ Paris 7, France.
28-02-13
Abstract
We investigate the algorithmic feasibility of checking whether
concurrent implementations of shared-memory objects adhere to their
given sequential specifications; sequential consistency,
linearizability, and conflict serializability are the canonical
variations of this problem. While verifying sequential consistency of
systems with unbounded concurrency is known to be undecidable, we
demonstrate that conflict serializability, and linearizability with
fixed linearization points are EXPSPACE-complete, while the general
linearizability problem is undecidable.
Our (un)decidability proofs, besides bestowing novel theoretical
results, also reveal novel program explorations strategies. For
instance, we show that every violation to conflict serializability is
captured by a conflict cycle whose length is bounded independently
from the number of concurrent operations. This suggests an incomplete
detection algorithm which only remembers a small subset of conflict
edges, which can be made complete by increasing the number of
remembered edges to the cycle-length bound. Similarly, our
undecidability proof for linearizability suggests an incomplete
detection algorithm which limits the number of ``barriers'' bisecting
non-overlapping operations. Our decidability proof of bounded-barrier
linearizability is interesting on its own, as it reduces the
consideration of all possible operation serializations to numerical
constraint solving. The literature seems to confirm that most
violations are detectable by considering very few conflict edges or
barriers.
(Joint work with Constantin Enea, Michael Emmi, and Jad Hamza. Will
appear in ESOP'13.)