文章基本信息

标题：Formal Construction of a Non-blocking Concurrent Queue Algorithm
作者：Jean-Raymond Abrial ; Dominique Cansell
期刊名称：Journal of Universal Computer Science
印刷版ISSN：0948-6968
出版年度：2005
卷号：11
期号：5
页码：744-770
出版社：Graz University of Technology and Know-Center
摘要：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).