feat(gust): WCET EVT cross-check on real F100 — static bounds dominate (v0.6.0 D1) - #229
Merged
Conversation
…nds (v0.6.0 D1)
VER-OS-WCET-001 requires synth's static per-function cycle bound to DOMINATE both
a measurement-based statistical (EVT) bound and every observed raw DWT sample, and
its kill-criterion is the negation of that. This lands the measurement half plus the
kill-criterion as a mechanical gate, for the two functions of the frozen os-tl node
that actually carry a static bound (`status: bounded` in repro-757/os-tl.wcet.json).
- benches/gust/src/bin/gust_wcet_evt.rs — F100 firmware DWT-sampling the DISSOLVED
`gust:os/time@0.1.0#deadline` (42 cyc) and `#elapsed` (71 cyc) out of the frozen
os-tl-fixed.o. N=40 per function over a wrap-boundary-heavy input set, integer
stats only, one machine-parseable line per sample plus a per-function summary.
Three things make the numbers mean something:
* a correctness gate runs FIRST (deadline==now+ticks, elapsed==now>=deadline over
all 20 pairs) — no timings are reported for code that computes the wrong thing;
* both functions open with a once-init guard whose byte
(__synth_wasm_seg_2+12) is 0x3a in the frozen .data image, so the store path the
bound covers (instr_count 18 vs 11) is never taken on a stock run. The harness
zeroes that byte for the `cold` half of the samples to exercise it, and PROVES
the decode at runtime before relying on it (byte reads 0x3a; reads 0x01 after a
zeroed call), degrading loudly to warm-only if the proof fails;
* the DWT is liveness-checked and the run REFUSES to emit timings where the cycle
counter is absent (qemu) rather than reporting emulated zeros.
Measurement overhead is calibrated two ways: `read_read` (two back-to-back CYCCNT
reads, SUBTRACTED) and `call_shim` (bl + bx lr, reported but NOT subtracted, so
samples stay conservative). The linked disassembly was checked: the only thing
between the two CYCCNT reads is the `bl` itself.
- benches/gust/drivers/check-wcet-evt.py — the kill-criterion as a build gate.
Reads the bounds from the committed synth-wcet-v1 sidecar (never hardcoded),
matches by WIT-export suffix, computes a block-maxima EVT statistic over the raw
samples, and exits 1 if an observed max OR the statistical bound exceeds the
static bound. Refuses to gate a `declined` sidecar entry, and fails on a truncated
capture, n<30, or a capture whose summary disagrees with its samples. `--self-test`
demonstrates the red state without hardware; `--emit-sample-capture {pass,fail}`
produces sidecar-derived fixtures. Output is explicit that for these straight-line
functions the sample distribution is degenerate, so the EVT bound is tight by
construction and this is a CROSS-CHECK, not an independent bound — and that DWT
numbers may only falsify the static model, never size a partition budget.
- build.rs links the object into the new bin behind the synth#746-class
defined-text-symbol guard; Cargo.toml gates the bin on target-f100 so the default
g474/thumbv7em build skips it (a cortex-m3 .o in a v7E-M image links to nothing).
Oracles (all run, exact output in the PR): f100 build clean with 0 undefined symbols
in the ELF and both `bl`s landing on the right exports; --self-test exits 1;
synthetic passing capture exits 0; default g474 --bins build exits 0 and skips the
bin. Pre-silicon smoke under qemu passes the correctness gate and the worst-path
decode proof, then correctly refuses to time (no DWT).
NOT YET DONE: no silicon numbers. The coordinator owns the board; nothing here
assumes or asserts a measured value.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…e (v0.6.0 D1) Closes the MEASUREMENT half of track T4 for the functions that actually carry a static bound, and records it as VER-OS-WCET-EVT-001 rather than closing VER-OS-WCET-001 — whose acceptance is stated over the trusted switch/MPU/HM object and the inner executor core, which still have NO static bound (synth declines them: reason=call needs T3 composition, reason=loop needs trip-count inference). Narrowing that artifact to match what was achieved would be moving the goalposts; it stays proposed with the gap stated. MEASURED on real STM32VLDISCOVERY silicon (openocd/ST-LINK-V1 via the Pi), DWT cycle counter, n=40 per function, inputs spanning the u64 wrap boundary: deadline min=34 max=40 mean=37 vs static 42 -> dominates, margin 2 cyc elapsed min=39 max=45 mean=42 vs static 71 -> dominates, margin 26 cyc Overhead calibrated (read_read=1 cyc subtracted; the caller's bl/bx shim 5 cyc deliberately NOT subtracted, so samples stay conservative). Worst-path honesty: both functions open with a once-init guard whose byte is non-zero in the frozen .data, so a stock call never executes the store block the bound covers. The harness zeroes it for half the samples and PROVES the decode at runtime first (path_variants=cold+warm) — measuring only the default path would have left the bounded path unmeasured. Noted-not-gated: deadline's naive tail projection (46 cyc) sits above its 42 cyc bound; the margin is thin and the checker prints that rather than hiding it. check-wcet-evt.py mechanizes the kill-criterion (exit 1 when observed or EVT bound exceeds the static bound), reads bounds from the committed sidecar, refuses to gate declined entries, and proves its own red state via --self-test. GATE GREEN on the committed capture. rivet validate PASS. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
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.
v0.6.0 workstream D1. Track T4 had an implemented requirement but an open V — the compiler emits sound static bounds, and nothing checked them against reality. This closes the measurement half, on real silicon.
Measured on a physical STM32VLDISCOVERY (DWT cycle counter, n=40 each)
synth --emit-wcet)gust:os/time@0.1.0#deadlinegust:os/time@0.1.0#elapsedThe static bound dominates every observed sample and the EVT statistical bound, for both functions —
check-wcet-evt.py→GATE GREEN. Inputs span the u64 wrap boundary (0, 1,u64::MAX, 2^63, 2^63−1, mixed magnitudes). Overhead calibrated:read_read=1 cycsubtracted; the caller'sbl/bxshim (5 cyc) deliberately not subtracted, so samples stay conservative.(Pleasing convergence: these are the same wrap-safe
deadline/elapsedI Kani-proved in #222 — the function is now both formally proven and timing-bounded-and-measured.)What this does NOT claim
It records
VER-OS-WCET-EVT-001and leavesVER-OS-WCET-001proposed. That artifact's acceptance is stated over every function of the trusted switch/MPU/HM object and the inner executor core — those still have no static bound at all (synth declines them loudly:reason=callneeds T3/spar composition,reason=loopneeds trip-count inference). Narrowing the artifact to match what I achieved would be moving the goalposts, so the gap is stated instead.Worst-path honesty (the subtle part)
Both functions open with a once-init guard whose byte is non-zero in the frozen
.dataimage — so a stock call never executes the store block the static bound covers (11 of 18 instructions run). Sampling only that would leave the bounded path unmeasured. The harness therefore zeroes that byte for half the samples, proves the decode at runtime before relying on it (path_variants=cold+warm), and restores it.Noted, not gated:
deadline's naive tail projection (max(block)+dispersion= 46 cyc) sits above its 42 cyc bound. The kill-criterion (observed or statistical > static) is not met, so the gate is green — but the margin is thin and the checker prints this rather than hiding it. No knob exists to turn that green; a human adjudicates.Mechanized kill-criterion
benches/gust/drivers/check-wcet-evt.pyreads bounds from the committed sidecar (never hardcoded), refuses to gate adeclinedentry rather than inventing a bound, exits 1 when an observed/statistical value exceeds the static bound, and proves its own red state via--self-test. Capture committed atsilicon/RESULTS-wcet-evt-f100.txt.rivet validatePASS.🤖 Generated with Claude Code