[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness

  • Conference paper
  • First Online:
Runtime Verification (RV 2020)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12399))

Included in the following conference series:

  • 888 Accesses

Abstract

This paper presents a general framework and methods for complete programming and checking of distributed algorithms at a high-level, as in pseudocode languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their safety and liveness properties, use DistAlgo, a high-level language for distributed algorithms. We give a complete executable specification of the checking framework, with a complete example algorithm and example safety and liveness properties.

This work was supported in part by NSF under grants CCF-1414078, CCF-1954837, CNS-1421893, and IIS-1447549, and ONR under grant N00014-20-1-2751.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    http://github.com/DistAlgo/distalgo/blob/master/benchmarks/controller.da.

References

  1. Birman, K., Joseph, T.: Exploiting virtual synchrony in distributed systems. In: Proceedings of the 11th ACM Symposium on Operating Systems Principles, pp. 123–138. ACM Press, November 1987

    Google Scholar 

  2. Birman, K., Malkhi, D., Renesse, R.V.: Virtually synchronous methodology for dynamic service replication. Technical report MSR-TR-2010-151, Microsoft Research (2010)

    Google Scholar 

  3. Birman, K.P., Joseph, T.A.: Reliable communication in the presence of failures. ACM Trans. Comput. Syst. (TOCS) 5(1), 47–76 (1987)

    Article  Google Scholar 

  4. Chand, S., Liu, Y.A.: What’s live? Understanding distributed consensus. Computing Research Repository arXiv:2001.04787 [cs.DC], January 2020. http://arxiv.org/abs/2001.04787

  5. Chand, S., Liu, Y.A., Stoller, S.D.: Formal verification of multi-Paxos for distributed consensus. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 119–136. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_8

    Chapter  Google Scholar 

  6. Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985)

    Article  MathSciNet  Google Scholar 

  7. Fokkink, W.: Distributed Algorithms: An Intuitive Approach. MIT Press, Cambridge (2013)

    MATH  Google Scholar 

  8. Francalanza, A., Pérez, J.A., Sánchez, C.: Runtime verification for decentralised and distributed systems. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 176–210. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_6

    Chapter  Google Scholar 

  9. Garg, V.K.: Elements of Distributed Computing. Wiley, New York (2002)

    Google Scholar 

  10. Gorbovitski, M., Rothamel, T., Liu, Y.A., Stoller, S.D.: Efficient runtime invariant checking: a framework and case study. In: Proceedings of the 6th International Workshop on Dynamic Analysis, pp. 43–49. ACM Press (2008)

    Google Scholar 

  11. Gorbovitski, M., Tekle, K.T., Rothamel, T., Stoller, S.D., Liu, Y.A.: Analysis and transformations for efficient query-based debugging. In: Proceedings of the 8th IEEE International Working Conference on Source Code Analysis and Manipulation, pp. 174–183. IEEE CS Press (2008)

    Google Scholar 

  12. Grall, A.: Automatic generation of DistAlgo programs from Event-B models. In: Raschke, A., Méry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 414–417. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_34

    Chapter  Google Scholar 

  13. Hawblitzel, C., et al.: IronFleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles, pp. 1–17. ACM Press (2015)

    Google Scholar 

  14. Kane, C., Lin, B., Chand, S., Stoller, S.D., Liu, Y.A.: High-level cryptographic abstractions. In: Proceedings of the ACM SIGSAC 14th Workshop on Programming Languages and Analysis for Security. ACM Press, London, November 2019

    Google Scholar 

  15. Kshemkalyani, A., Singhal, M.: Distributed Computing: Principles, Algorithms, and Systems. Cambridge University Press, Cambridge (2008)

    Book  Google Scholar 

  16. Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125–143 (1977)

    Article  MathSciNet  Google Scholar 

  17. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)

    Article  Google Scholar 

  18. Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)

    Article  Google Scholar 

  19. Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133–169 (1998)

    Article  Google Scholar 

  20. Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)

    Google Scholar 

  21. Lin, B., Liu, Y.A.: DistAlgo: a language for distributed algorithms (2014). http://github.com/DistAlgo. Accessed March 2020

  22. Liskov, B., Cowling, J.: Viewstamped replication revisited. Technical report MIT-CSAIL-TR-2012-021, Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge (2012)

    Google Scholar 

  23. Liu, Y.A.: Logical clocks are not fair: what is fair? A case study of high-level language and optimization. In: Proceedings of the Workshop on Advanced Tools, Programming Languages, and Platforms for Implementing and Evaluating Algorithms for Distributed Systems, pp. 21–27. ACM Press (2018)

    Google Scholar 

  24. Liu, Y.A., Brandvein, J., Stoller, S.D., Lin, B.: Demand-driven incremental object queries. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, pp. 228–241. ACM Press (2016)

    Google Scholar 

  25. Liu, Y.A., Chand, S., Stoller, S.D.: Moderately complex Paxos made simple: high-level executable specification of distributed algorithm. In: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, pp. 15:1–15:15. ACM Press, October 2019

    Google Scholar 

  26. Liu, Y.A., Stoller, S.D.: From classical to blockchain consensus: what are the exact algorithms? In: Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, July–August 2019, pp. 544–545. ACM Press (2019)

    Google Scholar 

  27. Liu, Y.A., Stoller, S.D., Chand, S., Weng, X.: Invariants in distributed algorithms. In: Proceedings of the TLA+ Community Meeting, Oxford, U.K. (2018). http://www.cs.stonybrook.edu/~liu/papers/DistInv-TLA18.pdf

  28. Liu, Y.A., Stoller, S.D., Lin, B.: High-level executable specifications of distributed algorithms. In: Richa, A.W., Scheideler, C. (eds.) SSS 2012. LNCS, vol. 7596, pp. 95–110. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33536-5_11

    Chapter  Google Scholar 

  29. Liu, Y.A., Stoller, S.D., Lin, B.: From clarity to efficiency for distributed algorithms. ACM Trans. Program. Lang. Syst. 39(3), 12:1–12:41 (2017)

    Article  Google Scholar 

  30. 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, pp. 395–410. ACM Press (2012)

    Google Scholar 

  31. Lynch, N.A.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996)

    MATH  Google Scholar 

  32. Machado, N., Maia, F., Neves, F., Coelho, F., Pereira, J.: Minha: large-scale distributed systems testing made practical. In: Felber, P., Friedman, R., Gilbert, S., Miller, A. (eds.) 23rd International Conference on Principles of Distributed Systems (OPODIS 2019). LIPIcs, vol. 153, pp. 11:1–11:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

    Google Scholar 

  33. McMillan, K.L., Padon, O.: Ivy: a multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 190–202. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_12

    Chapter  Google Scholar 

  34. Microsoft Research: the TLA toolbox. http://lamport.azurewebsites.net/tla/toolbox.html. Accessed 27 Apr 2020

  35. Oki, B.M., Liskov, B.H.: Viewstamped replication: a new primary copy method to support highly-available distributed systems. In: Proceedings of the 7th Annual ACM Symposium on Principles of Distributed Computing, pp. 8–17. ACM Press (1988)

    Google Scholar 

  36. Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA), 108:1–108:31 (2017). Article no. 108

    Google Scholar 

  37. Raynal, M.: Algorithms for Mutual Exclusion. MIT Press, Cambridge (1986)

    MATH  Google Scholar 

  38. Stoller, S.D.: Detecting global predicates in distributed systems with clocks. Distrib. Comput. 13(2), 85–98 (2000). https://doi.org/10.1007/s004460050069

    Article  Google Scholar 

  39. Stoller, S.D., Liu, Y.A.: Transformations for model checking distributed java programs. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 192–199. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45139-0_12

    Chapter  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Stony Brook University, Stony Brook, NY, USA

    Yanhong A. Liu & Scott D. Stoller

Authors
  1. Yanhong A. Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Scott D. Stoller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yanhong A. Liu .

Editor information

Editors and Affiliations

  1. University of Southern California, Los Angeles, CA, USA

    Jyotirmoy Deshmukh

  2. AIT Austrian Institute of Technology GmbH, Vienna, Austria

    Dejan Ničković

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Liu, Y.A., Stoller, S.D. (2020). Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness. In: Deshmukh, J., Ničković, D. (eds) Runtime Verification. RV 2020. Lecture Notes in Computer Science(), vol 12399. Springer, Cham. https://doi.org/10.1007/978-3-030-60508-7_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-60508-7_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-60507-0

  • Online ISBN: 978-3-030-60508-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation