Authors: Robert Colvin and Lindsay Groves
Source: GZipped
PostScript (54kb); Adobe
PDF (154kb)
Abstract:The design of efficient algorithms for concurrent access to shared data structures is a challenging task. Standard lock-based algorithms are more complex than their sequential counterparts, and 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 central stack, and discuss how we verified several versions of this algorithm which use different underlying stack implementations. The algorithm we present is based on a published algorithm due to Hendler, Shavit and Yerushalmi, and incorporates simplifications and improvements that we discovered while attempting to verify the original algorithm. Our proofs were machine-checked using the PVS theorem prover.
Keywords: lock-free, stack, linearisability, verification, simulation, PVS