starkernel: item 4.1 -- hot words onto the Stadium, density-ranked eviction
Punch list §25 item 4.1 complete. Replaces the round-robin hotwords cache with Stadium density-ranked admission/eviction on the kernel side, via the §17.7 reservoir mechanism and a kernel-side word_id -> cell_index map (no DictEntry change, dict_hash untouched). Adds stadium_birth_hera() to close the cell-0 panic hazard, STADIUM_WORD_HEAT_QUANTUM/STADIUM_WORD_COOL_RATE_Q48 Kconfig knobs (flagged untuned), and a stadium_word_forget() FORGET coherence hook to close a recycled-word_id aliasing gap. Verified: all five hotwords_cache_* call sites in dictionary_management.c bypassed under __STARKERNEL__; word dispatch feeds the Stadium at all three vm_core.c physics_execution_heat_increment() sites; hosted make unaffected; all three architectures booted to ok> with matching dict_hash (0x3d4e1daf289da94f) and matching conservation stats (promotions=354 evictions=0, resident_sum=65536 reservoir=0 sum=65536). 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
bd92c57834
commit
3d0b9351bd
@@ -241,6 +241,72 @@ uint64_t stadium_density(size_t cell_index);
|
||||
*/
|
||||
#define STADIUM_HERA_CELL_INDEX ((size_t)0)
|
||||
|
||||
/*
|
||||
* stadium_birth_hera - Admits Hera as a real resident of cell 0 (FABRIC.md
|
||||
* item 3.6's invariant, actually enforced -- item 4.1 found that nothing had
|
||||
* ever called this until a word patron was about to become the first-ever
|
||||
* occupant of cell 0 by accident via the free list). Candidate: identity 0,
|
||||
* heat 0, mass 1, pinned (STADIUM_FLAG_PIN), behaviour COOL. Heat 0 means no
|
||||
* reservoir transfer is needed -- conservation holds trivially (the
|
||||
* reservoir keeps the VM's whole share; Hera's own cell contributes 0).
|
||||
* Being pinned excludes her from every eviction-candidate scan (§3), so the
|
||||
* stadium_evict() panic guard at STADIUM_HERA_CELL_INDEX stays correctly
|
||||
* dormant rather than reachable-by-accident.
|
||||
*
|
||||
* Idempotent: a second call is a no-op (returns 0) if she is already
|
||||
* resident. Must be called after stadium_boot_init() and before any word
|
||||
* ever dispatches (§6) -- kernel_main.c calls it immediately after
|
||||
* stadium_boot_init(), before M7's VM bootstrap.
|
||||
*
|
||||
* @return 0 on success (or already born), -1 if the Stadium is not
|
||||
* initialized or the admission was refused (should not happen: her
|
||||
* quota is granted in full, empty, at stadium_boot_init()).
|
||||
*/
|
||||
int stadium_birth_hera(void);
|
||||
|
||||
/*
|
||||
* stadium_reservoir_pull - Transfers up to `amount` (Q48.16) out of vm_id's
|
||||
* reservoir (FABRIC.md §17.7's reservoir mechanism). Clamped to what the
|
||||
* reservoir actually holds -- never goes negative, never invents heat.
|
||||
* Returns the amount actually pulled, which may be less than requested (or
|
||||
* 0, e.g. a drained reservoir or an unknown vm_id). Callers that go on to
|
||||
* fail their own operation (e.g. a refused stadium_admit()) MUST push the
|
||||
* pulled amount back via stadium_reservoir_push() to preserve
|
||||
* Σ(resident heat) + reservoir == Q48_ONE across the failed attempt.
|
||||
*
|
||||
* @param vm_id Owning VM's id.
|
||||
* @param amount Requested Q48.16 amount.
|
||||
* @return Amount actually pulled (0..amount).
|
||||
*/
|
||||
uint64_t stadium_reservoir_pull(VMUuid vm_id, uint64_t amount);
|
||||
|
||||
/*
|
||||
* stadium_reservoir_push - Credits `amount` (Q48.16) back into vm_id's
|
||||
* reservoir. The other half of every reservoir transfer (§17.7): cooling
|
||||
* returns heat here, a refused starter-grant rolls back here, and
|
||||
* stadium_evict() credits a departing patron's remaining heat here before
|
||||
* the cell returns to the free list -- the invariant is a transfer, never a
|
||||
* reset. No-op if vm_id has no quota (caller contract; mirrors
|
||||
* stadium_admit()'s silent refusal for the same case).
|
||||
*
|
||||
* @param vm_id Owning VM's id.
|
||||
* @param amount Q48.16 amount to credit.
|
||||
*/
|
||||
void stadium_reservoir_push(VMUuid vm_id, uint64_t amount);
|
||||
|
||||
/*
|
||||
* stadium_reservoir_peek - Read-only: vm_id's current reservoir balance
|
||||
* (Q48.16), for diagnostics/conservation checks. Does not mutate state.
|
||||
* Returns 0 for an unknown vm_id -- indistinguishable from a genuinely
|
||||
* drained reservoir, same as stadium_reservoir_pull()'s 0 return; callers
|
||||
* that need to tell those apart must already know whether vm_id has a
|
||||
* quota (e.g. via the same check they'd use before calling stadium_admit()).
|
||||
*
|
||||
* @param vm_id Owning VM's id.
|
||||
* @return Current reservoir balance, or 0 if vm_id has no quota.
|
||||
*/
|
||||
uint64_t stadium_reservoir_peek(VMUuid vm_id);
|
||||
|
||||
/*
|
||||
* stadium_evict - Reap the patron header at cell_index (FABRIC.md §17.2:
|
||||
* "reap means leaves the floor, not destroyed"). Dispatches its behaviour
|
||||
|
||||
@@ -0,0 +1,138 @@
|
||||
/*
|
||||
StarForth — Steady-State Virtual Machine Runtime
|
||||
|
||||
Copyright (c) 2023–2025 Robert A. James
|
||||
All rights reserved.
|
||||
|
||||
This file is part of the StarForth project.
|
||||
|
||||
Licensed under the StarForth License, Version 1.0 (the "License");
|
||||
you may not use this file except in compliance with the License.
|
||||
|
||||
You may obtain a copy of the License at:
|
||||
https://github.com/star.4th@proton.me/StarForth/LICENSE.txt
|
||||
|
||||
This software is provided "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
express or implied, including but not limited to the warranties of
|
||||
merchantability, fitness for a particular purpose, and noninfringement.
|
||||
|
||||
See the License for the specific language governing permissions and
|
||||
limitations under the License.
|
||||
|
||||
*/
|
||||
|
||||
/**
|
||||
* stadium_words.h - Word patrons on the Stadium (FABRIC.md §17.3/§17.7,
|
||||
* punch list item 4.1)
|
||||
*
|
||||
* The word-specific layer on top of the generic L0 engine (stadium.h).
|
||||
* Nothing in stadium.c/.h knows a word patron exists -- it only ever sees
|
||||
* cell_index, VMUuid, and StadiumPatronHeader. This file is where "word"
|
||||
* becomes a concrete meaning: a word_id -> cell_index map (kernel-side,
|
||||
* deliberately NOT a DictEntry field, decided 2026-08-05), the starter-grant
|
||||
* admission rule (Option B), and the reservoir-quantum touch/cool that feed
|
||||
* and drain a resident word's Stadium heat.
|
||||
*
|
||||
* `execution_heat` and `dict_hash` are untouched by anything in this file
|
||||
* (§17.7) -- this is a second, independent conserved quantity living in the
|
||||
* Stadium cell's `heat` field, not a representation of the first.
|
||||
*/
|
||||
|
||||
#ifndef STARKERNEL_VM_STADIUM_WORDS_H
|
||||
#define STARKERNEL_VM_STADIUM_WORDS_H
|
||||
|
||||
#ifdef __STARKERNEL__
|
||||
|
||||
#include <stdint.h>
|
||||
#include "starkernel/vm_uuid.h"
|
||||
|
||||
/*
|
||||
* stadium_words_init - Zeroes the word_id -> cell_index map (DICTIONARY_SIZE
|
||||
* entries, static -- no allocation). Must be called after stadium_boot_init()
|
||||
* and stadium_birth_hera(), before any word ever dispatches. Safe to call
|
||||
* again (re-zeroes); nothing does today.
|
||||
*/
|
||||
void stadium_words_init(void);
|
||||
|
||||
/*
|
||||
* stadium_word_dispatch - The per-dispatch entry point (FABRIC.md §17.7),
|
||||
* called once per DictEntry touched at each of vm_core.c's three
|
||||
* physics_execution_heat_increment() call sites -- deliberately mirroring
|
||||
* that function's existing call pattern 1:1, including the entry != canon
|
||||
* double-touch case, rather than inventing a different shape.
|
||||
*
|
||||
* If word_id is already resident: applies the redirected Loop #3 cooling
|
||||
* (fraction of the cell's own current heat, scaled by elapsed_ticks since
|
||||
* this word's own last touch -- STADIUM_WORD_COOL_RATE_Q48) crediting the
|
||||
* cooled amount back to vm_id's reservoir, then pulls
|
||||
* STADIUM_WORD_HEAT_QUANTUM from the reservoir into the cell (both clamped
|
||||
* to what the reservoir actually holds).
|
||||
*
|
||||
* If word_id is not resident (or the map's entry is stale -- self-healing
|
||||
* check against the cell's discriminator bit and identity, covers both a
|
||||
* prior eviction and a FORGET/redefine word_id reuse this function did not
|
||||
* itself clear): attempts Option B starter-grant admission -- pulls
|
||||
* STADIUM_WORD_HEAT_QUANTUM from the reservoir, builds an unpinned COOL
|
||||
* candidate, calls stadium_admit(). On refusal, pushes the pulled quantum
|
||||
* back (rollback, preserves conservation across the failed attempt). On
|
||||
* success, records the mapping and increments the promotion counter.
|
||||
*
|
||||
* No-op if word_id == WORD_ID_INVALID, word_id >= DICTIONARY_SIZE, or the
|
||||
* word layer has not been initialized.
|
||||
*
|
||||
* @param vm_id Owning VM. Hardcoded to vm_uuid_hera() at every
|
||||
* call site today -- Tripod is pruned to Hera alone
|
||||
* (item 0.1), and she is the only VM with a Stadium
|
||||
* quota. Revisit when item 4.2 restores Hermes.
|
||||
* @param word_id The dispatching DictEntry's stable word_id.
|
||||
* @param heartbeat_ticks Current vm->heartbeat.tick_count (virtual tick,
|
||||
* never wall-clock -- same convention as every other
|
||||
* decay computation in this tree).
|
||||
*/
|
||||
void stadium_word_dispatch(VMUuid vm_id, uint32_t word_id, uint64_t heartbeat_ticks);
|
||||
|
||||
/*
|
||||
* stadium_word_forget - Coherence hook for FORGET (word_id recycling).
|
||||
* vm_dictionary_untrack_entry() must call this BEFORE the word_id is pushed
|
||||
* onto vm->recycled_word_ids -- otherwise the next word assigned the same
|
||||
* recycled id would alias onto the forgotten word's still-resident cell and
|
||||
* its stale heat (same failure class as the 2026-08-02 block_words.c
|
||||
* aliasing bug). Evicts the cell if word_id is resident (crediting its heat
|
||||
* back to the reservoir via stadium_evict()'s own credit path) and clears
|
||||
* the map entry. No-op if word_id is not resident, out of range, or the
|
||||
* word layer is not initialized.
|
||||
*
|
||||
* @param word_id The DictEntry's word_id, about to be recycled.
|
||||
*/
|
||||
void stadium_word_forget(uint32_t word_id);
|
||||
|
||||
/*
|
||||
* stadium_words_stats - Promotion/eviction counters (same shape as the old
|
||||
* cache's HotwordsStats.promotions/.evictions, not that struct -- §25.5's
|
||||
* acceptance for item 4.1). Promotion = a successful starter-grant
|
||||
* admission. Eviction = this word's cell was reaped by another admission's
|
||||
* eviction fallback (stadium_admit()'s density comparison), detected
|
||||
* lazily via the self-healing stale check in stadium_word_dispatch(), or
|
||||
* explicitly via stadium_word_forget().
|
||||
*/
|
||||
void stadium_words_stats(uint64_t *promotions, uint64_t *evictions);
|
||||
|
||||
/*
|
||||
* stadium_words_print_boot_diagnostics - Console output satisfying item
|
||||
* 4.1's "observable via a diagnostic word or boot console output"
|
||||
* acceptance line. Prints promotions/evictions, then
|
||||
* Σ(resident heat) + reservoir against Q48_ONE as a conservation check --
|
||||
* not required by the acceptance text, but the mechanism proves nothing if
|
||||
* this silently doesn't hold. The heat sum is taken over ALL resident
|
||||
* Stadium cells, not scoped by owner -- correct only because vm_id is the
|
||||
* sole VM with any Stadium quota today (item 0.1's Hera-only pruning); the
|
||||
* per-cell owner byte is private to stadium.c and has no public accessor.
|
||||
* Revisit the scoping when item 4.2 restores Hermes.
|
||||
*
|
||||
* @param vm_id The VM whose reservoir to read (vm_uuid_hera() today).
|
||||
*/
|
||||
void stadium_words_print_boot_diagnostics(VMUuid vm_id);
|
||||
|
||||
#endif /* __STARKERNEL__ */
|
||||
|
||||
#endif /* STARKERNEL_VM_STADIUM_WORDS_H */
|
||||
Reference in New Issue
Block a user