线性化算法的机器认证证明通用技术
分布式、并行与集群计算
2023-02-14 v2 数据结构与算法
形式语言与自动机理论
摘要
线性一致性（线性izability）长期以来一直是并发数据结构一致性的黄金标准。然而，线性一致性的证明可能冗长且复杂，难以生成，甚至验证也极为耗时。本工作中，我们通过在生成机器可验证的线性一致性及其近亲强线性一致性证明方面引入简单、通用、可靠且完备的证明方法，来解决此问题。通用性指我们的方法适用于任何对象类型；可靠性指仅当算法是线性一致（相应为强线性一致）时，才能用我们的方法证明其正确；完备性指任何线性一致（相应为强线性一致）的实现都能用我们的方法得证。我们通过为 Herlihy-Wing 队列和 Jayanti 的单扫描器快照生成线性一致性证明，以及为 Jayanti-Tarjan 并查集对象生成强线性一致性证明，来展示我们方法的简洁与强大。这三个证明均由 TLAPS（行为时序逻辑证明系统）机器验证。
引用
@article{arxiv.2302.00737,
title = {A Universal Technique for Machine-Certified Proofs of Linearizable Algorithms},
author = {Prasad Jayanti and Siddhartha Jayanti and Ugur Y. Yavuz and Lizzie Hernandez},
journal= {arXiv preprint arXiv:2302.00737},
year = {2023}
}
备注
31 pages