Module total_order_log 

The total-order log port: what a layer above a totally ordered log may depend on, and the whole of what it may.

Built on the model of crate::link and crate::detector, and for the same reason. An implementation keeps its own Cmd and Ind — that vocabulary is the algorithm’s, not the port’s — and the port supplies the three translations a layer above actually needs: build an append, build a read, and classify an indication. Pinning the port to one pair of types would admit exactly one implementation, which is the failure link.rs records: four session_* broadcast modules existed because a layer written against one link’s vocabulary could not compose over another’s.

One suite is written against this port and every implementation behind it is held to it, so that where two implementations differ is visible rather than asserted. Here the pair is crash-stop against fail-recovery, and what differs is exactly one thing: whether the ordered sequence survives a restart.

The read is a departure, and this is where it is recorded

The book’s abstraction is total-order broadcast — ⟨ tob, Broadcast | m ⟩ and ⟨ tob, Deliver | p, m ⟩, with no read at all. Both algorithms behind this port nonetheless maintain delivered, the totally ordered sequence, and a log’s clients read it. So TotalOrderLog::read exposes what the page keeps and does not offer: a departure of one method rather than of the algorithm.

A read is served from the reading process’s own copy. That is all either algorithm can honestly do — a read observing every completed append would have to go through consensus or hold a lease, which is not on the page and would change what is being transcribed. So the claim is a total order, not linearizability: a process whose round has not yet decided has not yet extended its sequence, and its read says so rather than waiting. What two reads anywhere in a run do guarantee is that one result is a prefix of the other, because both are prefixes of one agreed sequence.

Enums

LogInd

What an indication from any totally ordered log amounts to, in the port’s own vocabulary.

Traits

TotalOrderLog

What a layer above a totally ordered log may depend on, and the whole of what it may.