Lamport Paxos的自动证明
Towards an Automatic Proof of Lamport's Paxos
摘要：
Lamport著名的Paxos共识协议通常被视为一个复杂的难以理解的算法。尽管它的复杂性，在本文中，我们采取了一个步骤，自动证明Paxos的安全性，利用其规范中的三个结构特征：空间规律性在其无序域，时间规律性在其完全有序域，其层次组成。通过仔细集成这些结构特征的IC3PO，一种新的模型检验算法，我们能够推断出一个归纳不变量，完全匹配的人写的一个以前获得了显着的手工努力，使用交互式定理证明。虽然已经进行了各种尝试来验证不同版本的Paxos，但据我们所知，这是Lamport原始Paxos规范的自动推断归纳不变量的第一次演示。我们注意到，这些结构特征并不是Paxos特有的，IC3PO可以作为一个自动通用协议验证工具。
英文摘要：
Lamport's celebrated Paxos consensus protocol is generally viewed as a complex hard-to-understand algorithm. Notwithstanding its complexity, in this paper, we take a step towards automatically proving the safety of Paxos by taking advantage of three structural features in its specification: spatial regularity in its unordered domains, temporal regularity in its totally-ordered domain, and its hierarchical composition. By carefully integrating these structural features in IC3PO, a novel model checking algorithm, we were able to infer an inductive invariant that identically matches the human-written one previously derived with significant manual effort using interactive theorem proving. While various attempts have been made to verify different versions of Paxos, to the best of our knowledge, this is the first demonstration of an automatically-inferred inductive invariant for Lamport's original Paxos specification. We note that these structural features are not specific to Paxos and that IC3PO can serve as an automatic general-purpose protocol verification tool.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
