Proving the Correctness of Simpson's 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method

摘要

This paper describes a rely-guarantee proof to show that Simpson's 4-slot single-reader, single-writer ACM is Lamport atomic (as described fully in the paper). First an abstract ACM specification is proved Lamport atomic using an exhaustive assertional method. A formal model of Simpson's 4-slot is then given and this has been proved to be a refinement of the abstract specification using Nipkow's retrieve relation rule. Simpson's 4-slot is then shown to be Lamport atomic using an interleaved concurrency rely-guarantee proof method for shared variable concurrency.