TY - GEN
T1 - High-level executable specifications of distributed algorithms
AU - Liu, Yanhong A.
AU - Stoller, Scott D.
AU - Lin, Bo
PY - 2012
Y1 - 2012
N2 - This paper describes a method for specifying complex distributed algorithms at a very high yet executable level, focusing in particular on general principles for making properties and invariants explicit while keeping the control flow clear. This is critical for understanding the algorithms and proving their correctness. It is also critical for generating efficient implementations using invariant-preserving transformations, ensuring the correctness of the optimizations. We have studied and experimented with a variety of important distributed algorithms, including well-known difficult variants of Paxos, by specifying them in a very high-level language with an operational semantics. In the specifications that resulted from following our method, critical properties and invariants are explicit, making the algorithms easier to understand and verify. Indeed, this helped us discover improvements to some of the algorithms, for correctness and for optimizations.
AB - This paper describes a method for specifying complex distributed algorithms at a very high yet executable level, focusing in particular on general principles for making properties and invariants explicit while keeping the control flow clear. This is critical for understanding the algorithms and proving their correctness. It is also critical for generating efficient implementations using invariant-preserving transformations, ensuring the correctness of the optimizations. We have studied and experimented with a variety of important distributed algorithms, including well-known difficult variants of Paxos, by specifying them in a very high-level language with an operational semantics. In the specifications that resulted from following our method, critical properties and invariants are explicit, making the algorithms easier to understand and verify. Indeed, this helped us discover improvements to some of the algorithms, for correctness and for optimizations.
UR - https://www.scopus.com/pages/publications/84868296311
U2 - 10.1007/978-3-642-33536-5_11
DO - 10.1007/978-3-642-33536-5_11
M3 - Conference contribution
AN - SCOPUS:84868296311
SN - 9783642335358
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 95
EP - 110
BT - Stabilization, Safety, and Security of Distributed Systems - 14th International Symposium, SSS 2012, Proceedings
T2 - 14th International Symposium on Stabilization, Safety, and Security of Distributed Systems, SSS 2012
Y2 - 1 October 2012 through 4 October 2012
ER -