starkernel: item 3.7 -- per-VM free lists (Phase 3 core complete, for real)
Punch list §25 item 3.7 complete. Added to §25.4 after starting item 4.1 surfaced it as an unbuilt prerequisite -- 3.6's earlier "Phase 3 core complete" claim is corrected in this same commit. StadiumVMQuota table (size STADIUM_MAX_VM_COUNT, linearly searched by vm_id -- capsule_birth.c's vm_id is monotonic and never reused, so it cannot index a table directly, and a 4-entry scan costs nothing). New per-cell stadium_owner byte array records which quota a cell belongs to, needed so eviction returns a freed cell to the correct VM's list and so eviction search stays scoped to the evicting VM's own residents (quota isolation). Free-list linkage reuses each cell's `link` field as a next-free pointer while unresident -- link is documented only as generic "index into the Stadium, not a pointer," so this is a repurposing, not a header change. Does not answer the separate, still-open question of which field carries a multi-cell patron's first continuation-cell index; item 3.5's mass != 1 refusal stands exactly as it was. Boot-time: every cell chained into one list in ascending index order, granted whole to vm_id 0 (Hera), the only VM that exists. Ascending order preserves item 3.6's "Hera is patron zero" invariant once real birth-wiring lands. stadium_admit()'s signature changed to take vm_id -- a change to code shipped in item 3.5, amended there. Pops the calling VM's free-list head first (O(1)); only falls back to a same-VM-scoped eviction search if empty. Caught a real bug before the boot run: the header zero-fill on eviction (and the initial free-list build) both left contains == 0, but 0 is Hera's valid index -- the same collision item 3.1's STADIUM_CONTAINS_NONE fix addressed, recurring at a new site. Fixed by explicitly setting contains = STADIUM_CONTAINS_NONE at both free-list sites. Explicitly out of scope, reported not invented: granting quota to any VM other than Hera is capacity arbitration (item 1.3 left "how much moves per transfer" open). stadium_owner is set once at boot and never rewritten, so quota_slot_for_vm() refuses every vm_id != 0 permanently until item 4.2 adds the grant path and owner-array writes. Verified: three-architecture boot (amd64, aarch64, riscv64), all reaching ok> with identical dict_hash=0x3d4e1daf289da94f matching the item-3.6 baseline. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
72487e7fff
commit
e55111c2c5
@@ -116,6 +116,14 @@ typedef char stadium_cell_size_check[(sizeof(StadiumCell) == STADIUM_CELL_BYTES)
|
||||
typedef char stadium_contains_depth_configured_check[(STADIUM_CONTAINS_DEPTH_MAX > 0) ? 1 : -1];
|
||||
typedef char stadium_capacity_tick_configured_check[(STADIUM_CAPACITY_TICK > 0) ? 1 : -1];
|
||||
|
||||
/*
|
||||
* Item 3.7: the per-cell owner array stores a quota-slot index in a single
|
||||
* uint8_t, so STADIUM_MAX_VM_COUNT must fit in one byte. Default 4, so this
|
||||
* holds by a wide margin -- checked because it is depended on, not because
|
||||
* it is expected to fail.
|
||||
*/
|
||||
typedef char stadium_max_vm_count_fits_owner_byte_check[(STADIUM_MAX_VM_COUNT <= 255) ? 1 : -1];
|
||||
|
||||
/*
|
||||
* stadium_boot_init - Boot-time allocation (FABRIC.md item 3.2, §17.6 position
|
||||
* (b)). Sizes the global cell array from the memory budget actually observed
|
||||
@@ -128,10 +136,21 @@ typedef char stadium_capacity_tick_configured_check[(STADIUM_CAPACITY_TICK > 0)
|
||||
* PMM-backed region needed for this) and explicitly zero-filled, since
|
||||
* kmalloc does not zero.
|
||||
*
|
||||
* (Item 3.7) Also allocates a per-cell owner byte array (which VM's quota a
|
||||
* cell belongs to) and chains every cell into a single free list, in
|
||||
* ascending index order, granted in full to vm_id 0 (Hera) -- the only VM
|
||||
* that exists (item 0.1). Ascending order guarantees the first-ever
|
||||
* admission pops cell 0, preserving item 3.6's "Hera is patron zero"
|
||||
* invariant once real birth-wiring calls stadium_admit() for the first
|
||||
* time. The free-list next-pointer reuses each cell's own `link` field
|
||||
* while unresident -- a repurposing of documented-but-unspecified storage,
|
||||
* not a header change; see stadium_admit()'s doc for why this doesn't
|
||||
* answer the separate, still-open continuation-chain question.
|
||||
*
|
||||
* Must be called after M6 (kmalloc_init) and before any VM is born (§6). Does
|
||||
* not halt boot on failure -- nothing downstream consumes the Stadium yet.
|
||||
*
|
||||
* @return 0 on success, -1 if kmalloc failed for either allocation.
|
||||
* @return 0 on success, -1 if kmalloc failed for any of the three allocations.
|
||||
*/
|
||||
int stadium_boot_init(void);
|
||||
|
||||
@@ -224,7 +243,10 @@ uint64_t stadium_density(size_t cell_index);
|
||||
/*
|
||||
* stadium_evict - Reap the patron header at cell_index (FABRIC.md §17.2:
|
||||
* "reap means leaves the floor, not destroyed"). Dispatches its behaviour
|
||||
* (§18.3), clears its item-3.1 discriminator bit, zeroes its header.
|
||||
* (§18.3), clears its item-3.1 discriminator bit, zeroes its header, and
|
||||
* (item 3.7) returns the freed cell to the free list of whichever VM's
|
||||
* quota it was drawn from -- looked up via the internal per-cell owner
|
||||
* record, not passed by the caller.
|
||||
*
|
||||
* PANICS (does not return) if cell_index == STADIUM_HERA_CELL_INDEX and the
|
||||
* cell is actually resident -- FABRIC.md §20.5 #3: Hera is pinned (§3), but
|
||||
@@ -248,29 +270,53 @@ uint64_t stadium_density(size_t cell_index);
|
||||
int stadium_evict(size_t cell_index);
|
||||
|
||||
/*
|
||||
* stadium_admit - Place a candidate patron header into the Stadium (FABRIC.md
|
||||
* §19.3).
|
||||
* StadiumVMQuota - per-VM ownership of a subset of the global cell array
|
||||
* (FABRIC.md §22.3, item 3.7: "each VM holds its own free-list head index
|
||||
* into the global array"). A small table, linearly searched by vm_id --
|
||||
* capsule_birth.c's vm_id is monotonic and never reused (next_vm_id only
|
||||
* increments, even across VM death), so it cannot index this table
|
||||
* directly, and STADIUM_MAX_VM_COUNT is small enough (default 4) that a
|
||||
* linear scan costs nothing. Not exposed outside stadium.c: nothing outside
|
||||
* needs to inspect quota state directly yet.
|
||||
*/
|
||||
|
||||
/* Sentinel meaning "no VM owns this slot yet." Distinct from a real vm_id
|
||||
* (capsule_birth.c reserves 0 for Hera, so 0 cannot double as "unused" here
|
||||
* either -- same shape of mistake STADIUM_CONTAINS_NONE was fixed for). */
|
||||
#define STADIUM_QUOTA_SLOT_EMPTY ((uint32_t)-1)
|
||||
|
||||
/*
|
||||
* stadium_admit - Place a candidate patron header into the Stadium, scoped
|
||||
* to vm_id's quota (FABRIC.md §19.3, §22.3, item 3.7).
|
||||
*
|
||||
* First scans for an unused cell (discriminator bit clear and mass == 0) and
|
||||
* places the candidate there directly -- §19.3's density comparison only
|
||||
* governs the full case, not this one. If none is free, finds the
|
||||
* least-dense resident (discriminator bit set, mass > 0, not pinned, not
|
||||
* `contains`-gated -- pinned and gated residents are never eviction
|
||||
* candidates, per §3 and item 1.1) and evicts it via stadium_evict() only if
|
||||
* the candidate is strictly denser (§19.3: "denser than," not "at least as
|
||||
* dense as"). Otherwise refuses.
|
||||
* Pops vm_id's free-list head first (O(1)) if non-empty. Only if that VM's
|
||||
* free list is exhausted does this fall back to eviction -- scoped to that
|
||||
* SAME VM's own resident patrons only (quota isolation: a VM's admission can
|
||||
* never evict another VM's patron), finding the least-dense evictable
|
||||
* resident (not pinned, not `contains`-gated -- per §3 and item 1.1) and
|
||||
* evicting it via stadium_evict() only if the candidate is strictly denser
|
||||
* (§19.3: "denser than," not "at least as dense as"). Otherwise refuses.
|
||||
*
|
||||
* Does not itself assert anything about which resident this turns out to be
|
||||
* -- the item-3.6 rule that patron zero (Hera) must never actually be
|
||||
* selected is a separate, later check at the eviction site.
|
||||
*
|
||||
* REFUSES if vm_id has no quota granted (only Hera, vm_id 0, has one today
|
||||
* -- granted the entire array at stadium_boot_init(), since she is the only
|
||||
* VM that exists per item 0.1). Granting quota to additional VMs, and
|
||||
* transferring capacity between them, is capacity ARBITRATION -- item 1.3
|
||||
* left "how much capacity moves per eligible transfer" explicitly open, so
|
||||
* this item does not invent it. Only the boot-time all-to-Hera grant exists.
|
||||
*
|
||||
* REFUSES any candidate with mass != 1. A multi-cell patron (mass > 1, e.g.
|
||||
* §23.3's 1024-byte block at mass 19) needs its continuation chain allocated
|
||||
* too, which needs the per-VM free lists §22.3 describes -- item 3.2's DONE
|
||||
* note already deferred those (not this item's scope, they are granted when
|
||||
* Hera assigns a VM its quota). Admitting only the header and leaking the
|
||||
* rest would break capacity conservation, so this refuses rather than doing
|
||||
* that. Revisit when the free lists exist.
|
||||
* §23.3's 1024-byte block at mass 19) needs a continuation chain, and no
|
||||
* header field is documented anywhere as carrying the index of a patron's
|
||||
* first continuation cell -- `link` is described only as generic "index
|
||||
* into the Stadium, not a pointer." This item repurposes `link` for a
|
||||
* different, non-conflicting use (the free-list next-pointer, while a cell
|
||||
* is unresident -- see stadium.c), but does not invent an answer to the
|
||||
* continuation-chain question, which stays open. Item 3.5's refusal
|
||||
* therefore stands exactly as it was.
|
||||
*
|
||||
* REQUIRES candidate->contains to be either STADIUM_CONTAINS_NONE or a valid
|
||||
* index (< the current cell count) -- refuses otherwise. This does NOT catch
|
||||
@@ -281,14 +327,16 @@ int stadium_evict(size_t cell_index);
|
||||
* "meant to be 0" from "forgot to set it" from inside this function --
|
||||
* callers must set every field, `contains` included.
|
||||
*
|
||||
* @param candidate Header to admit. Copied into the winning cell as-is;
|
||||
* @param vm_id Owning VM's id (capsule_birth.c's registry). Allocation
|
||||
* is scoped to this VM's own quota.
|
||||
* @param candidate Header to admit. Copied into the winning cell as-is;
|
||||
* caller fills in every field including mass and heat.
|
||||
* @return The cell index admitted into, or STADIUM_CELL_NONE if refused
|
||||
* (mass != 1, invalid contains, Stadium full and candidate not
|
||||
* denser than the least-dense evictable resident, or no evictable
|
||||
* resident exists at all).
|
||||
* (vm_id has no quota, mass != 1, invalid contains, that VM's
|
||||
* quota full and candidate not denser than its least-dense
|
||||
* evictable resident, or it has no evictable resident at all).
|
||||
*/
|
||||
size_t stadium_admit(const StadiumPatronHeader *candidate);
|
||||
size_t stadium_admit(uint32_t vm_id, const StadiumPatronHeader *candidate);
|
||||
|
||||
#endif /* __STARKERNEL__ */
|
||||
|
||||
|
||||
Reference in New Issue
Block a user