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
Liste complète des métadonnées

https://hal.inria.fr/inria-00000120
Contributor : Dominique Cansell <>
Submitted on : Thursday, June 23, 2005 - 10:06:26 AM
Last modification on : Wednesday, April 3, 2019 - 1:15:48 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, Springer, 2005, Atomicity in System Design and Execution (Proceedings of Dagstuhl-Seminar 04181), 11 (5), pp.744-770. ⟨inria-00000120⟩

Share

Metrics

Record views

240