Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables

TL;DR

This paper demonstrates that using only message history variables simplifies specifications and proofs of distributed consensus algorithms like Paxos, making them more understandable and easier to verify with less manual effort.

Contribution

It introduces a method to specify and prove distributed algorithms using solely message history variables, reducing complexity and proof effort compared to traditional approaches.

Findings

Specifications are more declarative and simpler.

Proofs require fewer invariants and are more efficiently checked.

Verification time is significantly reduced, enabling successful mechanical checking.

Abstract

This paper studies specifications and proofs of distributed algorithms when only message history variables are used, using the Basic Paxos and Multi-Paxos algorithms for distributed consensus as precise case studies. We show that not using and maintaining other state variables yields simpler specifications that are more declarative and easier to understand. It also allows easier proofs to be developed by needing fewer invariants and facilitating proof derivations. Furthermore, the proofs are mechanically checked more efficiently. We show that specifications in TLA+, Lamport's temporal logic of actions, and proofs in TLAPS, the TLA+ Proof System (TLAPS) are reduced by a quarter or more for single-value Paxos and by about half or more for multi-value Paxos. Overall we need about half as many manually written invariants and proof obligations. Our proof for Basic Paxos takes about 25% less time for TLAPS to check, and our proofs for Multi-Paxos are checked within 1.5 minutes whereas prior proofs fail to be checked by TLAPS.