Moderately Complex Paxos Made Simple
Yanhong A. Liu, Saksham Chand, Scott D. Stoller · 2019
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.