A Universal Technique for Machine-Certified Proofs of Linearizable Algorithms

TL;DR

This paper introduces a universal, sound, and complete method for machine-verifiable proofs of linearizability in concurrent data structures, simplifying verification and ensuring correctness.

Contribution

The authors present a novel proof technique applicable to any object type that guarantees soundness and completeness, verified by TLAPS, for linearizability and strong linearizability.

Findings

Successfully proved linearizability of Herlihy-Wing queue

Verified single-scanner snapshot correctness

Proved strong linearizability of union-find object

Abstract

Linearizability has been the long standing gold standard for consistency in concurrent data structures. However, proofs of linearizability can be long and intricate, hard to produce, and extremely time consuming even to verify. In this work, we address this issue by introducing simple $universal$, $sound$, and $complete$ proof methods for producing machine-verifiable proofs of linearizability and its close cousin, strong linearizability. Universality means that our method works for any object type; soundness means that an algorithm can be proved correct by our method only if it is linearizable (resp. strong linearizable); and completeness means that any linearizable (resp. strong linearizable) implementation can be proved so using our method. We demonstrate the simplicity and power of our method by producing proofs of linearizability for the Herlihy-Wing queue and Jayanti's single-scanner snapshot, as well as a proof of strong linearizability of the Jayanti-Tarjan union-find object. All three of these proofs are machine-verified by TLAPS (the Temporal Logic of Actions Proof System).