Current Results
Relevant source files
- docs/performance/current-results.md
- docs/performance/evidence/2ef74f0/manifest.toml
- docs/performance/evidence/2ef74f0/verifier-host.log
- docs/performance/evidence/hil-v03-20260724/README.md
- docs/performance/evidence/hil-v03-20260724/provisional.toml
- kernel/crates/kernel_bpf/benches/verifier.rs
- scripts/hil/v03b-reduce.py
There is exactly one attributable campaign today: a host-side benchmark of the BPF verifier. Everything else is either a provisional hardware observation or historical. Read the evidence policy first.
Attributable: host BPF verifier at 2ef74f0
| Field | Value |
|---|---|
| Source | 2ef74f0d43b6beeebf24e984d7b8c74ad1b27e8f |
| Date | 2026-07-17 |
| Toolchain | nightly-2026-07-02, rustc 1.98.0-nightly (4c9d2bfe4 2026-07-01) |
| Host | Linux 7.0.9 x86_64, AMD Ryzen 7 7735HS, 16 logical CPUs |
| Command | CARGO_TERM_COLOR=never cargo bench --locked -p kernel_bpf --bench verifier --features embedded-profile |
Criterion, 100 samples per group after warm-up; values are the reported 95% confidence intervals for verification time.
| Benchmark | 95% CI |
|---|---|
| minimal program | 943.28 to 945.39 ns |
| arithmetic program | 1.6903 to 1.6936 µs |
| 10 instructions | 3.1151 to 3.1216 µs |
| 50 instructions | 15.257 to 15.293 µs |
| 100 instructions | 31.437 to 31.465 µs |
| 500 instructions | 180.98 to 183.22 µs |
| 1000 instructions | 376.43 to 379.28 µs |
| linear control flow | 1.9926 to 1.9994 µs |
| one branch | 2.3288 to 2.3420 µs |
| multiple branches | 3.3792 to 3.3837 µs |
This is a single unpinned developer-host run, not a latency objective and not a cross-machine comparison. Criterion’s change annotations (versus an untracked local baseline) are not part of the claim. The roughly linear growth with instruction count is consistent with the bounded-fragment argument, but the campaign measures time on one host, not the state-count bound itself.
Provisional: Raspberry Pi 5 v0.3 HIL (2026-07-24)
Retained for engineering use only. Every deployed-image record says worktree_dirty = true, and clean rebuilds of later commits produced different kernel8.img hashes, so these binaries cannot be tied to exact source commits.
| Field | Value |
|---|---|
| Hardware | Raspberry Pi 5 (8 GB, RP1); Shrike-Lite GPIO22 stimulus; fx2lafw logic analyzer at 24 MHz; Pi Debug Probe UART |
| Boundary | GPIO23 sensor edge, verified BPF reflex, ARM-A monitor, GPIO12 GPIO-level actuation |
| Timebase | on-chip CNTVCT_EL0, converted with CNTFRQ_EL0 |
| Reduction | python3 scripts/hil/v03b-reduce.py --warmup 16 latency-smoke-uart.log latency-main-uart.log (two cold boots, 16 warm-up samples dropped from each, nearest-rank percentiles) |
| Metric | n | median | p95 | p99 | p99.9 | max | target | result |
|---|---|---|---|---|---|---|---|---|
| M-A monitor decision overhead | 10,164 | 37 ns | 55 ns | 55 ns | 55 ns | 55 ns | under 5 µs | target met (provisional) |
| M-C IRQ entry to actuate, software path | 10,162 | 4.500 µs | 5.462 µs | 5.481 µs | 5.500 µs | 6.888 µs | under 1 µs | target failed |
- M-C meets its sample count but not its latency target: the median is 4.5 times the 1 µs target.
- One GPIO23-rising to GPIO12-falling analyzer sample measured 9.25 µs; it validates the rig only and is not a distribution.
- V03-C logged
PI5_V03C n=1000 escapes=0 safed=450, a successful provisional observation, not an acceptance result. - V03-D (physical e-stop edge to output low, N of at least 100) has not run.
- No hardware-PWM latency is claimed: output was GPIO-level because RP1
clk_pwm0bring-up is unresolved.
Historical claims and their disposition
| Legacy campaign | Disposition |
|---|---|
| QEMU x86 boot, BPF-load and timer numbers | Invalid as timing evidence: the H-02 HPET tick-to-nanosecond conversion was wrong, and no raw capture or hash was kept |
Pi 5 boot, memory, BPF and interrupt numbers at bedc93c | Historical only: commit and hardware named, but no UART capture or artifact hash |
| Raspberry Pi OS / Linux comparison | Historical only: no raw dmesg, cyclictest, binary or hashes |
| 2026-06 host verifier table | Superseded by 2ef74f0 |
| Pi 5 verifier/WCET calibration and admission tables | Historical only: UART text not committed, kernel artifact not hashed |
| ARM-A monitor and GPIO latency | Provisional (above): dirty deployed image prevents promotion |
The README’s interpreter and JIT per-instruction figures (about 50 ns per instruction interpreted on x86_64, under 5 ns JIT overhead) predate this contract and are not backed by an attributable campaign; shipped profiles do not use a JIT at all (ADR-0004).
What would make new RT claims credible
Per the README, multi-core real-time claims need the per-CPU run-queue work (#57), a 24-hour soak with P99 and P99.9 histograms (#74), and attributable comparisons against Zephyr, NuttX or Linux PREEMPT_RT (#78), all captured under the evidence contract.