SandTable: Scalable Distributed System Model Checking with Specification-Level State Exploration

Implementation-level distributed system model checkers (DMCKs) have proven valuable in verifying the correctness of real distributed systems. However, they primarily focus on state space reduction, and often have a bottleneck on another crucial dimension: exploration speed. To scale DMCK, we introduce SandTable, a technique for lifting state-space exploration from the implementation level to the specification level, and confirming bugs at the implementation level. We made SandTable practical through a methodology consisting of four essential parts: (1) writing specifications that adhere to the implementation, (2) checking conformance to enhance specification quality and reduce false positives and false negatives, (3) exploring the state space with heuristics for effectiveness and efficiency, and (4) confirming bugs and verifying their fixes in the implementation.

We implemented SandTable with the design of transparently verifying unmodified distributed systems on POSIX systems. SandTable was integrated into eight well-established open-source distributed systems that implement consensus protocols such as Raft and Zab. SandTable identified 23 bugs in total, with 18 new bugs, 17 confirmed, and 13 fixed. SandTable demonstrates exceptional scalability, with