2021/10/12 by Tangliu Wen, Wen, Tangliu
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Parallel Computing and Optimization Techniques #Real-Time Systems Scheduling #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.2110.05801
openalex publication_date 2021/10/12 · openalex created_date 2021/10/25 · openalex updated_date 2026/07/28
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.