Multi-Grained Specifications for Distributed System Model Checking and Verification

TL;DR

This paper demonstrates a multi-grained specification approach using TLA+ and model checking to verify ZooKeeper's correctness, effectively balancing detail and scalability in evolving distributed systems.

Contribution

It introduces a novel multi-grained specification methodology that manages the trade-off between detail and scalability in model checking complex, evolving distributed systems.

Findings

Detected six severe bugs and verified their fixes

Developed composable multi-grained specifications

Improved protocol design for correctness

Abstract

This paper presents our experience specifying and verifying the correctness of ZooKeeper, a complex and evolving distributed coordination system. We use TLA+ to model fine-grained behaviors of ZooKeeper and use the TLC model checker to verify its correctness properties; we also check conformance between the model and code. The fundamental challenge is to balance the granularity of specifications and the scalability of model checking -- fine-grained specifications lead to state-space explosion, while coarse-grained specifications introduce model-code gaps. To address this challenge, we write specifications with different granularities for composable modules, and compose them into mixed-grained specifications based on specific scenarios. For example, to verify code changes, we compose fine-grained specifications of changed modules and coarse-grained specifications that abstract away details of unchanged code with preserved interactions. We show that writing multi-grained specifications is a viable practice and can cope with model-code gaps without untenable state space, especially for evolving software where changes are typically local and incremental. We detected six severe bugs that violate five types of invariants and verified their code fixes; the fixes have been merged to ZooKeeper. We also improve the protocol design to make it easy to implement correctly.