A simple proof of three properties on Simpson's 4-slot Algorithm
This work provides a simpler proof for a known algorithm in concurrent programming, which is incremental as it extends previous proofs by focusing on additional properties and using less sophisticated methods.
The paper tackles the problem of proving three properties (data-race freedom, data coherence, and data freshness) for Simpson's 4-slot algorithm, resulting in a simple proof using inductive and transition invariants that implies linearisability.
In this paper we present an invariance proof of three properties on Simpson's 4-slot algorithm, i.e. data-race freedom, data coherence and data freshness, which together implies linearisability of the algorithm. It is an extension of previous works whose proof focuses mostly on data-race freedom. In addition, our proof uses simply inductive invariants and transition invariants, whereas previous work uses more sophisticated machinery like separation logics, rely-guarantee or ownership transfer.