  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.
