Formal verification of Multi-Paxos for distributed consensus

DOI10.1007/978-3-319-48989-6_8MaRDI QIDQ2281632zbMATH OpenOpenAlexFDO

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

Publication date 3 January 2020

Full work available at URL https://arxiv.org/abs/1606.01387

Mathematics Subject Classification ID

Temporal logic (03B44) Distributed systems (68M14) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Paxos is an important algorithm for a set of distributed processes to agree on a single value or a sequence of values, for which it is called Basic Paxos or Multi-Paxos, respectively. Consensus is critical when distributed services are replicated for fault-tolerance, because non-faulty replicas must agree on the state of the system or the sequence of operations that have been performed. Unfortunately, consensus algorithms including Multi-Paxos in particular are well-known to be difficult to understand, and their accurate specifications and correctness proofs remain challenging, despite extensive studies ever since Lamport introduced Paxos. This article 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 automatically checked using TLAPS, the TLA+ Proof System. The proof is for the safety property of the algorithm. 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 and results for proving complex invariants using invariance lemmas and increments, for proving properties about sets and tuples to help the proof check succeed in significantly reduced time, and for overall proof improvement leading to considerably reduced proof size.

Recommendations

• Formal modeling and verification of Paxos based on Coq
• Paxos consensus, deconstructed and abstracted
• Formal Verification of Distributed Algorithms
• Verification of consensus algorithms using satisfiability solving
• Revisiting the PAXOS algorithm

Cited in

(20)

• Revisiting the PAXOS algorithm
• Proving properties of the Chord protocol using the ASM formalism
• Multi-scale verification of distributed synchronisation
• On the correctness of Egalitarian Paxos
• Mechanical verification of concurrency control and recovery protocols
• scientific article; zbMATH DE number 7295743 (Why is no real title available?)
• Formal modeling and verification of Paxos based on Coq
• The DHCP Failover Protocol: A Formal Perspective
• scientific article; zbMATH DE number 1953037 (Why is no real title available?)
• Model checking Paxos in Spin
• scientific article; zbMATH DE number 7267129 (Why is no real title available?)
• Formal specification and verification
• A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract)
• Automated verification of multi-party agreements and scheduling of sending messages in distributed ledger systems
• Quorum tree abstractions of consensus protocols
• Symbolic model checking for TLA+ made faster
• The consensus machine: formalising consensus in the presence of malign agents
• Verification of consensus algorithms using satisfiability solving
• State machines for large scale computer software and systems
• Verification of distributed systems with the axiomatic system of MSVL

This page was built for publication: Formal verification of Multi-Paxos for distributed consensus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2281632)