diff --git a/artifacts/gust_safety_release_line.yaml b/artifacts/gust_safety_release_line.yaml index 54a10d7..370e2c1 100644 --- a/artifacts/gust_safety_release_line.yaml +++ b/artifacts/gust_safety_release_line.yaml @@ -591,6 +591,60 @@ artifacts: - type: related-to target: DD-OS-BUILD-001 + - id: VER-OS-WCET-EVT-001 + type: sw-verification + title: "EVT cross-check of synth's static WCET against real STM32F100 DWT samples — bounds dominate on the two bounded gust:os/time functions" + method: test + status: verified + release: v0.6.0 + description: > + Partial evidence for REQ-OS-WCET-001 (track T4), covering the MEASUREMENT + half of the cross-check on the functions that actually carry a static bound + today. This artifact deliberately does NOT close VER-OS-WCET-001, whose + acceptance is stated over every function of the trusted switch/MPU/HM object + and the inner executor core — those functions still have no static bound + (synth declines them loudly: reason=call needs T3/spar inter-procedural + composition, reason=loop needs trip-count inference). Narrowing that artifact + to match what was achieved would be moving the goalposts; it stays proposed. + WHAT IS ESTABLISHED. The dissolved, frozen os-tl node + (drivers/os-node/repro-757/os-tl-fixed.o) exports two functions with sound + static bounds from synth `--emit-wcet` (schema synth-wcet-v1, cortex-m3, + zero-wait-state instruction-memory model): `gust:os/time@0.1.0#deadline` = + 42 cyc and `#elapsed` = 71 cyc. gust_wcet_evt links that exact object into an + STM32F100 image and samples both through the DWT cycle counter on REAL + silicon (n=40 each, inputs spanning the u64 wrap boundary: 0, 1, u64::MAX, + 2^63, 2^63-1 and mixed magnitudes), calibrating and subtracting the + read-to-read overhead (1 cyc) while deliberately NOT subtracting the caller's + bl/bx shim (5 cyc), so samples stay conservative. MEASURED (2026-07-28, + STM32VLDISCOVERY, openocd/ST-LINK-V1 over the Pi): + deadline n=40 min=34 max=40 mean=37 — static 42 dominates, margin 2 cyc; + elapsed n=40 min=39 max=45 mean=42 — static 71 dominates, margin 26 cyc. + The EVT block-maxima statistical bound (6 blocks) equals the observed max for + both (40 / 45): these are straight-line branch-free functions, so the sample + distribution is near-degenerate and the statistical bound is tight BY + CONSTRUCTION — it is a cross-check of the static model, not an independent + bound, and is reported as such. WORST-PATH HONESTY. Both functions open with a + once-init guard whose byte is non-zero in the frozen .data image, so a stock + call never executes the store block the static bound covers (11 of 18 + instructions execute). The harness therefore zeroes that byte for half the + samples, PROVES the decode at runtime before relying on it, and reports + path_variants=cold+warm; measuring only the default path would have left the + bounded path unmeasured. NOTED, NOT GATED: for deadline the naive tail + projection max(block)+dispersion = 46 cyc sits ABOVE the 42 cyc static bound — + the margin is thin (2 cyc) and the checker prints this rather than hiding it. + MECHANIZED. drivers/check-wcet-evt.py reads the bounds from the committed + sidecar (never hardcoded), refuses to gate a `declined` entry rather than + inventing a bound, and EXITS 1 when an observed or statistical value exceeds + the static bound — REQ-OS-WCET-001's kill-criterion made executable. Its red + state is demonstrable without hardware (`--self-test`). Kill-criterion for + THIS artifact: a DWT sample or statistical bound exceeds the static bound for + a gated function, or the runtime path-decode proof fails (harness then reports + warm-only rather than claiming worst-path coverage). + tags: [gust, os, track-t4, wcet, evt, dwt, silicon, f100, verified] + links: + - type: verifies + target: REQ-OS-WCET-001 + - id: VER-OS-WCET-001 type: sw-verification title: "Sound per-function static-WCET emission cross-checked against a statistical (EVT) bound, on the trusted object's functions" diff --git a/benches/gust/Cargo.toml b/benches/gust/Cargo.toml index 819cbce..f1aed75 100644 --- a/benches/gust/Cargo.toml +++ b/benches/gust/Cargo.toml @@ -34,6 +34,14 @@ target-f100 = [] name = "gust_adc_silicon" required-features = ["target-f100"] +# gust_wcet_evt links the frozen os-tl-fixed.o, a synth `--target cortex-m3` +# relocatable object: linking it into a thumbv7em (M4/G474RE) image silently yields +# an empty ELF, so the bin is F100/thumbv7m-only and the default target-g474re build +# must skip it (VER-OS-WCET-001 measurement half). +[[bin]] +name = "gust_wcet_evt" +required-features = ["target-f100"] + [profile.release] panic = "abort" opt-level = "z" diff --git a/benches/gust/build.rs b/benches/gust/build.rs index 66eab48..0f90fec 100644 --- a/benches/gust/build.rs +++ b/benches/gust/build.rs @@ -329,6 +329,25 @@ fn main() { println!("cargo:rerun-if-changed=iso_contain.x"); println!("cargo:rerun-if-changed=build.rs"); + // VER-OS-WCET-001 measurement half (v0.6.0 T4/D1): gust_wcet_evt DWT-samples the + // two `status: bounded` exports of the SAME frozen os-tl node whose static cycle + // bounds live in repro-757/os-tl.wcet.json (emitted by drivers/emit-wcet.sh via + // synth --emit-wcet). Linked UNPLACED (no .data rename / no iso_contain.x) — this + // bin is about timing, not the I-ISO straddle. The .o is a synth --target cortex-m3 + // object, so the bin is thumbv7m/target-f100 only (see Cargo.toml required-features). + let wcet_obj = Path::new(&manifest).join("drivers/os-node/repro-757/os-tl-fixed.o"); + if wcet_obj.exists() { + // synth#746-class guard: the two functions being timed must actually be + // DEFINED text symbols — a silently-dropped export would otherwise surface as + // a link error at best, or a bound with nothing behind it at worst. + check_defined_text_symbols( + &wcet_obj, + &["gust:os/time@0.1.0#deadline", "gust:os/time@0.1.0#elapsed"], + ); + println!("cargo:rustc-link-arg-bin=gust_wcet_evt={}", wcet_obj.display()); + println!("cargo:rerun-if-changed={}", wcet_obj.display()); + } + // The dissolved thin-seam ADC driver (drivers/adc-thin -> loom -> synth --target // cortex-m3 --all-exports --relocatable): the whole STM32F1 ADC single-conversion // path — SMPR sample-time + SQR regular-sequence config and the diff --git a/benches/gust/drivers/check-wcet-evt.py b/benches/gust/drivers/check-wcet-evt.py new file mode 100755 index 0000000..f0068e6 --- /dev/null +++ b/benches/gust/drivers/check-wcet-evt.py @@ -0,0 +1,477 @@ +#!/usr/bin/env python3 +"""check-wcet-evt.py — VER-OS-WCET-001's kill-criterion, made mechanical. + +T4 / v0.6.0 workstream D1. `REQ-OS-WCET-001` gets sound per-function STATIC cycle +bounds from synth itself (`--emit-wcet`, schema `synth-wcet-v1`; emitted + gated by +`drivers/emit-wcet.sh`). `VER-OS-WCET-001` says those bounds only count as evidence +if something can falsify them: + + "The static bound SHALL dominate both the statistical bound and every observed + raw DWT high-water-mark for that function. Kill-criterion: a function's static + bound is exceeded by its statistical bound or by an observed DWT sample [...]" + +This script is that kill-criterion as a build gate. It takes the semihosting capture +of `src/bin/gust_wcet_evt.rs` (real STM32F100 silicon, DWT CYCCNT) plus the committed +sidecar, and exits 1 if either half of the domination claim is violated. + +DIRECTION OF EVIDENCE — read this before quoting any number below. DWT measurement +may only ever FALSIFY the static model. Nothing here licenses sizing a partition +budget from a measured value; that is the standing rule in `drivers/emit-wcet.sh` and +the second half of the artifact's kill-criterion. + +WHAT THE "STATISTICAL BOUND" IS, HONESTLY. The estimator is block maxima: split the +N samples into >=5 blocks, take each block's max, report max(block maxima) — the +classical EVT block-maxima statistic. For a straight-line, branch-free function like +`gust:os/time#deadline` / `#elapsed` the per-sample distribution is DEGENERATE (the +same instruction sequence every time on an in-order, zero-wait-state core), so the +block maxima collapse onto a single value and the statistic is tight BY CONSTRUCTION +and numerically equal to the observed max. That is a real property of the code under +test, not a defect of the estimator — but it does mean this is a CROSS-CHECK of the +static model against silicon, NOT an independent statistical bound. A genuine +Gumbel/GEV tail fit needs a non-degenerate sample distribution (input-dependent +paths, caches, contention); none of those exist on this target for these functions. +The dispersion of the block maxima is reported so a reader can see this for +themselves rather than take it on trust. + +USAGE + check-wcet-evt.py CAPTURE [--sidecar PATH] gate a capture (exit 0/1) + check-wcet-evt.py - [--sidecar PATH] ... from stdin + check-wcet-evt.py --emit-sample-capture pass print a synthetic PASSING capture + check-wcet-evt.py --emit-sample-capture fail print a synthetic OVER-BOUND capture + check-wcet-evt.py --self-test demonstrate the red state; EXITS 1 + +HOW TO PRODUCE A CAPTURE + Build `src/bin/gust_wcet_evt.rs` for the F100 (see its module doc), flash the + STM32VLDISCOVERY and stream semihosting exactly as `silicon/run-adc.sh` does for + the ADC anchor, then: ... | check-wcet-evt.py - + qemu is NOT a substitute: it models no DWT, and the firmware refuses to emit + timings there rather than reporting emulated numbers. + +INPUT CONTRACT (printed by gust_wcet_evt.rs) + WCET-EVT CAL read_read= call_shim= path_variants= + WCET-EVT-SAMPLE i= cyc= path= (optional, repeated) + WCET-EVT n= min= max= mean= overhead= + WCET-EVT DONE + +Stdlib only, integer arithmetic only, no third-party dependencies. +""" + +import argparse +import json +import os +import re +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +DEFAULT_SIDECAR = os.path.join(HERE, "os-node", "repro-757", "os-tl.wcet.json") + +MIN_SAMPLES = 30 # SWREQ-MEAS-MS02: N >= 30 +MIN_BLOCKS = 5 # block-maxima needs enough blocks to be a maxima series at all + +RE_CAL = re.compile( + r"^WCET-EVT\s+CAL\s+read_read=(\d+)\s+call_shim=(\d+)\s+path_variants=(\S+)\s*$" +) +RE_SAMPLE = re.compile( + r"^WCET-EVT-SAMPLE\s+(\S+)\s+i=(\d+)\s+cyc=(\d+)\s+path=(\S+)\s*$" +) +RE_SUMMARY = re.compile( + r"^WCET-EVT\s+(?!CAL\b|DONE\b)(\S+)\s+n=(\d+)\s+min=(\d+)\s+max=(\d+)" + r"\s+mean=(\d+)\s+overhead=(\d+)\s*$" +) +RE_DONE = re.compile(r"^WCET-EVT\s+DONE\s*$") + + +# -------------------------------------------------------------------------- +# sidecar +# -------------------------------------------------------------------------- +def load_sidecar(path): + """Read synth's static bounds. Never hardcode a cycle count anywhere.""" + with open(path) as fh: + doc = json.load(fh) + if doc.get("schema") != "synth-wcet-v1": + raise SystemExit( + f"check-wcet-evt: {path}: schema {doc.get('schema')!r}, expected 'synth-wcet-v1'" + ) + return doc + + +def static_bound(doc, short_name, sidecar_path): + """Resolve a printed short name (e.g. 'deadline') to its sidecar entry. + + Matched by WIT-export suffix ('#'), which must be UNAMBIGUOUS: two + functions ending in the same name would make the bound lookup a coin flip, so + that is an error rather than a pick-the-first. + """ + hits = [f for f in doc["functions"] if f["name"].endswith("#" + short_name)] + if not hits: + hits = [f for f in doc["functions"] if f["name"] == short_name] + if len(hits) != 1: + raise SystemExit( + f"check-wcet-evt: {len(hits)} sidecar entries match '#{short_name}' in " + f"{sidecar_path} (need exactly 1): {[f['name'] for f in hits]}" + ) + fn = hits[0] + if fn.get("status") != "bounded": + raise SystemExit( + f"check-wcet-evt: sidecar entry {fn['name']} has status " + f"{fn.get('status')!r} (reason: {fn.get('reason')!r}) — there is no static " + f"bound to cross-check. Measuring it is fine; GATING it is not." + ) + return fn["name"], int(fn["cycles"]), int(fn.get("instr_count", 0)) + + +# -------------------------------------------------------------------------- +# EVT block maxima (integer, dependency-free) +# -------------------------------------------------------------------------- +def block_maxima(samples, min_blocks=MIN_BLOCKS): + """Split into as many equal blocks as possible (>= min_blocks) and return the + per-block maxima. Any remainder samples are appended to the last block so no + observation is silently dropped.""" + n = len(samples) + nblocks = min_blocks + # prefer ~sqrt(n) blocks (a common block-maxima heuristic), floored at min_blocks + k = max(min_blocks, int(n ** 0.5)) + while k > min_blocks and n // k < 2: + k -= 1 + nblocks = k if n // k >= 2 else min_blocks + size = n // nblocks + maxima = [] + for b in range(nblocks): + lo = b * size + hi = n if b == nblocks - 1 else (b + 1) * size + maxima.append(max(samples[lo:hi])) + return maxima + + +# -------------------------------------------------------------------------- +# capture parsing +# -------------------------------------------------------------------------- +def parse_capture(text): + cal = None + samples = {} + summaries = [] + done = False + for line in text.splitlines(): + line = line.strip() + m = RE_CAL.match(line) + if m: + cal = { + "read_read": int(m.group(1)), + "call_shim": int(m.group(2)), + "path_variants": m.group(3), + } + continue + m = RE_SAMPLE.match(line) + if m: + samples.setdefault(m.group(1), []).append( + {"i": int(m.group(2)), "cyc": int(m.group(3)), "path": m.group(4)} + ) + continue + m = RE_SUMMARY.match(line) + if m: + summaries.append( + { + "fn": m.group(1), + "n": int(m.group(2)), + "min": int(m.group(3)), + "max": int(m.group(4)), + "mean": int(m.group(5)), + "overhead": int(m.group(6)), + } + ) + continue + if RE_DONE.match(line): + done = True + return cal, samples, summaries, done + + +# -------------------------------------------------------------------------- +# the gate +# -------------------------------------------------------------------------- +def gate(text, sidecar_path, out=sys.stdout): + """Return 0 (pass) / 1 (fail). Every failure prints WHY and WHICH artifact + clause it violates.""" + doc = load_sidecar(sidecar_path) + cal, samples, summaries, done = parse_capture(text) + fails = [] + notes = [] + + print( + f"check-wcet-evt: VER-OS-WCET-001 cross-check\n" + f" sidecar : {sidecar_path}\n" + f" schema : {doc['schema']} core_class: {doc.get('core_class')} " + f"wait_states: {doc.get('wait_states')}\n" + f" model : {doc.get('memory_assumption')}", + file=out, + ) + + if not summaries: + print( + " FAIL: no 'WCET-EVT n=.. min=.. max=.. mean=..' line in the capture " + "— nothing to gate (truncated capture, or the firmware never ran).", + file=out, + ) + return 1 + if not done: + fails.append( + "capture has no 'WCET-EVT DONE' terminator — it is TRUNCATED, so an " + "over-bound sample could be sitting in the part that was lost" + ) + if cal is None: + notes.append( + "no 'WCET-EVT CAL' line: measurement overhead is unknown, so the " + "call-overhead attribution below is unavailable" + ) + else: + print( + f" overhead : read_read={cal['read_read']} cyc (SUBTRACTED from every " + f"sample) call_shim={cal['call_shim']} cyc (bl + bx lr; NOT subtracted " + f"— samples stay conservative)\n" + f" paths : {cal['path_variants']}", + file=out, + ) + if cal["path_variants"] != "cold+warm": + notes.append( + f"path_variants={cal['path_variants']}: the firmware could NOT force " + "the once-init store path, so the longest path the static bound " + "covers was not exercised — the cross-check is weaker than intended" + ) + + print(file=out) + for s in summaries: + short = s["fn"] + full, static, instr = static_bound(doc, short, sidecar_path) + raw = [x["cyc"] for x in sorted(samples.get(short, []), key=lambda d: d["i"])] + + # ---- sample-count / integrity checks ----------------------------- + if s["n"] < MIN_SAMPLES: + fails.append( + f"{short}: n={s['n']} < {MIN_SAMPLES} (SWREQ-MEAS-MS02 requires N>=30)" + ) + if raw and len(raw) != s["n"]: + fails.append( + f"{short}: summary says n={s['n']} but {len(raw)} WCET-EVT-SAMPLE lines " + f"were captured — the capture is inconsistent" + ) + if raw and max(raw) != s["max"]: + fails.append( + f"{short}: summary max={s['max']} disagrees with the raw samples " + f"(max={max(raw)}) — the capture is inconsistent" + ) + + # ---- the statistical (EVT block-maxima) bound --------------------- + if raw and len(raw) >= MIN_SAMPLES: + maxima = block_maxima(raw) + stat = max(maxima) + disp = max(maxima) - min(maxima) + stat_src = ( + f"block maxima over {len(maxima)} blocks of ~{len(raw)//len(maxima)}, " + f"dispersion {disp} cyc" + ) + if disp == 0: + stat_src += " (DEGENERATE: every block max identical — tight by " + stat_src += "construction, see the header)" + projected = stat + disp # informational tail headroom only; NOT gated + else: + maxima, disp = [], None + stat = s["max"] + stat_src = ( + "no raw WCET-EVT-SAMPLE lines (or n<30): falling back to the reported " + "max as a DEGENERATE stand-in — this is NOT a block-maxima estimate" + ) + projected = None + notes.append( + f"{short}: statistical bound could not be computed from raw samples; " + f"used the reported max instead" + ) + + # ---- the artifact's two domination clauses ------------------------ + obs_bad = s["max"] > static + stat_bad = stat > static + verdict = "FAIL" if (obs_bad or stat_bad) else "PASS" + print( + f" [{verdict}] {short} -> {full}\n" + f" static (synth --emit-wcet) : {static:>6} cyc " + f"({instr} instr, model-sound)\n" + f" statistical (EVT blk-max) : {stat:>6} cyc [{stat_src}]\n" + f" observed max (raw DWT) : {s['max']:>6} cyc " + f"(n={s['n']}, min={s['min']}, mean={s['mean']})\n" + f" margin static-observed : {static - s['max']:>6} cyc", + file=out, + ) + if projected is not None and disp: + flag = " (ABOVE the static bound)" if projected > static else "" + print( + f" [info, NOT gated] tail-headroom projection " + f"max(blk)+dispersion = {projected} cyc{flag}", + file=out, + ) + + if obs_bad: + msg = ( + f"{short}: observed DWT max {s['max']} > static bound {static} " + f"(+{s['max'] - static}) — VER-OS-WCET-001 kill-criterion: " + f"'a function's static bound is exceeded by [...] an observed DWT sample'" + ) + if cal and 0 < s["max"] - static <= cal["call_shim"]: + msg += ( + f"\n ATTRIBUTION: the exceedance ({s['max'] - static}) is " + f"<= the calibrated call_shim overhead ({cal['call_shim']} cyc). " + f"Reported samples still contain the caller's `bl`, which is NOT " + f"part of the callee's static bound. This may be measurement " + f"attribution rather than an unsound bound — it is reported, not " + f"absorbed: the gate stays RED for a human to adjudicate." + ) + fails.append(msg) + if stat_bad and not obs_bad: + fails.append( + f"{short}: statistical bound {stat} > static bound {static} — " + f"VER-OS-WCET-001 kill-criterion: 'a function's static bound is " + f"exceeded by its statistical bound'" + ) + print(file=out) + + for n in notes: + print(f" note: {n}", file=out) + if notes: + print(file=out) + + if fails: + print("check-wcet-evt: GATE RED — VER-OS-WCET-001 kill-criterion met:", file=out) + for f in fails: + print(f" * {f}", file=out) + return 1 + + print( + "check-wcet-evt: GATE GREEN — the static bound dominates both the statistical " + "bound and every observed raw DWT sample, for every gated function.\n" + " Reminder: this cross-checks the static model; it does NOT license sizing " + "any partition budget from a measured value.", + file=out, + ) + return 0 + + +# -------------------------------------------------------------------------- +# synthetic captures (fixtures for the oracles, and for --self-test) +# -------------------------------------------------------------------------- +def synth_capture(mode, sidecar_path): + """Build a synthetic capture from the REAL sidecar bounds. + + 'pass' sits a fixed margin under each static bound; 'fail' pushes exactly one + sample of one function one cycle over it. Neither hardcodes a cycle count — + both are derived from the sidecar, so the fixtures stay correct if synth's + model changes. + """ + doc = load_sidecar(sidecar_path) + lines = ["gust-wcet-evt: SYNTHETIC capture (%s) — NOT a silicon measurement" % mode] + lines.append("WCET-EVT CAL read_read=2 call_shim=7 path_variants=cold+warm") + n = 40 + for short in ("deadline", "elapsed"): + _full, static, _instr = static_bound(doc, short, sidecar_path) + base = max(1, static - 5) + vals = [] + for i in range(n): + # A small deterministic ripple so min/mean/max are distinct. NOTE the + # block maxima still come out degenerate — which is exactly what real + # silicon looks like for these functions, so the fixture is faithful. + vals.append(base + (i % 3)) + if mode == "fail" and short == "deadline": + vals[17] = static + 1 # one sample, one cycle over: the kill-criterion + for i, v in enumerate(vals): + lines.append( + "WCET-EVT-SAMPLE %s i=%d cyc=%d path=%s" + % (short, i, v, "cold" if i < n // 2 else "warm") + ) + lines.append( + "WCET-EVT %s n=%d min=%d max=%d mean=%d overhead=2" + % (short, n, min(vals), max(vals), sum(vals) // len(vals)) + ) + lines.append("WCET-EVT DONE") + return "\n".join(lines) + "\n" + + +def self_test(sidecar_path): + """Prove the gate can go RED without hardware. + + Runs the PASSING fixture (must be green) and then the OVER-BOUND fixture (must + be red), and EXITS 1 BY DESIGN so the red state is directly observable in the + oracle transcript. Exit 2 means the self-test itself is broken. + """ + print("=" * 78) + print("check-wcet-evt --self-test: case 1/2 — synthetic PASSING capture") + print("=" * 78) + rc_pass = gate(synth_capture("pass", sidecar_path), sidecar_path) + print() + if rc_pass != 0: + print( + "check-wcet-evt SELF-TEST BROKEN: the passing fixture did not go green " + f"(rc={rc_pass}); the gate cannot be trusted in either direction." + ) + return 2 + + print("=" * 78) + print( + "check-wcet-evt --self-test: case 2/2 — synthetic OVER-BOUND capture\n" + "(one deadline sample = static bound + 1; this MUST go red)" + ) + print("=" * 78) + rc_fail = gate(synth_capture("fail", sidecar_path), sidecar_path) + print() + if rc_fail != 1: + print( + "check-wcet-evt SELF-TEST BROKEN: the over-bound fixture did NOT go red " + f"(rc={rc_fail}) — the kill-criterion is not wired up." + ) + return 2 + + print( + "check-wcet-evt --self-test: OK — passing fixture green (exit 0), over-bound " + "fixture red (exit 1).\n" + "Exiting 1 BY DESIGN: --self-test reports the demonstrated RED verdict, so a " + "nonzero exit here is the expected, correct result." + ) + return 1 + + +def main(argv=None): + ap = argparse.ArgumentParser( + description=( + "VER-OS-WCET-001 cross-check: fail if a measured or EVT-statistical " + "bound exceeds synth's static bound." + ), + formatter_class=argparse.RawDescriptionHelpFormatter, + epilog=__doc__, + ) + ap.add_argument( + "capture", + nargs="?", + help="semihosting capture from gust_wcet_evt ('-' for stdin)", + ) + ap.add_argument("--sidecar", default=DEFAULT_SIDECAR, help="synth-wcet-v1 JSON") + ap.add_argument( + "--self-test", + action="store_true", + help="demonstrate the gate's red state without hardware; EXITS 1 BY DESIGN", + ) + ap.add_argument( + "--emit-sample-capture", + choices=("pass", "fail"), + help="print a synthetic capture (derived from the sidecar) and exit 0", + ) + args = ap.parse_args(argv) + + if args.emit_sample_capture: + sys.stdout.write(synth_capture(args.emit_sample_capture, args.sidecar)) + return 0 + if args.self_test: + return self_test(args.sidecar) + if not args.capture: + ap.error("a CAPTURE path (or '-') is required unless --self-test/--emit-sample-capture") + + text = sys.stdin.read() if args.capture == "-" else open(args.capture).read() + return gate(text, args.sidecar) + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/benches/gust/silicon/RESULTS-wcet-evt-f100.txt b/benches/gust/silicon/RESULTS-wcet-evt-f100.txt new file mode 100644 index 0000000..d23f41b --- /dev/null +++ b/benches/gust/silicon/RESULTS-wcet-evt-f100.txt @@ -0,0 +1,115 @@ +Open On-Chip Debugger 0.12.0+dev-snapshot (2026-02-16-16:07) +Licensed under GNU GPL v2 +For bug reports, read + http://openocd.org/doc/doxygen/bugs.html +DEPRECATED: OpenOCD support for ST-Link HLA transport will be dropped soon! +Consider updating your ST-Link firmware to a version >= V2J24 (2015) +Warn : DEPRECATED: auto-selecting transport "swd (hla)". Use 'transport select swd' to suppress this message. +Info : The selected transport took over low-level target control. The results might differ compared to plain JTAG/SWD +Info : clock speed 1000 kHz +Info : STLINK V1J13S0 (API v2) VID:PID 0483:3744 +Error: SRST error +Info : [stm32f1x.cpu] Cortex-M3 r1p1 processor detected +Info : [stm32f1x.cpu] target has 6 breakpoints, 4 watchpoints +Info : [stm32f1x.cpu] Examination succeed +Info : [stm32f1x.cpu] starting gdb server on 3333 +Info : Listening on port 3333 for gdb connections +[stm32f1x.cpu] halted due to debug-request, current mode: Thread +xPSR: 0x01000000 pc: 0x08000400 msp: 0x20002000 +semihosting is enabled +[stm32f1x.cpu] halted due to debug-request, current mode: Thread +xPSR: 0x01000000 pc: 0x08000400 msp: 0x20002000, semihosting +** Programming Started ** +Info : device id = 0x10016420 +Info : flash size = 128 KiB +Warn : Adding extra erase range, 0x08002478 .. 0x080027ff +** Programming Finished ** +** Verify Started ** +** Verified OK ** +gust-wcet-evt: DWT cycle sampling of the DISSOLVED gust:os/time exports on real STM32F100 silicon (VER-OS-WCET-001 measurement half; static bounds come from drivers/os-node/repro-757/os-tl.wcet.json, checked by drivers/check-wcet-evt.py) +# correctness: deadline==now+ticks, elapsed==now>=deadline over 20 pairs — IDENTICAL ok +# worst-path: once-init guard __synth_wasm_seg_2+12 @ 0x20000024 — store path REACHABLE (decode proven) +WCET-EVT CAL read_read=1 call_shim=5 path_variants=cold+warm +WCET-EVT-SAMPLE deadline i=0 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=1 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=2 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=3 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=4 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=5 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=6 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=7 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=8 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=9 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=10 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=11 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=12 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=13 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=14 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=15 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=16 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=17 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=18 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=19 cyc=40 path=cold +WCET-EVT-SAMPLE deadline i=20 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=21 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=22 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=23 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=24 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=25 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=26 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=27 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=28 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=29 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=30 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=31 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=32 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=33 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=34 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=35 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=36 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=37 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=38 cyc=34 path=warm +WCET-EVT-SAMPLE deadline i=39 cyc=34 path=warm +WCET-EVT deadline n=40 min=34 max=40 mean=37 overhead=1 +WCET-EVT-SAMPLE elapsed i=0 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=1 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=2 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=3 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=4 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=5 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=6 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=7 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=8 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=9 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=10 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=11 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=12 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=13 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=14 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=15 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=16 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=17 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=18 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=19 cyc=45 path=cold +WCET-EVT-SAMPLE elapsed i=20 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=21 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=22 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=23 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=24 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=25 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=26 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=27 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=28 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=29 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=30 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=31 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=32 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=33 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=34 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=35 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=36 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=37 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=38 cyc=39 path=warm +WCET-EVT-SAMPLE elapsed i=39 cyc=39 path=warm +WCET-EVT elapsed n=40 min=39 max=45 mean=42 overhead=1 +WCET-EVT DONE diff --git a/benches/gust/src/bin/gust_wcet_evt.rs b/benches/gust/src/bin/gust_wcet_evt.rs new file mode 100644 index 0000000..53f18dc --- /dev/null +++ b/benches/gust/src/bin/gust_wcet_evt.rs @@ -0,0 +1,477 @@ +//! gust-wcet-evt — DWT cycle sampling of two DISSOLVED functions, for the +//! measurement side of `VER-OS-WCET-001` (v0.6.0 track T4, workstream D1). +//! +//! `REQ-OS-WCET-001` gets its static per-function cycle bounds from synth itself +//! (`--emit-wcet`, schema `synth-wcet-v1` — see `drivers/emit-wcet.sh`). Those +//! bounds are only *evidence* if something can falsify them. `VER-OS-WCET-001` +//! says how: the static bound SHALL dominate both a measurement-based statistical +//! (EVT) bound and every observed raw DWT sample, and its kill-criterion is +//! exactly the negation of that. This firmware is the measurement half; the gate +//! half is `drivers/check-wcet-evt.py`, which consumes the lines printed below. +//! +//! DIRECTION OF EVIDENCE (this is not a budget source): DWT numbers here may only +//! ever FALSIFY the static model. No partition budget is, or may be, sized from a +//! raw DWT high-water-mark — see the standing rule in `drivers/emit-wcet.sh`. +//! +//! ## What is measured +//! The frozen dissolved node `drivers/os-node/repro-757/os-tl-fixed.o` (synth +//! 0.45.1 dissolve of the archived `repro-757/loom.wasm`; the same object the +//! I-ISO no-fault control links) exports two functions the sidecar reports as +//! `status: bounded`: +//! +//! gust:os/time@0.1.0#deadline (now: u64, ticks: u64) -> u64 now + ticks +//! gust:os/time@0.1.0#elapsed (now: u64, deadline: u64) -> u32 now >= deadline +//! +//! Both are straight-line and branch-free *in their arithmetic*, so the sample +//! distribution is near-degenerate by construction — this is a cross-check of the +//! static model against silicon, NOT an independent statistical bound. The checker +//! says so in its own output too. +//! +//! ## The one data-dependent branch, and why the harness pokes .data +//! Each function opens with a once-init guard the dissolve emitted: +//! +//! ldr.w r5, [pc, #..] @ literal = R_ARM_ABS32 __synth_wasm_seg_2 + 0xc +//! ldrb r5, [r6, #0] +//! cmp r5, #0 +//! bne.n @ taken -> SHORT path (11 instrs) +//! ... strb.w r8, [r4] @ untaken-> STORE path (17-18 instrs) +//! +//! In the frozen `.data` image that guard byte (`__synth_wasm_seg_2 + 12`, i.e. +//! `.data + 0x24`) holds `0x3a` (it overlaps the `"gust:os up\n"` literal), so on +//! a stock run the branch is ALWAYS taken and the store path is never executed. +//! The sidecar's `instr_count: 18` shows the static bound covers the STORE path — +//! so sampling only the short path would leave the worst path unmeasured, i.e. +//! would make the cross-check weaker than the artifact asks for. +//! +//! So this harness samples BOTH: for the `cold` half of the samples it zeroes that +//! guard byte first (making the branch fall through into the store), for the `warm` +//! half it leaves it alone. `preflight_guard()` PROVES the decode above on the real +//! object at runtime (byte reads 0x3a; after zeroing it and calling `deadline` it +//! reads 0x01) before any of this is relied on — if that fails the run degrades to +//! warm-only sampling and says so, rather than silently claiming worst-path +//! coverage. The byte is restored to `0x3a` at the end. Nothing else in the object +//! is touched, and neither `#now`/`#line`/`run` (the functions that read that +//! string) are called. +//! +//! ## Measurement overhead +//! `read_read` = the cycle delta of two back-to-back CYCCNT reads with NOTHING +//! between them; it is subtracted from every sample, so a reported sample is the +//! call's own cycles. `call_shim` = the delta across a `bl` to a bare `bx lr` — +//! reported but NOT subtracted, so every reported sample stays CONSERVATIVE (it +//! still contains the caller's `bl` and argument marshalling). If a sample lands +//! above its static bound by less than `call_shim`, the checker annotates that +//! attribution instead of hiding it. +//! +//! ## Output contract (parsed by drivers/check-wcet-evt.py) +//! WCET-EVT CAL read_read= call_shim= path_variants= +//! WCET-EVT-SAMPLE i= cyc= path= +//! WCET-EVT n= min= max= mean= overhead= +//! WCET-EVT DONE +//! +//! ## Build +//! F100 / thumbv7m only — the object is a synth `--target cortex-m3` .o and linking +//! it into a thumbv7em image silently yields an empty ELF, so the bin carries +//! `required-features = ["target-f100"]` and the default g474 build skips it: +//! cd benches/gust && cp targets/generated/memory-stm32f100.x memory.x && +//! cargo build --release --bin gust_wcet_evt --no-default-features \ +//! --features target-f100 --target thumbv7m-none-eabi +//! Flash + capture is the coordinator's job; this file never assumes a number. +//! Model the flash/capture step on `silicon/run-adc.sh` (same board, same +//! ST-LINK/V1-over-Pi path), then pipe the capture to +//! `drivers/check-wcet-evt.py -`. +//! +//! ## Pre-silicon smoke test (no board needed) +//! `main` runs the two OBJECT-level gates BEFORE touching the DWT, so a plain +//! `cargo run` on the committed (qemu lm3s6965evb) `memory.x` exercises everything +//! except the timing itself. qemu models no DWT, so it stops at step 3 — which is +//! the correct behaviour, not a bug: +//! # correctness: deadline==now+ticks, elapsed==now>=deadline over 20 pairs — IDENTICAL ok +//! # worst-path: once-init guard __synth_wasm_seg_2+12 @ 0x20000024 — store path REACHABLE (decode proven) +//! gust-wcet-evt FAIL: DWT cycle counter unavailable or not advancing (DEMCR=0x00000000 ...) +#![no_std] +#![no_main] + +use core::hint::black_box; +use core::ptr::{addr_of, read_volatile, write_volatile}; +use cortex_m_rt::entry; +use cortex_m_semihosting::{debug, hprintln}; +use panic_halt as _; + +#[cfg(not(feature = "target-f100"))] +compile_error!( + "gust_wcet_evt: build with --no-default-features --features target-f100 --target \ + thumbv7m-none-eabi (os-tl-fixed.o is a synth --target cortex-m3 relocatable object; \ + linking it into a thumbv7em/M4 image silently produces an empty ELF)" +); +#[cfg(feature = "target-f100")] +#[path = "../../targets/generated/gust_target_stm32f100.rs"] +#[allow(dead_code)] +mod target; +use target::BOARD; + +// --------------------------------------------------------------------------- +// The dissolved node's imports. `read32`/`write32` are the ONLY undefined symbols +// in os-tl-fixed.o; they are reached from `#now` / `#line` / `run`, none of which +// this firmware calls. They exist so the object links, and are deliberately inert. +// --------------------------------------------------------------------------- +#[no_mangle] +pub extern "C" fn read32(addr: u32) -> u32 { + unsafe { read_volatile(addr as *const u32) } +} +#[no_mangle] +pub extern "C" fn write32(addr: u32, val: u32) { + unsafe { write_volatile(addr as *mut u32, val) } +} + +extern "C" { + // Exact mangled WIT export names, verbatim from `arm-none-eabi-nm` on the object. + #[link_name = "gust:os/time@0.1.0#deadline"] + fn wcet_deadline(now: u64, ticks: u64) -> u64; + #[link_name = "gust:os/time@0.1.0#elapsed"] + fn wcet_elapsed(now: u64, deadline: u64) -> u32; + // Start of the object's third data segment — the once-init guard byte lives at + // +12 (see the module comment; proven at runtime by preflight_guard()). + static __synth_wasm_seg_2: u8; + // Bare `bl`-able `bx lr`, for the call-overhead calibration. + fn wcet_call_shim(); +} + +core::arch::global_asm!( + ".section .text.wcet_call_shim", + ".global wcet_call_shim", + ".thumb_func", + "wcet_call_shim:", + " bx lr", +); + +// --------------------------------------------------------------------------- +// DWT cycle counter (Cortex-M3, ARMv7-M ARM C1.8). Raw registers rather than the +// cortex-m PAC wrapper so the enable sequence and the CYCCNT zeroing are explicit. +// --------------------------------------------------------------------------- +const DEMCR: *mut u32 = 0xE000_EDFC as *mut u32; +const DEMCR_TRCENA: u32 = 1 << 24; +const DWT_CTRL: *mut u32 = 0xE000_1000 as *mut u32; +const DWT_CTRL_CYCCNTENA: u32 = 1 << 0; +const DWT_CTRL_NOCYCCNT: u32 = 1 << 25; // RO: 1 = no cycle counter implemented +const DWT_CYCCNT: *mut u32 = 0xE000_1004 as *mut u32; + +#[inline(always)] +fn cyc() -> u32 { + unsafe { read_volatile(DWT_CYCCNT as *const u32) } +} + +/// Enable TRCENA, then CYCCNTENA, then zero CYCCNT. Returns false if the part has +/// no cycle counter or the counter does not actually advance. +fn dwt_enable() -> bool { + unsafe { + write_volatile(DEMCR, read_volatile(DEMCR) | DEMCR_TRCENA); + if read_volatile(DWT_CTRL) & DWT_CTRL_NOCYCCNT != 0 { + return false; + } + write_volatile(DWT_CYCCNT, 0); + write_volatile(DWT_CTRL, read_volatile(DWT_CTRL) | DWT_CTRL_CYCCNTENA); + } + // Liveness: the counter must advance. + let a = cyc(); + for _ in 0..16 { + cortex_m::asm::nop(); + } + cyc() != a +} + +// --------------------------------------------------------------------------- +// Inputs. Wrap-boundary heavy, per SWREQ-MEAS-MS02's "varied input set": both +// functions are 64-bit and their only interesting silicon behaviour is the +// adds/adc and cmp/sbcs carry chain, so the set is built around 0, 1, 2^63, +// 2^63-1, 2^32, u64::MAX and mixed small/large pairs. +// `static` + read_volatile so nothing is constant-folded into the call site. +// --------------------------------------------------------------------------- +const NIN: usize = 20; +static INPUTS: [(u64, u64); NIN] = [ + (0, 0), + (0, 1), + (1, 0), + (1, 1), + (u64::MAX, 1), + (1, u64::MAX), + (u64::MAX, u64::MAX), + (u64::MAX - 1, 1), + (1 << 63, 1 << 63), + ((1u64 << 63) - 1, 1), + (1, (1u64 << 63) - 1), + ((1u64 << 63) - 1, (1u64 << 63) - 1), + (0, u64::MAX), + (u64::MAX, 0), + (0x0000_0000_FFFF_FFFF, 1), + (1, 0x0000_0000_FFFF_FFFF), + (0xFFFF_FFFF_0000_0000, 0x0000_0001_0000_0000), + (12_345, 67_890), + (0xDEAD_BEEF_CAFE_BABE, 0x0123_4567_89AB_CDEF), + (u64::MAX - 1, u64::MAX - 1), +]; + +/// N = 2 passes over the input set (pass 0 = cold/worst path, pass 1 = warm). +/// 40 >= the N>=30 the measurement framework requires, and gives the checker's +/// block-maxima estimator 6 blocks of ~6 (it needs >= 5). +const NSAMP: usize = 2 * NIN; + +static mut CYC_DEADLINE: [u32; NSAMP] = [0; NSAMP]; +static mut CYC_ELAPSED: [u32; NSAMP] = [0; NSAMP]; + +// The once-init guard byte inside the object's data (see module comment). +const GUARD_OFF: usize = 12; +const GUARD_FROZEN: u8 = 0x3a; // ':' of "gust:os up\n" in the frozen .data image + +#[inline(always)] +fn guard_ptr() -> *mut u8 { + unsafe { (addr_of!(__synth_wasm_seg_2) as *mut u8).add(GUARD_OFF) } +} + +// --------------------------------------------------------------------------- +// Measurement primitives. `#[inline(never)]` so every sample of a given function +// goes through ONE identical instruction sequence; the arguments are forced into +// registers with black_box before the first CYCCNT read so argument marshalling +// is not charged to the callee. +// --------------------------------------------------------------------------- +// The result is consumed with `black_box` (a zero-instruction compiler barrier) +// rather than a volatile store: a store would need its destination address +// materialised from the literal pool AFTER the call, i.e. INSIDE the measurement +// window, charging 2-3 phantom cycles to the callee. Verified in the linked +// disassembly: the only instructions between the two `ldr rN, [DWT_CYCCNT]` are +// the `bl` itself. +#[inline(never)] +fn measure_deadline(now: u64, ticks: u64) -> u32 { + let now = black_box(now); + let ticks = black_box(ticks); + let t0 = cyc(); + let r = unsafe { wcet_deadline(now, ticks) }; + let t1 = cyc(); + let _ = black_box(r); + t1.wrapping_sub(t0) +} + +#[inline(never)] +fn measure_elapsed(now: u64, deadline: u64) -> u32 { + let now = black_box(now); + let deadline = black_box(deadline); + let t0 = cyc(); + let r = unsafe { wcet_elapsed(now, deadline) }; + let t1 = cyc(); + let _ = black_box(r); + t1.wrapping_sub(t0) +} + +#[inline(never)] +fn measure_call_shim() -> u32 { + let t0 = cyc(); + unsafe { wcet_call_shim() }; + let t1 = cyc(); + t1.wrapping_sub(t0) +} + +/// Two back-to-back CYCCNT reads with nothing between: the irreducible cost of +/// the measurement itself. Minimum over repeats (the M3 is in-order and this is +/// deterministic; the min is the un-perturbed value). +fn calibrate_read_read() -> u32 { + let mut best = u32::MAX; + for _ in 0..64 { + let a = cyc(); + let b = cyc(); + let d = b.wrapping_sub(a); + if d < best { + best = d; + } + } + best +} + +fn calibrate_call_shim(read_read: u32) -> u32 { + let mut best = u32::MAX; + for _ in 0..64 { + let d = measure_call_shim(); + if d < best { + best = d; + } + } + best.saturating_sub(read_read) +} + +// --------------------------------------------------------------------------- +// Correctness gate: the thing being timed must be the thing that is specified. +// deadline(now, ticks) == now.wrapping_add(ticks); elapsed(now, dl) == now >= dl. +// --------------------------------------------------------------------------- +fn correctness_gate() -> u32 { + let mut bad = 0u32; + for i in 0..NIN { + let (now, arg) = INPUTS[i]; + let got_d = unsafe { wcet_deadline(black_box(now), black_box(arg)) }; + if got_d != now.wrapping_add(arg) { + bad += 1; + } + let got_e = unsafe { wcet_elapsed(black_box(now), black_box(arg)) }; + if got_e != u32::from(now >= arg) { + bad += 1; + } + } + bad +} + +/// Prove the once-init guard decode on the real object before relying on it: +/// the byte must read `0x3a` in the frozen image, and after zeroing it a call to +/// `#deadline` must set it to `0x01` (the `strb` in the store path). Returns true +/// only if BOTH hold, i.e. only if zeroing really does select the worst path. +fn preflight_guard() -> bool { + let p = guard_ptr(); + unsafe { + if read_volatile(p) != GUARD_FROZEN { + return false; + } + write_volatile(p, 0); + let _ = wcet_deadline(black_box(7), black_box(9)); + read_volatile(p) == 1 + } +} + +fn stats(s: &[u32]) -> (u32, u32, u32) { + let mut mn = u32::MAX; + let mut mx = 0u32; + let mut sum = 0u64; + for &v in s { + if v < mn { + mn = v; + } + if v > mx { + mx = v; + } + sum += v as u64; + } + (mn, mx, (sum / s.len() as u64) as u32) +} + +#[entry] +fn main() -> ! { + let _ = hprintln!( + "gust-wcet-evt: DWT cycle sampling of the DISSOLVED gust:os/time exports on real \ + {} silicon (VER-OS-WCET-001 measurement half; static bounds come from \ + drivers/os-node/repro-757/os-tl.wcet.json, checked by drivers/check-wcet-evt.py)", + BOARD + ); + + // ORDER MATTERS. The two OBJECT-level gates below need no cycle counter, so + // they run FIRST: that makes a plain `cargo run` under qemu lm3s6965evb a real + // pre-silicon smoke test of everything except the timing (does the object link + // and run? does it still compute the right answers? does the worst-path poke + // still decode?), and only the DWT step is silicon-gated. + + // --- 1. correctness gate: time the thing the bound is actually about ---- + let bad = correctness_gate(); + if bad != 0 { + let _ = hprintln!( + "gust-wcet-evt FAIL: {} functional mismatch(es) over the {} input pairs — refusing \ + to report timings for code that does not compute what the bound is about", + bad, + NIN + ); + debug::exit(debug::EXIT_FAILURE); + loop {} + } + let _ = hprintln!("# correctness: deadline==now+ticks, elapsed==now>=deadline over {} pairs — IDENTICAL ok", NIN); + + // --- 2. worst-path availability ---------------------------------------- + // NOTE: correctness_gate() above already called #deadline; with the frozen + // guard byte the store path is skipped, but restore it anyway so the decode + // proof below starts from the exact frozen image. + unsafe { write_volatile(guard_ptr(), GUARD_FROZEN) }; + let cold_ok = preflight_guard(); + let _ = hprintln!( + "# worst-path: once-init guard __synth_wasm_seg_2+{} @ {:?} — store path {}", + GUARD_OFF, + guard_ptr(), + if cold_ok { "REACHABLE (decode proven)" } else { "NOT reachable" } + ); + + // --- 3. DWT: the only silicon-gated step -------------------------------- + if !dwt_enable() { + // Loud + diagnosable: this is the guard that stops the harness inventing + // zeros on a part (or an emulator) with no working cycle counter. qemu's + // lm3s6965evb hits this path, which is correct — icount is not silicon. + let _ = hprintln!( + "gust-wcet-evt FAIL: DWT cycle counter unavailable or not advancing \ + (DEMCR=0x{:08x} DWT_CTRL=0x{:08x} CYCCNT=0x{:08x}) — refusing to report \ + timings; VER-OS-WCET-001 needs real silicon, not an emulated counter", + unsafe { read_volatile(DEMCR as *const u32) }, + unsafe { read_volatile(DWT_CTRL as *const u32) }, + cyc() + ); + debug::exit(debug::EXIT_FAILURE); + loop {} + } + + // --- 4. calibration ----------------------------------------------------- + let read_read = calibrate_read_read(); + let call_shim = calibrate_call_shim(read_read); + let _ = hprintln!( + "WCET-EVT CAL read_read={} call_shim={} path_variants={}", + read_read, + call_shim, + if cold_ok { "cold+warm" } else { "warm-only" } + ); + if !cold_ok { + let _ = hprintln!( + "# NOTE: once-init guard decode did NOT hold on this object (expected \ + __synth_wasm_seg_2+{}==0x{:02x}, and 0x01 after a zeroed call) — sampling the \ + SHORT path only; the store path the static bound covers is NOT exercised.", + GUARD_OFF, + GUARD_FROZEN + ); + } + + // --- 5. sampling -------------------------------------------------------- + // pass 0 = cold (guard zeroed before each call -> store path taken, the path + // the sidecar's instr_count=18 corresponds to); pass 1 = warm (stock guard). + for pass in 0..2usize { + for i in 0..NIN { + let (now, arg) = INPUTS[i]; + let idx = pass * NIN + i; + + if pass == 0 && cold_ok { + unsafe { write_volatile(guard_ptr(), 0) }; + } + let d = measure_deadline(now, arg); + unsafe { CYC_DEADLINE[idx] = d.saturating_sub(read_read) }; + + if pass == 0 && cold_ok { + unsafe { write_volatile(guard_ptr(), 0) }; + } + let e = measure_elapsed(now, arg); + unsafe { CYC_ELAPSED[idx] = e.saturating_sub(read_read) }; + } + } + // Leave the object's data exactly as the frozen image has it. + unsafe { write_volatile(guard_ptr(), GUARD_FROZEN) }; + + // --- 6. report ---------------------------------------------------------- + for (name, arr) in [ + ("deadline", unsafe { &*addr_of!(CYC_DEADLINE) }), + ("elapsed", unsafe { &*addr_of!(CYC_ELAPSED) }), + ] { + for i in 0..NSAMP { + let path = if i < NIN && cold_ok { "cold" } else { "warm" }; + let _ = hprintln!("WCET-EVT-SAMPLE {} i={} cyc={} path={}", name, i, arr[i], path); + } + let (mn, mx, mean) = stats(arr); + let _ = hprintln!( + "WCET-EVT {} n={} min={} max={} mean={} overhead={}", + name, + NSAMP, + mn, + mx, + mean, + read_read + ); + } + let _ = hprintln!("WCET-EVT DONE"); + + debug::exit(debug::EXIT_SUCCESS); + loop {} +}