Simplifying proofs of linearisability using layers of abstraction
Brijesh Dongol, John Derrick · 2014
Abstract: Linearisability has become the standard correctness criterion for con-current data structures, ensuring that every history of invocations and responses of concurrent operations has a matching sequential history. Existing proofs of linearis-ability 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 a 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 ap-proach 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.