Adds SkHermesChannel: a channel is an index into a boot-time, stadium_max_vm_count()-sized table (same sizing pattern task 3.1 established for the switch table -- no separate numeric rule was ruled for this table, so task 3.1's bound is extended directly, flagged as such rather than restated as a new ruling). No name field, mirroring messaging.4th's own nameless CH-ARENA. The common channel (index 0) is created at boot and permanent. Hera subscribes explicitly in kernel_main.c (she is the one VM never born through capsule_birth_baby()); every other VM -- Tripod fleet and future WIREBIND identities alike -- subscribes inside capsule_birth_baby() itself, the single choke point every other birth already passes through. Inert: no publish, no dispatch, no ACK/NACK, no ACL hook (tasks 3.3, 3.6, 3.7). Verified live on all three architectures: channel table sized to 50/202/50 slots (matching switch-signal's own per-arch sizing), common-channel fleet self-test confirms all four Tripod members are members, and a synthetic create/subscribe/unsubscribe/ destroy round-trip against a private topic passes, including refusing to destroy the common channel. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
380 lines
18 KiB
C
380 lines
18 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.
|
||
|
||
*/
|
||
|
||
/**
|
||
* kernel_hermes.h - Kernel-resident Hermes: message and membership
|
||
* structures (FABRIC-3.6.md task 2.1, item 28; design: FABRIC-3.5.md
|
||
* SIII/SXXXIII/SXXXIV).
|
||
*
|
||
* Phase 2, task 2.1 ONLY: type definitions, wired to nothing, drawing no
|
||
* heat. No allocator, no send/deliver/reap logic, no registration
|
||
* anywhere -- those are tasks 2.2 onward, each its own commit. This file
|
||
* existing and compiling changes no VM's dictionary and no runtime
|
||
* behaviour; that is deliberate (FABRIC-3.5.md SXXII.4: Phase 2 structures
|
||
* come first and prove nothing until the allocator is built on top, SXL.4
|
||
* item 41).
|
||
*
|
||
* SkHermesMessage mirrors capsules/common/messaging.4th's live MSG-CELLS
|
||
* layout (9 cells: MSG-TYPE@/FROM@/TO@/PADDR@/PLEN@/STADIUM-CELL@/SEQ@/
|
||
* CH@/ORIG-TYPE@) field-for-field, per FABRIC-3.5.md SXXXIII.4 item 1 --
|
||
* "roughly half the file is accessors that become struct fields." The
|
||
* Stadium-cell field is the heat coupling itself: a message's heat is not
|
||
* a field of its own, it IS the Stadium cell it occupies (SXL.4's
|
||
* consumption model, SXXXIX.4's per-VM invariant) -- there is deliberately
|
||
* no separate heat field here to keep that single-source-of-truth.
|
||
*
|
||
* SkHermesMembership is the "one broadcast membership list" SXXXIII.4
|
||
* item 3 and SXXXIII.5 recommend in place of messaging.4th's 28-word
|
||
* channel abstraction (CH-REQUEST/ACCEPT/CONFIRM/CLOSE/MINT-ID and the
|
||
* CH-NEGOTIATING/OPEN/CLOSING state machine) -- traced to have exactly one
|
||
* live caller, CH-ADD-MBR, everything else channel-shaped is unexercised.
|
||
* Whether kernel-Hermes ever adds negotiation on top is item 27, an open
|
||
* Phase 3 ruling (FABRIC-3.6.md B1) -- this structure does not answer
|
||
* that question, it only holds a flat list, which is correct either way.
|
||
*/
|
||
|
||
#ifndef STARKERNEL_VM_KERNEL_HERMES_H
|
||
#define STARKERNEL_VM_KERNEL_HERMES_H
|
||
|
||
#ifdef __STARKERNEL__
|
||
|
||
#include <stddef.h>
|
||
#include <stdint.h>
|
||
#include "starkernel/vm_uuid.h" /* VMUuid */
|
||
#include "starkernel/q48_16.h" /* Q48_ONE */
|
||
|
||
/*
|
||
* SK_HERMES_MSG_MAX / SK_HERMES_MEMBER_MAX - sizing. Mirrors
|
||
* messaging.4th's own MSG-MAX (32) and MBR-MAX (64) as a starting point --
|
||
* kernel-Hermes is a single central pool rather than N per-VM arenas, so
|
||
* these may need revisiting once real traffic exists to size against. Not
|
||
* a ruling, just where the FORTH precedent already was.
|
||
*/
|
||
#define SK_HERMES_MSG_MAX 32
|
||
#define SK_HERMES_MEMBER_MAX 64
|
||
|
||
/*
|
||
* SK_HERMES_Q_SLOT - per-message admission heat, task 2.2 (item 28).
|
||
* messaging.4th:44-46 derives Q.SLOT as the reservoir remaining after
|
||
* COMMON-CH's own Q.1/3 floor, split across MSG-MAX + (CH-MAX-1) slots --
|
||
* a floor that exists to reserve heat for the one live channel object
|
||
* itself. Kernel-Hermes has no such object: SXXXIII.4 item 3 and
|
||
* SXXXIII.5 replace the channel abstraction with a flat membership list
|
||
* that carries no Stadium heat of its own, so there is nothing left for a
|
||
* floor to protect. Deliberately simpler here rather than carrying the
|
||
* old formula's now-unmotivated term forward: reservoir split evenly
|
||
* across message slots only.
|
||
*/
|
||
#define SK_HERMES_Q_SLOT ((uint64_t)Q48_ONE / SK_HERMES_MSG_MAX)
|
||
|
||
/*
|
||
* SkHermesMessage - one message slot, field-for-field mirror of
|
||
* messaging.4th's 9-cell MSG layout.
|
||
*
|
||
* @field type Message type code (SPAWN/PAUSE/RESUME/KILL-style
|
||
* codes are Category A/dead per task 0.1/0.4; live
|
||
* types today are CONSOLE-CMD-EVENT(7),
|
||
* ELEVATE-REQUEST(8), BLK-ATTACH-EVENT(9), messaging.4th
|
||
* reserved sentinels MSG-NACKED(253)/MSG-DELIVERED(255)).
|
||
* @field from Sending VM (mirrors MSG-FROM@).
|
||
* @field to Target VM (mirrors MSG-TO@).
|
||
* @field payload_addr Out-of-line payload address (mirrors MSG-PADDR@).
|
||
* FABRIC-3.5.md SXLIII.6.1 (item 44, still open): a
|
||
* payload above INPUT_BUFFER_SIZE-1 (1024) bytes cannot
|
||
* be drained in one interpret call -- bound or chunk it
|
||
* before Phase 3, not here.
|
||
* @field payload_len Payload length in bytes (mirrors MSG-PLEN@).
|
||
* @field stadium_cell Index into the Stadium cell array this message's
|
||
* heat currently occupies, or a sentinel meaning "none"
|
||
* (mirrors MSG-STADIUM-CELL@) -- the heat coupling
|
||
* itself; see this file's own top comment.
|
||
* @field seq Monotonic send sequence (mirrors MSG-SEQ@).
|
||
* @field channel Broadcast/channel marker; unused today (mirrors
|
||
* MSG-CH@) -- item 27 territory, not decided here.
|
||
* @field orig_type Original type before a NACK/redeliver rewrite
|
||
* (mirrors MSG-ORIG-TYPE@).
|
||
* @field in_use Free-list occupancy flag for task 2.2's allocator.
|
||
* Not present in the FORTH layout (which uses
|
||
* MSG-TYPE@ 0<> as its own live/free test) -- kept
|
||
* explicit here rather than overloading `type == 0`,
|
||
* since kernel-Hermes's held/pulled/returned/consumed
|
||
* ledger (task 2.4, SXL.4) needs an unambiguous
|
||
* occupancy bit independent of the type field's value.
|
||
*/
|
||
typedef struct {
|
||
uint32_t type;
|
||
VMUuid from;
|
||
VMUuid to;
|
||
void *payload_addr;
|
||
uint32_t payload_len;
|
||
int32_t stadium_cell;
|
||
uint32_t seq;
|
||
uint32_t channel;
|
||
uint32_t orig_type;
|
||
int in_use;
|
||
VMUuid owner; /* VM whose reservoir funded this message (task 2.7) */
|
||
} SkHermesMessage;
|
||
|
||
/*
|
||
* SkHermesMembership - one flat broadcast membership list: every VM that
|
||
* has joined, no per-member state beyond identity. Replaces the 28-word
|
||
* channel abstraction; see this file's own top comment for why.
|
||
*
|
||
* @field members Member VM identities, valid for indices < count.
|
||
* @field count Number of valid entries in members[].
|
||
*/
|
||
typedef struct {
|
||
VMUuid members[SK_HERMES_MEMBER_MAX];
|
||
size_t count;
|
||
} SkHermesMembership;
|
||
|
||
/*
|
||
* sk_hermes_alloc - Heat-coupled allocate (task 2.2, item 28): pull
|
||
* SK_HERMES_Q_SLOT from vm_id's own Stadium reservoir, admit a real
|
||
* Stadium-floor patron with that heat (behaviour DELIVER, matching
|
||
* messaging.4th's own `SB-DELIVER STADIUM-ADMIT`), and claim a free
|
||
* message slot recording the admitted cell. Refuses cleanly, rolling
|
||
* back anything already pulled/admitted, if reservoir, arena, or the
|
||
* Stadium floor itself refuses.
|
||
*
|
||
* CORRECTED in task 2.3 (see this file's .c counterpart's own top
|
||
* comment): the first cut of this function never admitted a real
|
||
* Stadium patron, which left held message heat invisible to SXL.4's
|
||
* conservation invariant while allocated. It now does, which is what
|
||
* makes sk_hermes_release()'s eviction meaningful.
|
||
*
|
||
* Wired to nothing outside this file's own self-test (kernel_main.c) as
|
||
* of task 2.2/2.3 -- no FORTH word, no capsule interaction, no protocol
|
||
* logic (send/deliver/reap are later tasks). Exercised only by a
|
||
* synthetic-VM self-test; does not change any real VM's dictionary.
|
||
*
|
||
* @param vm_id Caller whose reservoir is charged.
|
||
* @param out_msg On success, set to the claimed slot. Untouched on
|
||
* refusal.
|
||
* @return 0 on success, -1 on refusal (insufficient reservoir, no free
|
||
* slot, or the Stadium floor itself refused admission -- this
|
||
* function does not distinguish the three in the return value;
|
||
* all three leave all state exactly as it was).
|
||
*/
|
||
int sk_hermes_alloc(VMUuid vm_id, SkHermesMessage **out_msg);
|
||
|
||
/*
|
||
* sk_hermes_release - Return a message's heat via the Stadium eviction
|
||
* path (task 2.3, item 28), mirroring MSG-FREE-NODE
|
||
* ("DUP 5 CELLS + @ STADIUM-EVICT DROP"). stadium_evict() itself returns
|
||
* the departing patron's remaining heat to its owning VM's reservoir --
|
||
* this function does not touch the reservoir directly, matching the
|
||
* FORTH shape exactly. Clears the slot (in_use = 0) whether or not
|
||
* eviction succeeds, since a message this function was asked to release
|
||
* should not remain allocated either way.
|
||
*
|
||
* @param msg A slot previously returned by sk_hermes_alloc(). Refused
|
||
* (returns -1, no effect) if NULL or already released.
|
||
* @return 0 on successful eviction, -1 if msg was invalid or eviction
|
||
* itself was refused by the Stadium floor.
|
||
*/
|
||
int sk_hermes_release(SkHermesMessage *msg);
|
||
|
||
/*
|
||
* sk_hermes_ledger - Task 2.4 (item 28), the four counters FABRIC-3.5.md
|
||
* SXXXVII.3/SXL.4 name: held, pulled, returned, consumed. Each is touched
|
||
* at exactly one call site:
|
||
*
|
||
* held += pulled amount -- sk_hermes_alloc(), on success only
|
||
* held -= returned amount -- sk_hermes_release(), on success only
|
||
* pulled += pulled amount -- sk_hermes_alloc(), same site as held's
|
||
* returned += returned amount -- sk_hermes_release(), same site as held's
|
||
* held -= decay delta -- sk_hermes_decay(), same site as consumed's
|
||
* consumed += decay delta -- sk_hermes_decay() (task 2.5)
|
||
*
|
||
* The audit invariant this ledger exists to make checkable (task 2.6,
|
||
* epsilon zero): held == pulled - returned - consumed. All four are
|
||
* exact integers (SXXXVII.3: "Nothing here is a measurement. There is no
|
||
* noise to tolerate.") -- this accessor is how task 2.6's audit, task
|
||
* 2.7's Stage B proof, and task 2.8's scan cross-check all read the same
|
||
* four numbers, rather than each keeping its own copy.
|
||
*
|
||
* @param held Set to the current live total (may be NULL).
|
||
* @param pulled Set to the cumulative total ever pulled (may be NULL).
|
||
* @param returned Set to the cumulative total ever returned (may be
|
||
* NULL).
|
||
* @param consumed Set to the cumulative total ever consumed by decay
|
||
* (may be NULL).
|
||
*/
|
||
void sk_hermes_ledger(uint64_t *held, uint64_t *pulled, uint64_t *returned, uint64_t *consumed);
|
||
|
||
/*
|
||
* SK_HERMES_Q_DECAY - per-application decay factor, Q48.16. Identical to
|
||
* messaging.4th's `65208 CONSTANT Q-DECAY` (65208/65536 ~= 0.99499):
|
||
* FABRIC-3.5.md SXL.4 rules that the consumption economy is preserved
|
||
* exactly, not re-tuned.
|
||
*/
|
||
#define SK_HERMES_Q_DECAY ((uint64_t)65208)
|
||
|
||
/*
|
||
* sk_hermes_decay - Apply one decay step to a live message (task 2.5,
|
||
* item 28), mirroring MSG-COOL-ONE (`MSG-HEAT@ Q-DECAY Q.* MSG-HEAT!`):
|
||
* the message's Stadium-cell heat becomes q48_mul(heat, Q_DECAY). Unlike
|
||
* MSG-COOL-ONE, the destroyed difference is RECORDED (SXXXVII.3): the
|
||
* delta heat_before - heat_after is added to `consumed` and subtracted
|
||
* from `held`, so held == pulled - returned - consumed stays exact.
|
||
*
|
||
* @param msg A live slot from sk_hermes_alloc(). Refused (returns -1, no
|
||
* effect) if NULL, not in use, or holding no Stadium cell.
|
||
* @return 0 on success, -1 if refused.
|
||
*/
|
||
int sk_hermes_decay(SkHermesMessage *msg);
|
||
|
||
/*
|
||
* Task 2.6 (item 28): the self-audit, epsilon zero (SXXXVII.3).
|
||
*
|
||
* sk_hermes_audit_values - pure predicate: nonzero iff
|
||
* held == pulled - returned - consumed exactly. Separate from the live
|
||
* ledger so the check can be exercised with deliberately corrupted values
|
||
* without mutating real state.
|
||
*
|
||
* sk_hermes_audit - checks the live ledger (O(1), SXXXVII.4); on failure
|
||
* prints a console line and bumps a failure count. Called at the end of
|
||
* every successful mutation: alloc, release, decay.
|
||
*
|
||
* sk_hermes_audit_failure_count - cumulative failures seen by the live
|
||
* audit; must be 0 in a healthy kernel.
|
||
*/
|
||
int sk_hermes_audit_values(uint64_t held, uint64_t pulled, uint64_t returned, uint64_t consumed);
|
||
int sk_hermes_audit(void);
|
||
uint64_t sk_hermes_audit_failure_count(void);
|
||
|
||
/*
|
||
* Task 2.8 (item 28), SXXXVII.4: the scan that verifies the counters
|
||
* themselves. DIAGNOSTIC ONLY -- O(SK_HERMES_MSG_MAX), never called from
|
||
* alloc/release/decay.
|
||
*
|
||
* sk_hermes_scan_held - walks the message arena and sums the live Stadium
|
||
* cell heat of every in-use message (the ground truth `held` claims to
|
||
* track). Sets *live_count (may be NULL) to the messages counted.
|
||
*
|
||
* sk_hermes_scan_check - nonzero iff the scan sum equals the `held`
|
||
* counter exactly.
|
||
*/
|
||
uint64_t sk_hermes_scan_held(size_t *live_count);
|
||
int sk_hermes_scan_check(void);
|
||
|
||
/*
|
||
* Channel table (FABRIC-3.6.md task 3.2, B1 / FABRIC-3.5.md SXLV.1): B1
|
||
* overrules SXXXIII.5's single flat broadcast list -- messaging is
|
||
* publish/subscribe, one permanent common channel every VM joins at
|
||
* birth, private channels created by request/grant/deny (task 3.6, not
|
||
* this one). SkHermesMembership (task 2.1) becomes per-channel: one
|
||
* instance per SkHermesChannel table entry instead of one global list.
|
||
*
|
||
* INERT, same posture as task 2.1: this task wires channel existence and
|
||
* membership bookkeeping only. No publish, no dispatch, no ACK/NACK, no
|
||
* ACL hook (tasks 3.3, 3.6, 3.7) -- creating/destroying/subscribing a
|
||
* channel here changes no VM's dictionary and delivers no message.
|
||
*
|
||
* Sizing: SXLV.1 says the channel table has "no fixed channel maximum,
|
||
* same reasoning as SXLV.2" -- SXLV.2/task 3.1's own ruling is boot-time,
|
||
* RAM-derived sizing (Stadium's stadium_max_vm_count_val pattern), not a
|
||
* literal unbounded/growable table. No separate numeric sizing rule was
|
||
* ruled for the channel table specifically (task 3.0's five sub-items
|
||
* covered ACK cadence/ACL-hook-location/switch-table-sizing/chunk-
|
||
* framing/drain-cadence, not this). Extending task 3.1's already-ruled
|
||
* pattern directly -- same stadium_max_vm_count() bound, same
|
||
* kmalloc-at-boot shape -- is the smallest choice consistent with what
|
||
* was ruled, flagged here as an engineering extrapolation, not restated
|
||
* as a separate Captain Bob ruling.
|
||
*/
|
||
|
||
/* SK_HERMES_CHANNEL_COMMON - the permanent common channel's fixed index.
|
||
* Exists (in_use, empty membership) from sk_hermes_channels_boot_init()
|
||
* itself, before any VM is born -- every VM joins it at birth (task 3.2's
|
||
* own kernel_main.c/capsule_birth.c wiring), never destroyed. */
|
||
#define SK_HERMES_CHANNEL_COMMON 0
|
||
|
||
/*
|
||
* SkHermesChannel - one channel/topic: its membership plus an occupancy
|
||
* flag for the dynamic table below. No name field -- messaging.4th's own
|
||
* channel abstraction (CH-ARENA) has none either; a channel is identified
|
||
* by its table index, the same way a Stadium quota slot or a switch-
|
||
* signal slot is identified by index, not by string.
|
||
*/
|
||
typedef struct {
|
||
SkHermesMembership membership;
|
||
int in_use;
|
||
} SkHermesChannel;
|
||
|
||
/* Boot-time allocation: kmalloc's the channel table to
|
||
* stadium_max_vm_count() entries (see this section's own sizing note
|
||
* above) and creates the common channel (index SK_HERMES_CHANNEL_COMMON,
|
||
* in_use, empty membership -- members join at birth, not pre-populated
|
||
* here). Must run after stadium_boot_init() (that bound is 0, and this
|
||
* fails, until Stadium has computed it). Soft failure -- returns -1 and
|
||
* leaves the table unallocated (capacity 0, so every call below simply
|
||
* refuses) rather than halting boot, same posture as
|
||
* stadium_boot_init()/session_boot_init()/sk_vm_switch_signal_boot_init().
|
||
* Idempotent-unsafe: calling twice leaks the first allocation, so callers
|
||
* must call it exactly once. */
|
||
int sk_hermes_channels_boot_init(void);
|
||
|
||
/* sk_hermes_channel_create - allocate a new, empty, inert channel.
|
||
* Returns its table index, or -1 if the table is full or
|
||
* sk_hermes_channels_boot_init() was never called/failed. */
|
||
int sk_hermes_channel_create(void);
|
||
|
||
/* sk_hermes_channel_destroy - tear down a channel created by
|
||
* sk_hermes_channel_create(). Refuses (-1, no effect) if channel_id is
|
||
* SK_HERMES_CHANNEL_COMMON (the common channel is permanent, SXLV.1),
|
||
* out of range, or not in use. Clears membership. */
|
||
int sk_hermes_channel_destroy(int channel_id);
|
||
|
||
/* sk_hermes_channel_subscribe - add vm_id to channel_id's membership.
|
||
* Refuses (-1, no effect) if channel_id is invalid/not in use, vm_id is
|
||
* already a member, or the channel's membership is already at
|
||
* SK_HERMES_MEMBER_MAX. Idempotent in effect (a second call with the
|
||
* same args refuses rather than duplicating), not in return value. */
|
||
int sk_hermes_channel_subscribe(int channel_id, VMUuid vm_id);
|
||
|
||
/* sk_hermes_channel_unsubscribe - remove vm_id from channel_id's
|
||
* membership (compacts the list, same shape as
|
||
* sk_vm_switch_signal_unregister()). Refuses (-1, no effect) if
|
||
* channel_id is invalid/not in use or vm_id is not a member. */
|
||
int sk_hermes_channel_unsubscribe(int channel_id, VMUuid vm_id);
|
||
|
||
/* sk_hermes_channel_is_member - nonzero iff vm_id is currently a member
|
||
* of channel_id. Zero (not an error signal) if channel_id is invalid/not
|
||
* in use. */
|
||
int sk_hermes_channel_is_member(int channel_id, VMUuid vm_id);
|
||
|
||
/* sk_hermes_channel_member_count - current membership size of channel_id,
|
||
* or -1 if channel_id is invalid/not in use. */
|
||
int sk_hermes_channel_member_count(int channel_id);
|
||
|
||
/* sk_hermes_channel_capacity - the table's boot-time-computed capacity
|
||
* (0 if sk_hermes_channels_boot_init() was never called or failed) --
|
||
* DoE/test observability, mirrors sk_vm_switch_signal_slot_capacity(). */
|
||
int sk_hermes_channel_capacity(void);
|
||
|
||
#endif /* __STARKERNEL__ */
|
||
|
||
#endif /* STARKERNEL_VM_KERNEL_HERMES_H */
|