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.

‚Äč