FABRIC.md §21 — Q6 resolved: nested
Q6 leaned toward nested for the right conclusion and the wrong reason. Its premise -- that a single region "reintroduces locking, the one mechanism this architecture has otherwise never wanted" -- is false. Every mutex in the kernel build is a no-op (shim.c:415); the kernel compiles STARFORTH_MINIMAL and the shim stubs dict_lock and tuning_lock out entirely. The architecture has not avoided locking, it has locking, inert. The cost Q6 weighs is currently zero, so Q6 cannot be decided on it. Decided nested on six other grounds, the strongest being SMP-readiness: nested keeps messages the only boundary-crossers, so no shared memory and no locks ever, whereas a single region would need real locks and the present no-op stubs would silently become a correctness hole. The most practical is that the outer level already exists and works (§20.1) -- single-region means discarding a working two-level structure. Also records a step-one finding that lands before any Stadium work: enabling timer interrupts introduces genuine ISR-vs-mainline concurrency where none exists today. Making the mutexes real would deadlock a single hart outright, since an ISR spinning on a lock the mainline holds can never be released. The top-half/bottom-half split of §18.4 is the answer, stated as a rule: Nothing in interrupt context may mutate Stadium structure. Ever. That constraint should be written at the stub site so the no-op is not later "fixed" into a spinlock. Opens: two capacities to size rather than one, and elasticity (§12 Q4 / §7 / §17.6c) becomes the live fork now that nesting makes capacity transfer real. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Opus 5
parent
1a5cd3fc74
commit
421c1d7602
@@ -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.
|
||||
|
||||
Reference in New Issue
Block a user