一句话：提出通用、可靠且完备的前向推理证明方法，并在 TLAPS 中机器验证若干并发对象的线性一致性。
并发对象的线性一致性证明往往需要针对具体对象量身定制、且难以机器化验证。本文提出一套简单、通用（universal）、可靠（sound）且完备（complete）的前向推理证明方法，可同时处理线性一致性与强线性一致性：通用性指方法适用于任意对象类型；可靠性指凡能由该方法证明的算法必是（强）线性一致的；完备性指任何（强）线性一致的实现都能用该方法证明。作者以该方法分别给出 Herlihy-Wing 队列与 Jayanti 单扫描器快照（single-scanner snapshot）的线性一致性证明，以及 Jayanti-Tarjan 并查集对象的强线性一致性证明，三份证明均由 TLA+ 证明系统 TLAPS 完成机器验证，展示了方法的简洁性与证明能力。
We introduce simple, universal , sound , and complete proof methods for producing machine-verifiable proofs of linearizability and strong linearizability. Universality means that our method works for any object type; soundness means that an algorithm can be proved correct by our method only if it is linearizable (resp. strong linearizable); and completeness means that any linearizable (resp. strong linearizable) implementation can be proved so using our method. We demonstrate the simplicity and power of our method by producing proofs of linearizability for the Herlihy-Wing queue and Jayanti's single-scanner snapshot, as well as a proof of strong linearizability of the Jayanti-Tarjan union-find object. All three of these proofs are machine-verified by TLAPS (the TLA+ Proof System).
@article{paperbot2659,
title = {A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability},
author = {Prasad Jayanti and Siddhartha Jayanti and Ugur Y. Yavuz and Lizzie Hernandez},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632924}
}