Module logged_leader_driven_consensus 

Paxos that survives a restart.

Status: implementation. Space: bounded by membership, plus what the stubborn children hold outstanding — inherited from crate::logged_epoch_change and crate::logged_epoch_consensus, and retired for the consensus by each epoch’s Abort.

Cachin, Guerraoui & Rodrigues, Module 5.5 (LoggedUniformConsensus) and Algorithms 5.10–5.11 (“Logged Leader-Driven Consensus”), quoted from the book:

Algorithm 5.10: Logged Leader-Driven Consensus (part 1)
Implements: LoggedUniformConsensus, instance luc.
Uses:
    LoggedEpochChange, instance lec;
    LoggedEpochConsensus (multiple instances).

upon event ⟨ luc, Init ⟩ do
    val := ⊥; decision := ⊥; aborted := FALSE; proposed := FALSE;
    Obtain the initial leader ℓ0 from the logged epoch-change instance lec;
    Initialize a new instance lep.0 of logged epoch consensus with timestamp 0, leader ℓ0,
        and state (0, ⊥);
    (ets, ℓ) := (0, ℓ0);
    store(ets, ℓ, decision);

upon event ⟨ luc, Recovery ⟩ do
    retrieve(ets, ℓ, decision);
    retrieve(startts, start) of instance lec;
    (newts, newℓ) := (startts, start);
    retrieve(epochdecision) of instance lep.ets;
    if epochdecision ≠ ⊥ ∧ decision = ⊥ then
        decision := epochdecision;
        store(decision);
        trigger ⟨ luc, Decide | decision ⟩;
    aborted := FALSE;

upon event ⟨ luc, Propose | v ⟩ do
    val := v;

Algorithm 5.11: Logged Leader-Driven Consensus (part 2)

upon event ⟨ lec, StartEpoch | startts, start ⟩ do
    retrieve(startts, start) of instance lec;
    (newts, newℓ) := (startts, start);

upon (ets, ℓ) ≠ (newts, newℓ) ∧ aborted = FALSE do
    aborted := TRUE;
    trigger ⟨ lep.ets, Abort ⟩;

upon event ⟨ lep.ts, Aborted | state ⟩ such that ts = ets do
    (ets, ℓ) := (newts, newℓ);
    store(ets, ℓ);
    aborted := FALSE;
    proposed := FALSE;
    Initialize a new instance lep.ets of logged epoch consensus with timestamp ets, leader ℓ,
        and state state;

upon ℓ = self ∧ val ≠ ⊥ ∧ proposed = FALSE do
    proposed := TRUE;
    trigger ⟨ lep.ets, Propose | val ⟩;

upon event ⟨ lep.ts, Decide | epochdecision ⟩ such that ts = ets do
    retrieve(epochdecision) of instance lep.ets;
    if decision = ⊥ then
        decision := epochdecision;
        store(decision);
        trigger ⟨ luc, Decide | decision ⟩;

Two durable children under one durable parent

This is the first protocol here that keeps a record of its own and composes children that keep records of theirs, and it is the reason [recon_core::Slot] exists. Every other composition hands its children a NoStore, because a parent and a child sharing one store would each overwrite the other’s metadata — and would do it silently, with nothing failing until a recovery read back half of what it wrote.

A slot names the part of Durable that belongs to a child. The child’s set becomes a read-modify-write of this record: one write, not two, so a crash cannot land between the parent’s record and its child’s.

The book writes retrieve(startts, start) of instance lec and retrieve(epochdecision) of instance lep.ets — a parent reading its children’s records by name. Here it does that by handing each child its slot and letting the child’s own Recovery read it, which is the same thing said in the direction the composition already runs.

One slot for a child that is replaced every epoch

The book has one logged epoch consensus instance per timestamp, each with its own record. There is one slot here, holding whichever instance is live. That is not a loss: the only instance ever read is lep.ets, and ets is in this record too, so a slot holding the current instance is exactly what retrieve(...) of instance lep.ets asks for.

A crash can land between store(ets, ℓ) and the new instance’s own Init write, and both outcomes are safe. Land before it, and recovery reads the previous epoch’s epochdecision against the new ets — but a value that epoch decided is, by lock-in, the value every later epoch decides, so deciding it is right. Land after it, and recovery reads a fresh record against the old ets and has simply not decided yet.

Reading two lines the page does not quite give

upon (ets, ℓ) = (newts, newℓ) ∧ aborted = FALSE do … trigger ⟨ lep.ets, Abort ⟩ is printed with =, and must be ≠: aborting the epoch you are in because it is the one you want would abort every epoch immediately and decide nothing. The same OCR class as if v ≠ ⊥ then tmpval := v in Algorithm 5.6, which crate::epoch_consensus records for the same reason.

Init does not print an assignment to (newts, newℓ). It must be (0, ℓ0) — the same pair as (ets, ℓ) — or the standing condition above is true from the first event and the initial epoch is aborted before it does anything. Algorithm 5.7 sets (newts, newℓ) := (0, ⊥), which works there because its condition is written on the Aborted handler rather than as a standing one.

The decision is announced again after a recovery, and Module 5.5 has no integrity property

⟨ luc, Decide | decision ⟩ is specified as “notifies the upper layer that variable decision in stable storage contains the decided value of consensus” — a pointer to a record, not a one-shot event. Module 5.5 lists three properties where the fail-noisy Module 5.2 lists four: termination, validity and uniform agreement, with no integrity clause. The book dropped it, and the reason is exactly this: a logged indication may be raised again, and the layer above reads storage and must be idempotent. logged_link and logged_uniform_reliable_broadcast already work that way, and README.md states it as the rule for this whole model.

So a process that decided, crashed, and came back announces its decision once more. Algorithm 5.10’s Recovery handler as printed does not — it announces only when epochdecision ≠ ⊥ ∧ decision = ⊥, the case where the child’s record survived and this layer’s did not. Re-announcing the other case is the departure, and it is the module’s own indication wording taken at face value: a layer above that crashed with this one never saw the first indication, and there is no other event that would tell it.

LUC1 [conditional] Termination — every correct process that never crashes eventually
                   log-decides, provided a majority is correct and the leader detector settles.
                   "Correct" here means eventually up and staying up, so a process that keeps
                   crashing is not owed a decision
LUC2 [always]      Validity — a log-decided value was proposed by some process
LUC3 [always]      Uniform agreement — no two processes log-decide differently, **including
                   across crashes and recoveries, and while the leader detector is wrong**

There is deliberately no integrity clause, for the reason above. What replaces it is that the value never changes: a process announces the same decision every time, which LoggedLeaderDrivenConsensus::decision is the durable statement of.

Structs

Durable

Everything this stack keeps durably, as one rewritten value.

LoggedLeaderDrivenConsensus

Paxos in the fail-recovery model.

Enums

Cmd

Requests from the layer above.

Ind

Indications to the layer above.

Wire

The wire, multiplexing the epoch-change child and whichever epoch-consensus instance is live.