Verify Linearizability of Concurrent Stacks
This addresses the problem of ensuring correctness for concurrent data structures, particularly for developers and researchers in concurrent programming, though it is incremental as it builds on existing verification methods.
The paper tackles the challenge of verifying linearizability for concurrent stacks by proposing a new proof technique that simplifies proofs through an elimination mechanism and a stack theorem, applying it to verify two algorithms like the Treiber stack.
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.