The blocking half of the algorithm-level refinement.
A blocking configuration of the compiled algorithm is one where every process is wedged: every
scheduled code block blocks on a guard, and every .rx thread's channel is empty. The last
conjunct is what makes the transfer to the source exact. A compiled await Len(inbox) > k blocks
when inbox is short, which on its own says nothing about the source's channel — a message could
still be sitting in mailbox waiting to be relayed. But a blocking configuration has that
channel empty too (relayBlocking), so the invariant F_s(c) = inbox ++ F_t(c) collapses to
F_s(c) = ⟨⟩, and the source receive blocks for the same reason.
This is why T_rx is essential: a compiler that drops it has relayBlocking vacuously true, so it
can produce a wedged configuration with F_t(mailbox) ≠ ⟨⟩ — code deadlocked on
await Len(inbox) > 0 while a message rots in mailbox — which the source, reading the channel
directly, would have consumed. No matched source blocking run, so blocking is unprovable.
One process's blocking, transferred. A compiled process wedged at a related state — every scheduled block blocked and its receiving channel drained — is matched by the source process wedged, or by the source aborting.
The channel-drained conjunct (hdrain) is what procBlocking's relayBlocking supplies and what
makes the receive-guard case exact: with F_t(c) = ⟨⟩ the invariant gives F_s(c) = inbox, and a
compiled await Len(inbox) > k that blocks means the source's queue is emptied after its k
receives.
One process's doneness, transferred. A compiled process that has reached a sentinel on
every thread is matched by its source, which has the same scheduled label set (L_s = L_t) over the
same owned labels (ProcessRefines.ownedLabels_eq). A name resolving to no process owns nothing on
either side, so the doneness is vacuous there.
Whole-configuration doneness, transferred. Every process instance of the compiled algorithm
done implies every instance of the source done — procDoneTransfer per instance, since
procRelatesTo keeps L equal over the same owned labels. This is what restricts the reducing
refinement to Algebra.terminating (runs that end done) on both sides.
The immediate blocking half. NetworkPlusCal.Algebra.immediateBlock — the algorithm
deadlocked now — is matched by the source's, or by the source aborting now. Per-instance dispatch:
procBlockTransfer for the wedged processes, procDoneTransfer for the finished ones, and one
aborting instance is enough to land in the aborting fallback.
The whole blocking semantics. NetworkPlusCal.Algebra.blocking is step* ∘ᵣ₁ immediateBlock, so this is Blocking.starStutter at that — the immediate half above, lifted over
the run that precedes it by the same per-step Terminating the reducing and aborting halves use.
Any T_rx relay steps in that prefix stutter on the source side.
The terminating semantics, the paper's ⟦A⟧⁺. terminating_reducing cut down to runs that
end in a done configuration on both sides. The target restriction is free (Terminating.Mono); the
source restriction rides on algRelatesTo.isDone_of, since a shorter source set is otherwise harder
to land in.
The algorithm-level refinement, whole. All four components at the closed forms
Algebra.terminating/.aborting/.diverging/.blocking, against one state relation.
href/used/fresh are established from a compiled algorithm by Algorithm.toNetwork_spec
and the front end, and algRelatesTo at the initial states by Algorithm.init; the refinement
argument asks for nothing beyond those.
The pass is correct. Compiling an algorithm yields one whose algebra refines the source's,
under algRelatesTo at the mailbox the compiled algorithm itself determines.
Everything in this development meets here. Algorithm.toNetwork_spec is the syntactic half, the
four walks; algRelatesTo.refines is the refinement argument, Terminating/Aborting/Diverging/
Blocking at the four closed forms. triple_forall is the joint: BranchesRefine is needed at
every prefix function and the spec supplies one per instantiation.
The two front-end hypotheses are not the pass's. AlgorithmFresh is the syntactic conditions on the
source program and the generated inbox; MailboxUsed says a declared mailbox is one its process
receives on (checkReceiveChannels).
Relating Algorithm.init's initial states under algRelatesTo is a separate statement, and
Algorithm.toNetwork_spec reports globalState because that is what it is stated against.