Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Simplifying Linearizability Proofs with Reduction and Abstraction

Tayfun Elmas, Shaz Qadeer, Ali Sezgin, Omer Subasi, and Serdar Tasiran

Abstract

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.

Details

Publication typeInproceedings
Published inConference on Tools and Algorithms for the Construction and Analysis of Systems
PublisherSpringer Verlag
> Publications > Simplifying Linearizability Proofs with Reduction and Abstraction