Simplifying linearizability proofs with reduction and abstraction

The typical proof of linearizability establishes an abstraction map from the concurrent program to a sequential specification, and iden-tifies the commit points of operations. If the concurrent program uses fine-grained concurrency and complex synchronization, con-structing such a proof is difficult. We propose a sound proof sys-tem that significantly simplifies the reasoning about linearizability. Linearizability is proved by transforming an implementation into its specification within this proof system. The proof system com-bines reduction and abstraction, which increase the granularity of atomic actions, with variable introduction and hiding, which relate the synchronization mechanism of the implementation 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 demonstrate its effecacy and practicality on sev-eral highly-concurrent examples from the literature. 1