Module flooding_consensus 

Flooding consensus.

Cachin, Guerraoui & Rodrigues, Module 5.1 and Algorithm 5.1 (“Flooding Consensus”).

Status: academic, fail-stop. Space: bounded by membership and rounds. The state is one proposal set and one heard-from set per round entered, each holding at most one entry per process, and a run enters at most N rounds — so it is O(N²) and satisfies the rule in docs/bounded-space.md without any collection being added. That is not what makes it academic. What makes it academic is the assumption underneath it.

Processes flood their accumulated proposal sets in rounds. A process leaves a round when it has heard, in that round, from every process it has not been told has crashed. If a round ends having heard from exactly the same processes as the one before it, nobody new crashed, so everyone holds the same proposal set and it is safe to decide the minimum of it.

upon event ⟨ c, Init ⟩ do
    correct := Π;
    round := 1;
    decision := ⊥;
    receivedfrom := [∅]^N;
    proposals := [∅]^N;
    receivedfrom[0] := Π;

upon event ⟨ P, Crash | p ⟩ do
    correct := correct \ {p};

upon event ⟨ c, Propose | v ⟩ do
    proposals[1] := proposals[1] ∪ {v};
    trigger ⟨ beb, Broadcast | [PROPOSAL, 1, proposals[1]] ⟩;

upon event ⟨ beb, Deliver | p, [PROPOSAL, r, ps] ⟩ do
    receivedfrom[r] := receivedfrom[r] ∪ {p};
    proposals[r] := proposals[r] ∪ ps;

upon correct ⊆ receivedfrom[round] ∧ decision = ⊥ do
    if receivedfrom[round] = receivedfrom[round − 1] then
        decision := min(proposals[round]);
        trigger ⟨ beb, Broadcast | [DECIDED, decision] ⟩;
        trigger ⟨ c, Decide | decision ⟩;
    else
        round := round + 1;
        trigger ⟨ beb, Broadcast | [PROPOSAL, round, proposals[round − 1]] ⟩;

upon event ⟨ beb, Deliver | p, [DECIDED, v] ⟩ such that p ∈ correct ∧ decision = ⊥ do
    decision := v;
    trigger ⟨ beb, Broadcast | [DECIDED, decision] ⟩;
    trigger ⟨ c, Decide | decision ⟩;

Agreement rests entirely on strong accuracy

correct appears in exactly two places, and a false suspicion corrupts both. The round guard is correct ⊆ receivedfrom[round], so wrongly shrinking correct lets a process finish a round without having heard from a correct process, and two processes can then take min over different sets. The decision-adoption rule is guarded by p ∈ correct, so a process that wrongly suspects the decider discards its DECIDED message. The book’s own proof names the dependency: “Because of the strong accuracy property of the failure detector, no process that reaches the end of round r receives a proposal containing a smaller value than v.”

Losing the detector’s accuracy costs safety — two correct processes decide differently, permanently. Losing its completeness costs only liveness — everyone blocks, but nobody is wrong. The asymmetry is the reason this protocol is worth writing.

This layer keeps the perfect detector, and that is not an oversight

crate::eventually_perfect_failure_detector exists, and Ω moved onto it. This layer must not: it is the fail-stop algorithm, and its agreement rests on strong accuracy so completely that this suite exists largely to demonstrate what one false suspicion costs it. Giving it a detector allowed to be wrong would not make it deployable; it would make the demonstration untrue. crate::leader_driven_consensus is the algorithm that survives an inaccurate detector, and it is a different algorithm rather than this one reconfigured.

Why stabilising later does not help

The model these algorithms are written against is not one in which the set of correct processes decays. It is one of eventual stability: bounds come to hold, and after that point the correct set is agreed and stays agreed. docs/scope-annotated-modules.md names this Assumption F and observes that it is the partial-synchrony global stabilisation time and the ◇ of an eventually-accurate detector in the same clothes.

An eventually perfect detector would therefore withdraw a false suspicion, and every process would again be held correct by every other — and the split would still be there, because a decision is irrevocable and was taken while the system was unstable. This is what separates this protocol from the leader-driven family: flooding consensus commits during instability and so has nothing left for stabilisation to rescue, whereas a quorum-based algorithm declines to commit until no conflicting decision is possible. Stated this way the limitation survives replacing P with ◇P; “the detector never withdraws an accusation” would not.

Departures from the page

• receivedfrom and proposals are maps keyed by round rather than arrays of size N. Only rounds actually entered hold an entry; the bound is the same and for the same reason.
• The total order the book assumes on proposals (“we implicitly assume here that the set of all possible proposals is totally ordered and the order is known by all processes”) is a P: Ord bound. A value that cannot be totally ordered cannot be proposed.
• The standing condition is re-evaluated in a loop rather than once, because a message for a later round may arrive before this process enters it. It terminates: the guard requires this process to appear in receivedfrom[round], which happens only when its own broadcast for that round returns to it.
• A second Propose from the same process is ignored. The book’s model has one proposal per process, and Module 5.1 provides one decision per instance.
• ⟨c, Init⟩ is a separate event: new establishes the state, and [Protocol::on_init] starts the detector beneath, without which no round can ever complete after a crash. It was a Cmd::Start before the trait had an init event, which is why the only request now is Cmd::Propose.

Structs

FloodingConsensus

Regular consensus in the fail-stop model, over best-effort broadcast and a failure detector.

Enums

Cmd

Requests from the layer above.

Flood

What this layer puts on the wire: the two messages Algorithm 5.1 sends, and nothing else.

Ind

Indications to the layer above.

Wire

The wire type, multiplexing the two children. Typed, so a mis-route cannot compile.

Type Aliases

BebMsg

What best-effort broadcast puts on the wire for this layer’s payloads.

Carried

What a link beneath this layer must carry.