JUCS - Journal of Universal Computer Science 11(5): 744-770, doi: 10.3217/jucs-011-05-0744
Formal Construction of a Non-blocking Concurrent Queue Algorithm
expand article infoJean-Raymond Abrial‡, Dominique Cansell§
‡ ETH Zürich, Zürich, Switzerland§ Université de Metz & LORIA, France

Corresponding author: Jean-Raymond Abrial ( jabrial@inf.ethz.ch )

© Jean-Raymond Abrial, Dominique Cansell.
This article is freely available under the J.UCS Open Content License.
Citation: Abrial J-R, Cansell D (2005) Formal Construction of a Non-blocking Concurrent Queue Algorithm. JUCS - Journal of Universal Computer Science 11(5): 744-770. https://doi.org/10.3217/jucs-011-05-0744
Open Access
Abstract
This paper contains a completely formal (and mechanically proved) development of some algorithms dealing with a linked list supposed to be shared by various processes. These algorithms are executed in a highly concurrent fashion by an unknown number of such independent processes. These algorithms have been first presented in [MS96] by M.M. Michael and M.L. Scott. Two other developments of the same algorithms have been proposed recently in [YS03] (using the 3VMC Model Checker developed by E. Yahav) and in [DGLM04] (using I/O Automata and PVS).
Keywords
atomicity, concurrency, refinement, formal proof, prover