Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Agha, G.: Actors: a model of concurrent computation in distributed systems. MIT Press (1986)
Alvaro, P., Condie, T., Conway, N., Hellerstein, J., Sears, R.: I do declare: Consensus in a logic language. ACM SIGOPS Operating Systems Review 43(4), 25–30 (2010)
Berkeley Orders of Magnitude. Bloom Programming Language, http://www.bloom-lang.net/
Bickford, M.: Component Specification Using Event Classes. In: Lewis, G.A., Poernomo, I., Hofmeister, C. (eds.) CBSE 2009. LNCS, vol. 5582, pp. 140–155. Springer, Heidelberg (2009)
Castro, M., Liskov, B.: Practical Byzantine fault tolerance and proactive recovery. ACM Transactions on Computer Systems 20, 398–461 (2002)
Chandra, T.D., Griesemer, R., Redstone, J.: Paxos made live—An engineering perspective. In: Proceedings of the 26th Annual ACM Symposium on Principles of Distributed Computing (PODC), pp. 398–407 (2007)
CRASH Project. EventML, http://www.nuprl.org/software/#WhatisEventML (last dated February 13, 2012)
De Prisco, R., Lampson, B., Lynch, N.: Revisiting the Paxos algorithm. Theoretical Computer Science 243, 35–91 (2000)
Fidge, C.J.: Timestamps in message-passing systems that preserve the partial ordering. In: Proceedings of the 11th Australian Computer Science Conference, pp. 56–66 (1988)
Garg, V.K.: Elements of Distributed Computing. Wiley (2002)
Gray, J.: Notes on Data Base Operating Systems. In: Flynn, M.J., Jones, A.K., Opderbeck, H., Randell, B., Wiehle, H.R., Gray, J.N., Lagally, K., Popek, G.J., Saltzer, J.H. (eds.) Operating Systems. LNCS, vol. 60, pp. 393–481. Springer, Heidelberg (1978)
Gupta, A., Mumick, I.S., Subrahmanian, V.S.: Maintaining views incrementally. In: Proceedings of the 1993 ACM SIGMOD International Conference on Management of Data, pp. 157–166 (1993)
http://groups.csail.mit.edu/tds/ioa/distributions/IOA_Toolkit-tools.tar.gz , The Paxos code is under Examples/Paxos
Kaynar, D., Lynch, N., Segala, R., Vaandrager, F.: The Theory of Timed I/O Automata, 2nd edn. Morgan Claypool Publishers (2010)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21, 558–565 (1978)
Lamport, L.: The part-time parliament. ACM Transactions on Computer Systems 16(2), 133–169 (1998)
Lamport, L.: Paxos made simple. SIGACT News (Distributed Computing Column) 32(4), 51–58 (2001)
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)
Lamport, L.: The PlusCal Algorithm Language. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 36–60. Springer, Heidelberg (2009)
Lamport, L.: Byzantizing Paxos by Refinement. In: Peleg, D. (ed.) DISC 2011. LNCS, vol. 6950, pp. 211–224. Springer, Heidelberg (2011)
Liu, Y.A., Gorbovitski, M., Stoller, S.D.: A language and framework for invariant-driven transformations. In: Proceedings of the 8th International Conference on Generative Programming and Component Engineering, pp. 55–64 (2009)
Liu, Y.A., Stoller, S.D., Gorbovitski, M., Rothamel, T., Liu, Y.E.: Incrementalization across object abstraction. In: Proceedings of the 20th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 473–486 (2005)
Liu, Y.A., Stoller, S.D., Lin, B., Gorbovitski, M.: From clarity to efficiency for distributed algorithms. In: Proceedings of the 27th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (2012)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufman (1996)
Mattern, F.: Virtual time and global states of distributed systems. In: Proc. International Workshop on Parallel and Distributed Algorithms, pp. 120–131 (1989)
Mechanically checked safety proof of a Byzantine Paxos algorithm http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html (last modified September 1, 2011)
Paige, R., Koenig, S.: Finite differencing of computable expressions. ACM Transactions on Programming Languages and Systems 4(3), 402–454 (1982)
Raynal, M.: Distributed Algorithms and Protocols. Wiley (1988)
Raynal, M.: Communication and Agreement Abstractions for Fault-Tolerant Asynchronous Distributed Systems. Morgan & Claypool (2010)
Sirer, E.G.: Email, August 12 (2011)
van Renesse, R.: Paxos made moderately complex, October 11 (2011), An online version is at http://www.cs.cornell.edu/courses/CS7412/2011sp/paxos.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, Y.A., Stoller, S.D., Lin, B. (2012). High-Level Executable Specifications of Distributed Algorithms. In: Richa, A.W., Scheideler, C. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2012. Lecture Notes in Computer Science, vol 7596. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33536-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-33536-5_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33535-8
Online ISBN: 978-3-642-33536-5
eBook Packages: Computer ScienceComputer Science (R0)