Browse by author
Lookup NU author(s): Emeritus Professor Cliff JonesORCiD, Dr Ken Pierce
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
Arguing that intricate concurrent programs satisfy their specifications can be difficult; recording understandable explanations is important for subsequent readers. Abstraction is a key tool even for sequential programs. The purpose here is to explore some abstractions that help readers (and writers) understand the design of concurrent programs. As an illustration, the paper presents a formal development of a non-trivial parallel program: Simpson's implementation of asynchronous communication mechanisms. Although the correctness of this "4-slot algorithm" has been shown elsewhere, earlier proofs fail to offer much insight into the design. From an understandable (yet formal) design history of this one algorithm, the techniques employed in the explanation are teased out 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; furthermore, the atomicity assumptions implied by the rely/guarantee conditions are achieved by clever choice of data representations.
Author(s): Jones CB, Pierce KG
Publication type: Article
Publication status: Published
Journal: Formal Aspects of Computing
Year: 2011
Volume: 23
Issue: 3
Pages: 289-306
Print publication date: 28/04/2010
ISSN (print): 0934-5043
ISSN (electronic): 1433-299X
Publisher: Springer
URL: http://dx.doi.org/10.1007/s00165-010-0156-1
DOI: 10.1007/s00165-010-0156-1
Altmetrics provided by Altmetric
