Module epoch_consensus 

Read/write epoch consensus — the quorum core, and where Paxos’s safety argument lives.

Status: implementation. Space: bounded by membership.

Cachin, Guerraoui & Rodrigues, Module 5.4 and Algorithm 5.6 (“Read/Write Epoch Consensus”), quoted from the book:

Algorithm 5.6: Read/Write Epoch Consensus
Implements: EpochConsensus, instance ep, with timestamp ets and leader ℓ.
Uses:
    PerfectPointToPointLinks, instance pl;
    BestEffortBroadcast, instance beb.

upon event ⟨ ep, Init | state ⟩ do
    (valts, val) := state; tmpval := ⊥; states := [⊥]^N; accepted := 0;

upon event ⟨ ep, Propose | v ⟩ do                       // only leader ℓ
    tmpval := v;
    trigger ⟨ beb, Broadcast | [READ] ⟩;

upon event ⟨ beb, Deliver | ℓ, [READ] ⟩ do
    trigger ⟨ pl, Send | ℓ, [STATE, valts, val] ⟩;

upon event ⟨ pl, Deliver | q, [STATE, ts, v] ⟩ do       // only leader ℓ
    states[q] := (ts, v);

upon #(states) > N/2 do                                 // only leader ℓ
    (ts, v) := highest(states);
    if v ≠ ⊥ then tmpval := v;
    states := [⊥]^N;
    trigger ⟨ beb, Broadcast | [WRITE, tmpval] ⟩;

upon event ⟨ beb, Deliver | ℓ, [WRITE, v] ⟩ do
    (valts, val) := (ets, v);
    trigger ⟨ pl, Send | ℓ, [ACCEPT] ⟩;

upon event ⟨ pl, Deliver | q, [ACCEPT] ⟩ do             // only leader ℓ
    accepted := accepted + 1;

upon accepted > N/2 do                                  // only leader ℓ
    accepted := 0;
    trigger ⟨ beb, Broadcast | [DECIDED, tmpval] ⟩;

upon event ⟨ beb, Deliver | ℓ, [DECIDED, v] ⟩ do
    trigger ⟨ ep, Decide | v ⟩;

upon event ⟨ ep, Abort ⟩ do
    trigger ⟨ ep, Aborted | (valts, val) ⟩;
    halt;                                               // stop operating when aborted

Why two majorities are the whole algorithm

The leader reads from a majority and writes to a majority, and any two majorities of Π intersect. So if some epoch decided v — meaning a majority accepted it — then every later epoch’s read reaches at least one process that accepted v, and highest(states) returns it. if v ≠ ⊥ then tmpval := v is the line that makes the later leader adopt it instead of its own proposal. That is the entire reason two epochs cannot decide differently, and every other part of Paxos exists to arrange for it.

highest means highest timestamp, not highest value. It picks the state written in the most recent epoch, which is the one that may already have been decided.

halt is a safety property, not tidiness

upon event ⟨ ep, Abort ⟩ … halt; // stop operating when aborted. An instance that kept answering after being abandoned would be a second leader for its epoch under another name: it could still collect a quorum and decide, while the epoch that replaced it decided something else. The flag EpochConsensus::is_aborted reports is checked at the top of every handler, and the suite delivers a message to an aborted instance and asserts that nothing at all comes out.

Departure: directed replies travel by directed broadcast

As in crate::epoch_change, the book’s pl child is absorbed into the broadcast’s directed beb::Cmd::SendTo — one addressed process, one wire message, which is what pl, Send does. STATE and ACCEPT both travel that way. One child and one wire variant fewer, and the guarantee is unchanged.

EPC1 [always]  Validity — a decided value was proposed in this epoch, or was the highest-
               timestamped value some process had already accepted
EPC2 [always]  Uniform agreement — no two processes decide differently in one epoch
EPC3 [always]  Integrity — a process decides at most once
EPC4 [always]  Lock-in — a value decided in an earlier epoch is what a later one decides
EPC5 [always]  Abort behaviour — an abandoned instance reports its state and then is silent

Structs

EpochConsensus

Abortable consensus within one epoch.

State

(valts, val) — what a process has accepted, and when.

Tagged

An epoch message, stamped with the instance it belongs to.

Enums

Cmd

Requests from the layer above.

EpochMsg

What this layer puts on the wire, beneath the broadcast.

Ind

Indications to the layer above.

Type Aliases

BebMsg

What the broadcast beneath puts on the wire for this layer’s messages.