BPF verifier rewrite targets Rust with recursion and open loops

Alexei Starovoitov has posted an 82-patch series that redesigns the Linux BPF verifier so programs compiled from Rust can load as rustc and LLVM emit them, including code that uses trait objects, recursion, unwinding, and loops with no known bound.

The existing verifier walks every execution path and prunes when a previously seen state already covers the current one. That model breaks down on the control flow modern compilers produce. The series replaces path enumeration with a data-flow analysis: the verifier processes one basic block at a time, joins states that meet at a block into a single covering state, and continues from the join. Starovoitov rewrote the verifier documentation around that algorithm and eleven worked examples covering joins, widening, loops, subprograms, function tables, and recursion.

Practical effects follow. Recursion is allowed at load time; the kernel enforces stack and call budgets at run time and returns early when they are exhausted. Loops the analysis cannot bound receive an injected may_goto that stops them after a short time budget so a runaway program cannot lock up a CPU. A register may hold a pointer to one of a set of functions, as with Rust trait-object method calls, without forking a separate state for every possible target at the load site. Precision tracking, path pruning, and related machinery go away once joining replaces them.

A second part of the series puts the BPF stack in an arena so Rust programs can keep heap data and address-taken locals there, with supporting kfuncs. Only the opening block of fixes is proposed for immediate merge into the bpf tree. The arena stack and the joining verifier are posted for review. Companion test programs that exercise the model live in Starovoitov's public rust-bpf repository.