28560 articles – 22061 references  [version française]

inria-00000120, version 1

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

Jean-Raymond Abrial 1, Dominique Cansell () 2, 3

Journal of Universal Computer Science 11, 5 (2005) 744-770

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

  • 1:  Department of Computer Science (ETH Zurich)
  • ETH Zurich
  • 2:  MOSEL (INRIA Lorraine - LORIA)
  • INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • 3:  Université de Metz (UNIVERSITÉ DE METZ)
  • Université de Metz
  • Domain : Computer Science/Other
  • Keywords : atomicity – concurrency – refinement – formal proof – prover
  • Comment : l'article est disponible sur la page web suivante: http://www.jucs.org/jucs_11_5/formal_construction_of_a/http://www.jucs.org/
 
  • inria-00000120, version 1
  • http://hal.inria.fr/inria-00000120
  • oai:hal.inria.fr:inria-00000120
  • From: Dominique Cansell <>
  • Submitted on: Thursday, 23 June 2005 10:06:26
  • Updated on: Thursday, 29 June 2006 15:34:15