Elucidating concurrent algorithms via layers of abstraction and reification

  1. Lookup NU author(s)
  2. Professor Cliff Jones
  3. Dr Ken Pierce
Author(s)Jones CB, Pierce KG
Publication type Article
JournalFormal Aspects of Computing
Year2011
Volume23
Issue3
Pages289-306
ISSN (print)0934-5043
ISSN (electronic)1433-299X
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.
PublisherSpringer
URLhttp://dx.doi.org/10.1007/s00165-010-0156-1
DOI10.1007/s00165-010-0156-1
Actions    Link to this publication
Share