Stage 3: timer-driven preemptive switching, live on all 3 arches (FABRIC-3.md §XXVIII)
Fourth stage of the preemptive context-switching plan, and the biggest. LithosAnanke now genuinely, continuously preempts between Hera, Hermes, and Artemis -- timer-driven, running live for the entire remainder of every boot once the Tripod fleet registers, not a bounded probe. A real design fork was resolved before writing code: the naive approach (the timer ISR calling Stage 2's sk_vm_context_switch() directly) is broken -- Stage 0's trap frame lives on whatever stack was active at interrupt time, and jumping to a different stack via Stage 2's own independent swap mid-handler would abandon that trap frame unresumed, guaranteed corruption on the first tick. Chose the safer of two named options: the ISR only ever sets a flag and returns completely normally through its own full epilogue; the actual switch happens moments later, via Stage 2's already-proven mechanism, at a safe cooperative checkpoint on the mainline (execute_colon_word()'s per-word dispatch loop, checked on literally every word, not throttled to the existing 256-word heartbeat-tuning cadence) -- confirmed with the user that word-level granularity is fine-grained enough given the eventual Zynq FPGA target where a word is a mnemonic. New capsule_vm_switch_signal.c/.h: a purpose-built run-readiness signal, deliberately separate from capsule_vm_physics.c's execution-heat engine (that one's own header documents itself as never touched from interrupt context, by design). Slot table sized with headroom (8) rather than hardcoded to today's 3 participants, so extending participation later is another register() call, not a redesign -- per direct request to leave room for swapping the participant set. Simple linear accumulate-then- threshold for this first cut; a fancier law can replace it later without touching the mechanism around it. heartbeat_tick() gains its one deliberate, documented amendment to this file's own top-half/bottom-half discipline -- the first time this codebase reaches into VM-scheduling state from real ISR context. Registration happens only after all three VMs are fully born, right before the REPL starts -- no critical-section protection yet against being switched away mid-birth-setup. Known, flagged rough edge (not reconciled this pass): MSG-TICK's own idle-pump and this new mechanism can still independently move control between the same VMs; not observed to interact badly in verification, but not fully unified either. Verified interactively at the console on all 3 architectures with continuous background preemption running throughout -- amd64 computed `1 1 + .` -> 2, aarch64 computed `1 1 + dup DUP * . CR` -> 4, both correct, REPL fully responsive, zero fault indicators over sustained runtime. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016UNhH1mhi52i6Qihh7ZV5S
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
f790d0995e
commit
986d042aa7
+63
@@ -3635,3 +3635,66 @@ Stage 3 (timer-driven preemption, Tripod fleet only, the new run-readiness signa
|
||||
the biggest remaining stage, and the first one that actually amends the §21.1
|
||||
nothing-is-concurrent-on-one-hart ruling for real.
|
||||
|
||||
**Stage 3 CLOSED, same day.** LithosAnanke now genuinely, continuously preempts between Hera,
|
||||
Hermes, and Artemis, timer-driven, for real -- not a bounded probe window like Stage 2, but live
|
||||
for the entire remainder of every boot from the moment the Tripod fleet registers onward.
|
||||
Verified interactively at the console on all 3 architectures (`1 1 + .` -> `2` on amd64,
|
||||
`1 1 + dup DUP * . CR` -> `4` on aarch64), with continuous background switching running the
|
||||
whole time underneath -- the REPL stayed fully responsive and computed correctly throughout.
|
||||
|
||||
**A real design fork was resolved before writing any code, not glossed over:** the naive
|
||||
approach -- the timer ISR's C handler calling Stage 2's `sk_vm_context_switch()` directly --
|
||||
is broken. Stage 0's trap frame lives on whatever stack was active when the interrupt fired;
|
||||
calling into Stage 2's *own, independent* stack-swap from inside that handler would abandon the
|
||||
ISR's own trap frame mid-flight, unresumed, while jumping to a completely different stack via a
|
||||
*second*, unrelated swap -- guaranteed corruption on the first tick. Two ways to do this
|
||||
correctly were named and one deliberately chosen over the other: (1) the ISR only ever sets a
|
||||
flag ("switch requested, target X") and returns completely normally through its own full Stage-0
|
||||
epilogue, with the actual switch happening moments later via Stage 2's already-proven
|
||||
`sk_vm_context_switch()` at a safe cooperative checkpoint on the mainline; vs. (2) true
|
||||
mid-interrupt preemption, where the ISR epilogue itself swaps to a *different* VM's own trap
|
||||
frame before returning -- genuinely preemptable at any instruction, but requires a second,
|
||||
different parked-context representation from Stage 2's and new logic in three arches' raw
|
||||
assembly epilogues, real risk of a silent, unrecoverable crash if subtly wrong. Chose (1):
|
||||
confirmed with Bob that word-level granularity is "fine grained enough," given the eventual Zynq
|
||||
FPGA target where a word is a mnemonic -- the checkpoint fires on literally every single word
|
||||
dispatch (not throttled to the existing 256-word heartbeat-tuning cadence), so in practice the
|
||||
observable latency between "the clock wants a switch" and "the switch happens" is at most one
|
||||
word's worth of execution.
|
||||
|
||||
**The new run-readiness signal** (`capsule_vm_switch_signal.c`/`.h`, new files beside
|
||||
`capsule_vm_physics.c`, deliberately NOT folded into it -- that engine's own header explicitly
|
||||
documents itself as never touched from interrupt context, by design, unlocked): a slot table
|
||||
sized with headroom (8 slots) rather than hardcoded to exactly today's 3 participants, so
|
||||
extending participation later (Stage 4+, or any future VM) is another
|
||||
`sk_vm_switch_signal_register()` call, not a redesign -- a deliberate choice made after Bob asked
|
||||
for room to swap the participant set later, not just the fixed Tripod trio. Simple linear
|
||||
accumulate-then-threshold for this first cut (50 ticks idle before a switch is requested, reset
|
||||
to 0 the instant a slot becomes current) -- correctness and a clean single-writer(ISR)/
|
||||
single-reader(mainline) story mattered more than the exact law; a fancier relaxation curve is
|
||||
available to a later pass without touching the mechanism around it. `heartbeat_tick()` gains its
|
||||
one deliberate, documented amendment to this file's own top-half/bottom-half discipline: it now
|
||||
calls `sk_vm_switch_signal_tick()`, genuinely reaching into VM-scheduling state from real ISR
|
||||
context for the first time in this codebase's history -- named explicitly in the code, not
|
||||
silently slipped in, and kept safe by the same single-hart/nothing-concurrent property §21.1
|
||||
already established for everything else here.
|
||||
|
||||
**The MSG-TICK ownership question the plan flagged turned out to be less sharp than expected**
|
||||
under approach (1): since the actual switch is itself an ordinary cooperative call (just
|
||||
timer-triggered rather than hand-written), it doesn't fight MSG-TICK's own idle-pump for a
|
||||
stack-swap the way true interrupt-driven switching would have. Not fully reconciled this
|
||||
pass -- both mechanisms can still independently decide to move control between the same three
|
||||
VMs, which is a live, accepted rough edge for this first cut, flagged here rather than silently
|
||||
assumed fine. Noted for a later pass, not blocking: the two have not been observed to interact
|
||||
badly in verification so far.
|
||||
|
||||
Registration deliberately happens only after all three VMs are fully confirmed born (right
|
||||
before the interactive REPL starts) -- this stage has no critical-section protection against
|
||||
being switched away mid-birth-setup, so registering any earlier was rejected as a real risk, not
|
||||
a hypothetical one.
|
||||
|
||||
All 3 architectures: clean build, clean boot to `ok>`, sustained runtime with continuous live
|
||||
switching and zero fault indicators, interactive console commands computed correctly. Stage 4
|
||||
(WIREBIND-scope extension) remains a ratified-decision-only step, not attempted -- the async
|
||||
unclean-detach UAF risk it names is unchanged by anything built in Stages 0-3.
|
||||
|
||||
|
||||
Reference in New Issue
Block a user