Skip to main content
SpringerLink
Log in

Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2018)

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

Included in the following conference series:

  • 1496 Accesses

Abstract

This paper studies specifications and proofs of distributed algorithms when only message history variables are used, using Basic Paxos and Multi-Paxos for distributed consensus as precise case studies. We show that not using and maintaining other state variables yields simpler specifications that are more declarative and easier to understand. It also allows easier proofs to be developed by needing fewer invariants and facilitating proof derivations. Furthermore, the proofs are mechanically checked more efficiently.

We show that specifications in TLA+ and proofs in TLA+ Proof System (TLAPS) are reduced by 25% and 27%, respectively, for Basic Paxos, and 46% (from about 100 lines to about 50 lines) and 48% (from about 1000 lines to about 500 lines), respectively, for Multi-Paxos. Overall we need 54% fewer manually written invariants and our proofs have 46% fewer obligations. Our proof for Basic Paxos takes 26% less time than Lamport et al.’s for TLAPS to check, and our proofs for Multi-Paxos are checked by TLAPS within 1.5 min whereas prior proofs for Multi-Paxos fail to be checked in the new version of TLAPS.

This work was supported in part by NSF grants CCF-1414078 and CCF-1248184 and ONR grant N000141512208. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of these agencies.

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

Access this chapter

Log in via an institution
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

Notes

  1. 1.

    This is different than some other references of the term history variables that include sequences of local actions, i.e., execution history [6].

References

  1. Abadi, M., Lamport, L.: The existence of refinement mappings. Theoret. Comput. Sci. 82(2), 253–284 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  2. 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 

  3. Charron-Bost, B., Schiper, A.: The Heard-Of model: computing in distributed systems with benign faults. Distrib. Comput. 22(1), 49–71 (2009)

    Article  MATH  Google Scholar 

  4. Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA+ proof system: building a heterogeneous verification platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, p. 44. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14808-8_3

    Chapter  Google Scholar 

  5. Clarke, E.M.: Proving correctness of coroutines without history variables. Acta Inform. 13(2), 169–188 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  6. Clint, M.: Program proving: coroutines. Acta inform. 2(1), 50–63 (1973)

    Article  Google Scholar 

  7. Clint, M.: On the use of history variables. Acta Inform. 16(1), 15–30 (1981)

    Article  MATH  Google Scholar 

  8. Drăgoi, C., Henzinger, T.A., Zufferey, D.: PSync: a partially synchronous language for fault-tolerant distributed algorithms. ACM SIGPLAN Notices 51(1), 400–415 (2016)

    Article  MATH  Google Scholar 

  9. Gerla, M., Lee, E.-K., Pau, G., Lee, U.: Internet of vehicles: from intelligent grid to autonomous cars and vehicular clouds. In: 2014 IEEE World Forum on Internet of Things (WF-IoT), pp. 241–246. IEEE (2014)

    Google Scholar 

  10. Gorbovitski, M.: A system for invariant-driven transformations. Ph.D. thesis, Computer Science Department, Stony Brook University (2011)

    Google Scholar 

  11. Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S., Zill, B.: IronFleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles, pp. 1–17. ACM (2015)

    Google Scholar 

  12. Küfner, P., Nestmann, U., Rickmann, C.: Formal verification of distributed algorithms. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 209–224. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33475-7_15

    Chapter  Google Scholar 

  13. Lamport, L.: My writings : proving the correctness of multiprocess programs. https://lamport.azurewebsites.net/pubs/pubs.html. Accessed 10 Oct 2017

  14. Lamport, L.: The implementation of reliable distributed multiprocess systems. Comput. Netw. 2(2), 95–114 (1978)

    Google Scholar 

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

    Article  Google Scholar 

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

    Article  Google Scholar 

  17. Lamport, L.: Paxos made simple. ACM Sigact News 32(4), 18–25 (2001)

    Google Scholar 

  18. Lamport, L., Merz, S.: Auxiliary variables in TLA+. ArXiv e-prints, March 2017

    Google Scholar 

  19. Lamport, L., Merz, S., Doligez, D.: Paxos.tla. https://github.com/tlaplus/v1-tlapm/blob/master/examples/paxos/Paxos.tla. Accessed 6 Feb 2018

  20. 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 (PPDP), pp. 228–241. ACM (2016)

    Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

  23. Liu, Y.A.: Systematic Program Design: From Clarity To Efficiency. Cambridge University Press, Cambridge (2013)

    Book  Google Scholar 

  24. Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, pp. 137–151. ACM (1987)

    Google Scholar 

  25. Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs i. Acta Inform. 6(4), 319–340 (1976)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  Google Scholar 

  27. Paige, R., Koenig, S.: Finite differencing of computable expressions. ACM Trans. Program. Lang. Syst. (TOPLAS) 4(3), 402–454 (1982)

    Article  MATH  Google Scholar 

  28. Rothamel, T., Liu, Y.A.: Generating incremental implementations of object-set queries. In: Proceedings of the 7th International Conference on Generative Programming and Component Engineering, pp. 55–66. ACM (2008)

    Google Scholar 

  29. Schilling, K.: Perspectives for miniaturized, distributed, networked cooperating systems for space exploration. Robot. Auton. Syst. 90, 118–124 (2017)

    Article  Google Scholar 

  30. Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2(POPL), 28 (2017)

    Article  Google Scholar 

  31. Tschorsch, F., Scheuermann, B.: Bitcoin and beyond: a technical survey on decentralized digital currencies. IEEE Commun. Surv. Tutor. 18(3), 2084–2123 (2016)

    Article  Google Scholar 

  32. Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.: Verdi: a framework for implementing and formally verifying distributed systems. In: ACM SIGPLAN Notices, vol. 50, pp. 357–368. ACM (2015)

    Google Scholar 

  33. Zave, P.: Using lightweight modeling to understand Chord. ACM SIGCOMM Comput. Commun. Rev. 42(2), 49–57 (2012)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Stony Brook University, Stony Brook, NY, 11794, USA

    Saksham Chand & Yanhong A. Liu

Authors
  1. Saksham Chand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yanhong A. Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Saksham Chand .

Editor information

Editors and Affiliations

  1. NASA Langley Research Center, Hampton, Virginia, USA

    Aaron Dutle

  2. NASA Langley Research Center, Hampton, Virginia, USA

    César Muñoz

  3. NASA Langley Research Center, Hampton, Virginia, USA

    Anthony Narkawicz

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Chand, S., Liu, Y.A. (2018). Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds) NASA Formal Methods. NFM 2018. Lecture Notes in Computer Science(), vol 10811. Springer, Cham. https://doi.org/10.1007/978-3-319-77935-5_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-77935-5_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-77934-8

  • Online ISBN: 978-3-319-77935-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation