starkernel: item 4.2 -- Hermes native on the Stadium (complete)
Migrates Hermes's message/channel lifecycle onto the Stadium's unified heat/capacity economy: MSG-ALLOC/FREE-NODE and CH-ALLOC/FREE-NODE now route entirely through stadium_admit()/stadium_evict(), replacing the old local free-list + independent heat-field mechanism. Eight kernel-only STADIUM-* FORTH primitives (ADMIT, EVICT, RES@, RES-PULL, RES-PUSH, HEAT@, HEAT!, WORD-HEAT), VM.stadium_vm_id threaded through all three vm_core.c dispatch sites (replacing item 4.1's hardcoded vm_uuid_hera()), and the stadium_owner[idx] fix so evict-credit lands in the VM that actually admitted a patron, not whoever owned cell 0. This session's own contribution, on top of that pre-existing implementation: found and fixed two bugs blocking the item's own K≡1.0 conservation self-check (HERMES-K was reading 0, not 65536): - Q.SLOT admission-heat fix (capsules/hermes/init.4th): MSG-SEND/ CH-ACCEPT admitted with Q.1 (the entire fleet-wide "1.0" unit) per item, a leftover from before the Stadium migration when each message/channel had its own unconstrained heat field. Instantly drained the shared, finite reservoir. - Reservoir floor for word-execution admission (stadium_words.c): stadium_word_dispatch() (item 4.1) pulls STADIUM_WORD_HEAT_QUANTUM on every word dispatch, not just first admission -- exhausts a VM's entire reservoir in ~32 dispatches, starving any application-level economy sharing that VM's reservoir before it gets a chance to pull anything. word_dispatch_pull() now clamps word-execution's own pulls to leave a Q48_ONE/3 floor (same fair-share figure COMMON-CH's own floor already uses); application-level pulls are unaffected. - STADIUM-WORD-HEAT primitive + stadium_words_resident_heat(): the floor deliberately leaves word-execution residents holding real heat, invisible to HERMES-K's original formula (MSG+CH+reservoir, no term for word patrons). Adding this term closes K to exactly 65536 on all three architectures. Also rules on two open scope questions in FABRIC.md: MBR-ALLOC/ MBR-FREE-NODE stay off the Stadium (membership records have no heat field, never did -- the acceptance bullet's inclusion of them was a completeness gesture predating a check of the actual layout), and records the effort number (12 implementation files, +759/-120 lines). Verified: all three architectures boot clean, full self-test passes, Stadium conservation closes exactly (resident_sum + reservoir = Q48_ONE) at both the C/Stadium level and the FORTH-level HERMES-K check. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
0a7f144367
commit
5a28458b21
@@ -358,6 +358,10 @@ size_t stadium_admit(VMUuid vm_id, const StadiumPatronHeader *candidate) {
|
||||
stadium_quotas[slot].free_head = link_to_size(stadium_cell_array[idx].header.link);
|
||||
stadium_cell_array[idx].header = *candidate;
|
||||
bitmap_set(idx);
|
||||
/* Item 4.2 fix (§25.7): record ownership so stadium_evict()'s
|
||||
* reservoir credit and free-list return land on the VM that actually
|
||||
* admitted this patron, not whatever owner[idx] held at boot. */
|
||||
stadium_owner[idx] = (uint8_t)slot;
|
||||
return idx;
|
||||
}
|
||||
|
||||
@@ -395,6 +399,11 @@ size_t stadium_admit(VMUuid vm_id, const StadiumPatronHeader *candidate) {
|
||||
stadium_quotas[slot].free_head = link_to_size(stadium_cell_array[idx].header.link);
|
||||
stadium_cell_array[idx].header = *candidate;
|
||||
bitmap_set(idx);
|
||||
/* Same fix as the free-list-pop path above -- stadium_evict() just wrote
|
||||
* owner[idx] = slot as part of reaping least_dense_index, so this is
|
||||
* currently a no-op in practice, but it must not be assumed to stay a
|
||||
* no-op: this is the correctness statement, not a redundant write. */
|
||||
stadium_owner[idx] = (uint8_t)slot;
|
||||
return idx;
|
||||
}
|
||||
|
||||
@@ -453,6 +462,45 @@ int stadium_grant_quota(VMUuid new_vm_id, VMUuid from_vm_id) {
|
||||
return 0;
|
||||
}
|
||||
|
||||
/* Shared by stadium_cell_heat_get()/_set(): resident AND owned by vm_id's
|
||||
* own quota slot. Returns the quota slot on success, -1 on any refusal. */
|
||||
static int owned_resident_slot(VMUuid vm_id, size_t cell_index) {
|
||||
int slot = quota_slot_for_vm(vm_id);
|
||||
if (slot < 0) return -1;
|
||||
if (cell_index >= stadium_ncells) return -1;
|
||||
if (!bitmap_get(cell_index)) return -1;
|
||||
if (stadium_owner[cell_index] != (uint8_t)slot) return -1;
|
||||
return slot;
|
||||
}
|
||||
|
||||
uint64_t stadium_cell_heat_get(VMUuid vm_id, size_t cell_index) {
|
||||
if (owned_resident_slot(vm_id, cell_index) < 0) return 0;
|
||||
return stadium_cell_array[cell_index].header.heat;
|
||||
}
|
||||
|
||||
int stadium_cell_heat_set(VMUuid vm_id, size_t cell_index, uint64_t new_heat) {
|
||||
int slot = owned_resident_slot(vm_id, cell_index);
|
||||
uint64_t old_heat, delta, pulled;
|
||||
|
||||
if (slot < 0) return -1;
|
||||
|
||||
old_heat = stadium_cell_array[cell_index].header.heat;
|
||||
if (new_heat == old_heat) return 0;
|
||||
|
||||
if (new_heat > old_heat) {
|
||||
delta = new_heat - old_heat;
|
||||
pulled = (delta > stadium_quotas[slot].reservoir) ? stadium_quotas[slot].reservoir : delta;
|
||||
if (pulled < delta) return -1; /* insufficient -- no partial credit, no mutation */
|
||||
stadium_quotas[slot].reservoir -= pulled;
|
||||
} else {
|
||||
delta = old_heat - new_heat;
|
||||
stadium_quotas[slot].reservoir += delta;
|
||||
}
|
||||
|
||||
stadium_cell_array[cell_index].header.heat = new_heat;
|
||||
return 0;
|
||||
}
|
||||
|
||||
uint64_t stadium_reservoir_pull(VMUuid vm_id, uint64_t amount) {
|
||||
int slot = quota_slot_for_vm(vm_id);
|
||||
uint64_t pulled;
|
||||
@@ -478,6 +526,25 @@ uint64_t stadium_reservoir_peek(VMUuid vm_id) {
|
||||
return stadium_quotas[slot].reservoir;
|
||||
}
|
||||
|
||||
int stadium_quota_slot_for_vm(VMUuid vm_id) {
|
||||
return quota_slot_for_vm(vm_id);
|
||||
}
|
||||
|
||||
uint64_t stadium_resident_sum(VMUuid vm_id) {
|
||||
int slot = quota_slot_for_vm(vm_id);
|
||||
uint64_t sum = 0;
|
||||
size_t i;
|
||||
|
||||
if (slot < 0) return 0;
|
||||
|
||||
for (i = 0; i < stadium_ncells; i++) {
|
||||
if (!bitmap_get(i)) continue;
|
||||
if (stadium_owner[i] != (uint8_t)slot) continue;
|
||||
sum += stadium_cell_array[i].header.heat;
|
||||
}
|
||||
return sum;
|
||||
}
|
||||
|
||||
/*
|
||||
* FABRIC.md item 3.6 / item 4.1: see stadium.h's doc. Idempotent via the
|
||||
* item-3.1 discriminator bitmap -- if cell 0 already reads as resident,
|
||||
|
||||
Reference in New Issue
Block a user