TY - GEN
T1 - Moderately complex paxos made simple
T2 - 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
AU - Liu, Yanhong A.
AU - Chand, Saksham
AU - Stoller, Scott D.
N1 - Publisher Copyright:
© 2019 ACM.
PY - 2019/10/7
Y1 - 2019/10/7
N2 - 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. Additionally, we show the basic concepts in Paxos that are fundamental in many distributed algorithms and show that they are captured concisely in our specifications.
AB - 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. Additionally, we show the basic concepts in Paxos that are fundamental in many distributed algorithms and show that they are captured concisely in our specifications.
KW - Distributed algorithms
KW - Distributed consensus executable specification
KW - High-level specification
KW - Message-history queries
KW - Paxos
UR - https://www.scopus.com/pages/publications/85083363691
U2 - 10.1145/3354166.3354180
DO - 10.1145/3354166.3354180
M3 - Conference contribution
AN - SCOPUS:85083363691
T3 - ACM International Conference Proceeding Series
BT - Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
PB - Association for Computing Machinery
Y2 - 7 October 2019 through 9 October 2019
ER -