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: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2005

Pages: 34

Print publication date: 01/04/2005

Source Publication Date: April 2005

Report Number: 905

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne