Model Checking Simpson's Four-Slot Fully Asynchronous Communication Mechanism

John Rushby

Technical Report, July 2002

Abstract

Simpson's four-slot fully asynchronous communication mechanism allows single reader and writer processes to access a shared memory in such a way that interference between concurrent reads and writes is avoided, the reader always accesses the most recent data stored by the writer, and neither process need wait for the other. In computer science parlance, it is a means for implementing a wait-free atomic register.

We use the SAL model checking environment to examine this mechanism and show that concurrent reads and writes are indeed noninterfering but that access to the most recently written data requires the unattractive assumption that some of the control registers are already atomic. We exhibit counterexamples that reveal incorrect operation when the control registers are not atomic, and also when the mechanism is modified (following a suggestion of Simpson) so that control registers are written only when their values will be changed. We do successfully verify the algorithm when its control registers are assumed to be atomic.

The requirement for atomic control registers is unattractive: it means that any application that uses Simpson's mechanism must be accompanied by separate, strong evidence that its implementation of the control registers satisfies this requirement. We recommend formal examination of alternative algorithms (such as that of Anderson and Gouda) that operate under weaker assumptions.

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

BibTeX Entry


@TECHREPORT{Rushby02:Simpson,
	TITLE = {Model Checking {Simpson's} Four-Slot Fully Asynchronous
		Communication Mechanism},
	AUTHOR = {John Rushby},
	INSTITUTION = csl,
	ADDRESS = mp,
	MONTH = jul,
	YEAR = 2002
}


Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page