Benchmarks

Relevant source files

The README states that the current benchmark authority contains one attributable host-verifier campaign. Legacy Pi, QEMU and Linux numbers are archived until they are rerun with retained raw logs and artifact hashes. These programs generate measurements; they are not themselves published results.

Two benchmark binaries are installed in /bin: benchmark and verifier_bench.

benchmark

userspace/benchmarks/system prints “AXIOM BENCHMARK RESULTS” and runs two measurements. Boot time and memory footprint are printed by the kernel during boot, not here.

Step	Measurement
Benchmark 1	BPF program load time: loads a trivial program (`r0 = 42; exit`) 10 times and reports per-run, min, max and average in microseconds
Benchmark 2	Timer interrupt interval: attaches a BPF program to the timer that writes into a ringbuf, collects 100 samples, and prints a summary. Reports an incomplete collection with poll counts if fewer arrive

It uses helpers such as ktime_get_ns, get_interrupt_latency_ns, get_boot_time_ms, get_kernel_heap_kb and get_kernel_image_mb.

verifier_bench

userspace/benchmarks/verifier is the verifier-cost driver. It loads straight-line and shaped BPF programs of increasing size so that a kernel built with --features verifier-cost emits an AXIOM VERIFIER COST marker for each load. Its shapes mirror kernel_bpf::cost_corpus, so on-device cycles, the host states_explored curve and the host wall-clock curve describe the same programs.

Item	Value
Measurement sizes	10, 50, 100, 500, 1000 instructions
Calibration sizes	100 and 1000
Maximum instructions	1000
Shapes	straight-line, memory, div, ktime, map, copy, ringbuf
Execution timing	`BPF_BENCH_EXEC` (feature-gated kernel command) runs a program 64 times and emits `AXIOM EXEC COST`
Admission self-test	Attach commits utilization, so the admission gate fires at `BPF_PROG_ATTACH`

Collecting the curve


# 1. Build a separate instrumented Pi image
cargo xtask build rpi5 -- release embedded-rpi5,verifier-cost
 
# 2. Boot it, run /bin/verifier_bench, capture UART to a log
 
# 3. Parse the serial log
cargo xtask bench verifier -- verifier-cost.log \
  -o verifier-cost.csv --plot verifier-cost.png --cntfrq 54000000

scripts/benchmark/verifier-cost.py accepts a log path (or - for stdin), -o/--csv, --plot, --cntfrq (counter frequency in Hz, for microsecond conversion) and --height (abstract-domain height for the budget overlay). Marker format:


AXIOM VERIFIER COST prog_id=N insns=N states=N cycles=N [wcet=N]
AXIOM EXEC COST prog_id=N insns=N runs=N cycles=N

The script’s docstring notes the Pi 5 counter frequency is about 54 MHz; pass --cntfrq to convert cycles to microseconds. The verifier-cost feature is measurement instrumentation (off by default) and is not for production images. See Hardware-in-the-loop.