Advertisement

High-Level Executable Specifications of Distributed Algorithms

  • Yanhong A. Liu
  • Scott D. Stoller
  • Bo Lin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7596)

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.

Keywords

Operational Semantic Pseudo Code Mutual Exclusion Receive Message Synchronization Condition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Agha, G.: Actors: a model of concurrent computation in distributed systems. MIT Press (1986)Google Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Berkeley Orders of Magnitude. Bloom Programming Language, http://www.bloom-lang.net/
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Castro, M., Liskov, B.: Practical Byzantine fault tolerance and proactive recovery. ACM Transactions on Computer Systems 20, 398–461 (2002)CrossRefGoogle Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    CRASH Project. EventML, http://www.nuprl.org/software/#WhatisEventML (last dated February 13, 2012)
  8. 8.
    De Prisco, R., Lampson, B., Lynch, N.: Revisiting the Paxos algorithm. Theoretical Computer Science 243, 35–91 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Garg, V.K.: Elements of Distributed Computing. Wiley (2002)Google Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    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)Google Scholar
  13. 13.
  14. 14.
    Kaynar, D., Lynch, N., Segala, R., Vaandrager, F.: The Theory of Timed I/O Automata, 2nd edn. Morgan Claypool Publishers (2010)Google Scholar
  15. 15.
    Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21, 558–565 (1978)zbMATHCrossRefGoogle Scholar
  16. 16.
    Lamport, L.: The part-time parliament. ACM Transactions on Computer Systems 16(2), 133–169 (1998)CrossRefGoogle Scholar
  17. 17.
    Lamport, L.: Paxos made simple. SIGACT News (Distributed Computing Column) 32(4), 51–58 (2001)Google Scholar
  18. 18.
    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)Google Scholar
  19. 19.
    Lamport, L.: The PlusCal Algorithm Language. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 36–60. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  20. 20.
    Lamport, L.: Byzantizing Paxos by Refinement. In: Peleg, D. (ed.) DISC 2011. LNCS, vol. 6950, pp. 211–224. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  21. 21.
    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)Google Scholar
  22. 22.
    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)Google Scholar
  23. 23.
    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)Google Scholar
  24. 24.
    Lynch, N.A.: Distributed Algorithms. Morgan Kaufman (1996)Google Scholar
  25. 25.
    Mattern, F.: Virtual time and global states of distributed systems. In: Proc. International Workshop on Parallel and Distributed Algorithms, pp. 120–131 (1989)Google Scholar
  26. 26.
    Mechanically checked safety proof of a Byzantine Paxos algorithmhttp://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html (last modified September 1, 2011)
  27. 27.
  28. 28.
    Paige, R., Koenig, S.: Finite differencing of computable expressions. ACM Transactions on Programming Languages and Systems 4(3), 402–454 (1982)zbMATHCrossRefGoogle Scholar
  29. 29.
  30. 30.
    Raynal, M.: Distributed Algorithms and Protocols. Wiley (1988)Google Scholar
  31. 31.
    Raynal, M.: Communication and Agreement Abstractions for Fault-Tolerant Asynchronous Distributed Systems. Morgan & Claypool (2010)Google Scholar
  32. 32.
    Sirer, E.G.: Email, August 12 (2011)Google Scholar
  33. 33.
    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

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Yanhong A. Liu
    • 1
  • Scott D. Stoller
    • 1
  • Bo Lin
    • 1
  1. 1.Computer Science DepartmentState University of New York at Stony BrookUSA

Personalised recommendations