迈向 Lamport 的 Paxos 的自动证明
计算机科学中的逻辑
2021-10-29 v1 分布式、并行与集群计算
形式语言与自动机理论
摘要
Lamport 著名的 Paxos 共识协议通常被认为是一个复杂且难以理解的算法。尽管其复杂，本文中我们通过利用其规范中的三个结构特征，向自动证明 Paxos 的安全性迈出了一步：其无序域中的空间正则性、其全序域中的时间正则性，以及其层次化组合。通过在 IC3PO（一种新颖的模型检测算法）中精心整合这些结构特征，我们推断出了一个归纳不变量，其与先前通过交互式定理证明付出大量人工努力所得到的人工书写不变量完全一致。尽管已有各种尝试验证不同版本的 Paxos，但据我们所知，这是针对 Lamport 原始 Paxos 规范自动推断归纳不变量的首次展示。我们注意到这些结构特征并非 Paxos 所特有，且 IC3PO 可作为一种自动的通用协议验证工具。
引用
@article{arxiv.2108.08796,
title = {Towards an Automatic Proof of Lamport's Paxos},
author = {Aman Goel and Karem A. Sakallah},
journal= {arXiv preprint arXiv:2108.08796},
year = {2021}
}
备注
"to be published in Formal Methods in Computer-Aided Design (FMCAD) 2021, see https://fmcad.org/FMCAD21"