Skip to Main content Skip to Navigation
Journal articles

Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity)

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).
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/inria-00000120
Contributor : Dominique Cansell Connect in order to contact the contributor
Submitted on : Thursday, June 23, 2005 - 10:06:26 AM
Last modification on : Friday, February 4, 2022 - 3:19:03 AM

Identifiers

  • HAL Id : inria-00000120, version 1

Collections

Citation

Jean-Raymond Abrial, Dominique Cansell. Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity). Journal of Universal Computer Science, Graz University of Technology, Institut für Informationssysteme und Computer Medien, 2005, Atomicity in System Design and Execution (Proceedings of Dagstuhl-Seminar 04181), 11 (5), pp.744-770. ⟨inria-00000120⟩

Share

Metrics

Record views

112