Simplifying proofs of linearisability using layers of abstraction

TL;DR

This paper introduces a new method for verifying linearisability in concurrent data structures that avoids identifying linearisation points by using an interval-based logic to relate concrete behaviors to coarse-grained abstractions.

Contribution

It proposes an alternative verification approach that simplifies proofs of linearisability by eliminating the need to pinpoint linearisation points, applicable to complex algorithms like lazy set.

Findings

Verification without linearisation points is feasible using interval-based logic.

Applied to lazy set, the method confirms linearisability without analyzing internal linearisation points.

The approach simplifies correctness proofs for concurrent data structures.

Abstract

Linearisability has become the standard correctness criterion for concurrent data structures, ensuring that every history of invocations and responses of concurrent operations has a matching sequential history. Existing proofs of linearisability require one to identify so-called linearisation points within the operations under consideration, which are atomic statements whose execution causes the effect of an operation to be felt. However, identification of linearisation points is a non-trivial task, requiring a high degree of expertise. For sophisticated algorithms such as Heller et al's lazy set, it even is possible for an operation to be linearised by the concurrent execution of a statement outside the operation being verified. This paper proposes an alternative method for verifying linearisability that does not require identification of linearisation points. Instead, using an interval-based logic, we show that every behaviour of each concrete operation over any interval is a possible behaviour of a corresponding abstraction that executes with coarse-grained atomicity. This approach is applied to Heller et al's lazy set to show that verification of linearisability is possible without having to consider linearisation points within the program code.