Skip to main content
SpringerLink
Log in

Formal Verification of Multi-Paxos for Distributed Consensus

  • Conference paper
  • First Online:
FM 2016: Formal Methods (FM 2016)

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

Included in the following conference series:

Abstract

This paper describes formal specification and verification of Lamport’s Multi-Paxos algorithm for distributed consensus. The specification is written in TLA+, Lamport’s Temporal Logic of Actions. The proof is written and checked using TLAPS, a proof system for TLA+. Building on Lamport, Merz, and Doligez’s specification and proof for Basic Paxos, we aim to facilitate the understanding of Multi-Paxos and its proof by minimizing the difference from those for Basic Paxos, and to demonstrate a general way of proving other variants of Paxos and other sophisticated distributed algorithms. We also discuss our general strategies for proving properties about sets and tuples that helped the proof check succeed in significantly reduced time.

This work was supported in part by NSF grants CCF-1414078, CCF-1248184, and CNS-1421893, ONR grant N000141512208, and AFOSR grant FA9550-14-1-0261. 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

References

  1. Burrows, M.: The Chubby lock service for loosely-coupled distributed systems. In: Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation, pp. 335–350. USENIX Association (2006)

    Google Scholar 

  2. Chand, S., Liu, Y.A., Stoller, S.D.: Formal Verification of Multi-Paxos for Distributed Consensus. arXiv preprint arXiv:1606.01387 (2016)

  3. 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, pp. 398–407 (2007)

    Google Scholar 

  4. Charron-Bost, B., Merz, S.: Formal verification of a consensus algorithm in the Heard-Of model. Int. J. Softw. Inform. 3(2–3), 273–303 (2009)

    Google Scholar 

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

  6. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  7. Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Upper Saddle River (1986)

    Google Scholar 

  8. Delzanno, G., Tatarek, M., Traverso, R.: Model checking Paxos in Spin. In: Proceedings of the 5th International Symposium on Games, Automata, Logics and Formal Verification, pp. 131–146 (2014)

    Google Scholar 

  9. Drăgoi, C., Henzinger, T.A., Zufferey, D.: Psync: A partially synchronous language for fault-tolerant distributed algorithms. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 400–415 (2016)

    Google Scholar 

  10. Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 110–121 (2005)

    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 (2015)

    Google Scholar 

  12. INRIA: The Coq Proof Assistant. http://coq.inria.fr/. (Last released January 2016)

  13. Isard, M.: Autopilot: Automatic data center management. ACM SIGOPS Oper. Syst. Rev. 41(2), 60–67 (2007)

    Article  Google Scholar 

  14. Kellomäki, P.: An annotated specification of the consensus protocol of Paxos using superposition in PVS. Report 36, Institute of Software Systems, Tampere University of Technology (2004)

    Google Scholar 

  15. Killian, C.E., Anderson, J.W., Braud, R., Jhala, R., Vahdat, A.M.: Mace: language support for building distributed systems. In: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 179–188 (2007)

    Google Scholar 

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

    Article  Google Scholar 

  17. Lamport, L.: Paxos made simple. SIGACT News (Distrib. Comput. Column) 32(4), 51–58 (2001)

    Google Scholar 

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

    Google Scholar 

  19. Lamport, L.: Fast Paxos. Distrib. Comput. 19(2), 79–103 (2006). http://research.microsoft.com/pubs/64624/tr-2005-112.pdf

    Article  MATH  Google Scholar 

  20. Lamport, L.: Byzantizing paxos by refinement. In: Peleg, D. (ed.) DISC 2011. LNCS, vol. 6950, pp. 211–224. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24100-0_22

    Chapter  Google Scholar 

  21. Lamport, L.: My writings. http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#lamport-paxos. Accessed 24 Jan 2016. Lamport’s history of paper [16]

  22. Lamport, L., Merz, S., Doligez, D.: A TLA spefication of the Paxos Consensus algorithm described in Paxos Made Simple and a TLAPS-checked proof of its correctness. file /tlapm/examples/paxos/Paxos.tla in TLAPS distribution, November 2012. http://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-1.4.3.tar.gz. Accessed 28 Nov 2014

  23. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17511-4_20

    Chapter  Google Scholar 

  24. Liu, X., Guo, Z., Wang, X., Chen, F., Lian, X., Tang, J., Wu, M., Kaashoek, M.F., Zhang, Z.: D3S: debugging deployed distributed systems. In: Proceedings of the 5th USENIX Symposium on Networked Systems Design and Implementation, pp. 423–437. USENIX Association (2008)

    Google Scholar 

  25. Microsoft Research: The TLA Toolbox. http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html. Accessed 4 Jan 2016

  26. Microsoft Research-Inria Joint Center: TLA+ Proof System (TLAPS). http://tla.msr-inria.inria.fr/tlaps/. (Last released June 2015)

  27. Ongaro, D., Ousterhout, J.: In search of an understandable consensus algorithm. In: 2014 USENIX Annual Technical Conference (USENIX ATC 14), pp. 305–319. USENIX Association (2014). http://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro

  28. PRL Project: EventML. http://www.nuprl.org/software/#WhatisEventML. Accessed 21 Sep 2012

  29. van Renesse, R., Altinbuken, D.: Paxos made moderately complex. ACM Comput. Surv. 47(3), 1–36 (2015)

    Article  Google Scholar 

  30. Schiper, N., Rahli, V., van Renesse, R., Bickford, M., Constable, R.L.: Developing correctly replicated databases using formal tools. In: Proceedings of the 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, pp. 395–406. IEEE CS Press (2014)

    Google Scholar 

  31. Spin Community: Verifying Multi-threaded Software with Spin. http://spinroot.com/spin/whatispin.html. (Last released January 1, 2016)

  32. SRI: PVS Specification and Verification System. http://pvs.csl.sri.com/. (Last released February 11, 2013)

  33. University of Cambridge: Isabelle (a generic proof assistant). http://isabelle.in.tum.de/. (Last released May 25, 2015)

  34. 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: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 357–368 (2015)

    Google Scholar 

  35. Yabandeh, M., Knezevic, N., Kostic, D., Kuncak, V.: CrystalBall: predicting and preventing inconsistencies in deployed distributed systems. In: Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, pp. 229–244. USENIX Association (2009)

    Google Scholar 

  36. Yang, J., Chen, T., Wu, M., Xu, Z., Liu, X., Lin, H., Yang, M., Long, F., Zhang, L., Zhou, L.: MoDist: transparent model checking of unmodified distributed systems. In: Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, pp. 213–228. USENIX Association (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Stony Brook University, Stony Brook, New York, 11794, USA

    Saksham Chand, Yanhong A. Liu & Scott D. Stoller

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

  3. Scott D. Stoller
    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. Newcastle University, Newcastle upon Tyne, United Kingdom

    John Fitzgerald

  2. US Naval Research Laboratory, Washington, District of Columbia, USA

    Constance Heitmeyer

  3. ISTI-CNR, Pisa, Italy

    Stefania Gnesi

  4. University of Cyprus, Nicosia, Cyprus

    Anna Philippou

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Chand, S., Liu, Y.A., Stoller, S.D. (2016). Formal Verification of Multi-Paxos for Distributed Consensus. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-48989-6_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-48988-9

  • Online ISBN: 978-3-319-48989-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation