Linearizability has been the long standing gold standard for consistency in concurrent data structures. However, proofs of linearizability can be long and intricate, hard to produce, and extremely time consuming even to verify. In this work, we address this issue by introducing simple $universal$, $sound$, and $complete$ proof methods for producing machine-verifiable proofs of linearizability and its close cousin, 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 Temporal Logic of Actions Proof System).

翻译：线性化一直是并发数据结构中一致性的长期黄金标准。然而，线性化的证明可能冗长且复杂，难以产生，甚至验证起来极为耗时。在本工作中，我们通过引入简单、通用、可靠且完备的证明方法来解决这一问题，以生成机器可验证的线性化及其近亲——强线性化证明。通用性意味着我们的方法适用于任何对象类型；可靠性意味着仅当算法是线性化（或强线性化）时，我们的方法才能证明其正确性；完备性意味着任何线性化（或强线性化）实现都可以使用我们的方法得到证明。我们通过为Herlihy-Wing队列和Jayanti的单扫描快照生成线性化证明，以及为Jayanti-Tarjan并查集对象生成强线性化证明，展示了我们方法的简洁性和强大能力。这三个证明均由TLAPS（时态逻辑动作证明系统）完成机器验证。