Punch list §25 item 3.3 complete. StadiumBehaviour (stadium.h) enumerates exactly the four tags §18.3 already names -- MIGRATE, DELIVER, EXPIRE, COOL -- mapped from §17.1's patron table: blocks->MIGRATE, messages->DELIVER, ACLs->EXPIRE, words and VMs both->COOL. Nothing invented; the tag set and mapping were already in the document. stadium_dispatch(cell_index, behaviour) dispatches on the tag only, never asks what kind of patron departed. Handlers are stubs -- the real actions belong to subsystems not yet migrated onto the Stadium (Phase 4). Nothing calls stadium_dispatch() yet; item 3.5 is its first consumer. The switch is exhaustive with no default case, making §13's "closed enumeration, fixed at build time" a compiler-enforced property under this project's -Wall -Werror rather than just prose. Verified live: temporarily deleted the COOL case, rebuild failed with error: enumeration value 'STADIUM_BEHAVIOUR_COOL' not handled in switch [-Werror=switch], restored it, confirmed clean again. The header's behaviour field stays uint8_t, not the enum type itself, since C does not guarantee an enum's underlying type and that field's offset is load-bearing for item 3.1's validated 64-byte layout. Verified: three-architecture boot (amd64, aarch64, riscv64), all reaching ok> with identical dict_hash=0x3d4e1daf289da94f matching the item-3.2 baseline. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
183 lines
8.3 KiB
C
183 lines
8.3 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. Valid values are StadiumBehaviour (§18.3)
|
||
* tags cast to uint8_t -- kept as uint8_t rather than the enum type
|
||
* itself since C does not guarantee an enum's underlying type, and
|
||
* this field's offset is load-bearing for the 64-byte layout item
|
||
* 3.1 validated. */
|
||
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);
|
||
|
||
/*
|
||
* StadiumBehaviour - the closed code-field enumeration (FABRIC.md §13, §18.3).
|
||
* The engine dispatches on this tag and never asks a patron what kind it is
|
||
* -- §3's entire point. Two patrons may share a tag: a VM's tag is COOL, the
|
||
* same tag a word carries (§18.3). Mapped from §17.1's patron table:
|
||
*
|
||
* MIGRATE -- blocks: reap event is migration back to Artemis (§17.2)
|
||
* DELIVER -- messages: reap event is delivery
|
||
* EXPIRE -- ACLs: reap event is TTL expiry
|
||
* COOL -- words and VMs: reap event is cooling off the floor
|
||
*
|
||
* Closed and fixed at build time -- see stadium_dispatch()'s exhaustive
|
||
* switch for how the compiler enforces that.
|
||
*/
|
||
typedef enum {
|
||
STADIUM_BEHAVIOUR_MIGRATE = 0,
|
||
STADIUM_BEHAVIOUR_DELIVER,
|
||
STADIUM_BEHAVIOUR_EXPIRE,
|
||
STADIUM_BEHAVIOUR_COOL
|
||
} StadiumBehaviour;
|
||
|
||
/*
|
||
* stadium_dispatch - Calls the behaviour handler for a patron's code field.
|
||
* The engine calls this at reap and never asks what kind of patron departed
|
||
* (§3, §18.3) -- only cell_index and behaviour cross this boundary.
|
||
*
|
||
* Handlers are stubs today: the real migrate-to-Artemis / deliver / expire /
|
||
* cool actions belong to their own subsystems, which have not been migrated
|
||
* onto the Stadium yet (Phase 4, §25.5). Nothing calls stadium_dispatch()
|
||
* yet either -- that begins with item 3.5 (admission and eviction).
|
||
*
|
||
* @param cell_index Index into the Stadium of the patron header dispatching.
|
||
* @param behaviour Which of the closed tag set to invoke.
|
||
*/
|
||
void stadium_dispatch(size_t cell_index, StadiumBehaviour behaviour);
|
||
|
||
#endif /* __STARKERNEL__ */
|
||
|
||
#endif /* STARKERNEL_VM_STADIUM_H */ |