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.
Fri 27 OctDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00
|Geo-Distribution of Actor-Based Services|
Philip A. Bernstein Microsoft Research, Sebastian Burckhardt Microsoft Research, Sergey Bykov Microsoft, n.n., Natacha Crooks University of Texas at Austin, USA, Jose Faleiro Yale University, USA, Gabriel Kliot Google, n.n., Alok Kumbhare Microsoft Research, n.n., Muntasir Raihan Rahman Microsoft, Vivek Shah University of Copenhagen, Denmark, Adriana Szekeres University of Washington, USA, Jorgen Thelin Microsoft Research, RedmondDOI
|Paxos Made EPR: Decidable Reasoning about Distributed Protocols|
Oded Padon Tel Aviv University, Giuliano Losa University of California at Los Angeles, USA, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv universityDOI
|Verifying Strong Eventual Consistency in Distributed Systems|
Victor B. F. Gomes University of Cambridge, UK, Martin Kleppmann University of Cambridge, Dominic P. Mulligan University of Cambridge, Alastair R. Beresford University of Cambridge, UKDOI
|Verifying Distributed Programs via Canonical Sequentialization|
Alexander Bakst , Klaus v. Gleissenthall University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USADOI