Expand description
Leader-driven consensus — Paxos.
Status: implementation. Space: bounded by membership.
Cachin, Guerraoui & Rodrigues, Module 5.2 (UniformConsensus) and Algorithm 5.7
(“Leader-Driven Consensus”), quoted from the book:
Algorithm 5.7: Leader-Driven Consensus
Implements: UniformConsensus, instance uc.
Uses:
EpochChange, instance ec;
EpochConsensus (multiple instances).
upon event ⟨ uc, Init ⟩ do
val := ⊥; proposed := FALSE; decided := FALSE;
Obtain the leader ℓ0 of the initial epoch with timestamp 0 from epoch-change instance ec;
Initialize a new instance ep.0 of epoch consensus with timestamp 0, leader ℓ0, state (0, ⊥);
(ets, ℓ) := (0, ℓ0);
(newts, newℓ) := (0, ⊥);
upon event ⟨ uc, Propose | v ⟩ do
val := v;
upon event ⟨ ec, StartEpoch | newts′, newℓ′ ⟩ do
(newts, newℓ) := (newts′, newℓ′);
trigger ⟨ ep.ets, Abort ⟩;
upon event ⟨ ep.ts, Aborted | state ⟩ such that ts = ets do
(ets, ℓ) := (newts, newℓ);
proposed := FALSE;
Initialize a new instance ep.ets of epoch consensus with timestamp ets, leader ℓ, and
state state;
upon ℓ = self ∧ val ≠ ⊥ ∧ proposed = FALSE do
proposed := TRUE;
trigger ⟨ ep.ets, Propose | val ⟩;
upon event ⟨ ep.ts, Decide | v ⟩ such that ts = ets do
if decided = FALSE then
decided := TRUE;
trigger ⟨ uc, Decide | v ⟩;§The child is replaced while running, and the state is what carries across
Every other layer in this repository constructs its children once. This one does not: each epoch
gets a new epoch-consensus instance, seeded with the state the previous one returned when it
was aborted. CLAUDE.md’s rule still holds — the field is one concrete type, replaced, not a map
from timestamp to instance resolved while running — but it is the first layer here whose child is
rebuilt at all.
The abort handshake is asynchronous and the wait is load-bearing. Abort is a request;
Aborted is its answer, carrying (valts, val). The replacement is not constructed until that
answer arrives, because the state it carries is what stops the new epoch contradicting the old
one. Aborting and immediately replacing — which is the obvious implementation — loses it, and
with it the property the whole algorithm exists to have.
§Addition: epoch-consensus traffic is tagged with its epoch
The book writes ep.ts and such that ts = ets, so instances are addressed by timestamp and a
message for one never reaches another. Nothing in this codebase’s wire does that for free, and
the consequence of omitting it is a safety failure rather than a lost message: a WRITE from
epoch 7 arriving after epoch 11 has begun would be accepted and recorded at timestamp 11,
inventing an acceptance that never happened.
The stamp lives in ep::Tagged, inside the child, rather than in this layer’s wire. The epoch
is the instance’s own identity, so the instance stamps what it sends and drops what is not
addressed to it — and this layer cannot forget to. An earlier draft put it here, and the type
system objected for an unrelated reason, which turned out to be pointing at the better place.
UC1 [always] Validity — a decided value was proposed by some process
UC2 [always] Uniform agreement — no two processes decide differently, **including while the
leader detector is wrong and two processes each believe they lead**
UC3 [always] Integrity — a process decides at most once
UC4 [conditional] Termination — every correct process decides, provided a majority is correct
and the leader detector eventually settlesUC4 is conditional on both, and saying so is the point. A majority that never forms, or a
detector that never settles, leaves this waiting — which is what FLP requires of it and what
flooding_consensus pretends away by assuming a perfect detector.
Structs§
- Leader
Driven Consensus - Paxos: uniform consensus over an epoch-change and a sequence of abortable epoch consensuses.