# BPF Verifier
The verifier sweep boots every declared scheduler in a KVM VM, across
a range of topologies, and checks three things against the real
kernel: that each scheduler's BPF programs pass the kernel verifier
(capturing per-program `verified_insns`), that the scheduler actually
turns on — attaches as the active sched_ext scheduler — and that it
dispatches an injected workload (a task makes forward progress after
attach).
## Design
The verifier sweep follows ktstr's two core principles.
**Fidelity without overhead.** Each scheduler binary runs inside a
VM on the same kernel the scheduler targets 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
```sh
# Run every declared scheduler against the kernel discovered via
# KTSTR_KERNEL (or the cache).
cargo ktstr verifier
# Run against a specific kernel build.
cargo ktstr verifier --kernel ../linux
# Sweep across multiple kernels (each cell runs against its own).
cargo ktstr verifier --kernel 6.14.2 --kernel 6.15.0
# Sweep a single declared scheduler across topologies (skip the rest).
cargo ktstr verifier --scheduler scx-ktstr
# Print the raw verifier log without cycle collapse.
cargo ktstr verifier --raw
```
See [cargo-ktstr verifier](cargo-ktstr.md#verifier) for the
full flag list.
## How it works
`cargo ktstr verifier` is a thin dispatcher around
`cargo nextest run -E 'test(/^verifier/) & !test(/^verifier::/)'` (the
filter matches the `verifier/...` cells but excludes the verifier
module's own `verifier::tests::*` unit tests, which also start with
"verifier"). The matrix that nextest runs is generated by the test
binaries themselves.
1. **Cell emission** — every test binary that links the
ktstr test support and contains at least one
`declare_scheduler!` declaration emits a
`verifier/<sched>/<kernel>/<preset>: test` listing for each
(declared scheduler × kernel-list entry × accepted topology preset)
cell. The sweep runs each scheduler ACROSS topologies because two
things vary with topology: `verified_insns` (a scheduler that bakes
topology-derived config like `nr_cpus` into `.rodata` hands the
verifier different known constants, so it processes a different
instruction count per topology) and whether a scheduler attaches and
dispatches (a scheduler can attach on one topology and wedge on
another — odd LLC counts, wide CPU counts, SMT). Every cell boots in
no_perf_mode, so a
preset is emitted only when the scheduler's constraints accept it
under `accepts_no_perf_mode`. A scheduler whose constraints accept no
preset on this host emits no cell; `--scheduler <NAME>` restricts the
sweep to a single declared scheduler.
2. **Per-cell dispatch** — nextest invokes the test binary once
per cell with `--exact verifier/<sched>/<kernel>/<preset>`.
The binary's `#[ctor]` intercepts the prefix, parses the cell
name into its three components, resolves the scheduler binary and
kernel directory, looks up the named gauntlet preset for its
topology, and boots a single VM dedicated to that cell.
3. **Verifier collection** — inside the VM, the scheduler
loads its BPF programs via `scx_ops_load!`; the real kernel
verifier runs against them. 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; the VM forwards it to the host inside
the `===SCHED_OUTPUT_START===` / `===SCHED_OUTPUT_END===`
markers — over the virtio-console bulk port when available,
falling back to the COM2 console stream otherwise.
4. **Attach + dispatch check** — the guest init runs a scheduler
attach gate on every boot: it confirms the scheduler process
survived BPF load and that `/sys/kernel/sched_ext/state` reached
`enabled`. The kernel sets `enabled` only after `ops.init`,
per-task init, and switching eligible tasks to the sched_ext
class, so `enabled` proves the scheduler turned on and is
scheduling — not merely that its BPF loaded. On failure the guest
sends a `SchedulerDied` / `SchedulerNotAttached` lifecycle frame;
the cell consumes that verdict and FAILs. The check is
positive-confirmation: attach is confirmed only when the guest
reaches its post-attach dispatch phase (a `PayloadStarting` frame),
so a guest that vanishes early — e.g. a kernel panic that reboots
without emitting any frame — FAILs rather than passing by default.
Then, because the verifier VM has no `#[ktstr_test]` body, Phase 5
injects a SpinWait workload sized to the guest's online CPUs and,
when a worker makes forward progress (proof the scheduler dispatched
a task onto a CPU), emits a `WorkloadDispatched` frame. A cell PASSes
only when BOTH frames arrive: a scheduler that attaches but never
dispatches a runnable task is a distinct, worse failure the attach
gate alone cannot catch. The probe workers run as SCHED_EXT, so the
BPF scheduler dispatches them under any switch mode (full or
`SCX_OPS_SWITCH_PARTIAL`); both checks are scheduler-agnostic (kernel
sysfs state + generic SCHED_EXT worker progress), so they hold for
every declared scheduler.
5. **Rendering** — a per-program summary (with the attach + dispatch
status), the verifier log with cycle collapse (or raw, with
`--raw`), and, after nextest returns, one `verified_insns` table per
declared scheduler (rows = kernel, cols = BPF program, cell = the
count across topologies) followed by a topology × scheduler PASS/FAIL
grid.
Eevdf + KernelBuiltin scheduler variants have no userspace
binary to load BPF programs from, so they are skipped at
cell-emission time. The cell handler resolves the kernel label
first. A bare `--exact verifier/...` run with an empty
`KTSTR_KERNEL_LIST` therefore errors with exit 1 before the SKIP
arm is ever reached. The `SKIP`-banner/exit-0 arm fires only after
a successful kernel-label lookup — i.e. under the
`cargo ktstr verifier` dispatcher — and exists purely as
defense-in-depth for a direct `--exact verifier/<eevdf>/...`
invocation.
## Matrix dimensions + filters
The verifier sweep matrix has three dimensions: declared scheduler,
kernel, and topology preset. The kernel axis is driven by the
operator's `--kernel` set, not by per-scheduler `declare_scheduler!`
declarations: the dispatcher always exports `KTSTR_KERNEL_LIST`
(`label1=path1;label2=path2;...`) to the nextest invocation — even with
no `--kernel` flag it synthesizes a single entry from the
auto-discovered kernel. The topology axis is the set of gauntlet
presets whose topology each scheduler's constraints accept under
no_perf_mode. The test binary's lister walks these dimensions and emits
one cell per (declared scheduler × kernel-list entry × accepted
topology preset). `--scheduler <NAME>` narrows the scheduler axis to a
single declared scheduler.
Each scheduler's `declare_scheduler!` `kernels = [...]`
declaration acts as a **per-scheduler filter** on the matrix:
- Empty (`kernels = []`) accepts every kernel-list entry — the
scheduler verifies against everything the operator passes.
- `Version` specs (`"6.14.2"`) match entries whose raw label
equals the version (or whose sanitized label equals the
sanitized form of the version).
- `Range` specs (`"6.14..6.16"`, `"6.14..=6.16"`) match
entries whose raw version falls in the inclusive range,
parsed via the same `decompose_version_for_compare` helper
the operator-side range expansion uses.
- `Path` / `CacheKey` / `Git` specs match by sanitized-label
equality.
```sh
# Scheduler declares kernels = ["6.14..6.16"]
# Operator runs --kernel 6.14.2 --kernel 6.15.0 --kernel 6.17.0
# Dispatcher's KTSTR_KERNEL_LIST labels: 6.14.2, 6.15.0, 6.17.0
# (sanitized to kernel_6_14_2 etc. in the cell names below)
# Scheduler filter: 6.14.2 ∈ [6.14, 6.16] ✓
# 6.15.0 ∈ [6.14, 6.16] ✓
# 6.17.0 ∈ [6.14, 6.16] ✗ — rejected
# Cells emitted (one per accepted topology preset, e.g. tiny-1llc):
# verifier/<sched>/kernel_6_14_2/<preset>
# verifier/<sched>/kernel_6_15_0/<preset>
cargo ktstr verifier --kernel 6.14.2 --kernel 6.15.0 --kernel 6.17.0
# No --kernel: dispatcher auto-discovers one kernel via the
# cache + filesystem chain and synthesizes a single-entry
# KTSTR_KERNEL_LIST. The auto-discovered entry's raw label is
# derived from the resolved path (`path_<basename>_<hash6>`;
# sanitized to `kernel_path_<basename>_<hash6>` in cell names).
# Schedulers with non-empty `kernels = [...]` may filter the
# entry out — operators wanting deterministic coverage should
# always pass --kernel.
cargo ktstr verifier
```
The verifier cell handler resolves the per-cell kernel
directory by looking up the cell's sanitized label in
`KTSTR_KERNEL_LIST` — there is no single-kernel fallback that
would silently run a cell against an unrelated kernel. A label
that doesn't appear in the list errors out with an actionable
diagnostic naming the present labels and pointing at both fix
paths (add `--kernel <SPEC>` or drop the matching entry from
`declare_scheduler!`).
## Output
### Brief (default)
An attach-status line, then a per-program summary line:
```text
scheduler: attached (sched_ext enabled)
dispatch: confirmed (injected workload ran)
ktstr_enqueue verified_insns=500
```
`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`)
Full raw verifier log without cycle collapse. Use for
debugging verification failures where the exact register
state at each iteration matters. The flag exports
`KTSTR_VERIFIER_RAW=1` for the nextest invocation; the
in-binary cell handler reads it via `env::var_os` and switches
the `format_verifier_output` rendering branch.
### Summary tables
After nextest returns, `cargo ktstr verifier` prints two views.
First, one `verified_insns` table per declared scheduler: rows are
kernel version, columns are BPF program, and each cell is that
program's `verified_insns` summarized across the topologies that ran
it — a single number when topology-flat, `lo..hi` when it varies, `-`
when that program reported no stats on that kernel:
```text
verifier verified_insns (per scheduler; rows: kernel, cols: BPF program, cell: range across topologies):
scx_ktstr:
kernel ktstr_dispatch ktstr_enqueue
kernel_6_14_2 1200 500
```
Then a topology × scheduler PASS/FAIL grid (one row per topology, one
column per scheduler; `-` where a scheduler emitted no cell for that
topology). Kernels fold into the cell: ✅ means the scheduler verified,
turned on, AND dispatched the injected workload on every kernel that ran
it; ❌ means it failed on every kernel; 🇽 means it passed on at least one
kernel and failed on another (only reachable in a multi-kernel sweep).
The exact failing (scheduler / kernel / topology) tuples are listed
under the grid:
```text
verifier summary: 4 ✅ 0 ❌ 0 🇽
topology scx_ktstr scx_other
tiny-1llc ✅ ✅
tiny-2llc ✅ ✅
```
## 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!` that enables a store through a null pointer in
`ktstr_dispatch` — the invalid access the verifier rejects. On
failure, libbpf prints the verifier log to stderr.
**`--verify-loop`** — sets a `.rodata` variable that enables an
unrolled 8-iteration loop followed by a store through a null pointer
in `ktstr_dispatch`. The null-pointer store is the invalid access the
verifier rejects (deliberately not a `while(1)`, whose infinite-loop
analysis could keep `scx_ops_load` from returning within the host's
scheduler-attach poll). On rejection libbpf prints the full
instruction trace to stderr, exercising cycle collapse.