Module reliable_broadcast 

Regular reliable broadcast.

Cachin, Guerraoui & Rodrigues, Module 3.2 and Algorithm 3.3 (“Eager Reliable Broadcast”).

Status: transcription. Space: unbounded. delivered grows with every message delivered, and the book omits its collection deliberately. Deployable once it is windowed — which weakens no duplication to hold within the retention window. See docs/bounded-space.md.

Best-effort broadcast promises nothing when the sender crashes partway through: some processes deliver, others do not, and they disagree for ever. This layer adds agreement — if any correct process delivers a message, every correct process eventually does — by having every process relay each message the first time it delivers it. The redundancy therefore lives at the other processes, which is why this guarantee survives the sender’s crash where best-effort broadcast’s does not.

upon event ⟨ rb, Broadcast | m ⟩ do
    trigger ⟨ beb, Broadcast | [DATA, self, m] ⟩;

upon event ⟨ beb, Deliver | p, [DATA, s, m] ⟩ do
    if m ∉ delivered then
        delivered := delivered ∪ {m};
        trigger ⟨ rb, Deliver | s, m ⟩;
        trigger ⟨ beb, Broadcast | [DATA, s, m] ⟩;

The relay is unconditional on first delivery — the book’s eager scheme. Algorithm 3.2, the lazy variant, relays only when a perfect failure detector reports the sender crashed; that abstraction below does not exist here, and eager needs no failure detector at all. It pays for that in messages.

Scope tags, in the notation of docs/scope-annotated-modules.md:

RB1 [always]       Validity
RB2 [incarnation]  No duplication  — the delivered set is volatile
RB3 [always]       No creation
RB4 [always]       Agreement       — bridged by redundancy at the other processes

Two departures from the page, both for reasons already met lower in the stack:

• The book deduplicates on message content, assuming messages are unique across senders. Here each broadcast carries an identifier — its originator and a per-sender sequence number — and deduplication is on that, so identical content broadcast twice is delivered twice.
• ⟨rb, Init⟩ is not a separate event; new establishes the same state.

Over a link that reports scope boundaries

L is a parameter, so this one module is also what session_reliable_broadcast used to be. Algorithm 3.3 is unchanged; what changes is the scope its agreement holds within.

Over a perfect link a relay always arrives, because the link retransmits until it does. Over a session link it may not, and this layer has nothing with which to retry:

• It relays once, on first delivery. That is what makes eager reliable broadcast eager.
• It keeps delivered as a set of identifiers, not payloads — so even knowing a relay was lost, it has no copy to send again. Retaining payloads would be state growing with messages, which docs/bounded-space.md forbids without a window.
• It is fail-silent. Algorithm 3.3 uses no failure detector, so it cannot conclude that a process is gone and stop expecting to reach it.

So when a relay is lost to a scope ending, nothing retries and nothing gives up. This layer cannot bridge, so it propagates: the boundary is reported upward in its own Ind rather than absorbed, which is what docs/conditional-guarantees.md requires of a layer in that position.

RB1 [session]       Validity
RB2 [incarnation]   No duplication — `delivered` is volatile, so a restart forgets it
RB3 [always]        No creation
RB4 [session]       Agreement — within the scopes carrying the relay, and not across one

RB2 is [incarnation] for the reason docs/scope-annotated-modules.md gives as Corollary 7.2, and by the same argument: the redundancy that would have to survive is delivered, that set is held in memory, and the boundary it cannot cross is this process’s own ⟨Init⟩. A recipient that restarts and is then relayed a message it had already delivered — which the eager relay of a peer that did not restart will happily do — delivers it a second time. [always] would be the claim that a volatile set survives a crash.

This is not a defect to be fixed here. It is the honest reading of Algorithm 3.3 on a link that can lose a suffix, and it is exactly what uniform reliable broadcast does not share — that one has a failure detector, and between reconnection and accusation it has no third outcome. Reading the two together is the sharpest available argument for why uniform reliable broadcast needs a detector at all.

Structs

BroadcastId

Names one broadcast uniquely: who originated it, and their sequence number for it.

Data

What this layer adds to the wire: the originator, and the payload.

ReliableBroadcast

Broadcast with agreement, over best-effort broadcast.

Enums

Cmd

Requests from the layer above.

Ind

Indications to the layer above.

Type Aliases

Carried

What a link beneath this layer must carry.

Wire

The wire type: this layer’s data, carried by best-effort broadcast.