Browse by author
Lookup NU author(s): Professor Cliff JonesORCiD, Dr Ken Pierce
This paper presents a novel formal development of a non-trivial parallel program: Simpson's implementation of asynchronous communication mechanisms (ACMs). Although the correctness of the "4-slot algorithm" has been shown elsewhere, earlier developments are by no means intuitive. The aims of this paper include both the presentation of an understandable (yet formal) design history and the establishment of another way of "splitting (software) atoms". Using the "fiction of atomicity" as an aid to understanding the initial steps of development, the top-level specification is developed to code. 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 choice of data representation. The development method herein is compared with other approaches --in a spirit of cooperation-- as the authors believe that constructive comparison elucidates many of the finer points in the "4-slot" specification/development and of parallel programs in general.
Author(s): Jones CB, Pierce KG
Publication type: Report
Publication status: Published
Series Title: School of Computing Science Technical Report Series
Year: 2010
Pages: 21
Print publication date: 01/01/2010
Source Publication Date: January 2010
Report Number: 1186
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/1186.pdf
