Simplifying Linearizability Proofs with Reduction and Abstraction

The typical proof of linearizability establishes an abstrac-

tion map from the concurrent program to a sequential specification, and

identifies the commit points of operations. If the concurrent program uses

fine-grained concurrency and complex synchronization, constructing such

a proof is difficult. We propose a sound proof system that significantly

simplifies the reasoning about linearizability. Linearizability is proved by

transforming an implementation into its specification within this proof

system. The proof system combines reduction and abstraction, which in-

crease the granularity of atomic actions, with variable introduction and

hiding, which syntactically relate the representation of the implemen-

tation to that of the specification. We construct the abstraction map

incrementally, and eliminate the need to reason about the location of

commit points in the implementation. We have implemented our method

in the QED verifier and demonstrated its effectiveness and practicality

on several highly-concurrent examples from the literature.

tacas10.pdf
PDF file

In  Conference on Tools and Algorithms for the Construction and Analysis of Systems

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details

TypeInproceedings
> Publications > Simplifying Linearizability Proofs with Reduction and Abstraction