利用TLA+规范提高ZooKeeper协调服务的可靠性
Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeper Coordination Service
AI总结：
本文通过为ZooKeeper开发三级TLA+规范（协议、系统、测试），提高其可靠性，消除协议歧义，指导探索性测试，发现深层缺陷，并已合并入官方项目。
摘要：
ZooKeeper是一种协调服务，广泛用作各种分布式系统的骨干。尽管其可靠性至关重要，但对于规模和复杂度达到ZooKeeper级别的工业级系统而言，测试是不够的，深层缺陷仍可能被发现。为此，我们求助于正式的TLA+规范，以进一步提高ZooKeeper的可靠性。我们的主要目标是可用性和自动化，而非完全验证。我们为ZooKeeper增量式地开发了三个级别的规范。我们首先获得协议规范，它明确规定了ZooKeeper背后的Zab协议。然后我们进一步细化，获得系统规范，它作为系统开发的超级文档。为了进一步利用模型级规范来提高代码级实现的可靠性，我们开发了测试规范，它指导ZooKeeper实现的探索性测试。这些正式规范有助于消除协议设计中的歧义，并提供全面的系统文档。它们还有助于发现系统实现中的关键深层缺陷，这些缺陷超出了最先进测试技术的范围。我们的规范已合并到Apache ZooKeeper官方项目中。
英文摘要：
ZooKeeper is a coordination service, widely used as a backbone of various distributed systems. Though its reliability is of critical importance, testing is insufficient for an industrial-strength system of the size and complexity of ZooKeeper, and deep bugs can still be found. To this end, we resort to formal TLA+ specifications to further improve the reliability of ZooKeeper. Our primary objective is usability and automation, rather than full verification. We incrementally develop three levels of specifications for ZooKeeper. We first obtain the protocol specification, which unambiguously specifies the Zab protocol behind ZooKeeper. We then proceed to a finer grain and obtain the system specification, which serves as the super-doc for system development. In order to further leverage the model-level specification to improve the reliability of the code-level implementation, we develop the test specification, which guides the explorative testing of the ZooKeeper implementation. The formal specifications help eliminate the ambiguities in the protocol design and provide comprehensive system documentation. They also help find critical deep bugs in system implementation, which are beyond the reach of state-of-the-art testing techniques. Our specifications have been merged into the official Apache ZooKeeper project.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
