Drain at the outermost checkpoint -- FABRIC-3.6.md task 3.4

sk_hermes_drain_checkpoint() interprets one queued payload per checkpoint
(ruled: one message per checkpoint), reusing sk_vm_at_outermost_interpret()
and placed before the switch-signal block in vm_core.c's existing
cooperative checkpoint (sk_vm_context_switch() doesn't return until
switched back to, so drain must come first or it silently never runs on
a switching checkpoint).

Amends FABRIC-3.5.md SXLIII.5, caught by advisor() before writing the
naive version: "recursive drain is prevented for free" via
g_vm_interpret_depth is true but only for same-message re-drain -- it
doesn't cover the separate same-VM reentrancy hazard FABRIC-3.md SXX
already named for Hera specifically (VMCallState saves rsp/exit_colon/
ecw_nesting only, never input_buffer/input_length/input_pos). Draining
calls vm_interpret() on the same vm whose own vm_interpret() call is
still paused mid-word at the checkpoint; without saving and restoring
the cursor by hand, the enclosing REPL line or LOAD block would be
silently truncated. sk_hermes_drain_checkpoint() snapshots and restores
input_buffer/input_length/input_pos/mode/error/abort_requested around
the call. Not a divergence from the ruling -- cursor preservation is the
implementer's own obligation inside the ruled mechanism.

Gated behind a system-wide pending-total counter so the common
no-message-in-flight case costs one integer read per word dispatch, not
a stadium_max_vm_count()-sized queue scan (also flagged by advisor() as
a real hot-path cost, not deferred).

