Re: [PATCH bpf-next v3 00/45] bpf: A verifier that joins states

[Eduard Zingerman <eddyz87@gmail.com>]

On Fri, 2026-11-06 at 03:50 +0000, Alexei Starovoitov wrote:
> From: Alexei Starovoitov <ast@kernel.org>
> 
> The verifier follows each path of a prog, and each branch can double the
> number of paths. The work grows with the paths, not with the prog:
>   insns processed                                    today    this series
>   rust-bpf  scx_beerland/beerland_init_task        1000001 *        17893
>   rust-bpf  scx_qmap/qmap_init_cids                 131088 *          196
>   scx       scx_eevdf/eevdf_dispatch                350041          15199
>   Cilium    bpf_host/cil_to_netdev, Oct 2026         64658           7472
>   * "BPF program is too large", "The sequence of 8193 jumps is too complex"
> 
> Authors cut their progs until they fit. Nobody can cut core, alloc and the
> crates of Rust: of the 653 progs of https://github.com/4ast/rust-bpf 187
> load today, 170 hit one of these limits, 164 get "infinite loop detected"
> and 122 "recursive call". Now 648 load, and no corpus of C progs loses one.
> For rust-bpf both kernels have 4 kfuncs on top, see Numbers.
> 
> The idea
> ========
> Do not follow paths. Where paths meet, join their states: r1=1 and r1=5
> give r1=[1,5]. Repeat until no state changes. States stay apart only if
> they have no join, or if a later check depends on the difference.
>   loops      counted by scalar evolution: one state covers all iterations
>              walked: a state per iteration, while constants decide an exit
>              all other loops: join at the head, widen, add may_goto
>   subprogs   A static subprog is verified for the states at its entry, not
>              for each chain of calls. Recursion is the same, with widening.
>   run time   may_goto limits the time of loops and of recursion. r10 limits
>              the depth: it must be in the upper half of its kernel stack.
> 
> What users see
> ==============
>  - The limits of 1M processed insns and 8192 jumps are gone. The limits are
>    on states, for a prog of N insns: 1024 at an insn, 16 * N + 4096 at
>    a time, 256 * N + 64K in all.
>  - "infinite loop detected" is gone: the verifier adds may_goto. A loop
>    that has no exit gets "loop at insn N never exits".
>  - may_goto is also added to 5 progs of the table below that load today:
>    loop1, loop2, loop5, tcp_autolowat_enqueue_rcvq (GCC), chaos_enqueue.
>  - Recursion is allowed on x86-64 and arm64. Patch 22 lists the exceptions.
>  - All added may_goto of an invocation share its time slice of 250 ms. Then
>    the prog returns 0. A subprog that cannot unwind, or a frame that holds
>    a lock or a reference, leaves the loop. The stderr stream has the cause.
>  - A join loses the relation between scalars. This is rejected now:
>      if (c) { i = 3; n = 4; } else { i = 7; n = 8; }
>      x = arr[n - i];                                    n - i is [-3, 5]
>  - A cgroup_skb prog whose r0 can be 2 or 3 attaches to egress only. That
>    holds for a range too: 'return 1' and 'return 2' are joined to [1, 2].
>  - The log has no "mark_precise:", "N: safe", "depth=" and no scc column.
>    Level 2 shows "from 13 to 9: within", "joined" or "widened" where states
>    meet. The statistics line keeps its format: "limit 0", "mark_read 0".
>  - BPF_F_TEST_STATE_FREQ is accepted and has no effect.
> 
> Numbers
> =======
> A: bpf-next 8424858a5de0. B: this series, the same objects. The selftests
> that the series adds or changes are not counted. None of them is lost.
> 
> Corpus                 Progs  Lost  Gained  Insns  States   Mem  Time
> ---------------------  -----  ----  ------  -----  ------  ----  ----
> selftests               3043     0       1   -63%   +120%  -18%  -27%
> selftests, no_alu32     2905     0       1   -66%    +86%  -27%  -34%
> selftests, cpuv4        2914     0       1   -64%    +96%  -27%  -32%
> selftests, bpf_gcc      2733     0       5   -69%    +96%  -16%  -24%
> 37 builds of Cilium     5189     0       0   -75%    +11%   -6%  -31%
> sched-ext/scx            495     0       0   -89%    -34%  -66%  -67%
> scx, as BPF CI has it    428     0       0   -85%    -22%  -38%  -39%
> tools/sched_ext          240     0       0   -69%    +37%   +3%  -11%
> public progs of Meta     511     0       0   -85%    -35%  -55%  -48%
> all                    18458     0       8   -74%    +10%  -19%  -36%
> 
> Progs load in A and in B. The per cent compare sums over these progs:
> 75.1M -> 19.2M processed insns, 61 -> 39 s. Mem is mem_peak of veristat.
> Time is the best of 3 runs on kernels without debug options. B counts each
> state that arrives at a basic block as a state, A only those that it saves.
> Gained: loop3 in the 4 builds, 4 progs that A rejects only in GCC's code.
> Of the progs that take 1000 insns or more in B, two take over 5% more than
> in A. loop5, 82 -> 4182: a walk up to its limit of 4096 insns, then a join.
> res_spin_lock_test_held_lock_max, 2356 -> 4088: states that hold different
> numbers of locks have no join.
> 
> rust-bpf               Progs  load in A  load in B  B: insns   time
> 16 schedulers            225         52        225      1.6M  1.9 s
> crates                   428        135        423      7.3M  9.4 s
> For rust-bpf A and B have the kfuncs of patches 30-31 of [1] on top. They
> are in no series now. No released compiler emits the code of rust-bpf.
> 
> How to read the series
> ======================
> Start with patch 7, the overview. Then 4-5, 13-14, 15, 17 and 19.
>   1-2    what is added to a prog: may_goto, the checks of recursion
>   3-5    union and widening of a range, join.c: the join of two states
>   6-10   data structures of flow.c, passes ahead of the main pass: order of
>          the insns, places for may_goto, what later checks depend on
>   11-14  the sets of states, iterations, what is not joined, the merge
>   15-18  how states move: edges, calls and exits, loops, added edges
>   19     the switch. The check of one insn against one state is the same.
>   20-22  more counted loops, static subprogs on their own, recursion
>   23-26  removal of pruning, precision tracking and SCCs: 3382 lines
>   27-28  callx: a pointer to one of a set of functions, live registers
>   29-38  code that needs more than that: casts, the context in a struct,
>          subprogs that check for their caller, loops that are not counted
>   39-45  selftests: 39-40 adjust tests, 41-45 add tests
> Each patch builds. Patches 1-18 add the code that patch 19 switches to.
> Some selftests fail from patch 19 to 39.

Hi Alexei,

regarding the Meta veristat failures. Please find distilled examples here:
https://github.com/eddyz87/bpf/tree/ast-new-verifier-v3-meta-tests
Applied as commits on top of your series.
All slop but seem to add up.

...