Browse by author
Lookup NU author(s): Emeritus Professor Cliff JonesORCiD, Dr Ken Pierce
This paper presents a formal development of a non-trivial parallel program: Simpson's implementation of asynchronous communication mechanisms (ACMs). Although the correctness of this “4-slot algorithm" has been shown elsewhere, earlier proofs fail to over much insight into the design. The aims of this paper include both the presentation of an understandable (yet formal) design history of this one algorithm and teasing out of the techniques employed in the explanation for wider application. Among these techniques is using a “fiction of atomicity" as an aid to understanding the initial steps of development. The rely-guarantee approach is, here, combined with notions of read/write frames and “phased" specifications; the atomicity assumptions implied by rely/guarantee conditions are realised by clever choices of data representation.
Author(s): Jones CB, Pierce KG
Publication type: Report
Publication status: Published
Series Title: School of Computing Science Technical Report Series
Year: 2009
Pages: 20
Print publication date: 01/08/2009
Source Publication Date: August 2009
Report Number: 1166
Institution: School of Computing Science, University of Newcastle upon Tyne
Place Published: Newcastle upon Tyne
URL: http://www.cs.ncl.ac.uk/publications/trs/papers/1166.pdf
