Module perfect_link 

Perfect point-to-point links.

Cachin, Guerraoui & Rodrigues, Module 2.3 and Algorithm 2.2 (“Eliminate Duplicates”).

Status: academic as written. Space: unbounded. Within a TCP or QUIC session, PL1–PL3 come from the transport. The deployable equivalent is a session link: those guarantees from the session, plus an event when the session changes and an unknown suffix may have been lost. It needs less state than this, not more — within a session the transport does not duplicate, so there is nothing to deduplicate.

delivered here grows with every message received. See docs/bounded-space.md.

Built over the stubborn link, which delivers a message infinitely often. This layer keeps the first copy of each message and discards the rest, yielding reliable delivery with no duplication and no creation.

upon event ⟨ pl, Send | q, m ⟩ do
    trigger ⟨ sl, Send | q, m ⟩;

upon event ⟨ sl, Deliver | p, m ⟩ do
    if m ∉ delivered then
        delivered := delivered ∪ {m};
        trigger ⟨ pl, Deliver | p, m ⟩;

One deliberate departure. The book deduplicates on the message content, m, which silently assumes every message is distinct. Send the same bytes twice on purpose and the second is swallowed. This implementation tags each transmission with an identifier — the sender and a sequence number — and deduplicates on that instead, so a genuine resend of identical content is delivered twice, as the layer above expects.

That identifier is the only thing this stack puts on the wire: the stubborn link below adds nothing, and best-effort broadcast above adds nothing.

The counter lives exactly as long as the set it keys

Both are volatile, and a crash takes both, so the pairing holds: a restarted sender re-mints (me, 1) at exactly the point where every recipient’s delivered has also been forgotten, and the recipient re-delivers the old messages anyway — no_duplication_does_not_survive_the_recipient_restarting records that. PL2 is scoped to an incarnation here, which is the crash-stop model’s premise: a crashed process is not correct, and nothing is promised across the restart the simulator can nevertheless perform.

The hazard to watch for is the mismatched pair — a durable set keyed by a volatile counter, where the recipient remembers what the sender has forgotten and discards new messages as duplicates. crate::logged_link is that configuration, and makes the counter durable.

Structs

MsgId

Names one transmission uniquely across the system.

PerfectLink

Reliable delivery, exactly once, over a stubborn link.

Wire

What crosses the wire: the identifier, and the payload it belongs to.

Enums

Cmd

Requests from the layer above.

Ind

Indications to the layer above.