ePrints

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

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

Downloads

• Published version [.pdf]

Abstract

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

Publication status: Published

Series Title: Department of Computing Science Technical Report Series

Year: 2002

Pages: 54

Print publication date: 01/01/2002

Source Publication Date: January 2002

Report Number: 756

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

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/756.pdf

Share