Verify Linearizability of Concurrent Stacks

TL;DR

This paper introduces a new proof technique for verifying the linearizability of concurrent stacks, simplifying correctness proofs by using an extended partial order and applying it to well-known algorithms.

Contribution

A novel proof method that reduces linearizability verification to conditions based on happened-before order, validated on Treiber and Time-Stamped stacks.

Findings

Proved soundness of the elimination mechanism.

Reduced linearizability proof to happened-before conditions.

Validated approach on two popular concurrent stack algorithms.

Abstract

Proving linearizability of concurrent data structures is crucial for ensuring their correctness, but is challenging especially for implementations that employ sophisticated synchronization techniques. In this paper, we propose a new proof technique for verifying linearizability of concurrent stacks. We first prove the soundness of the elimination mechanism, a common optimization used in concurrent stacks, which enables simplifying the linearizability proofs. We then present a stack theorem that reduces the problem of proving linearizability to establishing a set of conditions based on the happened-before order of operations. The key idea is to use an extended partial order to capture when a pop operation can observe the effect of a push operation. We apply our proof technique to verify two concurrent stack algorithms: the Treiber stack and the Time-Stamped stack, demonstrating its practicality. Our approach provides a systematic and compositional way to prove linearizability of concurrent stacks.