Comparison Under Abstraction for Verifying Linearizability
Daphna Amit, Noam Rinetzky, Thomas Reps, Mooly Sagiv, and Eran Yahav
Linearizability is one of the main correctness criteria for
implementations of concurrent data structures. A data structure is
linearizable if its operations appear to execute atomically. Verifying
linearizability of concurrent unbounded linked data structures is a
challenging problem because it requires correlating executions that
manipulate (unbounded-size) memory states. We present a static
analysis for verifying linearizability of concurrent unbounded linked
data structures. The novel aspect of our approach is the ability to
prove that two (unboundedsize) memory layouts of two programs are
isomorphic in the presence of abstraction. A prototype implementation
of the analysis verified the linearizability of several published
concurrent data structures implemented by singly-linked lists.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)