可线性化算法机器证明的一种通用技术
A Universal Technique for Machine-Certified Proofs of Linearizable Algorithms
摘要：
线性化一直是并发数据结构一致性的黄金标准。然而，线性化的证明可能是漫长而复杂的，难以产生，甚至验证也非常耗时。在这项工作中，我们解决这个问题，通过介绍简单的$universal$，$sound$，和$complete$证明方法生产机器可验证的证明线性化和它的近亲，强线性化。普适性意味着我们的方法适用于任何对象类型;可靠性意味着算法只有在可线性化时才能被我们的方法证明是正确的。强可线性化的）;而完备性意味着任何可线性化的（分别是强线性化）的实现可以证明，所以使用我们的方法。我们证明了我们的方法的简单性和权力，通过生产证明的线性化的Herlihy-Wing队列和Jayanti的单扫描仪快照，以及证明的强线性化的Jayanti-Tarjan联盟找到对象。所有这三个证明都是通过TLAPS（动作证明系统的时间逻辑）进行机器验证的。
英文摘要：
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).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
