A simple proof of three properties on Simpson's 4-slot Algorithm
Software Engineering
2021-12-14 v1 Logic in Computer Science
Programming Languages
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.
Cite
@article{arxiv.2112.06233,
title = {A simple proof of three properties on Simpson's 4-slot Algorithm},
author = {Xu Wang and Qiwen Xu},
journal= {arXiv preprint arXiv:2112.06233},
year = {2021}
}