Go home now Header Background Image
Search
Submission Procedure
share: |
 
Follow us
 
 
 
 
Volume 11 / Issue 5

available in:   PDF (132 kB) PS (91 kB)
 
get:  
Similar Docs BibTeX   Write a comment
  
get:  
Links into Future
 
DOI:   10.3217/jucs-011-05-0744

 

Formal Construction of a Non-blocking Concurrent Queue Algorithm

Jean-Raymond Abrial (ETH Z├╝rich, Switzerland)

Dominique Cansell (Universite de Metz & LORIA, France)

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

Keywords: atomicity, concurrency, formal proof, prover, refinement

Categories: D.1.3