Add sk_hermes_alloc(), the heat-coupled allocator -- FABRIC-3.6.md task 2.2, item 28
The piece FABRIC-3.5.md SXXXIII.6 calls "what remains genuinely hard,"
built and proven first per its own recommendation. Added
src/starkernel/vm/kernel_hermes.c (wired into Makefile.starkernel's
LOADER_EXTRA_SRCS -- this repo lists vm/*.c files explicitly, no glob)
and sk_hermes_alloc()'s declaration in kernel_hermes.h.
Checks stadium_reservoir_peek(vm_id) >= SK_HERMES_Q_SLOT before
touching the reservoir at all -- refusal this way needs no rollback,
since nothing was pulled -- with an explicit rollback path
(stadium_reservoir_push) kept defensively for the pull-then-short case,
though nothing in this single-core kernel is expected to reach it.
SK_HERMES_Q_SLOT = Q48_ONE / SK_HERMES_MSG_MAX (2048), deliberately
simpler than messaging.4th's own formula, which reserves a Q.1/3 floor
for COMMON-CH's own Stadium heat -- kernel-Hermes has no such object
(SXXXIII.4/SXXXIII.5's flat membership list carries no heat of its
own), so there is nothing left for that floor to protect.
Self-test in kernel_main.c, same diagnostic-only synthetic-VM pattern
as the existing Stadium quota grant self-test (lo=3, distinct from
that test's lo=1): reads back the actual granted reservoir rather than
assuming a number, derives expected_n from it, allocates to refusal,
and checks the refusal lands at exactly expected_n, the reservoir
doesn't move on the refused attempt (rollback proven, not assumed),
and the final reservoir is exactly reservoir0 minus got_n times
Q_SLOT.
Three-arch boot clean: amd64/aarch64/riscv64 all reach [zuse@Hera] ok>,
zero UNKNOWN WORD, dict_hash unmoved from task 2.1 (pure C, no FORTH
touched). All three print identical self-test arithmetic: reservoir0=
65536 Q_SLOT=2048 expected_n=32 got_n=32 reservoir_after=0. No compiler
warnings.
Noted, not fixed: Q_SLOT's divisor and SK_HERMES_MSG_MAX are the same
32, so reservoir and arena exhaustion land at exactly the same count by
construction -- this test can't distinguish which refusal reason
fired, only that refusal is correct and rolls back correctly.
Deliberately not evidence for stadium_conserved(): allocating alone
(no release yet, task 2.3) leaves pulled heat held off the Stadium
floor, so the two-term check would correctly read false right now if
run mid-hold. That's expected, not a bug -- Stage B (task 2.7) is
defined as "before and after the alloc/free cycle," not "continuously
during." This task's self-test checks reservoir arithmetic directly
instead.
Authorized by Captain Bob ("Yes continue").
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
f10fa7ae83
commit
9d129fdb1c
+44
-1
@@ -506,8 +506,51 @@ Hestia; headless policy intact.
|
|||||||
in a later task. Item 27 (channel negotiation vs. broadcast, Phase 3 blocker B1) is not
|
in a later task. Item 27 (channel negotiation vs. broadcast, Phase 3 blocker B1) is not
|
||||||
answered by this structure and isn't meant to be — a flat membership list is correct either
|
answered by this structure and isn't meant to be — a flat membership list is correct either
|
||||||
way; the negotiation question is about behaviour built on top, not this shape.
|
way; the negotiation question is about behaviour built on top, not this shape.
|
||||||
- [ ] **2.2** — Allocate: pull `Q.SLOT` from the caller's reservoir; roll back on refusal.
|
- [x] **2.2** — Allocate: pull `Q.SLOT` from the caller's reservoir; roll back on refusal.
|
||||||
*Check:* N allocs against a known reservoir; refusal at the right count.
|
*Check:* N allocs against a known reservoir; refusal at the right count.
|
||||||
|
2026-09-19 · `logs/20260919-205534/amd64/`, `logs/20260919-205645/aarch64/`,
|
||||||
|
`logs/20260919-205817/riscv64/` — all three reach `[zuse@Hera] ok>`, zero `UNKNOWN WORD`,
|
||||||
|
`dict_hash` triple unmoved from task 2.1's baseline (pure C, no FORTH touched). All three
|
||||||
|
print `Kernel-Hermes alloc self-test: PASS` with **identical arithmetic**:
|
||||||
|
`reservoir0=65536 Q_SLOT=2048 expected_n=32 got_n=32 reservoir_after=0`.
|
||||||
|
|
||||||
|
Added `sk_hermes_alloc(VMUuid, SkHermesMessage**)` (`src/starkernel/vm/kernel_hermes.c`,
|
||||||
|
new file, wired into `Makefile.starkernel`'s `LOADER_EXTRA_SRCS` list since this repo lists
|
||||||
|
`vm/*.c` files explicitly rather than globbing). Checks
|
||||||
|
`stadium_reservoir_peek(vm_id) >= SK_HERMES_Q_SLOT` **before** touching the reservoir at
|
||||||
|
all — refusal this way needs no rollback, since nothing was pulled — with an explicit
|
||||||
|
rollback path (`stadium_reservoir_push`) kept for the pull-then-short case defensively,
|
||||||
|
though nothing in this single-core kernel is expected to reach it. `SK_HERMES_Q_SLOT`
|
||||||
|
defined as `Q48_ONE / SK_HERMES_MSG_MAX` (2048) — **deliberately simpler than
|
||||||
|
`messaging.4th`'s own formula**, which reserves a `Q.1/3` floor for `COMMON-CH`'s own
|
||||||
|
Stadium heat; kernel-Hermes has no such object (`SXXXIII.4`/`SXXXIII.5`'s flat membership
|
||||||
|
list carries no heat of its own), so there is nothing left for that floor to protect.
|
||||||
|
|
||||||
|
**Self-test, not a FORTH-visible check** (matching the existing `Stadium quota grant
|
||||||
|
self-test` pattern already in `kernel_main.c`): mints a second synthetic VM
|
||||||
|
(`lo=3`, distinct from the existing self-test's `lo=1`) via `stadium_grant_quota()`,
|
||||||
|
reads back its actual granted reservoir (always a fresh `Q48_ONE` per
|
||||||
|
`stadium_grant_quota()`'s own code — not assumed), derives `expected_n` from it rather
|
||||||
|
than hardcoding 32, allocates until refusal, and checks **all three** of: the refusal
|
||||||
|
lands at exactly `expected_n`, the reservoir doesn't move on the refused attempt (rollback
|
||||||
|
proven, not just assumed), and the final reservoir equals `reservoir0 − got_n × Q_SLOT`
|
||||||
|
exactly.
|
||||||
|
|
||||||
|
**Noted, not fixed:** `SK_HERMES_Q_SLOT = Q48_ONE / SK_HERMES_MSG_MAX` and
|
||||||
|
`SK_HERMES_MSG_MAX = 32` together mean reservoir exhaustion and arena exhaustion land at
|
||||||
|
*exactly* the same count by construction — this test cannot distinguish which refusal
|
||||||
|
reason fired, only that refusal fires at the right count and rolls back correctly. Not a
|
||||||
|
defect at this stage (nothing yet needs the arena to outlive the reservoir), but worth
|
||||||
|
remembering if `SK_HERMES_MSG_MAX` is ever resized independently of `Q_SLOT`'s divisor.
|
||||||
|
|
||||||
|
**Deliberately not evidence for `stadium_conserved()`** — per the watch-list raised before
|
||||||
|
starting Phase 2: allocating alone (no release yet, that's task 2.3) leaves pulled heat
|
||||||
|
held by kernel-Hermes, off the Stadium floor entirely, so the two-term
|
||||||
|
`stadium_resident_sum + reservoir == Q48_ONE` check would correctly read **false** right
|
||||||
|
now if run mid-hold — that is expected, not a bug, and is exactly why Stage B (task 2.7) is
|
||||||
|
defined as "before and after the alloc/free cycle," not "continuously during." This task's
|
||||||
|
self-test checks reservoir arithmetic directly instead, which is the right instrument for
|
||||||
|
what task 2.2 alone claims.
|
||||||
- [ ] **2.3** — Release: return remaining heat via the eviction path. *Check:* reservoir
|
- [ ] **2.3** — Release: return remaining heat via the eviction path. *Check:* reservoir
|
||||||
restored exactly for an undecayed message.
|
restored exactly for an undecayed message.
|
||||||
- [ ] **2.4** — The four counters: `held`, `pulled`, `returned`, `consumed` (§XL.4). *Check:*
|
- [ ] **2.4** — The four counters: `held`, `pulled`, `returned`, `consumed` (§XL.4). *Check:*
|
||||||
|
|||||||
+2
-1
@@ -552,7 +552,8 @@ LOADER_EXTRA_SRCS := \
|
|||||||
$(KERNEL_SRC)/vm/stadium.c \
|
$(KERNEL_SRC)/vm/stadium.c \
|
||||||
$(KERNEL_SRC)/vm/stadium_words.c \
|
$(KERNEL_SRC)/vm/stadium_words.c \
|
||||||
$(KERNEL_SRC)/vm/stadium_blocks.c \
|
$(KERNEL_SRC)/vm/stadium_blocks.c \
|
||||||
$(KERNEL_SRC)/vm/session.c
|
$(KERNEL_SRC)/vm/session.c \
|
||||||
|
$(KERNEL_SRC)/vm/kernel_hermes.c
|
||||||
|
|
||||||
KERNEL_EXTRA_SRCS := $(LOADER_EXTRA_SRCS)
|
KERNEL_EXTRA_SRCS := $(LOADER_EXTRA_SRCS)
|
||||||
|
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
# Capsule Block Manifest — Auto-generated
|
# Capsule Block Manifest — Auto-generated
|
||||||
<!-- Generated by mkcapsule --manifest 2026-09-20T00:46:42Z -->
|
<!-- Generated by mkcapsule --manifest 2026-09-20T00:58:14Z -->
|
||||||
<!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. -->
|
<!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. -->
|
||||||
<!-- Hand-written justifications and immutability notes live -->
|
<!-- Hand-written justifications and immutability notes live -->
|
||||||
<!-- in MANIFEST.md alongside this auto-generated index. -->
|
<!-- in MANIFEST.md alongside this auto-generated index. -->
|
||||||
|
|||||||
@@ -61,18 +61,32 @@
|
|||||||
#include <stddef.h>
|
#include <stddef.h>
|
||||||
#include <stdint.h>
|
#include <stdint.h>
|
||||||
#include "starkernel/vm_uuid.h" /* VMUuid */
|
#include "starkernel/vm_uuid.h" /* VMUuid */
|
||||||
|
#include "starkernel/q48_16.h" /* Q48_ONE */
|
||||||
|
|
||||||
/*
|
/*
|
||||||
* SK_HERMES_MSG_MAX / SK_HERMES_MEMBER_MAX - sizing only, not yet load-
|
* SK_HERMES_MSG_MAX / SK_HERMES_MEMBER_MAX - sizing. Mirrors
|
||||||
* bearing (nothing allocates against these until task 2.2). Mirrors
|
|
||||||
* messaging.4th's own MSG-MAX (32) and MBR-MAX (64) as a starting point --
|
* 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
|
* kernel-Hermes is a single central pool rather than N per-VM arenas, so
|
||||||
* these may need revisiting once task 2.2's allocator has real traffic to
|
* these may need revisiting once real traffic exists to size against. Not
|
||||||
* size against. Not a ruling, just where the FORTH precedent already was.
|
* a ruling, just where the FORTH precedent already was.
|
||||||
*/
|
*/
|
||||||
#define SK_HERMES_MSG_MAX 32
|
#define SK_HERMES_MSG_MAX 32
|
||||||
#define SK_HERMES_MEMBER_MAX 64
|
#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
|
* SkHermesMessage - one message slot, field-for-field mirror of
|
||||||
* messaging.4th's 9-cell MSG layout.
|
* messaging.4th's 9-cell MSG layout.
|
||||||
@@ -133,6 +147,30 @@ typedef struct {
|
|||||||
size_t count;
|
size_t count;
|
||||||
} SkHermesMembership;
|
} SkHermesMembership;
|
||||||
|
|
||||||
|
/*
|
||||||
|
* sk_hermes_alloc - Heat-coupled allocate (task 2.2, item 28): pull
|
||||||
|
* SK_HERMES_Q_SLOT from vm_id's own Stadium reservoir and claim a free
|
||||||
|
* message slot. Refuses cleanly, touching neither the reservoir nor the
|
||||||
|
* arena, if either is unavailable -- "roll back on refusal" is satisfied
|
||||||
|
* by never pulling until affordability is confirmed, not by pulling then
|
||||||
|
* undoing (though the rollback path exists too, for the pull-then-fail
|
||||||
|
* case the check-first ordering is not expected to reach).
|
||||||
|
*
|
||||||
|
* Wired to nothing outside this file's own self-test (kernel_main.c) as
|
||||||
|
* of task 2.2 -- no FORTH word, no capsule interaction, no protocol logic
|
||||||
|
* (send/deliver/reap are later tasks). This function existing and being
|
||||||
|
* exercised by a synthetic-VM self-test does not change any real VM's
|
||||||
|
* dictionary or Stadium state.
|
||||||
|
*
|
||||||
|
* @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 or no free
|
||||||
|
* slot -- task 2.2 does not distinguish the two in the return
|
||||||
|
* value; both leave all state exactly as it was).
|
||||||
|
*/
|
||||||
|
int sk_hermes_alloc(VMUuid vm_id, SkHermesMessage **out_msg);
|
||||||
|
|
||||||
#endif /* __STARKERNEL__ */
|
#endif /* __STARKERNEL__ */
|
||||||
|
|
||||||
#endif /* STARKERNEL_VM_KERNEL_HERMES_H */
|
#endif /* STARKERNEL_VM_KERNEL_HERMES_H */
|
||||||
|
|||||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@@ -58,6 +58,7 @@ EFI_RUNTIME_SERVICES *g_sk_runtime_services = NULL;
|
|||||||
#include "starkernel/vm/stadium.h"
|
#include "starkernel/vm/stadium.h"
|
||||||
#include "starkernel/vm/stadium_words.h"
|
#include "starkernel/vm/stadium_words.h"
|
||||||
#include "starkernel/vm/stadium_blocks.h"
|
#include "starkernel/vm/stadium_blocks.h"
|
||||||
|
#include "starkernel/vm/kernel_hermes.h"
|
||||||
#include "starkernel/session.h"
|
#include "starkernel/session.h"
|
||||||
#include "starkernel/capsule_generated.h"
|
#include "starkernel/capsule_generated.h"
|
||||||
#include "starkernel/capsule_loader.h"
|
#include "starkernel/capsule_loader.h"
|
||||||
@@ -829,6 +830,52 @@ static void kernel_main_deep(BootInfo *boot_info) {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/* FABRIC-3.6.md task 2.2 (item 28) self-test: sk_hermes_alloc()'s
|
||||||
|
* heat-coupled allocate, against its own synthetic VM (lo=3, distinct
|
||||||
|
* from the lo=1 test-vm just above) -- same diagnostic-only reasoning
|
||||||
|
* as that block: never used for anything else, never perturbs the
|
||||||
|
* real birth pool. "Unit path: N allocs against a VM with known
|
||||||
|
* reservoir; refusal at the right count" -- reads the actual granted
|
||||||
|
* reservoir back (stadium_grant_quota() splits Hera's free cells, not
|
||||||
|
* a fixed Q48_ONE) rather than assuming a number, so N is derived,
|
||||||
|
* not hardcoded. */
|
||||||
|
{
|
||||||
|
VMUuid alloc_test_id;
|
||||||
|
alloc_test_id.hi = 0;
|
||||||
|
alloc_test_id.lo = 3;
|
||||||
|
int grant_rc = stadium_grant_quota(alloc_test_id, vm_uuid_hera());
|
||||||
|
console_puts("Kernel-Hermes alloc self-test: ");
|
||||||
|
if (grant_rc != 0) {
|
||||||
|
console_println("SKIPPED (quota grant failed)");
|
||||||
|
} else {
|
||||||
|
uint64_t reservoir0 = stadium_reservoir_peek(alloc_test_id);
|
||||||
|
uint64_t expected_n = reservoir0 / SK_HERMES_Q_SLOT;
|
||||||
|
uint64_t got_n = 0;
|
||||||
|
SkHermesMessage *msg;
|
||||||
|
int ok = 1;
|
||||||
|
|
||||||
|
while (sk_hermes_alloc(alloc_test_id, &msg) == 0) {
|
||||||
|
got_n++;
|
||||||
|
if (got_n > expected_n) { ok = 0; break; } /* over-allocated */
|
||||||
|
}
|
||||||
|
if (got_n != expected_n) ok = 0;
|
||||||
|
/* One more attempt past exhaustion must also refuse, and must
|
||||||
|
* not move the reservoir any further -- "roll back on
|
||||||
|
* refusal" verified, not just assumed. */
|
||||||
|
uint64_t reservoir_after_n = stadium_reservoir_peek(alloc_test_id);
|
||||||
|
if (sk_hermes_alloc(alloc_test_id, &msg) == 0) ok = 0;
|
||||||
|
if (stadium_reservoir_peek(alloc_test_id) != reservoir_after_n) ok = 0;
|
||||||
|
if (reservoir_after_n != reservoir0 - got_n * SK_HERMES_Q_SLOT) ok = 0;
|
||||||
|
|
||||||
|
console_println(ok ? "PASS" : "FAIL");
|
||||||
|
print_uint(" reservoir0=", reservoir0);
|
||||||
|
print_uint(" Q_SLOT=", SK_HERMES_Q_SLOT);
|
||||||
|
print_uint(" expected_n=", expected_n);
|
||||||
|
print_uint(" got_n=", got_n);
|
||||||
|
print_uint(" reservoir_after=", reservoir_after_n);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
/* FABRIC-3.md SXX (2026-09-12, supersedes the Phase C note this used to
|
/* FABRIC-3.md SXX (2026-09-12, supersedes the Phase C note this used to
|
||||||
* be): Hera now DOES get her own common:messaging.4th arena, like
|
* be): Hera now DOES get her own common:messaging.4th arena, like
|
||||||
* every other VM -- root-caused, not special-cased around. The real
|
* every other VM -- root-caused, not special-cased around. The real
|
||||||
|
|||||||
@@ -0,0 +1,75 @@
|
|||||||
|
/*
|
||||||
|
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.c - Kernel-resident Hermes: the heat-coupled allocator
|
||||||
|
* (FABRIC-3.6.md task 2.2, item 28).
|
||||||
|
*/
|
||||||
|
|
||||||
|
#ifdef __STARKERNEL__
|
||||||
|
|
||||||
|
#include <string.h>
|
||||||
|
#include "starkernel/vm/kernel_hermes.h"
|
||||||
|
#include "starkernel/vm/stadium.h"
|
||||||
|
|
||||||
|
static SkHermesMessage sk_hermes_msgs[SK_HERMES_MSG_MAX];
|
||||||
|
|
||||||
|
static int sk_hermes_find_free_slot(void) {
|
||||||
|
int i;
|
||||||
|
for (i = 0; i < SK_HERMES_MSG_MAX; i++) {
|
||||||
|
if (!sk_hermes_msgs[i].in_use) return i;
|
||||||
|
}
|
||||||
|
return -1;
|
||||||
|
}
|
||||||
|
|
||||||
|
int sk_hermes_alloc(VMUuid vm_id, SkHermesMessage **out_msg) {
|
||||||
|
int slot;
|
||||||
|
uint64_t pulled;
|
||||||
|
|
||||||
|
if (!out_msg) return -1;
|
||||||
|
|
||||||
|
/* Check affordability before touching the reservoir at all -- this is
|
||||||
|
* what "roll back on refusal" reduces to when the check happens
|
||||||
|
* first: there is nothing to roll back. */
|
||||||
|
if (stadium_reservoir_peek(vm_id) < SK_HERMES_Q_SLOT) return -1;
|
||||||
|
|
||||||
|
slot = sk_hermes_find_free_slot();
|
||||||
|
if (slot < 0) return -1; /* arena full, reservoir untouched */
|
||||||
|
|
||||||
|
pulled = stadium_reservoir_pull(vm_id, SK_HERMES_Q_SLOT);
|
||||||
|
if (pulled < SK_HERMES_Q_SLOT) {
|
||||||
|
/* Should not happen given the peek check above (nothing else runs
|
||||||
|
* between the two calls on this single-core, cooperative kernel),
|
||||||
|
* but roll back explicitly rather than trust that invariant
|
||||||
|
* silently. */
|
||||||
|
if (pulled > 0) stadium_reservoir_push(vm_id, pulled);
|
||||||
|
return -1;
|
||||||
|
}
|
||||||
|
|
||||||
|
memset(&sk_hermes_msgs[slot], 0, sizeof(SkHermesMessage));
|
||||||
|
sk_hermes_msgs[slot].in_use = 1;
|
||||||
|
*out_msg = &sk_hermes_msgs[slot];
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
#endif /* __STARKERNEL__ */
|
||||||
Reference in New Issue
Block a user