Machine-checked model improves safety of diskless distributed leases
PaxosLease Revisited: A Checked Model of Diskless Distributed Leases
Distributed, Parallel, and Cluster Computing
Summary
Distributed systems need a way to grant temporary exclusive access to resources without writing to disk. The authors provide a detailed, computer-verified description of a protocol called PaxosLease that does this safely and efficiently. They identify timing and message handling details that matter to avoid having two owners at once. Their work includes formal proofs and working code to help system builders understand and implement the protocol correctly.
What this means in practice
- •For distributed system engineers: Build fault-tolerant distributed locks that avoid disk writes during lease acquisition using a formally verified PaxosLease protocol.
- •For cloud infrastructure teams: Design leader election mechanisms with improved safety guarantees to reduce downtime in cloud services.
Authors
Márton Trencséni
Abstract
PaxosLease is a protocol by which a quorum of acceptors grants time-bounded exclusive ownership with no durable acceptor lease state and no disk write on the lease acquisition path. This paper gives a precise, machine-checked statement of the protocol and of its standard use, electing a Multi-Paxos leader that recovers once per epoch and then commits with single-round appends. Three results are new. First, the restart quarantine an acceptor must observe after losing its volatile state is the proposer attempt duration, a bound tight in the checked model and machine-checked at the boundary in both directions. Second, timer placement is safety-critical: starting the attempt timer at prepare-quorum receipt can produce two simultaneous lease owners. Third, when a proposer abandons an acquisition attempt and retries, messages left over from the abandoned attempt can make acceptors report a lease the proposer itself appears to own; unless such a report counts as open only while the proposer is renewing that exact lease, two simultaneous owners follow at any quarantine length. The lease transition system is formalized in TLA+ and checked by TLC, and the timing arithmetic is proved in TLAPS. An executable reference model encodes the same rules a second time, independently of the TLA+, so that a wrong rule has to survive two separate encodings. A single-file runnable demonstration gives the algorithm in readable Python code.