Simpson 4-槽算法三个性质的简单证明
软件工程
2021-12-14 v1 计算机科学中的逻辑
编程语言
摘要
在本文中，我们给出 Simpson 4-槽算法三个性质的不变量证明，即无数据竞争、数据一致性与数据新鲜性，它们共同蕴含该算法的可线性化。这是对先前工作的扩展，先前工作的证明主要聚焦于无数据竞争。此外，我们的证明仅使用简单的归纳不变量与转移不变量，而先前工作使用了如分离逻辑、rely-guarantee 或所有权转移等更为复杂的机制。
引用
@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}
}