Chapter 8
The calculus: components, fibers, nine rules
The question this chapter answers: chapters 4–7 describe what one plugin does and when two plugins leave each other alone. What does the runtime do, step by step, when plugins are inserted, satisfied, unsatisfied, retired? The paper writes that down as a small operational semantics: a fixed set of objects and nine rewrite rules on them. Nothing here is a proof yet — chapter 9 proves things about these rules. If you have read a state machine for a network protocol, that is the right frame: states, transitions, guards.
db provides db; search injects it. We insert both, let them settle, then disable db. Watch which rule fires at each moment and what "target" and "committed view" hold.
8.1 Objects
ℭΓ ∋ (d, p, e)
d: keys it declares (inject); p: keys it may provide; e: an effect iterator witnessed up to ≃_{d∪p} — no key outside p is one it installs a binding at.
In words: a component is the thing you write — an inject list, a provide list, and a loader generator whose undos work on the keys it names. search is ({db}, ∅, e_search); db is (∅, {db}, e_db).
⟨d, p, e, π, σ, τ, θ⟩
π parent name (or root); σ its own table (⊆ p, empty until it activates); τ retired flag; θ lifecycle state:
θ ∈ Inactive | Reloading(i, g, ω) | Active(g, ω) | Unloading(g, ω)
i: remaining iterator; g: accumulator built so far; ω : d → 𝔑: the committed view — for each declared key, the name of the fiber that provided it when the transition committed. Recording the provider, not the value, is what makes "equal value, different provider" still count as a change.
In words: a fiber is one running instance of a component, plus bookkeeping. The four lifecycle states are: Inactive — not running; Reloading — part-way through its loader steps, carrying the steps left (i), the undos so far (g), and which providers it started against (ω); Active — finished loading; Unloading — has decided to leave but has not yet run its undos. The committed view ω is "for each key I need, which fiber I got it from".
Registry (Def 50): fibers under names, parent pointers forming a tree. The coeffect context is derived: σ_γ = ⋃{σₘ : m is Active} — only Active fibers provide. Single-source discipline: O-Insert refuses a component whose provision overlaps an existing one, so each key has one possible provider (multiple providers go through realms, §4.4, or a broker, §6.2).
target_n(γ) = ⊥ if τ_n ∨ ¬(γ ⊧ d_n); otherwise k ↦ provider_k(γ)
In words: the target view answers "what should this fiber be running against right now?" — nothing (⊥) if it has been retired or a key it needs is missing; otherwise, for each key, the fiber currently providing it. The whole lifecycle is driven by comparing should (target) with did (committed view).
Every lifecycle rule fires on target_n agreeing or disagreeing with the committed ω_n. A state is quiescent when every fiber sits at its target.
8.2 The state machine
8.3 The nine rules
| Rule | Kind | From → to | Premise |
|---|---|---|---|
| O-Insert | orchestration ⇒ | absent → Inactive | fresh name; parent exists; p disjoint from every existing provision |
| O-Retire | orchestration ⇒ | sets τ | unconditional — it is a request; the lifecycle rules carry it out |
| O-Remove | orchestration ⇒ | Inactive → absent | retired, Inactive, empty table, no children |
| L-Begin | lifecycle ⟶ | Inactive → Reloading(e, id, ω) | ω = target ≠ ⊥ |
| L-Iter | lifecycle ⟶ | Reloading → Reloading(i′, g∘h, ω) | target still = ω; one iteration lands, inverse h prepended |
| L-Finish | lifecycle ⟶ | Reloading → Active(g∘h, ω) | target still = ω; last iteration |
| L-Divert | lifecycle ⟶ | Reloading → Unloading(g∘h, ω) | target ≠ ω; abort the in-flight iteration or let it land |
| L-Leave | lifecycle ⟶ | Active → Unloading(g, ω) | target ≠ ω — records the decision, acts on nothing |
| L-Unload | lifecycle ⟶ | Unloading → Inactive, state ← g(γ) | ¬relied_n: no installed fiber's committed view names n |
In words: three rules are things the orchestrator asks for (insert, retire, remove); six are things the system does on its own whenever their premise holds. Activation is Begin → Iter… → Finish; leaving is Leave (or Divert, if caught mid-load) → Unload. Every "on its own" rule is triggered by target ≠ committed view, or by having steps left to run.
O-Insert db, O-Insert search (both Inactive). db needs nothing, so target ≠ ⊥: L-Begin, L-Iter…, L-Finish → Active; now db ∈ σ_γ. search's target becomes {db ↦ db-fiber}: L-Begin (ω recorded), L-Iter…, L-Finish → Active. Disable db: O-Retire sets τ; db's target is ⊥ ≠ ω, so L-Leave → Unloading; db leaves σ_γ. search's target becomes ⊥ ≠ ω: L-Leave → Unloading; relied_search is false, so L-Unload runs its undos (still able to read db through ω) → Inactive. Now nobody's ω names db: L-Unload db → Inactive. O-Remove is now legal.
The rules are nondeterministic (any fiber may step next) and mention no scheduler, so anything proved over all sequences holds for every scheduling policy.
8.4 Why deactivation takes two steps
A consumer being torn down because its provider is leaving may need that very provider during teardown — a connection pool hands its connections back to whatever provided them. So the withdrawal must take effect only after the consumers' teardown. The rules separate the decision from the act:
A guard like ¬relied_n normally deadlocks. It doesn't here because an Unloading fiber is already outside σ_γ, so no new target can name it, and every consumer that committed to it is itself on the way out (Thm 73 turns this into "the guard always releases"). Note the guard orders along coeffects, not the fiber tree: a parent may run its inverse while a child is still Unloading.
8.5 Instantiation and confinement
Def 52. An iteration may itself insert a child component (with π = itself) and yields as its inverse the retirement of that child — retire, not remove, because an inverse must apply wherever it is reached, and O-Remove has premises. Unloading a parent therefore cascades: retiring children flips their targets to ⊥ and the ordinary rules drain them one level at a time.
Def 55, Lemma 57 (confinement). An effect function may write its own table and values at declared keys in providers' tables; may read only those; never reads a control field (so a component cannot branch on another fiber's lifecycle state). This is a consequence of the context-mediated iterator form, and it is what makes Table 1 of the paper a complete inventory of what each rule writes.