BPF verifier gains widening path for long bounded loops

Alexei Starovoitov has proposed a BPF verifier change that would accept long, simple bounded loops without simulating every iteration. Today the verifier’s cost scales with trip count, so a straightforward loop that runs hundreds of thousands of times is rejected as too large even when the body is trivial.

The new path treats loop heads more like open-coded iterators. When a state returns to the head, the verifier either proves it is already covered by a prior state and stops, or widens scalar ranges (and related spilled values) and continues. A loop such as stepping a counter by four up to a million and summing words from a buffer can then be checked in a couple of trips instead of a million. Range ends are tightened to values that actually belong to the tracked bit pattern so inequality exits can cut the range cleanly and the state converges.

Loops verified this way are not proven to terminate. If nothing ever leaves the strongly connected component, the program is still rejected. Otherwise the verifier inserts a may_goto on the back-edge; when that budget is exhausted the program ends via bpf_throw(). Loops that already go through may_goto or an iterator, and loops the verifier still walks to completion, are left alone. may_goto is skipped where exceptions are illegal (held references or locks, certain callbacks and global functions, JITs without exception support), and those cases fall back to the old walk.

Because widening discards precision, the series first tries the widening walk and, on failure, restores verifier side state and retries the classic per-iteration walk. Anything accepted today remains accepted; a handful of previously rejected selftests that can exit but need not are newly accepted with may_goto. Across the selftest corpus Starovoitov reports roughly a 13% drop in total instructions processed for programs that already loaded, with extreme cases (deep nested loops, large task iterators, timer races) falling from tens or hundreds of thousands of simulated instructions to a few hundred.

The work is still an early design dump aimed at bpf-next, with selftests for step sizes, nesting, non-terminating spin loops, and loops that must not gain may_goto because they hold a reference.