Paxos made EPR: decidable reasoning about distributed protocols

Abstract

Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in verifying such protocols. However, checking invariants of such protocols is undecidable and hard in practice, as it requires reasoning about an unbounded number of nodes and messages. Moreover, protocol actions and invariants involve both quantifier alternations and higher-order concepts such as set cardinalities and arithmetic.

This paper makes a step towards automatic verification of such protocols. We aim at a technique that can verify correct protocols and identify bugs in incorrect protocols. To this end, we develop a methodology for deductive verification based on effectively propositional logic (EPR)—a decidable fragment of first-order logic (also known as the Bernays-Schönfinkel-Ramsey class). In addition to decidability, EPR also enjoys the finite model property, allowing to display violations as finite structures which are intuitive for users. Our methodology involves modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check. The steps of the transformations are also mechanically checked, ensuring the soundness of the method. We have used our methodology to verify the safety of Paxos, and several of its variants, including Multi-Paxos, Vertical Paxos, Fast Paxos, Flexible Paxos and Stoppable Paxos. To the best of our knowledge, this work is the first to verify these protocols using a decidable logic, and the first formal verification of Vertical Paxos, Fast Paxos and Stoppable Paxos.

References

1. Francesco Alberti, Silvio Ghilardi, and Elena Pagani. 2016. Counting Constraints in Flat Array Fragments. In Automated Reasoning. Springer, Cham, 65–81.
2. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. 171–177.
3. Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Springer.
4. Ken Birman. 2010. A History of the Virtual Synchrony Replication Model. In Replication: Theory and Practice (Lecture Notes in Computer Science), Bernadette Charron-Bost, Fernando Pedone, and André Schiper (Eds.), Vol. 5959. Springer, 91–120.
5. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. 2015. Decidability of Parameterized Verification. Morgan & Claypool Publishers.
6. Michael Burrows. 2006. The Chubby Lock Service for Loosely-Coupled Distributed Systems. In 7th Symposium on Operating Systems Design and Implementation OSDI ’06), November 6-8, Seattle, WA, USA. USENIX Association, 335–350.
7. Saksham Chand, Yanhong A. Liu, and Scott D. Stoller. 2016. Formal Verification of Multi-Paxos for Distributed Consensus. In FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings 21. Springer, 119–136.
8. Bernadette Charron-Bost and André Schiper. 2009. The Heard-of Model: Computing in Distributed Systems with Benign Faults. Distributed Computing 22, 1 (2009), 49–71.
9. Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. 2010. The TLA+Proof System: Building a Heterogeneous Verification Platform. In Proceedings of the 7th International Colloquium Conference on Theoretical Aspects of Computing (ICTAC’10). Springer-Verlag, 44–44.
10. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2016. Using Crash Hoare Logic for Certifying the FSCQ File System. In 2016 USENIX Annual Technical Conference, USENIX ATC 2016, Denver, CO, USA, June 22-24, 2016.
11. Gregory V. Chockler, Idit Keidar, and Roman Vitenberg. 2001. Group communication specifications: a comprehensive study. ACM Comput. Surv. 33, 4 (2001), 427–469.
12. Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (Lecture Notes in Computer Science), Vol. 4963. Springer, 337–340.
13. Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. 2014. A Logic-Based Framework for Verifying Consensus Algorithms. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 161–181.
14. Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey. 2016. PSync: A Partially Synchronous Language for FaultTolerant Distributed Algorithms. ACM SIGPLAN Notices 51, 1 (2016), 400–415.
15. Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, and Sharon Shoham. 2017. Bounded Quantifier Instantiation for Checking Inductive Invariants. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I (Lecture Notes in Computer Science), Axel Legay and Tiziana Margaria (Eds.), Vol. 10205. 76–95.
16. Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP. 1–17.
17. Heidi Howard, Dahlia Malkhi, and Alexander Spiegelman. 2016. Flexible Paxos: Quorum Intersection Revisited. arXiv preprint arXiv:1608.06696 (2016).
18. Shachar Itzhaky. 2014. Automatic Reasoning for Pointer Programs Using Decidable Logics. Ph.D. Dissertation. Tel Aviv University.
19. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, and Mooly Sagiv. 2014. Modular reasoning about heap paths via effectively propositional formulas. In the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 385–396.
20. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, and Mooly Sagiv. 2013. Effectively-Propositional Reasoning about Reachability in Linked Data Structures. In CAV (LNCS), Vol. 8044. 756–772.
21. Daniel Jackson. 2006. Software Abstractions: Logic, Language, and Analysis. The MIT Press.
22. Mauro Jaskelioff and Stephan Merz. 2005. Proving the Correctness of Disk Paxos. Archive of Formal Proofs (June 2005). http://isa- afp.org/entries/DiskPaxos.shtml , Formal proof development.
23. Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder. 2017. A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM, 719–734.
24. Igor Konnov, Helmut Veith, and Josef Widder. 2015a. SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. In Computer Aided Verification. Springer, Cham, 85–102.
25. Igor V. Konnov, Helmut Veith, and Josef Widder. 2015b. What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. In Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (Lecture Notes in Computer Science), Manuel Mazzara and Andrei Voronkov (Eds.), Vol. 9609. Springer, 6–21.
26. Konstantin Korovin. 2008. iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. 292–298.
27. Leslie Lamport. 1994. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems (TOPLAS) 16, 3 (1994), 872–923.
28. Leslie Lamport. 1998. The Part-Time Parliament. ACM Trans. Comput. Syst. 16, 2 (1998), 133–169.
29. Leslie Lamport. 2001. Paxos Made Simple. (December 2001), 51–58. https://www.microsoft.com/en- us/research/publication/ paxos- made- simple/
30. Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.
31. Leslie Lamport. 2006. Fast Paxos. Distributed Computing 19, 2 (2006), 79–103.
32. Leslie Lamport, Dahlia Malkhi, and Lidong Zhou. 2008. Stoppable Paxos. Technical Report. TechReport, Microsoft Research. https://www.microsoft.com/en- us/research/publication/stoppable- paxos/
33. Leslie Lamport, Dahlia Malkhi, and Lidong Zhou. 2009. Vertical Paxos and Primary-Backup Replication. In Proceedings of the 28th ACM Symposium on Principles of Distributed Computing. ACM, 312–313.
34. Leslie Lamport, Dahlia Malkhi, and Lidong Zhou. 2010. Reconfiguring a State Machine. SIGACT News 41, 1 (03 2010), 63–73.
35. Butler Lampson. 2001. The ABCD’s of Paxos. In PODC, Vol. 1. 13.
36. K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning. Springer, 348–370.
37. Harry R. Lewis. 1980. Complexity results for classes of quantificational formulas. J. Comput. System Sci. 21, 3 (1980), 317 – 353.
38. Ognjen Maric, Christoph Sprenger, and David A. Basin. 2017. Cutoff Bounds for Consensus Algorithms. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Rupak Majumdar and Viktor Kuncak (Eds.), Vol. 10427. Springer, 217–237.
39. Kenneth L. McMillan. 2016. Modular specification and verification of a cache-coherent interface. In 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016, Ruzica Piskac and Muralidhar Talupur (Eds.). IEEE, 109–116.
40. Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. 2015. How Amazon web services uses formal methods. Commun. ACM 58, 4 (2015), 66–73.
41. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Vol. 2283. Springer Science & Business Media.
42. Diego Ongaro and John K. Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In 2014 USENIX Annual Technical Conference, USENIX ATC ’14, Philadelphia, PA, USA, June 19-20, 2014. 305–319. https://www.usenix.org/ conference/atc14/technical- sessions/presentation/ongaro
43. Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. 2017. Paxos made EPR: Decidable Reasoning about Distributed Protocols. Technical Report.
44. Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016. 614–630.
45. Robert Paige and Shaye Koenig. 1982. Finite Differencing of Computable Expressions. ACM Trans. Program. Lang. Syst. 4, 3 (1982), 402–454.
46. Ruzica Piskac, Leonardo Mendonça de Moura, and Nikolaj Bjørner. 2010. Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom. Reasoning 44, 4 (2010), 401–424.
47. Vincent Rahli, David Guaspari, Mark Bickford, and Robert L. Constable. 2015. 15th international workshop on automated verification of critical systems (avocs 2015). electronic communications of the easst 72 (2015).
48. Thomas W. Reps, Mooly Sagiv, and Alexey Loginov. 2010. Finite differencing of logical formulas for static analysis. ACM Trans. Program. Lang. Syst. 32, 6 (2010).
49. Alexandre Riazanov and Andrei Voronkov. 2002. The Design and Implementation of VAMPIRE. AI Commun. 15, 2,3 (Aug. 2002), 91–110. http://dl.acm.org/citation.cfm?id=1218615.1218620
50. N. Schiper, V. Rahli, R. V. Renesse, M. Bickford, and R. L. Constable. 2014. developing correctly replicated databases using formal tools. In 2014 44th annual ieee/ifip international conference on dependable systems and networks. 395–406.
51. Fred B. Schneider. 1990. Implementing Fault-Tolerant Services Using the State Machine Approach: A Tutorial. ACM Computing Surveys (CSUR) 22, 4 (1990), 299–319.
52. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Mechanized verification of fine-grained concurrent programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Steve Blackburn (Eds.). ACM, 77–87.
53. Klaus v. Gleissenthall, NikolajBjørner Bjørner, and Andrey Rybalchenko. 2016. Cardinalities and Universal Quantifiers for Verifying Parameterized Systems. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). ACM, 599–613.
54. Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski. 2009. SPASS Version 3.5. In Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. 140–145.
55. James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas E. Anderson. 2015. Verdi: a framework for implementing and formally verifying distributed systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015. 357–368.
56. Yuan Yu, Panagiotis Manolios, and Leslie Lamport. 1999. Model Checking TLA + Specifications. In Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME ’99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings (Lecture Notes in Computer Science), Laurence Pierre and Thomas Kropf (Eds.), Vol. 1703. Springer, 54–66.

Index Terms

• Networks

  • Network protocols

    • Protocol correctness

• Software and its engineering

  • Software organization and properties

    • Software functional properties

      • Formal methods

• Theory of computation

  • Logic

    • Logic and verification