Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeper Coordination Service

TL;DR

This paper demonstrates how formal TLA+ specifications can enhance the reliability of ZooKeeper by clarifying protocols, guiding testing, and identifying deep bugs beyond traditional testing methods.

Contribution

It introduces a multi-level specification approach for ZooKeeper using TLA+, integrating formal specs into the official project to improve reliability and documentation.

Findings

Formal specifications clarified protocol ambiguities

Deep bugs were identified that traditional testing missed

Specifications were integrated into the official ZooKeeper project

Abstract

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.