Derivation of a scalable lock-free stack algorithm

We show how a sophisticated, lock-free concurrent stack implementation can be derived from an abstract specification in a series of verifiable steps. The algorithm is a simplified version of one described by Hendler, Shavit and Yerushalmi [Hendler, D., N. Shavit and L. Yerushalmi, A scalable lock-free stack algorithm, in: SPAA 2004: Proceedings of the Sixteenth Annual ACM Symposium on Parallel Algorithms, June 27-30, 2004, Barcelona, Spain, 2004, pp. 206-215], which allows push and pop operations to be paired off and eliminated without affecting the central stack. This reduces contention on the stack compared with other implementations, and allows multiple pairs of push and pop operations to be performed in parallel. Our derivation introduces an abstract model of the elimination process, which allows the basic algorithmic ideas to be separated from implementation details, and provides a basis for explaining and comparing different variants of the algorithm. We show that the elimination stack algorithm is linearisable by showing that any execution of the implementation can be transformed into an equivalent execution of an abstract model of a linearisable stack. At each step in the derivation, this transformation reduces an execution of an entire operation at a time of the model at that level, or two in the case of a successful elimination, rather than translating one atomic action at a time as is done in simulation proofs