Stage MC-0d: Stadium partitioned by quota slot, one lock per slot (FABRIC-3.10.8 §3.5)
- Ruling (Captain Bob): per-slot locks, not "own path needs no lock" -- a lock only on the cross-slot side can't exclude an unlocked owner (Hermes release evicting a sender's cell while the sender admits). FABRIC-3.10.0 §3.6 amended. - StadiumVMQuota.lock covers the slot's lists, reservoir, consumed, word row and its cells. Word dispatch holds only its own slot lock for the whole dispatch (*_in_slot forms); peek-then-pull is one step. - g_lock_stadium: grant slot allocation (new slot published with release in_use) and the shared block table (ruled: the one shared-lock Stadium path). Taken before a slot lock. - Bitmap bytes set/cleared atomically (8 cells, possibly 8 slots). - Cross-slot writers moved under the owner's lock: Hermes decay (stadium_cell_decay), Hermes release ledger (stadium_evict_credit), session pin (stadium_cell_set_pin). stadium_conserved() one hold. - Word and block cell lookups check the cell is still this slot's. - Probe (removed), identical on all three ISAs: 10,746,599 of 10,746,616 word dispatches took exactly one lock (own slot), the 17 others all row growths; every live VM conserved; Hermes audit failures 0. - Findings reported: births/USE run a VM's words while another VM is the core's current VM (MC-3 claim must cover it); quota slots never released; owner admission can evict a live message cell (latent, 0). - Standard sequence on amd64/aarch64/riscv64: dict_hash set and G byte-identical, MINT/WIREBIND/USE ok, conservation true, 0 idle growth. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
co-authored by
Claude Opus 5.5
Claude Opus 5.5
parent
355909d46f
commit
02c4c7e620
@@ -319,3 +319,90 @@ These runs' `dict_hash` values differ from the table below only because the prob
|
||||
- The G string is byte-identical to MC-0b2, MC-0b and MC-0a on all three ISAs.
|
||||
- The ledger line is unchanged.
|
||||
- No stop condition was hit. **MC-0c done.**
|
||||
|
||||
### 3.5 MC-0d — Stadium partitioned by quota slot (2026-09-25)
|
||||
|
||||
**Ruling (Captain Bob, 2026-09-25): one lock per quota slot.** FABRIC-3.10.0 §3.6 said a VM's own Stadium row and cells need no lock, with a Stadium lock only for cross-slot operations. That can't be made sound: a lock taken only on the cross-slot side can't exclude an owner that takes none. Concrete race:
|
||||
- a receiver's drain runs `sk_hermes_release()` → `stadium_evict()` on the **sender's** message cell, which rewrites the sender's free list, resident list and reservoir;
|
||||
- meanwhile the sender, running on another core, is popping that same free list in `stadium_admit()`.
|
||||
|
||||
`stadium_grant_quota()` splits a donor's free list the same way. The amendment is recorded at FABRIC-3.10.0 §3.6.
|
||||
|
||||
**Second ruling: the block table takes the shared Stadium lock.** `stadium_blocks.c` keeps one open-addressed table for every VM, keyed by (slot, LBN). `stadium_block_dispatch()` therefore takes `g_lock_stadium`. It is the one shared-lock Stadium path, recorded for MC-3 to measure; block access is rare next to word dispatch.
|
||||
|
||||
**Change.**
|
||||
- **The slot lock.**
|
||||
- `StadiumVMQuota` gains `lock`, a spinlock.h lock word.
|
||||
- It covers the slot's free list, resident list, reservoir, consumed, word row and statistics, and the slot's cells: their headers, owner entries and resident-list links.
|
||||
- Every public Stadium function locks the slot it touches. A cell operation locks the cell's owning slot (`lock_cell_owner()` re-reads the owner once locked).
|
||||
- **Word dispatch** (`stadium_word_dispatch()`) holds its own VM's slot lock for the whole dispatch: row, cell, cooling, pull, and admission including its eviction fallback. It uses the new `*_in_slot` forms, so it takes no other lock (a row growth's `kmalloc` excepted).
|
||||
- The reservoir peek-then-pull is now one step under that lock.
|
||||
- **Global part: `g_lock_stadium`.**
|
||||
- Quota-slot allocation in grants. Each new slot is filled first, then published with a release store of `in_use`; `quota_slot_for_vm()` reads `in_use` with acquire.
|
||||
- The shared block table.
|
||||
- It is taken before a slot lock, never after.
|
||||
- **The residency bitmap:** a byte covers 8 cells, which can belong to different slots, so set and clear are atomic OR/AND.
|
||||
- **Cross-slot writers moved into Stadium, under the owner's lock:**
|
||||
- kernel-Hermes's decay: `stadium_cell_decay()`, the same `q48_mul` arithmetic, consumed recorded in the same step;
|
||||
- Hermes's release ledger: `stadium_evict_credit()` returns the heat actually credited, read in the same step as the eviction, where it used to be read from the cell beforehand;
|
||||
- `session_set_pinned()`'s pin bit: `stadium_cell_set_pin()`.
|
||||
- **`stadium_conserved()`** reads its three terms under one hold, so the sum is of one instant.
|
||||
- **Owner check** added to both dispatch paths' cell lookups: the cell must still be this slot's.
|
||||
- Without it, a word or block cell evicted to this slot's free list could move to another VM in a grant and be admitted there with a matching identity. Word ids and LBNs are shared across VMs, so the old row would then heat the other VM's cell.
|
||||
- This is latent on one core.
|
||||
- **Unpartitioned reads that remain:** `sk_hermes_scan_held()` (reads message cells under the Hermes lock), `session.c`'s bounds check, and `kernel_main.c`'s decay self-test. None writes.
|
||||
- **Lock order** (spinlock.h):
|
||||
1. `hermes`
|
||||
2. `switch`
|
||||
3. `registry`
|
||||
4. `stadium`
|
||||
5. a slot lock
|
||||
6. `doe`
|
||||
7. `log`
|
||||
8. `block`
|
||||
9. `console`
|
||||
10. `heap`
|
||||
11. `vmm`
|
||||
12. `pmm`
|
||||
|
||||
A VM's `dict_lock` sits above Stadium: `vm_core.c`'s heat bump dispatches the word under it. Nothing in the block path calls into Stadium, so MIGRATE's `blk_flush()` edge doesn't close a cycle.
|
||||
|
||||
**Probe** (temporary, removed before commit). It counted:
|
||||
- the per-core lock acquisitions made during each `stadium_word_dispatch()`;
|
||||
- slot-lock acquisitions made for a slot other than the running VM's own;
|
||||
- admission-fallback evictions of message (DELIVER) cells;
|
||||
- quota slots in use.
|
||||
|
||||
An `MC0D-PROBE` word in every VM printed these, with `stadium_conserved()` on **every** live VM and the Hermes audit-failure count. The results are identical on all three ISAs, count for count:
|
||||
|
||||
| ISA | log | word dispatches | exactly one lock (own slot) | more than one | …all at a row growth | conserved | Hermes audit failures | DELIVER-cell fallback evictions |
|
||||
|---|---|---|---|---|---|---|---|---|
|
||||
| amd64 | `logs/20260925-212159` | 10,746,616 | 10,746,599 | 17 | 17 | 7/7 | 0 | 0 |
|
||||
| aarch64 | `logs/20260925-213527` | 10,746,616 | 10,746,599 | 17 | 17 | 7/7 | 0 | 0 |
|
||||
| riscv64 | `logs/20260925-214855` | 10,746,616 | 10,746,599 | 17 | 17 | 7/7 | 0 | 0 |
|
||||
|
||||
The table shows the final (rajames) reading. At Hera's prompt, before MINT, the readings were 9,687,103 dispatches with 14 exceptions (all row growths), 5/5 conserved, and 268 cross-slot slot locks.
|
||||
|
||||
**Findings, reported and not fixed:**
|
||||
1. **The running VM isn't always the core's current VM.** Cross-slot slot locks went from 268 to 1,059,738 across MINT, WIREBIND, `USE` and `1 2 + .`, the same growth as word dispatches in that window.
|
||||
- A birth runs the child's capsule on the parent's stack (capsule_birth.c), and `USE` runs another VM's lines, so these dispatches are for a VM other than `sk_percpu()->current_vm`.
|
||||
- The Stadium locking is correct either way: it locks the dispatching VM's own slot.
|
||||
- But MC-3's claim (`running_on`) must cover a VM executed this way, not only one switched to.
|
||||
2. **Quota slots are never released.** `stadium.c` has no release path: `in_use` is set by grants and cleared only at boot.
|
||||
- The probe counted 13 slots in use against 7 registry entries. Boot self-tests grant quotas to test ids (`kernel_main.c`), and a dead VM keeps its slot and cells.
|
||||
- A long-running system eventually exhausts the RAM-sized slot table.
|
||||
3. **An owner's word admission can evict a live message cell.** The admission fallback evicts the owner's least-dense resident, skipping only pinned and containing cells. Hermes admits messages unpinned into the sender's quota.
|
||||
- After such an eviction, `msg->stadium_cell` is stale: the release would evict whatever occupies that cell next.
|
||||
- This run counted 0 such evictions (the quotas never ran dry of free cells), so it is latent.
|
||||
|
||||
**Standard sequence** (clean build, with the probe reverted; the tree is byte-identical to the saved stage diff).
|
||||
|
||||
| ISA | log | O-A (G, PREC, LOAD) | M7.1a hash | MINT / WIREBIND / USE / `1 2 + .` | idle growth | UNKNOWN / faults |
|
||||
|---|---|---|---|---|---|---|
|
||||
| amd64 | `logs/20260925-220202` | A=40 B=40, HHH, ok | `0x99b01134c3d3049c` | all ok, `3` | 0 B / 20 s | 0 / 0 |
|
||||
| aarch64 | `logs/20260925-221440` | A=40 B=40, HHH, ok | `0x99b01134c3d3049c` | all ok, `3` | 0 B / 20 s | 0 / 0 |
|
||||
| riscv64 | `logs/20260925-222740` | A=40 B=40, HHH, ok | `0x99b01134c3d3049c` | all ok, `3` | 0 B / 20 s | 0 / 0 |
|
||||
|
||||
- The G string is byte-identical to MC-0c and earlier on all three ISAs, so the O(ncells) audit scan now running under a slot lock didn't move it.
|
||||
- The `dict_hash` set is unchanged, and the ledger line reads `stadium_conserved(self)=true`.
|
||||
- No stop condition was hit. **MC-0d done, and with it MC-0: one core, fully locked, ready for MC-1.**
|
||||
|
||||
Reference in New Issue
Block a user