diff --git a/FABRIC.md b/FABRIC.md index ee18257..96b95e9 100644 --- a/FABRIC.md +++ b/FABRIC.md @@ -1293,3 +1293,115 @@ level it was born on. 4. **§20.5 #4 remains open.** Nesting is two levels here. Whether a patron may itself contain a Stadium — a tree rather than two tiers — is still deliberately unruled. Nothing requires it; it should be excluded on purpose rather than by omission. + +--- + +## 22. Elasticity resolved — elastic, via quota over a single cell pool + +§7, §12 Q4 and §17.6(c) are one question asked at three scales: is a VM's share of capacity +a hard bound, or elastic under pressure with transfer arbitrated by Hera? + +**Resolved: elastic.** And the layout that makes it cheap is a single global cell pool with +per-VM quotas, not separate physical arenas. + +**DECIDED.** + +### 22.1 Why elastic — §19 turns it into a feedback loop + +Under §19's definition, elasticity stops being a feature to implement and becomes a +negative feedback loop that runs itself: + +``` + VM gets busy → heat share rises → density rises + → capacity flows toward it → mass rises + → density falls back +``` + +Capacity flows **down the density gradient** — from sparse VMs toward dense ones. That is +diffusion. There is no threshold to choose, no damping constant, and nothing decides: it is +§4's *read, not decided* applied one level up. + +A hard bound offers none of this. It offers a number that had to be guessed correctly at +birth and stays wrong. + +§7's own argument is the practical half, and it holds: + +> *Under elasticity, birth sizes the rest volume rather than a cap — a more forgiving thing +> to have to guess right.* + +Predicting a VM's resting size is far easier than predicting its peak, and being wrong +self-corrects instead of persisting. + +### 22.2 The connection to §14 + +Heat concentrates where work happens — §14's driven-dissipative inversion, order sustained +by throughput. Capacity then follows heat. So the two distributions move in opposite +directions: **heat concentrates while density equalises.** + +That makes the flatness of the density distribution a real, measurable signal of a settled +system, distinct from the heat distribution's entropy that §14 already identifies as the +instrument worth having. Two signals, not one, and they say different things. + +### 22.3 The layout decision, which matters more than hard-versus-elastic + +Framing this as hard-versus-elastic obscures the real choice. Elastic is cheap or expensive +entirely according to how the Stadium is laid out, and §21's nesting decision does not +settle that. + +| Layout | Elastic cost | Isolation | §13 verification | +|---|---|---|---| +| Separate physical arenas | expensive — transferring capacity means moving memory, and arenas fragment against each other | physical | two index spaces | +| **One cell pool, per-VM quota** | **trivial — arithmetic on two integers** | logical (disjoint index sets) | **one index space, one total function** | +| Separate arenas, hard bounds | n/a | physical | two index spaces | + +**Chosen: one global array of cells, one global index space.** Nesting becomes a +*partition* of that index set rather than separate allocations. A VM's quota is a **count, +not a contiguous range**, so cells are drawn from a shared free list, there is no adjacency +requirement, no fragmentation, and index links keep working because indices are global. + +Two reasons this is the right trade: + +- **§13 gets simpler rather than harder.** One array, one datatype, one total function over + one finite index set. A partition of a finite set is trivial in HOL. Separate arenas + would mean two of everything and a cross-arena invariant to maintain. +- **§21's reasoning survives intact.** Its argument for nesting was K conserved per level + with messages as the only boundary-crossers — both preserved. SMP-safety also survives: + what matters is that VMs never touch each other's cells, and disjoint index sets give + that provided quota changes are arbitrated by Hera, which §7 already requires. + +What is given up is *physical* fault containment — a corrupt index could reach another VM's +patrons where separate arenas would fault instead. That was one of §21.3's six +discriminators and not the decisive one. It is a real cost, recorded here rather than +glossed. + +### 22.4 Capacity moves slower than heat — required, not preferred + +Two conserved quantities in motion can oscillate. Heat moves on traffic; capacity moves on +density. At comparable rates they chase each other and the ratio never settles. + +> **Heat responds tick by tick. Capacity responds to sustained density across many ticks.** + +This is §12 Q5's separation-of-timescales discipline — *"keep nested loop periods an order +of magnitude apart"* — arriving as a concrete instance rather than general advice, and it +partly answers Q5. + +The exact ratio is a tuning question, but the *ordering* is not: capacity must be the +slower loop. Getting this backwards produces a system that thrashes while every individual +rule looks correct. + +### 22.5 Open + +1. **The resting floor.** A VM that goes quiet loses capacity; if it wakes it may not + regain it fast enough. The obvious guard is a floor below which a quota cannot fall — + but that is a tuned number, which this design otherwise avoids. Decide it deliberately. + A principled alternative: floor a VM's quota at the mass of its pinned patrons, which is + not a tuned constant but a derived one. +2. **What arbitrates a transfer, concretely?** §7 says Hera. Under §22.3 a transfer is + arithmetic on two integers, so the mechanism is trivial — but *when* she does it, and on + what signal, is not yet stated. It should read off the density gradient (§22.1) rather + than a schedule. +3. **The exact timescale ratio** in §22.4. +4. **Does the outer Stadium's own capacity ever change?** §22 makes per-VM quotas elastic + within a fixed total. Whether that total is itself fixed for the machine's lifetime is + §20.5 #1, still open — and it should stay fixed, or §2's inescapable wall is not + inescapable.