Module stubborn_link 

Stubborn point-to-point links.

Cachin, Guerraoui & Rodrigues, Module 2.2 and Algorithm 2.1 (“Retransmit Forever”).

Status: academic. Space: unbounded — and unboundable. This is how a perfect link is built when the only thing underneath is a lossy datagram service — the simulator’s situation, and not a deployment’s, where TCP and QUIC retransmit already. It stays because everything above needs a perfect link and the simulator offers only fair-loss.

sent grows with every transmission, and that is not a defect to be fixed: it is SL1. The property below is that a message sent once is delivered an infinite number of times, so a link that let go would not be a bounded stubborn link — it would not be a stubborn link. There is no bounded form of this abstraction, and the answer to wanting one is crate::session_link, not a smaller sent. See docs/bounded-space.md.

What is true is that nothing retires an entry unless the layer above stops it, and nothing in this repository does — the perfect link never does, because Algorithm 2.2 never does. Every entry is therefore re-sent on every tick, and the cost grows with everything ever sent.

Turns a fair-loss network into one where a message sent between correct processes is eventually delivered, by retransmitting it at a fixed interval. The cost is unbounded duplication: the recipient delivers the message infinitely often. Suppressing that is the perfect link’s job, not this one’s.

upon event ⟨ sl, Init ⟩ do
    sent := ∅;
    starttimer(Δ);

upon event ⟨ sl, Send | q, m ⟩ do
    trigger ⟨ fll, Send | q, m ⟩;
    sent := sent ∪ {(q, m)};

upon event ⟨ Timeout ⟩ do
    forall (q, m) ∈ sent do trigger ⟨ fll, Send | q, m ⟩;
    starttimer(Δ);

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

Departures from the page

• The book’s ⟨ Init ⟩ starts the timer unconditionally and runs it for ever. This arms it lazily instead, when there is something to retransmit; see arm. Behaviourally equivalent, and it lets a run reach quiescence rather than tick indefinitely.

• Each transmission is named by a SendId so the layer above can retire it with Cmd::Stop. The book has no such request and never lets go. See Cmd::Send for the precondition that naming brings with it.

  Conservative, and worth saying why: SL1 is conditioned on a sender that sends m once, and says nothing about one that retracts. So with no caller the behaviour is exactly the book’s, and a layer that genuinely knows a transmission is finished may stop it without costing a property. Nothing in this repository calls it yet; only this module’s own suite does.

Structs

SendId

Identifies one stubborn transmission, so it can later be stopped.

StubbornLink

Retransmits until told to stop.

Enums

Cmd

Requests from the layer above.

Ind

Indications to the layer above.