一句话：用可见性关系为 Jayanti 的三个并发快照算法构建模块化、可复用的线性化证明。
本文研究并发算法的线性化验证，目标是在不显式构造线性化点的情况下获得模块化、可复用的证明。作者采用 Henzinger 等人提出的可见性关系作为抽象，对 Jayanti 的三个并发快照算法给出模块化证明。证明按 signature 划分为多个抽象层次：较低层处理具体算法细节，较高层组件被三个算法共享，从而同时适用于三者。该方法不仅复现了原本仅以非形式方式表述的 Jayanti 直觉，还以接口性质将其精确数学化，展示了可见性关系在并发快照算法验证中的有效性。
Visibility relations have been proposed by Henzinger et al. as an abstraction for proving linearizability of concurrent algorithms that obtains modular and reusable proofs. This is in contrast to the customary approach based on exhibiting the algorithm's linearization points. In this paper we apply visibility relations to develop modular proofs for three elegant concurrent snapshot algorithms of Jayanti. The proofs are divided by signatures into components of increasing level of abstraction; the components at higher abstraction levels are shared, i.e., they apply to all three algorithms simultaneously. Importantly, the interface properties mathematically capture Jayanti's original intuitions that have previously been given only informally.
@article{paperbot1539,
title = {Visibility reasoning for concurrent snapshot algorithms},
author = {Joakim Öhman and Aleksandar Nanevski},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498694}
}