Derivation of a scalable lock-free stack algorithm

Colvin, Robert and Groves, Lindsay (2007). Derivation of a scalable lock-free stack algorithm. In: Proceedings of the 11th Refinement Workshop (REFINE 2006). 11th Refinement Workshop (REFINE 2006), Macao, China, (55-74). 31 October 2006. doi:10.1016/j.entcs.2006.08.044

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Colvin, Robert
Groves, Lindsay
Title of paper Derivation of a scalable lock-free stack algorithm
Conference name 11th Refinement Workshop (REFINE 2006)
Conference location Macao, China
Conference dates 31 October 2006
Proceedings title Proceedings of the 11th Refinement Workshop (REFINE 2006)   Check publisher's open access policy
Journal name Electronic Notes in Theoretical Computer Science   Check publisher's open access policy
Place of Publication Amsterdam, Netherlands
Publisher Elsevier
Publication Year 2007
Year available 2007
Sub-type Fully published paper
DOI 10.1016/j.entcs.2006.08.044
Open Access Status
ISSN 1571-0661
Volume 187
Start page 55
End page 74
Total pages 20
Language eng
Abstract/Summary 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.
Subjects 08 Information and Computing Sciences
080309 Software Engineering
Keyword Algorithm
Concurrent lock-free stack
Abstract specification
Linearisable stack
Q-Index Code E1
Q-Index Status Provisional Code
Institutional Status UQ

Version Filter Type
Citation counts: Scopus Citation Count Cited 10 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Mon, 12 Jan 2009, 18:26:23 EST by Ms Karen Naughton on behalf of Faculty Of Engineering, Architecture & Info Tech