Toggle Main Menu Toggle Search

Open Access padlockePrints

Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification

Lookup NU author(s): Professor Cliff Jones, Dr Ken Pierce

Downloads

Full text for this publication is not currently held within this repository. Alternative links are provided below where available.


Abstract

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.


Publication metadata

Author(s): Jones CB, Pierce KG

Editor(s): Börger, E., Butler, M., Bowen, J.P., Boca, P.

Publication type: Conference Proceedings (inc. Abstract)

Publication status: Published

Conference Name: Abstract State Machines, B and Z: First International Conference (ABZ 2008)

Year of Conference: 2008

Pages: 360-377

ISSN: 0302-9743

Publisher: Springer-Verlag

URL: http://dx.doi.org/10.1007/978-3-540-87603-8_47

DOI: 10.1007/978-3-540-87603-8_47

Library holdings: Search Newcastle University Library for this item

Series Title: Lecture Notes in Computer Science

ISBN: 9783540876021


Actions

Link to this publication


Share