Robert Allan JamesandClaude Sonnet 5
eb0fd4fffa
Punch list §25 item 3.2 complete. stadium_boot_init() (src/starkernel/vm/stadium.c) sizes the global cell array at boot from a real memory-budget query rather than a hardcoded count: pmm_get_stats().free_bytes at the point of allocation, times the new STADIUM_MEMORY_PERCENT Kconfig symbol (default 1%), rounded down to whole 64-byte cells. Matches §17.6's position (b) literally. Also allocates the header/continuation discriminator bitmap item 3.1 declared but did not allocate. Both are kmalloc'd and explicitly zero-filled (kmalloc does not zero). Called from kernel_main.c immediately before sk_vm_bootstrap_parity(), i.e. before any VM exists (§6). Failure is soft -- logs and continues, does not halt boot -- matching the existing precedent one line below it (VM bootstrap parity failure does the same). Added a "Stadium: N cells (M KB)" boot console line at the allocation site so the acceptance logs are evidence the array was actually allocated, not just that the kernel still boots -- the same blind spot item 3.1's uncompiled-header gap exposed. Verified: three-architecture boot (amd64, aarch64, riscv64), all reaching ok> with identical dict_hash=0x3d4e1daf289da94f matching the item-3.1 baseline, and the Stadium boot line confirmed present in all three serial logs (amd64: 74234 cells/4639 KB, aarch64: 161329 cells/10083 KB, riscv64: 76122 cells/4757 KB). Not built here, reported per §25.0 rule 3: per-VM free lists (§22.3) -- granted when Hera assigns quota, not this item's scope. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
143 lines
6.4 KiB
C
143 lines
6.4 KiB
C
/*
|
||
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.h - The Stadium cell and header (FABRIC.md §3, punch list item 3.1)
|
||
*
|
||
* A cell is one of exactly two things: a patron header, or a continuation
|
||
* cell owned by exactly one patron. The union is closed, two-valued, and
|
||
* fixed at build time -- not a type field. See FABRIC.md §3.
|
||
*/
|
||
|
||
#ifndef STARKERNEL_VM_STADIUM_H
|
||
#define STARKERNEL_VM_STADIUM_H
|
||
|
||
#ifdef __STARKERNEL__
|
||
|
||
#include <stddef.h>
|
||
#include <stdint.h>
|
||
#include "starforth_config.h" /* STADIUM_CONTAINS_DEPTH_MAX, STADIUM_CAPACITY_TICK, STADIUM_MEMORY_PERCENT */
|
||
|
||
#define STADIUM_CELL_BYTES 64
|
||
|
||
/*
|
||
* StadiumPatronHeader - one member of the closed two-valued cell union
|
||
* (FABRIC.md §3). Nine wires: identity, heat, TTL, pin (a bit in `flags`),
|
||
* link, code field (`behaviour`), mass, payload, contains. `flags` bit 0 is
|
||
* `pin`; the remaining bits are reserved. `behaviour` is the closed code-field
|
||
* enumeration (§18.3) -- not yet defined, item 3.3's scope.
|
||
*
|
||
* Field order is largest-to-smallest so natural C99 alignment adds zero
|
||
* padding: every offset below is already a multiple of that field's own
|
||
* alignment, and the struct's total size (64) is a multiple of its max
|
||
* alignment (8), so no compiler inserts trailing padding either. Do not
|
||
* reorder without re-checking this holds on all three ISAs.
|
||
*/
|
||
typedef struct {
|
||
uint64_t identity; /* offset 0 -- handle or name, never a content hash while resident (§24.4) */
|
||
uint64_t heat; /* offset 8 -- Q48.16, conserved share of 1.0 (§19.1) */
|
||
uint32_t ttl; /* offset 16 -- remaining lifetime; messages and ACLs only (§17.1) */
|
||
uint32_t link; /* offset 20 -- index into the Stadium, not a pointer */
|
||
uint32_t contains; /* offset 24 -- index of the patron held inside this one, or none (item 1.1).
|
||
* Chains up to STADIUM_CONTAINS_DEPTH_MAX deep; reap-gating
|
||
* enforcement of that bound is item 3.5's scope, not this one's. */
|
||
uint16_t mass; /* offset 28 -- cells this patron occupies (§19.2) */
|
||
uint8_t flags; /* offset 30 -- bit 0 = pin; remaining bits reserved */
|
||
uint8_t behaviour; /* offset 31 -- code field, closed enumeration (§18.3) */
|
||
uint8_t payload[32]; /* offset 32 -- inline payload, used when mass == 1 */
|
||
} StadiumPatronHeader;
|
||
|
||
/*
|
||
* StadiumContinuationCell - the other member of the union. Owned by exactly
|
||
* one patron header, chained by `next`. Never ranked, never reaped, never
|
||
* dispatched (§3) -- pure floor space, accounted for in its owner's mass.
|
||
*/
|
||
typedef struct {
|
||
uint32_t next; /* offset 0 -- index of the next continuation cell, or none */
|
||
uint8_t payload[60]; /* offset 4 */
|
||
} StadiumContinuationCell;
|
||
|
||
/*
|
||
* StadiumCell - the closed two-valued union itself (§3). Which member is
|
||
* valid for a given array slot is NOT stored in the cell -- FABRIC.md's item
|
||
* 3.1 amendment to §3 rules this an external side bitmap, one bit per cell,
|
||
* kept outside the cell array. Declared here as the indexing contract this
|
||
* type expects; item 3.2 (boot-time allocation) allocates the bitmap itself.
|
||
*/
|
||
typedef union {
|
||
StadiumPatronHeader header;
|
||
StadiumContinuationCell continuation;
|
||
} StadiumCell;
|
||
|
||
/* C99-portable compile-time size assertions (no _Static_assert -- that's C11). */
|
||
typedef char stadium_header_size_check[(sizeof(StadiumPatronHeader) == STADIUM_CELL_BYTES) ? 1 : -1];
|
||
typedef char stadium_continuation_size_check[(sizeof(StadiumContinuationCell) == STADIUM_CELL_BYTES) ? 1 : -1];
|
||
typedef char stadium_cell_size_check[(sizeof(StadiumCell) == STADIUM_CELL_BYTES) ? 1 : -1];
|
||
|
||
/*
|
||
* Items 1.1 and 1.4 named this item as where their Kconfig symbols would be
|
||
* implemented. Neither has a consumer yet (item 3.5 for the depth cap,
|
||
* capacity arbitration -- not yet on the punch list -- for the tick); these
|
||
* checks only prove the symbols are defined and sane, the same discipline
|
||
* already applied to the byte-count checks above.
|
||
*/
|
||
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];
|
||
|
||
/*
|
||
* 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
|
||
* at boot -- STADIUM_MEMORY_PERCENT of pmm_get_stats().free_bytes at the
|
||
* point of the call, rounded down to whole STADIUM_CELL_BYTES cells -- rather
|
||
* than a hardcoded count. Also allocates the header/continuation discriminator
|
||
* bitmap item 3.1 declared but did not allocate: one bit per cell, bit set
|
||
* means the cell at that index is a patron header, clear means continuation
|
||
* or not yet in use. Both are kmalloc'd (freestanding kernel, no separate
|
||
* PMM-backed region needed for this) and explicitly zero-filled, since
|
||
* kmalloc does not zero.
|
||
*
|
||
* 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.
|
||
*/
|
||
int stadium_boot_init(void);
|
||
|
||
/* stadium_is_initialized - Whether stadium_boot_init() has succeeded. */
|
||
int stadium_is_initialized(void);
|
||
|
||
/* stadium_cell_count - Number of cells in the array, 0 if not initialized. */
|
||
size_t stadium_cell_count(void);
|
||
|
||
/* stadium_cells - Pointer to the cell array, NULL if not initialized. */
|
||
StadiumCell *stadium_cells(void);
|
||
|
||
/*
|
||
* stadium_header_bitmap - Pointer to the discriminator bitmap declared in
|
||
* item 3.1, NULL if not initialized. ceil(stadium_cell_count() / 8) bytes.
|
||
*/
|
||
uint8_t *stadium_header_bitmap(void);
|
||
|
||
#endif /* __STARKERNEL__ */
|
||
|
||
#endif /* STARKERNEL_VM_STADIUM_H */ |