The whole algorithm, one step at a time.
Below this file the two per-step obligations are already proved, one per kind of target thread:
algRelatesTo.block_step for a compiled code thread's block, algRelatesTo.rx_step for a
receiving thread's relay. What is left is the dispatch — deciding which of the two a target step
is — and that is a question about the compiled algebra, not about any state.
There is no interface for it. Each of the two obligations below resolves the stepping instance
against the compiled algebra pair GuardedPlusCal.Algorithm.algebra Ξ Ω algo /
NetworkPlusCal.Algorithm.algebra Ξ Ω algo' itself, and splits CodeTable.procReducing into its
labelled disjunct — a compiled code block — and its relay disjunct — a receiving thread's step.
The step it is holding is what proves the label is owned, so the unschedulable case never arises.
The pass's per-process refinement (ProcessesRefine) plus the front-end facts (MailboxUsed,
AlgorithmFresh) are what that needs and nothing more.
The source side is Relation.star Aₛ.step, not Aₛ.step. A receiving thread's step is
answered with no source step at all, so no single-step form can be stated — see
StrongRefinement.Terminating.starStutter, which is the shape that admits it and which
terminating_reducing below spends.
The pass at this level: the whole algorithm, compiled #
Algorithm.toNetwork maps Process.toNetwork over the algorithm's processes and keeps the
global state, so the syntactic half is Spec.mapM_list a fourth time and nothing more.
The semantic half — turning the resulting ProcessRefines into the label dispatch
algRelatesTo.step_or_stutter and .immediateAbort run — is a different kind of step and is not
here. It has to go through Algorithm.algebra's by-name lookup on both sides, and it is the first
place the two languages' Process.codeTables are compared rather than their syntax.
mb and rx, read off the compiled processes #
algRelatesTo is indexed by instances (ι = String × V) while the pass's data is positional in
a list, and Algorithm.algebra bridges the two by looking a process up under its name. So both
functions are that lookup composed with something local to the compiled process — no existential,
no choice, and .none for a process that has no receiving thread, which is exactly the mailbox a
receive-free process must have.
List.Forall₂.find?_right is what makes the lookup usable: the two find?s walk their lists in
step, so a target process found under a name is the compilation of the source process found under
the same one. ProcessRefines.name_eq is what makes the two predicates agree on related pairs.
The mailbox of the process an instance belongs to. An algorithm has no mailbox; its processes
do, and an instance's is its process's. Found by name, then read off the process's receiving thread —
.none when it has none.
The declared @mailbox field cannot serve: it is Option (String × List Expr), which carries
neither the generated inbox nor a Ref — rxMailbox's own doc says what is missing. What the
field is good for is the decision, and that enters procMailbox_eq below as a hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
What a process declares its mailbox to be, as the pass gets to assume it. After
checkReceiveChannels a @mailbox field is present exactly when the process has a receive to use
it, so a mailbox assignment that says .some is one whose process receives.
Only that direction is needed, and only that direction is a front-end fact. The converse — a process
that receives has a mailbox — is what BranchesFresh.mbox_some already carries down the ladder.
Equations
- Guarded2Network.MailboxUsed mbox algo = ∀ p ∈ algo.processes, ∀ (inbox : String), mbox p.name inbox ≠ none → Guarded2Network.ProcessReceives p
Instances For
The pass's output, as the algorithm level receives it. Algorithm.toNetwork_spec's
postcondition, named because everything below quantifies over it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instance resolution. A compiled process found under a name is the compilation of the source
process found under that same name — the step every clause below opens with, since both algebras
resolve an instance ⟨name, self⟩ by exactly this lookup.
List.Forall₂.find?_right is what makes it work: the two find?s walk their lists in step, so
agreement on the predicate at related pairs is enough, and ProcessRefines.name_eq is that
agreement. The target side is the hypothesis rather than the source's because that is the direction
algRelatesTo.step_or_stutter and .immediateAbort need it — a target step names a target label,
and resolving that label's owning process is the first thing either proof does.
procMailbox computes the mailbox the refinement was proved at. The per-process
ProcessRefines.rxMailbox_eq at the resolved instance.
Stated against the resolution's own p/inbox rather than existentially, because every consumer has
already run find?_refines and needs the two sides of the equation to be the same mailbox as the
ProcessRefines it is holding.
Both algebras answer a resolved instance from the process itself. Algorithm.algebra's
table is the by-name lookup composed with the process's own codeTable, and every ProcessRefines
field lemma is stated against that bare form — so each is one Option.elim in the way.
Both algebras answer a resolved instance from the process itself. Algorithm.algebra's
table is the by-name lookup composed with the process's own codeTable, and every ProcessRefines
field lemma is stated against that bare form — so each is one Option.elim in the way.
A generated inbox is never self. A mailbox procMailbox reports is one a process
registered a thread for, so its inbox is a name freshName generated, and no generated name is
self (Generated.ne_selfName). Spent inside algRelatesTo.step_or_stutter/.immediateAbort to
rewrite the source memory's selfName lookup through procRelatesTo.mem_agree' unchanged.
Load-bearing rather than hygiene: CodeTable.procReducing requires the memory to bind selfName,
and the source memory agrees with the target's only away from the generated name.
The source-side freshness obligation, at the top. Every process of the algorithm is
ProcessFresh at the channel the mailbox assignment gives its name.
c₀ and mbox are keyed by process name rather than carried per process, because that is how the
algorithm layer indexes: Algorithm.algebra resolves a process instance ⟨name, self⟩ by looking
name up. mbox's second argument is the name the pass will generate, which is why it is a function
and not a Mailbox — see ProcessFresh.
Equations
- Guarded2Network.AlgorithmFresh mbox c₀ algo = ∀ p ∈ algo.processes, Guarded2Network.ProcessFresh (mbox p.name) (c₀ p.name) p
Instances For
One target step, answered — and never answered by nothing forever. The per-step obligation in the three-way form a stuttering simulation needs: the source takes one step, or it takes none and the target's queued-message count strictly drops, or it aborts.
The middle disjunct is what a divergence argument needs and Terminating cannot express. A
receiving thread's step is answered with no source step at all, so an infinite target run could in
principle be answered by a source that never moves — except that a relay moves a message out of a
channel, and FIFOs.size counts exactly those. Only a send puts one back, and a send is a code
thread's step, which does move the source. So the target cannot relay forever without the source
keeping pace.
The proof reads the target step apart into an instance and one of procReducing's two disjuncts,
resolves the owning process (find?_refines), and hands the pieces to whichever per-step lemma
applies — block_step for the labelled disjunct, rx_step for the relay one.
Process.ownedLabels_of_reducing is what lets the code case start from the step already in hand
rather than from a separate membership hypothesis. A name that resolves to no process has an empty
table on both disjuncts, so both are dispatched first, and separately.
Reassembling the source's step is the only thing here that is not dispatch. Algebra.step wants a
CodeTable.procReducing, which wants the scheduled label to be one the source process owns and has
scheduled, and the memory to bind selfName. The first comes from the code branch's label agreement
together with procRelatesTo's L₂ = L₁; the second from memory agreement away from the generated
inbox, which is not self — and since both algebras read self off the instance's own identity,
that memory fact needs no translation between the two sides.
The algorithm-level Terminating, read off step_or_stutter: a source step is a one-step
run, a stutter is the empty one, and the abort disjunct passes through unchanged. The measure is
dropped here — Terminating has nowhere to put it, which is exactly why the divergence half needs
step_or_stutter directly.
Where the target goes wrong, so does the source. The aborting counterpart of
algRelatesTo.terminating. A .rx thread's step is in relay, not in procAborting, and has no
aborting rule at all, so every algorithm-level abort is a code thread's, answered by the source
block's through blockRefines_abort.
Simpler than the terminating case throughout, because an abort has no post-state: no algRelatesTo
witness is rebuilt, so none of the key bookkeeping appears.
And the whole reducing semantics. Algebra.reducing is step* by definition and
Algebra.aborting is step* ∘ᵣ₁ immediateAbort, so this is Terminating.starStutter at those and
nothing else — including its absorption side condition, which is Relation.star.star_lcomp₁_absorb
at exactly this shape.
And the whole diverging semantics. Algebra.diverging is step^∞ by definition, so this is
Diverging.omegaStutter at step_or_stutter — the same three-way obligation the other two halves
are built from, here with its measure disjunct finally load-bearing.
FIFOs.size is the measure: a receiving thread's relay moves one message out of a channel, and only
a send puts one back — and a send is a code thread's step, which does move the source. So the
target cannot relay forever while the source stands still, the source's steps are cofinal in the
target's, and deleting the idle indices leaves a genuine infinite source run.
And the whole aborting semantics. Algebra.aborting is step* ∘ᵣ₁ immediateAbort by
definition, so this is Aborting.starStutter at that — the immediate half above, lifted over the run
that precedes it by the same per-step Terminating the reducing half uses.
The whole algorithm, compiled — the syntactic half. The walk over the processes, plus the global state carried across unchanged.
globalState is reported because Algorithm.init is stated against it: the clause fixing every
declared channel's initial queue quantifies over algo.globalState.channels ++ .fifos, and the
initial-state obligation needs those to be the same two lists on both sides. Nothing in
algRelatesTo.refines wants it.
The initial state #
A StrongRefinement says nothing at all unless the two algorithms' initial states are related:
with algRelatesTo never holding, it is vacuously true. What gives Algorithm.toNetwork_refines
content is that every initial state of the compiled algorithm has one of the source's related to
it, and that is what this section proves.
Both inits have the same shape and their FIFO clause is identical on the two sides —
Algorithm.toNetwork_spec reports algo'.globalState = algo.globalState for exactly this reason —
so the source state is built on the target's own FIFO map, and the whole obligation is about the
instances. There the pass makes three differences to a process, and each is one clause of
procRelatesTo: the entry labels gain the receiving threads' (ProcessRefines.entryLabels_eq),
the locals gain the inbox (ProcessRefines.inits_eq), and the instance starts receiving on a key.
Only the last is beyond the pass. Nothing it compiles decides whether a channel's index expressions
evaluate, whether what they resolve to is a FIFO the module declared, or whether two instances
resolve to the same one. Those are the front end's, and InitKeys is where they enter.
The key each receiving instance starts on, and what the front end owes about it. A witness
function rather than an existential per instance, for the reason algRelatesTo's own ib is one:
the FIFO clauses speak about every key at once, and a per-instance existential would leave nothing
relating them.
- resolves (p : GuardedPlusCal.Process ComputableTLAPlus.Typ ComputablePlusCal.Expression) : p ∈ algo.processes → ∀ (self✝ : V) (σ : GuardedPlusCal.ProcState V), GuardedPlusCal.InitProc Ξ Ω self✝ p.inits p.entryLabels σ → ProcessReceives p → (key (p.name, self✝)).1 = (c₀ p.name).name ∧ List.Forall₂ (GuardedPlusCal.EvalStep Ξ Ω σ.1) (c₀ p.name).args (key (p.name, self✝)).2
The mailbox channel resolves, in each instance's own initial memory, to that instance's key.
- declared (p : GuardedPlusCal.Process ComputableTLAPlus.Typ ComputablePlusCal.Expression) : p ∈ algo.processes → ∀ (self✝ : V), ProcessReceives p → Finmap.lookup (key (p.name, self✝)) F ≠ none
And the key names a channel that exists.
algRelatesTocarries this as an invariant because a compiled relay aborts where the FIFO is absent and the source has no relay to abort with; establishing it at the initial state is this clause. - inj (p : GuardedPlusCal.Process ComputableTLAPlus.Typ ComputablePlusCal.Expression) : p ∈ algo.processes → ∀ q ∈ algo.processes, ∀ (self✝ self' : V), ProcessReceives p → ProcessReceives q → key (p.name, self✝) = key (q.name, self') → (p.name, self✝) = (q.name, self')
And no two receiving instances share one — the well-formedness condition that a process set's mailbox is indexed by
self(WellFormednessError.mailboxNotIndexedBySelf). Without it one FIFO would be accounted against two inboxes, and no relation ofalgRelatesTo's shape could hold.
Instances For
The initial states are related — the pass's correctness is not vacuous. Every initial state
of the compiled algorithm has one of the source's related to it under algRelatesTo, at the same
mailbox and receiving labels Algorithm.toNetwork_refines is stated against.
The source state is built on the target's FIFO map, which is what hglobal buys: the two inits'
channel clauses are then the same statement, so the map that satisfies one satisfies the other. What
is left is the instances, and each is the target's own with the pass's three differences undone —
ProcessRefines.inits_eq to strip the inbox back off the initial memory, .entryLabels_eq to
strip the receiving threads off the label set, and InitKeys to say what the inbox is accounting
for.
hnames is the front end's, and is not bookkeeping: Algorithm.algebra resolves an instance by
find? on its process name, so two processes sharing one would have every instance of the second
running the first's code. It is what pins find? to the process an instance actually came from, on
both sides — the target's names are the source's, pointwise, by ProcessRefines.name_eq.