Moderately Complex Paxos Made Simple: High-Level Executable Specification of Distributed Algorithms

TL;DR

This paper demonstrates how high-level executable specifications of complex Paxos variants can be created using DistAlgo, leading to simpler, more precise, and verifiable distributed algorithms that facilitate optimization and correctness proofs.

Contribution

The authors introduce a high-level language-based approach to specify complex Paxos variants, enabling clearer, more compact, and executable specifications that improve understanding and verification.

Findings

Specifications are complete and precise at a high level.

Simpler specifications reveal issues in previous designs.

Executable and optimizable specifications improve performance.

Abstract

This paper describes the application of a high-level language and method in developing simpler specifications of more complex variants of the Paxos algorithm for distributed consensus. The specifications are for Multi-Paxos with preemption, replicated state machine, and reconfiguration and optimized with state reduction and failure detection. The language is DistAlgo. The key is to express complex control flows and synchronization conditions precisely at a high level, using nondeterministic waits and message-history queries. We obtain complete executable specifications that are almost completely declarative---updating only a number for the protocol round besides the sets of messages sent and received. We show the following results: 1.English and pseudocode descriptions of distributed algorithms can be captured completely and precisely at a high level, without adding, removing, or reformulating algorithm details to fit lower-level, more abstract, or less direct languages. 2.We created higher-level control flows and synchronization conditions than all previous specifications, and obtained specifications that are much simpler and smaller, even matching or smaller than abstract specifications that omit many algorithm details. 3.The simpler specifications led us to easily discover useless replies, unnecessary delays, and liveness violations (if messages can be lost) in previous published specifications, by just following the simplified algorithm flows. 4.The resulting specifications can be executed directly, and we can express optimizations cleanly, yielding drastic performance improvement over naive execution and facilitating a general method for merging processes. 5.We systematically translated the resulting specifications into TLA+ and developed machine-checked safety proofs, which also allowed us to detect and fix a subtle safety violation in an earlier unpublished specification.