diff --git a/FABRIC.md b/FABRIC.md index 8094170..ee18257 100644 --- a/FABRIC.md +++ b/FABRIC.md @@ -1184,3 +1184,112 @@ decides where work goes; that remains capability-based routing. patrons were itself a VM, the structure is a tree rather than two levels. Nothing currently requires this, and §11 would call it speculative generality — but it should be ruled out deliberately, since the boot order in §6 does not forbid it. + +--- + +## 21. §12 Q6 resolved — nested + +> *Q6: Whether the arena is one region for the whole system or nested per VM. Nested implies +> K conserved at each level with messages as the only thing crossing a boundary, which would +> mean no shared-memory atomicity is ever needed. Single region is simpler but reintroduces +> locking — the one mechanism this architecture has otherwise never wanted.* + +**Resolved: nested.** The conclusion Q6 leaned toward is right; the reason it gives is not. + +**DECIDED.** + +### 21.1 The locking premise is false — locking is already free + +Every mutex in the kernel build is a no-op. `src/starkernel/vm/host/shim.c:415`: + +```c +void sf_mutex_lock(sf_mutex_t *mutex) { + (void)mutex; +} +``` + +`dict_lock` and `tuning_lock` (`include/vm.h:410,507`) are real `pthread_mutex_t` in the +hosted build (`platform_lock.h:58-63`), but the kernel compiles with +`-DSTARFORTH_MINIMAL=1` (`Makefile.starkernel:253`) and the shim stubs them out. The stated +rationale is accurate: *"Single-threaded kernel: no contention is possible at the VM +level."* + +So the cost Q6 weighs against the single-region option is currently **zero**. The +architecture has not avoided locking; it has locking, inert. Q6 cannot be decided on this +basis. + +### 21.2 Step one introduces real concurrency — and locks are the wrong answer for it + +This belongs in §16's substrate work, not here, but it surfaced while resolving Q6 and it +lands sooner than anything the Stadium needs. + +Once the timer interrupt fires on all three ISAs (§16.1), **the ISR preempts the +mainline.** That is genuine concurrency between two contexts sharing state on a single +hart. It does not exist today, which is precisely why the no-op stub is currently safe. + +Making the mutexes real would not fix it and would actively break it: on a single hart, an +ISR spinning on a lock the mainline holds **deadlocks outright**, because the mainline can +never run to release it. This is a well-known failure and it is easy to introduce by +reflex. + +The correct answer is already in the design — §18.4's top-half / bottom-half split: + +- **ISR (top half)** touches only a word-sized counter and a flag. Single writer. +- **Mainline (bottom half)** is the only context that mutates Stadium structure. + +No lock, no deadlock, and no reliance on atomicity beyond aligned word access. This is a +constraint on the L0 implementation, not a preference. + +> **Nothing in interrupt context may mutate Stadium structure. Ever.** + +### 21.3 What actually decides Q6 + +With locking removed from the argument, six discriminators remain: + +| | Nested | Single region | +|---|---|---| +| Matches what exists | `hotwords_cache`, `rolling_window`, dictionary are already per-VM; the physics registry is already outer | collapses a working two-level structure into one | +| Fault containment | a VM cannot corrupt another's Stadium | one bad patron reaches everything | +| Capacity transfer (§7) | meaningful — VMs have shares to trade | no per-VM share exists to transfer | +| K semantics | conserved per level; existing fleet K survives unchanged | fleet K needs re-deriving | +| Verification (§13) | prove the engine once, instantiate at both levels — demonstrates genericity | one arena, marginally simpler | +| **If SMP ever happens** | **messages are the only boundary-crossers → no shared memory, still no locks** | **needs real locks, and the no-op stubs become a live correctness hole** | + +The last row is the strongest, and it is what Q6 was reaching for. Nested does not avoid +locking *today* — nothing needs locking today. Nested avoids locking **permanently**, +including in a multi-hart future where the current stubs would silently stop being correct. + +The first row is the most practical: §20.1 established that the outer level already exists +and works. Single-region means discarding a working structure to build a simpler one, which +is a poor trade at this stage. + +### 21.4 The shape this fixes + +``` + Outer Stadium patrons: VMs + │ K conserved here + │ bounded — see §20.5 #1 + │ + ├── Hera's Stadium patrons: words, blocks, ACLs, messages + │ K conserved here, independently + │ + └── (future VMs) same shape, no special cases +``` + +Messages are the only patrons that cross a boundary. Everything else is confined to the +level it was born on. + +### 21.5 Consequences and open items + +1. **The no-op mutexes are now load-bearing in a way they were not before.** They are + correct today and correct under nesting, but only while the top/bottom discipline in + §21.2 holds. That discipline should be stated in the code at the stub site, so the next + reader does not "fix" the no-op into a spinlock and deadlock the kernel. +2. **Two capacities to size, not one.** §20.5 #1 (outer bound) and §17.6 (per-VM bound) are + now distinct questions with distinct answers. +3. **§12 Q4 / §7 / §17.6(c) elasticity becomes the live question.** Nesting is what makes + capacity transfer between VMs meaningful, so the hard-versus-elastic decision can no + longer be deferred as an abstraction — it is the next real fork. +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.