A simple proof of three properties on Simpson's 4-slot Algorithm

TL;DR

This paper provides a straightforward invariance proof demonstrating data-race freedom, data coherence, and data freshness in Simpson's 4-slot algorithm, establishing its linearisability with simple inductive invariants.

Contribution

It offers a simplified proof method for key properties of Simpson's 4-slot algorithm, extending prior work that focused mainly on data-race freedom.

Findings

Proves data-race freedom, data coherence, and data freshness

Establishes linearisability of the algorithm

Uses simple inductive invariants for proof

Abstract

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.