Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables

Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)

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 is a preview of subscription content, log in to check access

References

  1. 1.
    Abadi, M., Lamport, L.: The existence of refinement mappings. Theoret. Comput. Sci. 82(2), 253–284 (1991)MathSciNetCrossRefMATHGoogle Scholar
  2. 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 CrossRefGoogle Scholar
  3. 3.
    Charron-Bost, B., Schiper, A.: The Heard-Of model: computing in distributed systems with benign faults. Distrib. Comput. 22(1), 49–71 (2009)CrossRefMATHGoogle Scholar
  4. 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 CrossRefGoogle Scholar
  5. 5.
    Clarke, E.M.: Proving correctness of coroutines without history variables. Acta Inform. 13(2), 169–188 (1980)MathSciNetCrossRefMATHGoogle Scholar
  6. 6.
    Clint, M.: Program proving: coroutines. Acta inform. 2(1), 50–63 (1973)CrossRefGoogle Scholar
  7. 7.
    Clint, M.: On the use of history variables. Acta Inform. 16(1), 15–30 (1981)CrossRefMATHGoogle Scholar
  8. 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)CrossRefMATHGoogle Scholar
  9. 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. 10.
    Gorbovitski, M.: A system for invariant-driven transformations. Ph.D. thesis, Computer Science Department, Stony Brook University (2011)Google Scholar
  11. 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. 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 CrossRefGoogle Scholar
  13. 13.
    Lamport, L.: My writings : proving the correctness of multiprocess programs. https://lamport.azurewebsites.net/pubs/pubs.html. Accessed 10 Oct 2017
  14. 14.
    Lamport, L.: The implementation of reliable distributed multiprocess systems. Comput. Netw. 2(2), 95–114 (1978)Google Scholar
  15. 15.
    Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(3), 872–923 (1994)CrossRefGoogle Scholar
  16. 16.
    Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. (TOCS) 16(2), 133–169 (1998)CrossRefGoogle Scholar
  17. 17.
    Lamport, L.: Paxos made simple. ACM Sigact News 32(4), 18–25 (2001)Google Scholar
  18. 18.
    Lamport, L., Merz, S.: Auxiliary variables in TLA+. ArXiv e-prints, March 2017Google Scholar
  19. 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. 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. 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)CrossRefGoogle Scholar
  22. 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. 23.
    Liu, Y.A.: Systematic Program Design: From Clarity To Efficiency. Cambridge University Press, Cambridge (2013)CrossRefGoogle Scholar
  24. 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. 25.
    Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs i. Acta Inform. 6(4), 319–340 (1976)MathSciNetCrossRefMATHGoogle Scholar
  26. 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)CrossRefGoogle Scholar
  27. 27.
    Paige, R., Koenig, S.: Finite differencing of computable expressions. ACM Trans. Program. Lang. Syst. (TOPLAS) 4(3), 402–454 (1982)CrossRefMATHGoogle Scholar
  28. 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. 29.
    Schilling, K.: Perspectives for miniaturized, distributed, networked cooperating systems for space exploration. Robot. Auton. Syst. 90, 118–124 (2017)CrossRefGoogle Scholar
  30. 30.
    Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2(POPL), 28 (2017)CrossRefGoogle Scholar
  31. 31.
    Tschorsch, F., Scheuermann, B.: Bitcoin and beyond: a technical survey on decentralized digital currencies. IEEE Commun. Surv. Tutor. 18(3), 2084–2123 (2016)CrossRefGoogle Scholar
  32. 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. 33.
    Zave, P.: Using lightweight modeling to understand Chord. ACM SIGCOMM Comput. Commun. Rev. 42(2), 49–57 (2012)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Stony Brook UniversityStony BrookUSA

Personalised recommendations