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 higher-order concepts such as set cardinalities, arithmetic, and complex quantification.
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"onfinkel-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 and Flexible 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 and Fast Paxos.
Conference DayFri 27 OctDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00
|Geo-Distribution of Actor-Based Services|
Philip A. BernsteinMicrosoft Research, Sebastian BurckhardtMicrosoft Research, Sergey BykovMicrosoft, n.n., Natacha CrooksUniversity of Texas at Austin, USA, Jose FaleiroYale University, USA, Gabriel KliotGoogle, n.n., Alok KumbhareMicrosoft Research, n.n., Muntasir Raihan RahmanMicrosoft, Vivek ShahUniversity of Copenhagen, Denmark, Adriana SzekeresUniversity of Washington, USA, Jorgen ThelinMicrosoft Research, RedmondDOI
|Paxos Made EPR: Decidable Reasoning about Distributed Protocols|
Oded PadonTel Aviv University, Giuliano LosaUniversity of California at Los Angeles, USA, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv universityDOI
|Verifying Strong Eventual Consistency in Distributed Systems|
Victor B. F. GomesUniversity of Cambridge, UK, Martin KleppmannUniversity of Cambridge, Dominic P. MulliganUniversity of Cambridge, Alastair R. BeresfordUniversity of Cambridge, UKDOI
|Verifying Distributed Programs via Canonical Sequentialization|
Alexander Bakst, Klaus v. GleissenthallUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USADOI