  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.
