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)
@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
}