A simple proof of data-race freedom and coherence for simpson's 4-slot algorithm.

In this paper we present an invariance proof of two properties on Simpson's 4-slot algorithm, i.e. data-race freedom and data coherence, which, together with data freshness, implies linearisability of the algorithm. It is an extension of previous works which focus mostly on the proof of data-race freedom. In addition, our proof uses simply inductive invariants and transition invariants [7], whereas previous work uses more sophisticated machinery like separation logics, rely-guarantee or ownership transfer.