# BPF Verifier
The verifier pipeline boots a scheduler in a KVM VM and captures
per-program verifier statistics from the real kernel verifier.
## Design
The verifier pipeline follows ktstr's two core principles.
**Fidelity without overhead.** The scheduler binary runs inside a VM
on the same kernel the scheduler will run on in production. The
verifier that runs is the real verifier in the real kernel -- no
host-side BPF loading, no version skew between the host kernel's
verifier and the target kernel's verifier.
**Direct access over tooling layers.** No subprocess to bpftool or
veristat. The host reads per-program `verified_insns` directly from
guest memory via `bpf_prog_aux` introspection and applies cycle
collapse to verifier logs instead of truncating.
## Quick start
### CLI (via cargo-ktstr)
```sh
cargo ktstr verifier --scheduler scx_rustland
cargo ktstr verifier --scheduler scx_rustland --all-profiles
```
See [cargo-ktstr verifier](cargo-ktstr.md#verifier) for all flags.
### Library (via tests)
```sh
# Run the verifier pipeline test
cargo nextest run -E 'test(verifier_)'
```
## How it works
1. **Build** -- the framework builds the scheduler binary.
2. **Boot VM** -- the framework boots a single-CPU VM. The scheduler
loads its BPF programs via `scx_ops_load!`; the real kernel
verifier runs against them.
3. **Collect** -- the host reads per-program `verified_insns` from
`bpf_prog_aux` via guest physical memory introspection. On load
failure, libbpf prints the verifier log to stderr, which the VM
captures between `===SCHED_OUTPUT_START===` /
`===SCHED_OUTPUT_END===` markers.
4. **Format** -- per-program summary lines, then verifier logs with
cycle collapse applied (pass `raw: true` to skip collapse).
## Output
### Brief (default)
Per-program summary line:
```text
ktstr_enqueue verified_insns=500
```
Fields: `verified_insns` is the number of instructions the kernel
verifier processed, read from `bpf_prog_aux` via host-side memory
introspection.
On load failure, the scheduler log section shows libbpf's verifier
output with **cycle collapse** applied -- repeating loop iterations
are reduced to the first iteration, an omission marker, and the last
iteration:
```text
--- 8x of the following 10 lines ---
100: (bf) r0 = r1 ; frame1: R0_w=scalar(id=0,umin=0)
101: (bf) r1 = r2 ; frame1: R1_w=scalar(id=1,umin=1)
...
--- 6 identical iterations omitted ---
100: (bf) r0 = r1 ; frame1: R0_w=scalar(id=70,umin=700)
101: (bf) r1 = r2 ; frame1: R1_w=scalar(id=71,umin=701)
...
--- end repeat ---
```
### Raw (`--raw` / `raw: true`)
Full raw verifier log without cycle collapse. Use for debugging
verification failures where the exact register state at each iteration
matters.
### A/B diff
Boots two VMs -- one for each scheduler binary -- and compares
`verified_insns` per program:
```text
program A B delta
------------------------------------------------------------------------
ktstr_enqueue 500 450 +50
ktstr_dispatch 1200 1150 +50
```
## Cycle collapse algorithm
The kernel verifier unrolls loops by re-verifying each instruction
with updated register states. A bounded loop of 8 instructions
verified 100 times produces 800 near-identical lines -- differing
only in register-state annotations. Naive truncation loses context.
Cycle collapse preserves structure: the first iteration shows what
the loop does, the last shows the final state, and a count tells you
how many iterations were elided.
The algorithm normalizes lines by stripping variable annotations,
then detects repeating blocks:
1. **Normalize** -- strip `; frame1: R0_w=...` annotations, standalone
register dumps (`3041: R0=scalar()`), and inline branch-target state
after `goto pc+N`. Source comments (`; for (int j = 0; ...)`) are
preserved as cycle anchors.
2. **Detect** -- find the most frequent normalized line (the "anchor"),
compute gaps between anchor occurrences to determine the cycle
period, then verify consecutive blocks match after normalization.
Minimum period: 5 lines. Minimum repetitions: 3.
3. **Collapse** -- replace the cycle with the first iteration, an
omission count, and the last iteration. Run iteratively (up to 5
passes) to handle nested loops.
## scx-ktstr test flags
scx-ktstr supports these flags to exercise the verifier pipeline:
**`--fail-verify`** -- sets a `.rodata` variable before
`scx_ops_load!`, enabling a code path the BPF verifier rejects.
On failure, libbpf prints the verifier log to stderr.
**`--verify-loop`** -- sets a `.rodata` variable that enables an
unrolled loop followed by `while(1)` in `ktstr_dispatch`. The verifier
rejects the infinite loop and libbpf prints the full instruction
trace to stderr, exercising cycle collapse.