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 indepen- dent 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 Au- tomata and PVS).
['Jean-Raymond Abrial', 'Dominique Cansell']
Formal Construction of a Non-blocking Concurrent Queue Algorithm (a Case Study in Atomicity)