A Scalable Lock-Free Stack Algorithm and its Verification

The design of efficient software supporting concurrent access to shared data is a challenging task. Often such programs will have at their core algorithms which utilise conceptual locks to restrict access to the data, and which are significantly more complex than their sequential (non-concurrent) counterparts. Lock-free algorithms, which have been developed to avoid problems such as priority inversion and deadlock, are more complex still due to the larger scope for interference between processes. These algorithms become even more complex when further mechanisms are added to achieve good performance under a wide range of workloads. In this paper we present a lock-free algorithm that efficiently manages interference on a shared stack, by allowing complementary stack operations to be eliminated without altering the stack. The algorithm we present is based on a published algorithm due to Hendler, Shavit and Yerushalmi (2004), and incorporates simplifications and improvements that we discovered while attempting to verify the original algorithm. We present a high-level view of the formal verification of our algorithm, which was machine-checked using the PVS theorem prover.