Correct sk_hermes_alloc() to admit a real Stadium patron; add sk_hermes_release() -- FABRIC-3.6.md tasks 2.2 (amended) + 2.3
Real finding, caught before building release on a foundation that
couldn't support it: task 2.2's first cut of sk_hermes_alloc() pulled
reservoir heat but never admitted a real Stadium-floor patron -- just a
local in_use flag. FABRIC-3.5.md SXXXIII.4 item 1 says MSG-FREE-NODE
returns heat "via STADIUM-EVICT", which only means something if
allocation admitted something. SXL.4's own invariant, Sigma(resident
patron heat) + reservoir + consumed == Q48_ONE, cannot balance if held
heat is invisible to every term while held. Flagged to Captain Bob
before proceeding; authorized to correct 2.2 in the same pass as
building 2.3 on top of the fix.
sk_hermes_alloc() now calls stadium_admit() with heat = the pulled
amount, behaviour = STADIUM_BEHAVIOUR_DELIVER (matching messaging.4th's
own SB-DELIVER STADIUM-ADMIT exactly), and identity = the message's own
slot index (matching the FORTH precedent -- caught live in the first
boot of this fix that omitting this made stadium_dispatch()'s existing
DELIVER diagnostic print msg_idx=0 for every message instead of a
distinct value). The returned cell index is stored in the message's
own stadium_cell field. Stadium-floor refusal (independent of reservoir
affordability) rolls back the pull the same way the other refusal
paths already do.
sk_hermes_release() -- the function task 2.3 actually asks for -- calls
stadium_evict() on that cell, which itself returns the departing
patron's remaining heat to its owning VM's reservoir, matching
MSG-FREE-NODE's exact shape. Release does not touch the reservoir
directly.
Self-test (kernel_main.c) extended: keeps every allocated message's
pointer, allocates to exhaustion as before, releases all of them, and
checks the reservoir returns to precisely its starting value.
"Undecayed" is true by construction (no decay/TTL logic exists yet,
task 2.5) -- exact restoration, not approximate.
Three-arch boot clean: amd64/aarch64/riscv64 all reach [zuse@Hera] ok>,
zero UNKNOWN WORD, dict_hash unmoved from task 2.2. All three print
identical PASS arithmetic: reservoir0=65536, reservoir_after_alloc=0,
reservoir_final=65536. No compiler warnings.
stadium_dispatch()'s DELIVER-case console output (one line per
eviction) is pre-existing instrumentation, not new -- confirmed real
and load-bearing per stadium.c's own comment, verbose but expected.
Authorized by Captain Bob ("yes").
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
co-authored by
Claude Sonnet 5
Claude Sonnet 5
parent
9d129fdb1c
commit
2c1dc1753a
+57
-1
@@ -551,8 +551,64 @@ Hestia; headless policy intact.
|
||||
defined as "before and after the alloc/free cycle," not "continuously during." This task's
|
||||
self-test checks reservoir arithmetic directly instead, which is the right instrument for
|
||||
what task 2.2 alone claims.
|
||||
- [ ] **2.3** — Release: return remaining heat via the eviction path. *Check:* reservoir
|
||||
|
||||
**AMENDED 2026-09-20, while starting task 2.3 — see that entry for the full account.**
|
||||
This task's own first cut of `sk_hermes_alloc()` never admitted a real Stadium-floor
|
||||
patron; it only pulled reservoir heat and set a local flag. Corrected in the same commit
|
||||
as task 2.3, since release cannot evict something that was never admitted. The two-term
|
||||
`stadium_conserved()` non-evidence point above still holds — if anything it holds more
|
||||
precisely now that held heat really is off the floor (in the Stadium-admission sense) and
|
||||
not merely absent from a two-term check that never modeled it in the first place.
|
||||
- [x] **2.3** — Release: return remaining heat via the eviction path. *Check:* reservoir
|
||||
restored exactly for an undecayed message.
|
||||
2026-09-20 · `logs/20260920-041455/amd64/`, `logs/20260920-041619/aarch64/`,
|
||||
`logs/20260920-041752/riscv64/` — all three reach `[zuse@Hera] ok>`, zero `UNKNOWN WORD`,
|
||||
`dict_hash` triple unmoved from task 2.2's baseline. All three print
|
||||
`Kernel-Hermes alloc/release self-test: ... PASS` with **identical arithmetic**:
|
||||
`reservoir0=65536 ... reservoir_after_alloc=0 ... reservoir_final=65536` — exact
|
||||
restoration, not approximate.
|
||||
|
||||
**Real finding, not a clean continuation: task 2.2's allocator was missing a step.**
|
||||
§XXXIII.4 item 1 says `MSG-FREE-NODE` returns heat "via `STADIUM-EVICT`" — which only
|
||||
means something if allocation admitted a real Stadium patron in the first place. Task
|
||||
2.2's first cut didn't; it only pulled reservoir heat and flagged a local slot in use.
|
||||
Caught this before writing release on top of a foundation that couldn't support it, per
|
||||
§XL.4's own invariant: held message heat that is neither a resident patron nor reservoir
|
||||
nor `consumed` is invisible to the conservation equation entirely, which cannot be right.
|
||||
Flagged to Captain Bob before proceeding; authorized to correct task 2.2 in the same pass
|
||||
as building 2.3 on top of the fix, rather than patching around the gap.
|
||||
|
||||
**The fix, amending `src/starkernel/vm/kernel_hermes.c`'s `sk_hermes_alloc()`:** after
|
||||
pulling `SK_HERMES_Q_SLOT`, now calls `stadium_admit()` with a `StadiumPatronHeader` whose
|
||||
`heat` is the pulled amount, `behaviour = STADIUM_BEHAVIOUR_DELIVER` (matching
|
||||
`messaging.4th`'s own `SB-DELIVER STADIUM-ADMIT` at its `MSG-ALLOC` site exactly — same
|
||||
enum values, `SB-DELIVER`=1=`STADIUM_BEHAVIOUR_DELIVER`), and `identity` set to the
|
||||
message's own slot index (matching the FORTH precedent, and keeping
|
||||
`stadium_dispatch()`'s existing `DELIVER` diagnostic — "msg_idx=" — meaningful instead of
|
||||
every message printing 0; caught live in the first boot of this fix, since all 32
|
||||
admissions printed `msg_idx=0` before the identity fix). The returned cell index is
|
||||
stored in the message's own `stadium_cell` field. If the Stadium floor itself refuses
|
||||
admission (a third refusal path, independent of reservoir affordability), the pull is
|
||||
rolled back the same way the other refusal paths already do.
|
||||
|
||||
**`sk_hermes_release()`, the new function this task actually asks for:** calls
|
||||
`stadium_evict()` on the message's `stadium_cell` — which itself returns the departing
|
||||
patron's remaining heat to its owning VM's reservoir (`stadium.c`'s own comment: "the
|
||||
departing patron's remaining heat must flow back to its owner's reservoir"), so release
|
||||
does not touch the reservoir directly, matching `MSG-FREE-NODE`'s exact shape
|
||||
(`DUP 5 CELLS + @ STADIUM-EVICT DROP`). Clears the slot regardless of eviction's own
|
||||
return value, since a message asked to be released should not remain allocated either way.
|
||||
|
||||
**Self-test extended, not replaced:** the existing synthetic-VM self-test (task 2.2, `lo=3`)
|
||||
now keeps every allocated message's pointer in an array, allocates to exhaustion exactly as
|
||||
before, then releases all of them and checks the reservoir returns to precisely its
|
||||
starting value. "Undecayed" is true by construction here — no decay/TTL logic exists yet
|
||||
(task 2.5) — so this is exactly the case the check asks for: exact restoration, not
|
||||
approximate. `stadium_dispatch()`'s existing `DELIVER`-case console output (one line per
|
||||
eviction, pre-existing instrumentation, not new) is verbose but expected — confirmed
|
||||
real and load-bearing (`stadium.c`'s own comment: "has been real and live on every boot
|
||||
for weeks"), not something this task introduced. No compiler warnings on either edited
|
||||
file.
|
||||
- [ ] **2.4** — The four counters: `held`, `pulled`, `returned`, `consumed` (§XL.4). *Check:*
|
||||
each increments at exactly one site.
|
||||
- [ ] **2.5** — Decay: apply, and **record the delta into `consumed`** (§XXXVII.3). *Check:*
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
# Capsule Block Manifest — Auto-generated
|
||||
<!-- Generated by mkcapsule --manifest 2026-09-20T00:58:14Z -->
|
||||
<!-- Generated by mkcapsule --manifest 2026-09-20T08:17:49Z -->
|
||||
<!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. -->
|
||||
<!-- Hand-written justifications and immutability notes live -->
|
||||
<!-- in MANIFEST.md alongside this auto-generated index. -->
|
||||
|
||||
@@ -149,28 +149,51 @@ typedef struct {
|
||||
|
||||
/*
|
||||
* sk_hermes_alloc - Heat-coupled allocate (task 2.2, item 28): pull
|
||||
* SK_HERMES_Q_SLOT from vm_id's own Stadium reservoir and claim a free
|
||||
* message slot. Refuses cleanly, touching neither the reservoir nor the
|
||||
* arena, if either is unavailable -- "roll back on refusal" is satisfied
|
||||
* by never pulling until affordability is confirmed, not by pulling then
|
||||
* undoing (though the rollback path exists too, for the pull-then-fail
|
||||
* case the check-first ordering is not expected to reach).
|
||||
* SK_HERMES_Q_SLOT from vm_id's own Stadium reservoir, admit a real
|
||||
* Stadium-floor patron with that heat (behaviour DELIVER, matching
|
||||
* messaging.4th's own `SB-DELIVER STADIUM-ADMIT`), and claim a free
|
||||
* message slot recording the admitted cell. Refuses cleanly, rolling
|
||||
* back anything already pulled/admitted, if reservoir, arena, or the
|
||||
* Stadium floor itself refuses.
|
||||
*
|
||||
* CORRECTED in task 2.3 (see this file's .c counterpart's own top
|
||||
* comment): the first cut of this function never admitted a real
|
||||
* Stadium patron, which left held message heat invisible to SXL.4's
|
||||
* conservation invariant while allocated. It now does, which is what
|
||||
* makes sk_hermes_release()'s eviction meaningful.
|
||||
*
|
||||
* Wired to nothing outside this file's own self-test (kernel_main.c) as
|
||||
* of task 2.2 -- no FORTH word, no capsule interaction, no protocol logic
|
||||
* (send/deliver/reap are later tasks). This function existing and being
|
||||
* exercised by a synthetic-VM self-test does not change any real VM's
|
||||
* dictionary or Stadium state.
|
||||
* of task 2.2/2.3 -- no FORTH word, no capsule interaction, no protocol
|
||||
* logic (send/deliver/reap are later tasks). Exercised only by a
|
||||
* synthetic-VM self-test; does not change any real VM's dictionary.
|
||||
*
|
||||
* @param vm_id Caller whose reservoir is charged.
|
||||
* @param out_msg On success, set to the claimed slot. Untouched on
|
||||
* refusal.
|
||||
* @return 0 on success, -1 on refusal (insufficient reservoir or no free
|
||||
* slot -- task 2.2 does not distinguish the two in the return
|
||||
* value; both leave all state exactly as it was).
|
||||
* @return 0 on success, -1 on refusal (insufficient reservoir, no free
|
||||
* slot, or the Stadium floor itself refused admission -- this
|
||||
* function does not distinguish the three in the return value;
|
||||
* all three leave all state exactly as it was).
|
||||
*/
|
||||
int sk_hermes_alloc(VMUuid vm_id, SkHermesMessage **out_msg);
|
||||
|
||||
/*
|
||||
* sk_hermes_release - Return a message's heat via the Stadium eviction
|
||||
* path (task 2.3, item 28), mirroring MSG-FREE-NODE
|
||||
* ("DUP 5 CELLS + @ STADIUM-EVICT DROP"). stadium_evict() itself returns
|
||||
* the departing patron's remaining heat to its owning VM's reservoir --
|
||||
* this function does not touch the reservoir directly, matching the
|
||||
* FORTH shape exactly. Clears the slot (in_use = 0) whether or not
|
||||
* eviction succeeds, since a message this function was asked to release
|
||||
* should not remain allocated either way.
|
||||
*
|
||||
* @param msg A slot previously returned by sk_hermes_alloc(). Refused
|
||||
* (returns -1, no effect) if NULL or already released.
|
||||
* @return 0 on successful eviction, -1 if msg was invalid or eviction
|
||||
* itself was refused by the Stadium floor.
|
||||
*/
|
||||
int sk_hermes_release(SkHermesMessage *msg);
|
||||
|
||||
#endif /* __STARKERNEL__ */
|
||||
|
||||
#endif /* STARKERNEL_VM_KERNEL_HERMES_H */
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@@ -844,35 +844,51 @@ static void kernel_main_deep(BootInfo *boot_info) {
|
||||
alloc_test_id.hi = 0;
|
||||
alloc_test_id.lo = 3;
|
||||
int grant_rc = stadium_grant_quota(alloc_test_id, vm_uuid_hera());
|
||||
console_puts("Kernel-Hermes alloc self-test: ");
|
||||
console_puts("Kernel-Hermes alloc/release self-test: ");
|
||||
if (grant_rc != 0) {
|
||||
console_println("SKIPPED (quota grant failed)");
|
||||
} else {
|
||||
uint64_t reservoir0 = stadium_reservoir_peek(alloc_test_id);
|
||||
uint64_t expected_n = reservoir0 / SK_HERMES_Q_SLOT;
|
||||
uint64_t got_n = 0;
|
||||
SkHermesMessage *msgs[SK_HERMES_MSG_MAX];
|
||||
SkHermesMessage *msg;
|
||||
int ok = 1;
|
||||
size_t i;
|
||||
|
||||
while (sk_hermes_alloc(alloc_test_id, &msg) == 0) {
|
||||
while (got_n < SK_HERMES_MSG_MAX && sk_hermes_alloc(alloc_test_id, &msg) == 0) {
|
||||
msgs[got_n] = msg;
|
||||
got_n++;
|
||||
if (got_n > expected_n) { ok = 0; break; } /* over-allocated */
|
||||
}
|
||||
if (got_n != expected_n) ok = 0;
|
||||
/* One more attempt past exhaustion must also refuse, and must
|
||||
* not move the reservoir any further -- "roll back on
|
||||
* refusal" verified, not just assumed. */
|
||||
uint64_t reservoir_after_n = stadium_reservoir_peek(alloc_test_id);
|
||||
uint64_t reservoir_after_alloc = stadium_reservoir_peek(alloc_test_id);
|
||||
if (sk_hermes_alloc(alloc_test_id, &msg) == 0) ok = 0;
|
||||
if (stadium_reservoir_peek(alloc_test_id) != reservoir_after_n) ok = 0;
|
||||
if (reservoir_after_n != reservoir0 - got_n * SK_HERMES_Q_SLOT) ok = 0;
|
||||
if (stadium_reservoir_peek(alloc_test_id) != reservoir_after_alloc) ok = 0;
|
||||
if (reservoir_after_alloc != reservoir0 - got_n * SK_HERMES_Q_SLOT) ok = 0;
|
||||
|
||||
/* Task 2.3: release every allocated message via the Stadium
|
||||
* eviction path and confirm the reservoir is restored
|
||||
* exactly -- "reservoir restored exactly for an undecayed
|
||||
* message." No decay logic exists yet (task 2.5), so every
|
||||
* message allocated a moment ago is undecayed by
|
||||
* construction; this is the right point to prove exact
|
||||
* restoration before decay makes it inexact on purpose. */
|
||||
for (i = 0; i < got_n; i++) {
|
||||
if (sk_hermes_release(msgs[i]) != 0) ok = 0;
|
||||
}
|
||||
uint64_t reservoir_final = stadium_reservoir_peek(alloc_test_id);
|
||||
if (reservoir_final != reservoir0) ok = 0;
|
||||
|
||||
console_println(ok ? "PASS" : "FAIL");
|
||||
print_uint(" reservoir0=", reservoir0);
|
||||
print_uint(" Q_SLOT=", SK_HERMES_Q_SLOT);
|
||||
print_uint(" expected_n=", expected_n);
|
||||
print_uint(" got_n=", got_n);
|
||||
print_uint(" reservoir_after=", reservoir_after_n);
|
||||
print_uint(" reservoir_after_alloc=", reservoir_after_alloc);
|
||||
print_uint(" reservoir_final=", reservoir_final);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -23,7 +23,22 @@
|
||||
|
||||
/**
|
||||
* kernel_hermes.c - Kernel-resident Hermes: the heat-coupled allocator
|
||||
* (FABRIC-3.6.md task 2.2, item 28).
|
||||
* and its release path (FABRIC-3.6.md tasks 2.2/2.3, item 28).
|
||||
*
|
||||
* CORRECTION (task 2.3, found while starting it): task 2.2's first cut of
|
||||
* sk_hermes_alloc() pulled reservoir heat but never admitted a real
|
||||
* Stadium-floor patron -- it just set a local `in_use` flag. That is
|
||||
* wrong: FABRIC-3.5.md SXXXIII.4 item 1 states plainly that
|
||||
* "MSG-FREE-NODE returns it via STADIUM-EVICT", which only has something
|
||||
* to evict if allocation admitted something. More importantly, SXL.4's
|
||||
* invariant is Sigma(resident patron heat) + reservoir + consumed ==
|
||||
* Q48_ONE -- if held message heat is not a resident patron, it is
|
||||
* invisible to every term of that equation while held, which cannot be
|
||||
* right. Corrected here: sk_hermes_alloc() now calls stadium_admit()
|
||||
* with the pulled heat, storing the returned cell index in the message's
|
||||
* own stadium_cell field for release to evict later. Behaviour
|
||||
* DELIVER (1), matching messaging.4th's own `SB-DELIVER STADIUM-ADMIT`
|
||||
* at its MSG-ALLOC site.
|
||||
*/
|
||||
|
||||
#ifdef __STARKERNEL__
|
||||
@@ -45,6 +60,8 @@ static int sk_hermes_find_free_slot(void) {
|
||||
int sk_hermes_alloc(VMUuid vm_id, SkHermesMessage **out_msg) {
|
||||
int slot;
|
||||
uint64_t pulled;
|
||||
StadiumPatronHeader candidate;
|
||||
size_t cell;
|
||||
|
||||
if (!out_msg) return -1;
|
||||
|
||||
@@ -66,10 +83,54 @@ int sk_hermes_alloc(VMUuid vm_id, SkHermesMessage **out_msg) {
|
||||
return -1;
|
||||
}
|
||||
|
||||
memset(&candidate, 0, sizeof(candidate));
|
||||
/* Matches messaging.4th's own MSG-ALLOC: the slot's own index becomes
|
||||
* the admitted patron's identity, which stadium_dispatch()'s DELIVER
|
||||
* case later prints back as "msg_idx=" on release -- an arbitrary
|
||||
* distinct value would satisfy the conservation math just as well,
|
||||
* but this keeps the diagnostic meaningful instead of every message
|
||||
* printing identity 0. */
|
||||
candidate.identity = (uint64_t)slot;
|
||||
candidate.heat = pulled; /* the reservoir pull itself, unmodified */
|
||||
candidate.ttl = 0; /* decay/TTL is task 2.5's scope, not this one's */
|
||||
candidate.link = 0;
|
||||
candidate.contains = STADIUM_CONTAINS_NONE;
|
||||
candidate.mass = 1; /* message body lives in sk_hermes_msgs[], not here */
|
||||
candidate.flags = 0;
|
||||
candidate.behaviour = (uint8_t)STADIUM_BEHAVIOUR_DELIVER;
|
||||
|
||||
cell = stadium_admit(vm_id, &candidate);
|
||||
if (cell == STADIUM_CELL_NONE) {
|
||||
/* Stadium floor itself refused (unrelated to heat affordability,
|
||||
* already confirmed above) -- roll back the pull, same "leave
|
||||
* everything exactly as found" discipline as every other refusal
|
||||
* path here. */
|
||||
stadium_reservoir_push(vm_id, pulled);
|
||||
return -1;
|
||||
}
|
||||
|
||||
memset(&sk_hermes_msgs[slot], 0, sizeof(SkHermesMessage));
|
||||
sk_hermes_msgs[slot].in_use = 1;
|
||||
sk_hermes_msgs[slot].in_use = 1;
|
||||
sk_hermes_msgs[slot].stadium_cell = (int32_t)cell;
|
||||
*out_msg = &sk_hermes_msgs[slot];
|
||||
return 0;
|
||||
}
|
||||
|
||||
int sk_hermes_release(SkHermesMessage *msg) {
|
||||
int rc;
|
||||
|
||||
if (!msg || !msg->in_use) return -1;
|
||||
|
||||
/* stadium_evict() returns the departing patron's remaining heat to
|
||||
* its owner's reservoir itself (stadium.c: "the departing patron's
|
||||
* remaining heat must flow back to its owner's reservoir before the
|
||||
* cell returns to the free list") -- release does not touch the
|
||||
* reservoir directly, the eviction path does it, matching
|
||||
* MSG-FREE-NODE's own shape ("DUP 5 CELLS + @ STADIUM-EVICT DROP"). */
|
||||
rc = (msg->stadium_cell >= 0) ? stadium_evict((size_t)msg->stadium_cell) : -1;
|
||||
|
||||
memset(msg, 0, sizeof(*msg));
|
||||
return rc;
|
||||
}
|
||||
|
||||
#endif /* __STARKERNEL__ */
|
||||
|
||||
Reference in New Issue
Block a user