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

摘要

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.