Toggle Main Menu Toggle Search


The Formal Classification and Verification of Simpson's 4-slot Asynchronous Communication Mechanism

Lookup NU author(s): Neil Henderson, Dr Stephen Paynter



This paper critiques and extends Lamport's taxonomy of asynchroous registers. This extended taxonomy is used to characterise Simpson's 4-slot asynchronous communication mechanism. A formalisation of the Lamport atomic property and Simpson's original 4-Slot implementation is given in the PVS logic. We prove that the 4-slot is atomic using Nipkow's retrieve relation proof rules. A description is given of the formal proofs, which have been discharged in the PVS theorem prover.

Publication metadata

Author(s): Henderson N, Paynter S

Publication type: Report

Series Title: Department of Computing Science Technical Report Series

Year: 2002

Pages: 54

Source Publication Date: January 2002

Report Number: 756

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

Place Published: Newcastle upon Tyne