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).
Type de document :
Article dans une revue
Journal of Universal Computer Science, Springer, 2005, Atomicity in System Design and Execution (Proceedings of Dagstuhl-Seminar 04181), 11 (5), pp.744-770
Liste complète des métadonnées

https://hal.inria.fr/inria-00000120
Contributeur : Dominique Cansell <>
Soumis le : jeudi 23 juin 2005 - 10:06:26
Dernière modification le : samedi 20 octobre 2018 - 15:06:01

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

235