Module stubborn_broadcast 

Stubborn best-effort broadcast.

Cachin, Guerraoui & Rodrigues, §3.5.

Status: deployable in the fail-recovery model. Space: bounded by membership and by what is outstanding. It holds the process set and the messages it is still transmitting, and nothing per delivery.

upon event ⟨ sbeb, Broadcast | m ⟩ do
    forall q ∈ Π do trigger ⟨ sl, Send | q, m ⟩;

upon event ⟨ sl, Deliver | p, m ⟩ do
    trigger ⟨ sbeb, Deliver | p, m ⟩;

Why the repeats are the point

crate::best_effort_broadcast fans out over perfect links, which deduplicate and stop retransmitting once a message has arrived. That is right in the crash-stop model and wrong in the fail-recovery one: a process that was down when a message was sent has no record of it and no way to ask, so the only thing that reaches it is a sender that never stopped trying.

So this layer does not deduplicate, and must not. The repeats are what the layer above is for: crate::logged_uniform_reliable_broadcast checks its own durable log before acting, and is idempotent by construction. Deduplicating here would suppress exactly the retransmission a recovered process depends on.

Departures from the page

• The message carries no identifier, because nothing here deduplicates. That leaves the layer above to name its own messages, which is what it already does.

• Stop is offered so a caller that knows a message is everywhere can retire it. The book has no such request and never lets go; what is outstanding is the whole of the space claim above, so a Stop nobody can name would make that claim rest on nothing. The caller names the broadcast, and one name retires the fan-out of N link transmissions it became.

  Nothing in this repository calls it yet: crate::logged_uniform_reliable_broadcast never stops, because retransmission for ever is what reaches a recovered process, and its space is unbounded for that reason and says so.

Structs

BroadcastId

Names one broadcast, so the caller can later retire it.

StubbornBroadcast

Fan-out that never gives up.

Enums

Cmd

Requests from the layer above.

Ind

Indications to the layer above.