Toggle Main Menu Toggle Search

Open Access padlockePrints

Relaxing Atomicity and Verifying Correctness: Considering the Case of an Asynchronous Communication Mechanism

Lookup NU author(s): Dr Jonathan Burton



In an ideal world, where we could guarantee instantaneous, atomic data transfer --- whatever the type of the data being transferred --- shared memory communication between two concurrent processes could be implemented directly using single variables or registers, without any attendant access control policies or mechanisms. In practice, asynchronous communication mechanisms may be used to provide the illusion of atomic transfers of data while still allowing non-blocking reads and writes: that is, reads and writes may proceed concurrently without interfering with each other. In order to prove the correctness of such mechanisms, the natural approach would be to verify them against the specification provided by an idealised register with atomic, instantaneous --- and so sequential --- transfers of data. Yet such a verification is complicated by the fact that, in moving to the asynchronous communication mechanism from such a specification, additional concurrency has been introduced and so the (visible) behaviours of the mechanism are not directly comparable to those of the register. In this paper, we recall an extension of standard process algebraic refinement and show how it may be used to verify the correctness of a particular asynchronous communication mechanism, Simpson\'s 4-slot. In so doing, we look at a number of issues which seem significant in the consideration of correctness when the real atomicity of a specification has been relaxed in the move from specification to implementation.

Publication metadata

Author(s): Burton J

Publication type: Article

Publication status: Published

Journal: Journal of Universal Computer Science

Year: 2005

Volume: 11

Issue: 5

Pages: 771-802

Print publication date: 01/01/2005

Date deposited: 04/03/2011

ISSN (electronic): 0948-695X

Publisher: Know-Center Graz in cooperation with Springer


DOI: 10.3217/jucs-011-05-0771


Altmetrics provided by Altmetric


Find at Newcastle University icon    Link to this publication