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（动作时序逻辑证明系统）进行了机器验证。