Aspect-oriented linearizability proofs

TL;DR

This paper introduces a modular approach to proving linearizability of concurrent data structures, avoiding complex linearization point identification, and simplifies verification especially for advanced non-blocking algorithms.

Contribution

It proposes a novel, modular method for linearizability proofs that reduces complexity and scales better to complex concurrent algorithms.

Findings

Successfully verified the Herlihy and Wing queue using the new approach

Reduces proof complexity by avoiding linearization point identification

Applicable to advanced non-blocking concurrency patterns

Abstract

Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof.