FABRIC.md §22 — elasticity resolved: elastic, via quota over one cell pool
§7, §12 Q4 and §17.6(c) are one question at three scales. Resolved elastic. Under §19's density definition elasticity stops being a feature and becomes a negative feedback loop: a busy VM's heat share rises, density rises, capacity flows toward it, mass rises, density falls back. Capacity flows down the density gradient -- diffusion, no threshold, no damping constant. §4's "read, not decided" applied one level up. §7's own argument also holds: birth sizes the resting volume rather than a cap, which is far easier to guess right and self-corrects when wrong. The larger finding is that hard-versus-elastic was the wrong framing. Elastic is cheap or expensive entirely according to layout, which §21 did not settle. Chosen: one global array of cells, one global index space, per-VM quota as a count rather than a contiguous range. Cells come from a shared free list, so transfer is arithmetic on two integers -- no fragmentation, no adjacency requirement, index links keep working. This makes §13 simpler rather than harder: one array, one datatype, one total function over one finite index set, with nesting as a partition. §21's reasoning survives -- K per level and messages as the only boundary-crossers are both preserved, and SMP-safety holds so long as quota changes are arbitrated by Hera. What is given up is physical fault containment, recorded rather than glossed. Adds a required ordering: capacity must move slower than heat, or two conserved quantities chase each other and the ratio never settles. That is §12 Q5's separation of timescales arriving as a concrete instance. Opens: the resting floor (proposed derivation -- floor a quota at the mass of its pinned patrons, which is derived rather than tuned), what signal triggers a transfer, and the exact timescale ratio. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Opus 5
parent
421c1d7602
commit
d74872c222
@@ -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.
|
||||
|
||||
Reference in New Issue
Block a user