Trace-based derivation of a scalable lock-free stack algorithm

Groves, Lindsay and Colvin, Robert (2009) Trace-based derivation of a scalable lock-free stack algorithm. Formal Aspects of Computing, 21 1-2: 187-223. doi:10.1007/s00165-008-0092-5

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

Author Groves, Lindsay
Colvin, Robert
Title Trace-based derivation of a scalable lock-free stack algorithm
Journal name Formal Aspects of Computing   Check publisher's open access policy
ISSN 0934-5043
1433-299X
Publication date 2009-02-01
Sub-type Article (original research)
DOI 10.1007/s00165-008-0092-5
Volume 21
Issue 1-2
Start page 187
End page 223
Total pages 36
Place of publication Guildford, Surrey, United Kingdom
Publisher Springer
Collection year 2010
Language eng
Subject 08 Information and Computing Sciences
080399 Computer Software not elsewhere classified
890299 Computer Software and Services not elsewhere classified
Abstract 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 based on the scalable stack algorithm of Hendler et al. (Proceedings of the sixteenth annual ACM symposium on parallel algorithms, 27–30 June 2004, Barcelona, Spain, pp 206–215), which allows push and pop operations to be paired off and eliminated without affecting the central stack, thus reducing contention on the stack, and allowing multiple pairs of push and pop operations to be performed in parallel. Our algorithm uses a simpler data structure than Hendler, Shavit and Yerushalmi’s, and avoids an ABA problem. We first derive a simple lock-free stack algorithm using a linked-list implementation, and discuss issues related to memory management and the ABA problem. We then add an abstract model of the elimination process, from which we derive our elimination algorithm. This 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. Each step in the derivation is either a data refinement which preserves the level of atomicity, an operational refinement which may alter the level of atomicity, or a refactoring step which alters the structure of the system resulting from the preceding derivation. We verify our refinements using an extension of Lipton’s reduction method, allowing concurrent and non-concurrent aspects to be considered separately.
Keyword Refinement
Derivation
Lock-free algorithms
Concurrency
Stack
Elimination
Reduction, Linearisability
Atomicity
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status UQ
Additional Notes Published online 16 December 2008 ; Editorial: We are proud to present a Special Issue on Refinement, originating from the 11th BCS-FACS Refinement Workshop, held at Macao in October 2006.

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 6 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 8 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Tue, 24 Nov 2009, 23:01:06 EST