用于端到端线性化证明的前向推理机械化元理论
编程语言
2025-09-09 v1
摘要
在过去十年中，人们开发了许多技术来证明线性化，这是并发数据结构正确性的黄金标准。直观地说，线性化要求并发数据结构上的每个操作看起来都是瞬间完成的，即使与其他操作交错执行也是如此。最近，Jayanti 等人提出了首个可靠且完备的“前向推理”技术，用于随着时间向前推移证明线性化，该技术将并发数据结构的行为与参考原子数据结构相关联。该技术可用于在 TLA+ 中生成机器检查的线性化证明。然而，尽管 Jayanti 等人的方法被证明是可靠且完备的，但这一重要元理论结果的机械化仍然悬而未决。因此，目前无法生成经过验证的端到端线性化证明。为了减小这一可信计算基的规模，我们在 Rocq 中形式化了这种前向推理技术，并机械化了其可靠性和完备性的证明。作为案例研究，我们使用该方法为一个简单的并发寄存器生成了经过验证的端到端线性化证明。
引用
@article{arxiv.2509.06872,
title = {Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs},
author = {Zachary Kent and Ugur Y. Yavuz and Siddhartha Jayanti and Stephanie Balzer and Guy Blelloch},
journal= {arXiv preprint arXiv:2509.06872},
year = {2025}
}