利用 TLA+ 规约提升 ZooKeeper 协调服务的可靠性
分布式、并行与集群计算
2023-10-17 v2
摘要
ZooKeeper 是一种协调服务，被广泛用作各种分布式系统的骨干。尽管其可靠性至关重要，但对于像 ZooKeeper 这样规模和复杂度的工业级系统，测试是不充分的，仍然可以发现深层 bug。为此，我们求助于形式化 TLA+ 规约以进一步提升 ZooKeeper 的可靠性。我们的首要目标是可用性与自动化，而非完全验证。我们增量地开发了三个层级的 ZooKeeper 规约。我们首先获得了协议规约，它明确地规定了 ZooKeeper 背后的 Zab 协议。然后我们进一步细化，获得了系统规约，它作为系统开发的超级文档。为了进一步利用模型级规约来提升代码级实现的可靠性，我们开发了测试规约，用于指导 ZooKeeper 实现的探索性测试。形式化规约有助于消除协议设计中的歧义，并提供全面的系统文档。它们还有助于发现系统实现中关键的深层 bug，这些 bug 是最先进的测试技术无法触及的。我们的规约已被合并入官方 Apache ZooKeeper 项目。
引用
@article{arxiv.2302.02703,
title = {Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeper Coordination Service},
author = {Lingzhi Ouyang and Yu Huang and Binyu Huang and Xiaoxing Ma},
journal= {arXiv preprint arXiv:2302.02703},
year = {2023}
}