Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity) - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Journal Articles Journal of Universal Computer Science Year : 2005

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).

Domains

Other [cs.OH]
No file

Dates and versions

inria-00000120 , version 1 (23-06-2005)

Identifiers

  • HAL Id : inria-00000120 , version 1

Cite

Jean-Raymond Abrial, Dominique Cansell. Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity). Journal of Universal Computer Science, 2005, Atomicity in System Design and Execution (Proceedings of Dagstuhl-Seminar 04181), 11 (5), pp.744-770. ⟨inria-00000120⟩
118 View
0 Download

Share

Gmail Facebook X LinkedIn More