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.

翻译：在本文中,我们提供了辛普森四分位算法中三种属性(即数据-记录自由、数据一致性和数据新鲜度)的三个属性的不定证据,这共同意味着算法的线性。这是以前工作的延伸,其证据主要侧重于数据-记录自由。 此外,我们的证据仅使用感化变异和变异性,而以前的工作则使用更先进的机械,如分离逻辑、依赖保证或所有权转让。