walk-free B1: SysTick + SCB scheduler migration + batched-IRQ dispatch fix#518
Merged
Conversation
…ead of wedging the run loop step_batch's early-out broke the batch whenever a takeable exception was pending — including at executed == 0, BEFORE the first step_internal could dispatch it. Machine::run then saw zero progress and returned, and every batched caller (Machine::run(Some(n)) loops, the wasm step_batch wrapper) spun forever at the same PC the moment a walk- or scheduler-pended IRQ (e.g. an armed SysTick) became takeable between batches. Nothing hit this before because every IRQ-driven Cortex-M harness in-tree (firmware_survival, integration tests, the CLI single-step path) drives machine.step(), which dispatches inside step_internal. The walk-free B1 differential is the first gate to run IRQ firmware through the batched path — which is the whole point of walk deletion, so batched dispatch has to work. Fix: break only after the batch has made progress (executed > 0); at the batch top the pending exception is dispatched by step_internal exactly like the single-step path (byte-identical timing at interval 1). Both the SystemBus fast arm and the boxed dyn-Bus arm get the same rule.
…, scheduled exception-15 expiries, write-armed ICSR pend drain
The highest-value walker migration (plan Part 2, batch B1): every HAL
delay loop arms SysTick, so this is the batch that makes arbitrary user
firmware batchable.
SysTick (peripherals/systick.rs):
- Scheduler mode (event-scheduler + bus CycleClock attached): SYST_CVR is
derived lazily from the published clock with exact modular arithmetic
(advance_counter — closed-form replay of the walk's edge-triggered
countdown, property-tested against a literal tick-by-tick walk), so
&self reads stay fresh with zero walk. COUNTFLAG folds in on the same
lazy sync; word-read-clears, CVR-write-clears, TICKINT/ENABLE gating,
RVR=0 park and the Zephyr tickless-idle reload semantics preserved
exactly.
- The periodic exception (system exception 15, NOT an NVIC line) rides
scheduled events: arming writes emit (ticks_until_fire - 1, arm_seq)
through take_scheduled_events (the bus + 1 convention pins the expiry
to the exact legacy fire cycle); on_event claims accumulated wraps as
ONE exception-15 pend (pends merge exactly as silicon's single PENDST
bit) and reschedules from the just-synced state, so deadlines stay
absolute — no cumulative drift at any tick interval. Stale chains die
on an arm_seq token mismatch. Event results already route to
Cpu::set_exception_pending via EventResult::system_exception — the
system-exception arm of apply_event_result — so no new routing was
needed (a future C3-interrupt-matrix arm slots in beside it).
- Legacy mode (feature off / no clock) keeps the eager per-cycle walk
countdown byte-for-byte; the two modes are mutually exclusive by
construction on ONE predicate (the rtc_timer pattern).
SCB (peripherals/scb.rs):
- Its tick() was a write-latch drain: ICSR SET bits (NMI/PENDST/PENDSV)
drained one per cycle, NMI > SysTick > PendSV. That is not periodic
work, so it becomes a write-armed delay-0 event chain: one chain at a
time (drain_chain_armed), on_event drains ONE latch per event and
reschedules at +1 cycle while more remain — replicating the legacy
one-exception-per-cycle pacing exactly. AIRCR SYSRESETREQ stays on the
machine-level drain_scb_reset_request (untouched).
Tick-cost normalization: SysTick charged cycles:1 into the tick-cost
channel on every enabled tick (SCB per drained pend), inflating
total_cycles by ~1/cycle while armed — a sim artifact (real SysTick
consumes zero core cycles) structurally incompatible with walk deletion.
Both models now charge zero in both modes; the logic-capture cost-path
fixture and the metrics accounting test keep their coverage via a
dedicated CostTicker test peripheral and now also pin systick's cost at
zero.
Attach chokes: push_peripheral (the from_config twin of add_peripheral)
now hands every descriptor-built model the bus CycleClock;
configure_cortex_m attaches it to the SCB it installs by replacement.
Hand-built buses that bypass the chokes keep exact legacy semantics.
Gates:
- tests/systick_walk_differential.rs (replaces the Part-1 spike, as the
plan prescribes): hand-assembled Thumb firmware, walk-on reference vs
scheduler from the same bus assembly.
* delay-loop + SysTick-ISR-counter firmware (arms RVR/CVR/CSR, polls
CVR): per-instruction probes of total_cycles/PC/all registers/RAM
counters byte-identical at interval 1 (pins IRQ delivery cycles and
ISR count exactly).
* scheduler @ 64 vs walk-on @ 1: ISR count over a fixed window exact;
delivery quantisation bound (< one interval, delay-only) verified
against the reference's own delivery trace.
* ICSR.PENDSVSET firmware: PendSV delivery byte-identical at interval 1.
* cpsid-i/wfi + periodic wfi/ISR loop with idle fast-forward: FF clamps
to the SCHEDULED SysTick expiry, wakes with identical event
observables and one thread pass per wake, retiring <1/4 of the
instructions.
- B0 surface test updated: systick + scb leave the walk-forcing set in
event-scheduler builds (20 remain: 11 timers, dma1/2, i2c1-3, adc1,
exti, can1, dwt); the featureless lane honestly keeps 22. No bus flips
derive_walk_deletable yet (kw41z is closest: mcg, rsim, i2c1, dwt).
…ouched by walk-free B1; sim-validated tier, no silicon capture, so no drift_ack owed)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Batch B1 of the walk-free campaign — SysTick and SCB leave the per-cycle walk, and the armed-firmware differential flushed out a real pre-existing engine bug.
The bug (fixed first, own commit)
CortexM::step_batchbroke the batch when a takeable exception was pending — including atexecuted == 0, beforestep_internalcould dispatch it.Machine::runthen saw zero progress and returned; every batched caller spun forever at the same PC the moment a pended IRQ became takeable between batches. Unnoticed because every in-tree IRQ harness drivesmachine.step()— B1's differential is the first gate running IRQ firmware through the batched path (which is the whole point of walk freedom). Fix: break only after progress; at batch top the exception is dispatched exactly like the single-step path (per-instruction byte-identity pinned).SysTick
Lazy CVR via the bus CycleClock: exact closed-form replay of the edge-triggered countdown (property-tested against a literal tick-by-tick walk, incl. RVR-shrunk-mid-count), COUNTFLAG latch/read-clear semantics preserved, CVR-write does not cancel a latched pend (silicon behavior, unit-pinned). Expiry as scheduled events routing
system_exception: Some(15)through the existingapply_event_resultarm; accumulated wraps merge into one pend like silicon's single PENDST bit;arm_seqkills stale chains. Also normalizes the tick-cost artifact: legacy SysTick charged +1 cycle per enabled tick (inflating total_cycles ~2× while armed — real SysTick consumes no core cycles); both modes now charge 0.SCB
Its tick was an ICSR write-latch drain (one per cycle, NMI>ST>PendSV) — now a delay-0 event chain replicating that pacing exactly.
drain_scb_reset_requestuntouched.Evidence
tests/systick_walk_differential.rs: delay-loop + SysTick-ISR firmware — per-instruction probes (total_cycles, PC, all 16 registers, raw CVR polls, RAM counters) byte-identical walk vs scheduler at interval 1; ISR count exact at interval 64 with the documented grid-quantization bound; PendSV same-cycle;cpsid i; wfiwake + idle fast-forward clamping to the scheduled expiry. firmware_survival (real HAL/FreeRTOS/Zephyr) green both lanes.Surface: invaders walk-forcing set 22 → 20 (systick, scb out). kw41z is now 4 walkers from full walk-deletion derivation. All lanes green; known machine-local failures verified identical on origin/main.