Module logged_link 

Logged perfect point-to-point links.

Cachin, Guerraoui & Rodrigues, Module 2.4 and Algorithm 2.3 (“Log Delivered”).

Status: transcription. Space: unbounded — and on disk. Write cost: one append per message. delivered grows with every distinct message log-delivered and nothing retires an entry, as crate::perfect_link does, except that here the growth is a file rather than a heap. See docs/bounded-space.md; the fix is a delivered cursor rather than a delivered set, and it is a change with a proposal.

The indication carries the log, not the message

This is the whole of what the fail-recovery model changes about an interface, and the reason this protocol sits at the bottom of the stack where it can be seen.

A crash-stop protocol notifies the layer above by triggering ⟨ Deliver | m ⟩ once. A crash-recovery protocol cannot. It may crash immediately afterwards, and then neither it nor the layer above nor anyone else will ever know the indication happened — the message is lost in a notification that no longer exists. So the module writes the message into a set in stable storage, and the indication says only that the set may have changed:

upon event ⟨ lpl, Init ⟩ do
    delivered := ∅;
    store(delivered);

upon event ⟨ lpl, Recovery ⟩ do
    retrieve(delivered);
    trigger ⟨ lpl, Deliver | delivered ⟩;

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

upon event ⟨ sl, Deliver | p, m ⟩ do
    if not exists (p′, m′) ∈ delivered such that m′ = m then
        delivered := delivered ∪ {(p, m)};
        store(delivered);
        trigger ⟨ lpl, Deliver | delivered ⟩;

The layer above reads the set rather than receiving a message, and must be idempotent: the same set arrives again after every restart.

Reliable delivery is weaker here, and necessarily

Module 2.3 promises delivery if a correct process sends to a correct process. Module 2.4 promises it only if a process that never crashes does. The difference is not fussiness: a sender that crashes immediately after being asked to send may have no record that it was ever asked, and in the crash-recovery model a process that crashes and recovers is still correct. There is nothing left in the system to retransmit.

What the durable record buys

crate::perfect_link keeps its delivered set in memory, so a restart forgets it and the sender’s next retransmission is delivered a second time — no_duplication_does_not_survive_the_recipient_restarting records exactly that. Here the record survives, so LPL2 holds across incarnations rather than within one. That is the entire purchase, and it is what stable storage is for.

Departures from the page

• None worth the name for initialisation: ⟨ Init ⟩ and ⟨ Recovery ⟩ are both here, exactly one fires, and Init performs the book’s initial store — of the empty counter, this implementation’s metadata, rather than of the empty set. That write is what makes the branch real rather than emergent: after it, storage holds something, so every later restart recovers. The constructor does volatile setup only, because it runs in both cases and cannot emit effects.
• delivered is keyed by sender and a per-sender sequence number rather than by message content, for the reason crate::perfect_link gives: identical content sent twice is two messages and must be delivered twice.
• The send counter is therefore durable, held in the metadata and restored on recovery. See the note below; the obligation comes with the departure that created it.
• No Stop: the stubborn link beneath retransmits for ever, which in this model is a feature — it is how a process that was down when a message was sent receives it after recovering.

The send counter is the metadata

Content-keyed deduplication, as the book has it, needs no counter: a payload names itself, and a restart changes nothing. Identifier-keyed deduplication owes the counter the same durability as the set it keys — and this is the one it cannot recompute, because the log holds messages received, saying nothing about what this process sent.

Left volatile, a restarted sender re-mints (me, 1), (me, 2), …. A recipient whose durable log already holds those identifiers discards the new payloads as duplicates, permanently, while the stubborn link beneath retransmits them for ever. LPL1 does not formally break — it promises delivery only from a process that never crashes — but the loss is silent, and the simulator restarts processes freely.

So the counter is written before the message it names goes out, which is what the metadata is for: one small value, rewritten. A torn write discards that handler’s sends along with it, so the counter is never behind an identifier already on the wire; a write that lands before a crash burns an identifier, and a gap costs nothing. Keying the durable set by content instead would also work, at the price of the departure above.

The write cost is linear, not quadratic

One append per message log-delivered, and one metadata rewrite per message sent — a single u64, whose cost does not grow with what preceded it. Rewriting the whole set on each arrival would cost O(n²) over a run, which is the failure mode docs/bounded-space.md calls unbounded work: small per item, and growing without limit. That is the distinction the split between metadata and entries exists to make.

Deduplication is a lookup by identifier rather than a scan over pairs, for the same reason: a scan would make the read side quadratic while the write side was linear, and a cost note that mentions only one of them is not a cost note.

What is left is the indication, which carries the whole set and therefore copies it on every arrival. That one is the book’s interface rather than an implementation choice — see the note at the top on why the indication cannot be a message — and it goes away with the same change that bounds the record: a delivered cursor instead of a delivered set.

The record still grows without limit, so this remains a transcription. What appending changes is the cost of adding to it, not its size.

Structs

Log

The set of messages log-delivered, in stable storage.

LoggedLink

Perfect-link guarantees over log-delivery, so that they hold across a restart.

Enums

Cmd

Requests from the layer above.

Ind

Indications to the layer above.

Type Aliases

Wire

What goes on the wire: the payload and the identifier that names it.