FABRIC-3.10.8 MC-3a: the claim, the physics lock, per-core decision state

VM.running_on claimed by compare-and-swap on switch-in and released once
the context is saved (release_after, sk_vm_switch_finish); a lost claim
returns 1 and the caller re-decides; double claims counted. Per-core
entry_vm and decision_due. g_lock_physics over capsule_vm_physics.c
(rank between switch and registry). KILL refuses a VM running anywhere.
Probe: 15737 claims, 0 lost, 0 double; a core-1 claim of Hera refused.
3-ISA acceptance with a 28-VM churn clean, 0 order violations.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
2026-09-26 15:35:05 -04:00
co-authored by Claude Opus 5.5
parent 2e3b7ebe66
commit 4440faf352
18 changed files with 37725 additions and 45 deletions
+24
View File
@@ -1057,3 +1057,27 @@ The boot hart HSM chose (0) is the one OpenSBI names as `Boot HART ID`.
**Evidence (named in advance):**
- **Standard sequence on all three ISAs:** K-10 hashes, G byte-identical (one worker core), all ok `3`, 0 B idle growth, **0 lock-order violations** (so the new rank fits), 0 observer refusals.
- **Probe** (temporary word, amd64): the claim counters after O-A are claims > 0, **lost claims 0, double claims 0**. Posing as core 1, a claim of Hera (held by core 0) **fails** and is counted as lost; with `core_id` back at 0, nothing else changed.
### 7.6 MC-3a — executed (2026-09-26)
**Change.**
- **`VM.running_on`** (`vm.h`; zeroed by `vm_init`).
- `sk_vm_try_claim()` claims by compare-and-swap. `sk_vm_switch_set_current()` claims Hera for core 0 at boot.
- `sk_vm_context_switch()` claims `to` first and returns 1 if another core holds it. `note_switch_performed` moved inside it, after a successful claim, so a lost claim is not counted as a switch. The trampoline's call site re-decides on 1 (it used to panic on any non-zero return); the checkpoint and the idle point simply go on.
- The switch sets `release_after = from`. `sk_vm_switch_finish()` clears `from`'s `running_on` once its context is saved, and checks the incoming VM is this core's (the double-claim count). It runs on the resume path of `sk_vm_context_switch()` and at the top of a first-entry trampoline.
- **Per core:** `g_switch_entry_vm` became `sk_percpu_t.entry_vm`. Two cores priming first entries together would otherwise swap VMs. "Decision due" moved into `sk_percpu_t.decision_due`: `note_beat` marks this core, `note_mail` marks every core in the core table, and `take_decision_due` is an atomic exchange on this core.
- The stamps and switch counters were already under `g_lock_switch` since MC-0b, so the plan's "atomic stamps" needed no change.
- **`g_lock_physics`** (rank `physics`, between switch and registry). Every public function of `capsule_vm_physics.c` is now a wrapper over a static `*_locked` body. Internal calls (remove→retire, heartbeat_tick→tick, conserved/status→heat sum) go to the `_locked` forms. The file's "no locking" note is kept as history, headed by the new rule.
- **`KILL`** (`capsule_vm_kill_refusal()`) also refuses a VM with `running_on` set: "it is running on another core".
**Probe** (temporary `MC3A-PROBE`, amd64, after O-A; `logs/20260926-143403`): `claims=15737 lost=0 double=0; as core 1, claim of Hera refused; after: claims=15737 lost=1 double=0; Hera running_on=1`. There were 0 order violations in that run.
**Standard sequence, with a 28-VM churn this time** (clean build, probe reverted; the tree is byte-identical to the saved stage diff). The churn exercises the physics lock through 28 retire-and-removes, and the new KILL rule through 28 kills.
| ISA | log | result |
|---|---|---|
| amd64 | `logs/20260926-144228` | K-10 hashes, G A=40 B=40 byte-identical, HHH, births 32 / kills 28, all ok `3`, ledger 319488/316703 (the K-11 churn baseline), 0 B idle, 0 / 0; **0 order violations**, 0 observer refusals, 0 park wakes, 0 `LOCK:` |
| aarch64 | `logs/20260926-145937` | same |
| riscv64 | `logs/20260926-151755` | same; 0 `timed out` |
**MC-3a is complete.** Next: MC-3b, each worker core's interrupt controller and the IPI.