Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 11 / Issue 5

available in:   PDF (132 kB) PS (91 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-011-05-0744


Formal Construction of a Non-blocking Concurrent Queue Algorithm

Jean-Raymond Abrial (ETH Z├╝rich, Switzerland)

Dominique Cansell (Universite de Metz & LORIA, France)

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, formal proof, prover, refinement

Categories: D.1.3