Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables
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.
References
- 1.Abadi, M., Lamport, L.: The existence of refinement mappings. Theoret. Comput. Sci. 82(2), 253–284 (1991)MathSciNetCrossRefMATHGoogle 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 CrossRefGoogle 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)CrossRefMATHGoogle 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 CrossRefGoogle Scholar
- 5.Clarke, E.M.: Proving correctness of coroutines without history variables. Acta Inform. 13(2), 169–188 (1980)MathSciNetCrossRefMATHGoogle Scholar
- 6.Clint, M.: Program proving: coroutines. Acta inform. 2(1), 50–63 (1973)CrossRefGoogle Scholar
- 7.Clint, M.: On the use of history variables. Acta Inform. 16(1), 15–30 (1981)CrossRefMATHGoogle 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)CrossRefMATHGoogle 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 CrossRefGoogle 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)CrossRefGoogle Scholar
- 16.Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. (TOCS) 16(2), 133–169 (1998)CrossRefGoogle 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 2017Google 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)CrossRefGoogle 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)CrossRefGoogle 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)MathSciNetCrossRefMATHGoogle 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)CrossRefGoogle Scholar
- 27.Paige, R., Koenig, S.: Finite differencing of computable expressions. ACM Trans. Program. Lang. Syst. (TOPLAS) 4(3), 402–454 (1982)CrossRefMATHGoogle 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)CrossRefGoogle Scholar
- 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.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.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)CrossRefGoogle Scholar