Verified live on all three architectures: a self-test publishes a real
payload to Hermes, proves the depth gate via VM-EXEC-ing an existing
harmless colon word into Hermes (genuine nested vm_interpret(), depth 2,
must not drain), then drains directly from genuinely-outermost context
and confirms exactly one clean drain. dict_hash unmoved and identical
across architectures.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
2026-09-22 01:27:11 -04:00
co-authored by Claude Sonnet 5
parent 1f6343bc03
commit 2b1ba031a5
9 changed files with 28050 additions and 1 deletions
+28
View File
@@ -4593,6 +4593,34 @@ any checkpoint reached *during* the drain sees `depth > 1` and will not drain ag
counter that defines the safe boundary also makes the drain non-reentrant**, with no flag, no
lock and no new state.
**Amendment, found while building task 3.4 (2026-09-22): this claim is true and covers a
different hazard than the one that actually mattered.** Non-reentrant drain (the same message
cannot drain twice) is real, but `g_vm_interpret_depth` was built for *cross-VM* nesting — the
checkpoint's own comment frames it as "nested inside a `VM-EXEC`/`VM-CALL` dispatch **from
another VM's own `vm_interpret()` call**." A different VM means a different `VM` struct, so
`input_buffer`/`input_length`/`input_pos` never collide in that case. **Same-VM reentrancy —
draining calls `vm_interpret()` on the very `vm` whose own `vm_interpret()` call is still
paused on the C stack, mid-word, at the checkpoint that triggered the drain — is a genuinely
separate hazard §XLIII.5 never named.** `FABRIC-3.md` §XX had already flagged this exact class
for Hera specifically: the old messaging pump skipped her because "self-targeting `VM-EXEC`
would hit the same reentrancy class… (`input_buffer`/`input_pos` not being saved by
`vm_state_push`/`pop`)." Read directly: `VMCallState` (`vm_state_push()`/`vm_state_pop()`,
`mama_forth_words.c`) saves only `rsp`/`exit_colon`/`ecw_nesting` — never `input_buffer`,
`input_length`, or `input_pos`. Left unaddressed, the enclosing `vm_interpret()` call's own
while loop would silently lose the rest of its input line or block the moment a drain fires
mid-line — the same failure shape as the `INPUT_BUFFER_SIZE` 256 defect `.claude/CLAUDE.md`
calls non-negotiable, and trap #1 in `FABRIC-3.6.md`'s own START HERE ("a green boot is weak
evidence").
**Not a divergence from this section's ruling — the mechanism is exactly as ruled.** Cursor
preservation is the implementer's own obligation *inside* the ruled mechanism, the same way
§XLIV.1 found `mkcapsule`'s "1024-byte limit" was arithmetically right and operationally
incomplete: fixing one thing while leaving a real gap unnamed. `FABRIC-3.6.md` task 3.4's own
implementation snapshots `vm->input_buffer`/`input_length`/`input_pos`, plus `vm->mode` (a
checkpoint reached mid-colon-definition must not let a drained payload's words compile into
the enclosing definition) and `vm->error`/`abort_requested` (a bad message must not abort the
enclosing execution), around the `vm_interpret()` call, restoring all six afterward.
### XLIII.6 — Three constraints, named rather than discovered later
1. **`INPUT_BUFFER_SIZE` is 1025** — 1024 content bytes plus NUL, and `.claude/CLAUDE.md` calls
+37 -1
View File
@@ -862,10 +862,46 @@ ruling]** cannot be written precisely until Captain Bob settles the named sub-it
`dict_hash` for Hermes (`0xc95ef2d92fa0781f`) and Hestia (`0xfbde9fe105fd3b3d`) identical
across all three architectures, unmoved from tasks 3.1/3.2's values (this task touches no
capsule).
- [ ] **3.4** — **Drain at the outermost checkpoint** (§XLIII.3–.5). Reuse
- [x] **3.4** — **Drain at the outermost checkpoint** (§XLIII.3–.5). Reuse
`sk_vm_at_outermost_interpret()`; one message per checkpoint **[needs ruling 3.0e]**.
*Check:* a nested interpret does not drain; a queued payload is interpreted exactly once at
depth 1.
2026-09-22 · `logs/20260922-010622/amd64/`, `logs/20260922-011130/aarch64/`,
`logs/20260922-011648/riscv64/` — all three reach `[zuse@Hera] ok>`, zero `UNKNOWN WORD`,
`mkcapsule --lint capsules/` clean (38 files, 0 violations, unchanged -- no capsule
touched). **Finding, amended into `FABRIC-3.5.md` §XLIII.5** (caught by `advisor()` before
writing the naive version, not found live): §XLIII.5's "recursive drain is prevented for
free" via `g_vm_interpret_depth` is true but covers only same-message re-drain, not the
separate same-VM reentrancy hazard `FABRIC-3.md` §XX had already named for Hera
specifically (`VMCallState` saves `rsp`/`exit_colon`/`ecw_nesting` only, never
`input_buffer`/`input_length`/`input_pos`) -- draining calls `vm_interpret()` on the same
`vm` whose own `vm_interpret()` call is still paused mid-word at the checkpoint, which
would silently truncate the enclosing REPL line or LOAD block if the cursor isn't saved
and restored by hand. `sk_hermes_drain_checkpoint()` (kernel_hermes.c) snapshots
`input_buffer`/`input_length`/`input_pos`/`mode`/`error`/`abort_requested` around the
`vm_interpret()` call and restores all six -- `mode` forced to `MODE_INTERPRET` for the
duration (a checkpoint reached mid-colon-definition must not compile the payload's words
into the enclosing definition); `error`/`abort_requested` restored so a bad message can't
abort the enclosing execution. Placed in `vm_core.c`'s existing cooperative checkpoint
**before** the switch-signal block, not after (`sk_vm_context_switch()` does not return
until something switches back, so a drain placed after it would silently never run on any
checkpoint that switches). Gated behind a system-wide pending-total counter
(`sk_hermes_pending_total`, maintained in `queue_push()`/`sk_hermes_pending_pop()`) so the
common no-message-in-flight case costs one integer read per word dispatch, not a
`stadium_max_vm_count()`-sized queue-table scan -- flagged by `advisor()` as a real
hot-path cost against this project's own +0.0603% measurement floor, not deferred.
Self-test (kernel_main.c) publishes a real, stack-neutral payload (`"1 2 + DROP"`) to
Hermes (a real, already-born VM, not synthetic -- needed a genuine live dictionary),
proves the depth gate via `VM-EXEC`-ing the existing harmless colon word `WELCOME`
(`capsules/hermes/init.4th` block 4855) into Hermes from Hera's context -- a real, already-
proven-safe nested `vm_interpret()` call (`mama_forth_words.c`'s own VM-EXEC mechanism) --
confirming the message does NOT drain at the resulting depth 2, then calls
`sk_hermes_drain_checkpoint()` directly from this self-test's own genuinely-outermost C
context and confirms it DOES drain exactly once, with a further call a clean no-op.
Deliberately avoided the block/`LOAD` mechanism for the nested case -- real but touches
real disk-backed block storage, which a throwaway diagnostic has no business perturbing.
`dict_hash` for Hermes/Hestia unmoved and identical across all three architectures (this
task touches no capsule).
- [ ] **3.5** — **Payload bound and chunking** (B4) **[needs ruling 3.0d]**. Max 1024 bytes per
message; larger payloads sent as ordered chunks, reassembled before drain. *Check:*
1024-byte payload single message; 3000-byte payload chunked and reassembled byte-exact;
+59
View File
@@ -451,6 +451,65 @@ SkHermesMessage *sk_hermes_pending_peek(VMUuid vm_id);
* vm_id has no queue or an empty one. */
int sk_hermes_pending_pop(VMUuid vm_id);
/* Forward declaration only -- kernel_hermes.h deliberately does not
* include vm.h (kept decoupled from the full VM struct, same posture as
* every other type in this file), but sk_hermes_drain_checkpoint() below
* needs a VM* parameter. Matches vm.h's own `typedef struct VM VM;`
* shape exactly, so no redefinition conflict. */
typedef struct VM VM;
/*
* Drain at the outermost checkpoint (FABRIC-3.6.md task 3.4, SXLIII.3-.5;
* one message per checkpoint, ruled 2026-09-21). Called from
* execute_colon_word()'s existing cooperative checkpoint in vm_core.c,
* gated the same way the switch-signal checkpoint already is
* (sk_vm_at_outermost_interpret()).
*
* AMENDS SXLIII.5's own claim: "recursive drain is prevented for free"
* via g_vm_interpret_depth is true (the SAME message cannot drain twice),
* but that counter says nothing about a SEPARATE, real hazard SXLIII.5
* never named -- calling vm_interpret() on this same vm, from inside its
* own currently-running vm_interpret() call, overwrites vm->input_buffer/
* input_length/input_pos with the drained payload's own state.
* VMCallState (vm_state_push()/vm_state_pop(), mama_forth_words.c) saves
* only rsp/exit_colon/ecw_nesting -- never these three fields (the exact
* gap FABRIC-3.md SXX documents: "the same class... for input_buffer/
* input_pos not being saved by vm_state_push/pop"). Left unaddressed,
* the enclosing vm_interpret() call's own while loop would silently lose
* the rest of its input line/block the moment a drain fires mid-line --
* the same failure shape as the INPUT_BUFFER_SIZE 256 defect
* .claude/CLAUDE.md calls non-negotiable, and trap #1 in this document's
* own START HERE. Not a divergence from SXLIII.3's ruling (the mechanism
* is exactly as ruled); cursor/mode/error/abort preservation is this
* function's own implementation obligation, not a new design question.
*
* sk_hermes_drain_checkpoint() therefore snapshots vm->input_buffer/
* input_length/input_pos/mode/error/abort_requested before calling
* vm_interpret() on the queued payload, forces vm->mode to
* MODE_INTERPRET for the duration (a checkpoint reached mid-colon-
* definition must not let the payload's words compile into the
* enclosing definition), and restores all six afterward -- fully
* isolating the drain from whatever the enclosing execution was doing.
*
* Payload convention: payload_addr is trusted to point at a
* NUL-terminated C string (vm_interpret()'s own signature takes no
* length) -- payload_len is not consulted here. Bounding/validating that
* is task 3.5's scope (payload bound and chunking), not this one's.
*
* Fast path: sk_hermes_publish()/sk_hermes_pending_pop() maintain a
* single system-wide pending-total counter; this function reads it
* first and returns immediately if it is 0, so the common case (nothing
* in flight) costs one integer read on every word dispatch, not a
* stadium_max_vm_count()-sized queue-table scan.
*
* @param vm The VM at its own outermost checkpoint. NULL is refused.
* @return 1 if a message was drained cleanly, 0 if nothing was pending
* for this vm, -1 if a message was drained but interpreting its
* payload set vm->error (restored to its pre-drain value either
* way -- a bad message must not abort the enclosing execution).
*/
int sk_hermes_drain_checkpoint(VM *vm);
#endif /* __STARKERNEL__ */
#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
+72
View File
@@ -1432,6 +1432,78 @@ static void kernel_main_deep(BootInfo *boot_info) {
}
}
/* FABRIC-3.6.md task 3.4 self-test: drain at the outermost checkpoint.
* Publishes one real, stack-neutral payload ("1 2 + DROP") to Hermes
* (a real, already-born VM -- not a synthetic one, since this test
* needs a genuine live dictionary to interpret against) and proves
* the depth gate two ways:
*
* 1. VM-EXEC-ing "WELCOME" (an existing, harmless colon word
* already in Hermes's own dictionary, block 4855) from Hera's
* context nests a SECOND, genuine vm_interpret() call via
* VM-EXEC's own already-proven-safe mechanism
* (mama_forth_words.c's `vm_interpret(target, cmd_buf)`).
* Hermes's own checkpoint fires there at depth 2 and must NOT
* drain -- the pending message must still be there afterward.
* 2. Calling sk_hermes_drain_checkpoint() directly from this
* self-test's own C context -- genuinely outermost, since
* kernel_main.c is not itself inside any vm_interpret() call --
* must drain exactly the one message, and a further call with
* nothing left must be a clean no-op.
*
* Deliberately avoids the block/LOAD mechanism for the nested case:
* LOAD's nested vm_interpret() is real, but block storage is real
* disk-backed state (`block_subsystem.c`) that a throwaway
* diagnostic has no business touching -- VM-EXEC's cross-VM nesting
* proves the same depth gate without it. */
{
VMUuid pub_id3, hermes_id;
VMRegistryEntry hermes_drain_entry;
int drain_ok = 1;
int grant_rc;
int ch;
pub_id3.hi = 0;
pub_id3.lo = 11;
console_puts("Kernel-Hermes drain self-test: ");
if (capsule_vm_find_by_name_nocase("Hermes", &hermes_drain_entry) != 0 ||
hermes_drain_entry.state != VM_STATE_LIVE || !hermes_drain_entry.vm_ptr) {
console_println("SKIPPED (Hermes not live)");
} else {
hermes_id = hermes_drain_entry.vm_id;
grant_rc = stadium_grant_quota(pub_id3, vm_uuid_hera());
if (grant_rc != 0) {
console_println("SKIPPED (quota grant failed)");
} else {
ch = sk_hermes_channel_create();
if (ch < 0) drain_ok = 0;
if (drain_ok && sk_hermes_channel_subscribe(ch, hermes_id) != 0) drain_ok = 0;
if (drain_ok &&
sk_hermes_publish(pub_id3, ch, 0, (void *)"1 2 + DROP", 0) != 1) drain_ok = 0;
if (drain_ok && sk_hermes_pending_count(hermes_id) != 1) drain_ok = 0;
/* Nested (depth 2 during VM-EXEC's own call): must not drain. */
if (drain_ok) {
vm_interpret(mama, "S\" WELCOME\" S\" Hermes\" VM-EXEC");
if (mama->error) { mama->error = 0; drain_ok = 0; }
}
if (drain_ok && sk_hermes_pending_count(hermes_id) != 1) drain_ok = 0;
/* Outermost (this self-test's own C context): must drain. */
if (drain_ok &&
sk_hermes_drain_checkpoint((VM *)hermes_drain_entry.vm_ptr) != 1) drain_ok = 0;
if (drain_ok && sk_hermes_pending_count(hermes_id) != 0) drain_ok = 0;
if (drain_ok &&
sk_hermes_drain_checkpoint((VM *)hermes_drain_entry.vm_ptr) != 0) drain_ok = 0;
if (drain_ok && sk_hermes_channel_destroy(ch) != 0) drain_ok = 0;
console_println(drain_ok ? "PASS" : "FAIL");
}
}
}
/* Decided 2026-09-05: no console for the running system unless a
* thumbdrive is present -- headless by default (EMERGENCY_CONSOLE_
* ENABLED off), reusing that flag's own existing "does this build
+55
View File
@@ -50,6 +50,7 @@
#include "starkernel/q48_16.h"
#include "starkernel/kmalloc.h"
#include "console.h"
#include "vm.h" /* task 3.4 -- VM struct fields, vm_interpret() */
/* Freestanding: no libc printf. Prints an unsigned decimal, no leading
* zeros -- same small helper stadium.c/capsule_vm_switch_signal.c each
@@ -463,12 +464,20 @@ static SkHermesPendingQueue *find_or_create_queue(VMUuid vm_id) {
return &sk_hermes_queues[free_slot];
}
/* Task 3.4: system-wide sum of every queue's count, maintained alongside
* queue_push()/sk_hermes_pending_pop() below -- lets
* sk_hermes_drain_checkpoint() skip its per-VM queue lookup entirely
* (stadium_max_vm_count()-sized linear scan) on every word dispatch when
* nothing is pending anywhere, the overwhelmingly common case. */
static int sk_hermes_pending_total = 0;
static int queue_push(SkHermesPendingQueue *q, int msg_index) {
size_t tail;
if (q->count >= SK_HERMES_PENDING_MAX) return -1;
tail = (q->head + q->count) % SK_HERMES_PENDING_MAX;
q->slots[tail] = msg_index;
q->count++;
sk_hermes_pending_total++;
return 0;
}
@@ -529,7 +538,53 @@ int sk_hermes_pending_pop(VMUuid vm_id) {
if (!q || q->count == 0) return -1;
q->head = (q->head + 1) % SK_HERMES_PENDING_MAX;
q->count--;
sk_hermes_pending_total--;
return 0;
}
int sk_hermes_drain_checkpoint(VM *vm) {
SkHermesMessage *msg;
VMUuid self;
char saved_input[INPUT_BUFFER_SIZE];
size_t saved_length, saved_pos;
vm_mode_t saved_mode;
int saved_error, saved_abort;
int drain_error;
if (!vm) return -1;
if (sk_hermes_pending_total == 0) return 0; /* fast path -- see this
* counter's own doc comment */
self = vm->stadium_vm_id;
msg = sk_hermes_pending_peek(self);
if (!msg) return 0;
/* See kernel_hermes.h's own doc comment on this function for why all
* six of these must be preserved, not just the obvious ones. */
memcpy(saved_input, vm->input_buffer, sizeof(saved_input));
saved_length = vm->input_length;
saved_pos = vm->input_pos;
saved_mode = vm->mode;
saved_error = vm->error;
saved_abort = vm->abort_requested;
vm->mode = MODE_INTERPRET; /* a payload is never compiled into whatever
* the enclosing context was mid-defining */
vm_interpret(vm, (const char *)msg->payload_addr);
drain_error = vm->error;
memcpy(vm->input_buffer, saved_input, sizeof(saved_input));
vm->input_length = saved_length;
vm->input_pos = saved_pos;
vm->mode = saved_mode;
vm->error = saved_error; /* a bad message must not abort the
* enclosing execution */
vm->abort_requested = saved_abort;
sk_hermes_release(msg);
sk_hermes_pending_pop(self);
return drain_error ? -1 : 1;
}
#endif /* __STARKERNEL__ */
+14
View File
@@ -62,6 +62,7 @@
#include "starkernel/vm/stadium_words.h" /* item 4.1: word patrons on the Stadium */
#include "starkernel/capsule_vm_switch_signal.h" /* FABRIC-3.md §XXVIII Stage 3 */
#include "starkernel/vm/switch.h" /* FABRIC-3.md §XXVIII Stage 2 -- sk_vm_context_switch() */
#include "starkernel/vm/kernel_hermes.h" /* FABRIC-3.6.md task 3.4 -- sk_hermes_drain_checkpoint() */
#include "starkernel/capsule_birth.h" /* capsule_vm_registry_get() */
/* FABRIC-3.md §XXVIII Stage 3 correction (2026-09-13): forward-declared
@@ -910,6 +911,19 @@ void execute_colon_word(VM* vm)
}
#ifdef __STARKERNEL__
/* FABRIC-3.6.md task 3.4 (SXLIII.3-.5): the target drains its own
* pending queue here, in its own context, at its own outermost
* interpret checkpoint -- same gate, same placement, same
* defer-if-nested discipline the switch-signal checkpoint just
* below already uses (SXLIII.2/.4: this IS that machinery,
* generalized). Placed BEFORE the switch-signal block, not after:
* sk_vm_context_switch() below does not return until something
* later switches back to `vm`, so a drain placed after it would
* silently never run on any checkpoint that switches. */
if (sk_vm_at_outermost_interpret()) {
(void)sk_hermes_drain_checkpoint(vm);
}
/* FABRIC-3.md §XXVIII, Stage 3 (2026-09-13): the cooperative
* preemption checkpoint. Deliberately unconditional (every word,
* not throttled like the heartbeat cycle above) -- the check