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.
- Francesco Alberti, Silvio Ghilardi, and Elena Pagani. 2016. Counting Constraints in Flat Array Fragments. In Automated Reasoning. Springer, Cham, 65–81. Google ScholarDigital Library
- 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.Google Scholar
- Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Springer. Google ScholarCross Ref
- 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. Google ScholarCross Ref
- Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. 2015. Decidability of Parameterized Verification. Morgan & Claypool Publishers. Google ScholarCross Ref
- 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.Google Scholar
- 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. Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarCross Ref
- 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.Google Scholar
- Gregory V. Chockler, Idit Keidar, and Roman Vitenberg. 2001. Group communication specifications: a comprehensive study. ACM Comput. Surv. 33, 4 (2001), 427–469. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Heidi Howard, Dahlia Malkhi, and Alexander Spiegelman. 2016. Flexible Paxos: Quorum Intersection Revisited. arXiv preprint arXiv:1608.06696 (2016).Google Scholar
- Shachar Itzhaky. 2014. Automatic Reasoning for Pointer Programs Using Decidable Logics. Ph.D. Dissertation. Tel Aviv University.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Daniel Jackson. 2006. Software Abstractions: Logic, Language, and Analysis. The MIT Press.Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarCross Ref
- 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. Google ScholarCross Ref
- 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.Google Scholar
- Leslie Lamport. 1994. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems (TOPLAS) 16, 3 (1994), 872–923. Google ScholarDigital Library
- Leslie Lamport. 1998. The Part-Time Parliament. ACM Trans. Comput. Syst. 16, 2 (1998), 133–169. Google ScholarDigital Library
- Leslie Lamport. 2001. Paxos Made Simple. (December 2001), 51–58. https://www.microsoft.com/en- us/research/publication/ paxos- made- simple/Google Scholar
- Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.Google ScholarDigital Library
- Leslie Lamport. 2006. Fast Paxos. Distributed Computing 19, 2 (2006), 79–103. Google ScholarDigital Library
- 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/Google Scholar
- 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. Google ScholarDigital Library
- Leslie Lamport, Dahlia Malkhi, and Lidong Zhou. 2010. Reconfiguring a State Machine. SIGACT News 41, 1 (03 2010), 63–73.Google ScholarDigital Library
- Butler Lampson. 2001. The ABCD’s of Paxos. In PODC, Vol. 1. 13.Google Scholar
- K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning. Springer, 348–370.Google ScholarDigital Library
- Harry R. Lewis. 1980. Complexity results for classes of quantificational formulas. J. Comput. System Sci. 21, 3 (1980), 317 – 353. Google ScholarCross Ref
- 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. Google ScholarCross Ref
- 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. Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Vol. 2283. Springer Science & Business Media.Google Scholar
- 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/ongaroGoogle ScholarDigital Library
- Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. 2017. Paxos made EPR: Decidable Reasoning about Distributed Protocols. Technical Report.Google Scholar
- 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. Google ScholarDigital Library
- Robert Paige and Shaye Koenig. 1982. Finite Differencing of Computable Expressions. ACM Trans. Program. Lang. Syst. 4, 3 (1982), 402–454. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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).Google Scholar
- 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). Google ScholarDigital Library
- 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.1218620Google Scholar
- 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.Google Scholar
- Fred B. Schneider. 1990. Implementing Fault-Tolerant Services Using the State Machine Approach: A Tutorial. ACM Computing Surveys (CSUR) 22, 4 (1990), 299–319. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- 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.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarCross Ref
Index Terms
- Paxos made EPR: decidable reasoning about distributed protocols
Recommendations
Modularity for decidability of deductive verification with applications to distributed systems
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and ImplementationProof automation can substantially increase productivity in formal verification of complex systems. However, unpredictablility of automated provers in handling quantified formulas presents a major hurdle to usability of these tools. We propose to solve ...
Programming and proving with distributed protocols
Distributed systems play a crucial role in modern infrastructure, but are notoriously difficult to implement correctly. This difficulty arises from two main challenges: (a) correctly implementing core system components (e.g., two-phase commit), so all ...
Ivy: safety verification by interactive generalization
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and ImplementationDespite several decades of research, the problem of formal verification of infinite-state systems has resisted effective automation. We describe a system --- Ivy --- for interactively verifying safety of infinite-state systems. Ivy's key principle is ...
Comments