vault

Verifier Bounded Loops and Termination

15 min read

Verifier Bounded Loops and Termination

A BPF program runs inside the kernel, often with interrupts disabled or holding a lock, so a program that loops forever does not just waste CPU — it hangs the machine. The eBPF Verifier therefore must prove, before a program is allowed to load, that every loop it contains will provably terminate. The original BPF verifier solved this by the bluntest possible means: it forbade loops entirely, accepting only programs whose control-flow graph was a directed acyclic graph (DAG) — all jumps pointed forward, no instruction could ever be revisited (verifier.rst, v6.12). Since Linux 5.3 (2019) the verifier accepts bounded loops: it simulates the loop body iteration by iteration, tracking the loop variable’s value range, and proves the loop exits because that range eventually fails the loop condition (LWN 794934). Later kernels added cheaper, verifier-friendly iteration constructs — the bpf_loop helper (5.17) and open-coded iterators / bpf_for (6.4) — that move the termination guarantee into the runtime so the verifier no longer has to simulate every iteration (LWN 877062; LWN 925751). This note explains why termination matters, how each mechanism proves it, and the trade-offs between them.

This note is about termination — proving a loop ends. Its sibling Verifier Complexity Limits and State Pruning is about the verifier’s own budget — proving the verifier ends, i.e. that the static analysis itself does not run forever or explode. The two are intertwined (the brute-force way to prove a loop terminates is to simulate every iteration, which directly burns the verifier’s complexity budget), but they are distinct problems. Register value ranges — the raw material the termination proof reasons over — are tracked by the machinery described in Verifier Register State Tracking.

Mental Model

The deep reason this is hard is Rice’s theorem and the halting problem: there is no algorithm that, given an arbitrary program, decides whether it halts (halting problem). A verifier that insisted on deciding termination for any loop would be attempting the impossible. The BPF verifier sidesteps this the way all practical static analyzers do — it is conservative and sound but incomplete. It does not try to decide the general case; it accepts only loops whose termination it can prove by a specific, tractable argument, and rejects everything else, including many loops that do in fact terminate. A rejected program is not necessarily a buggy program; it is just one the verifier could not prove safe.

flowchart TB
  START["BPF program loaded"] --> CFG["check_cfg(): DFS over instructions<br/>build control-flow graph"]
  CFG --> BE{"back-edge<br/>detected?<br/>(jump to an instruction<br/>already on the DFS stack)"}
  BE -->|"no back-edge"| DAG["pure DAG — no loops<br/>(original 'forward jumps only' rule)"]
  BE -->|"back-edge + privileged<br/>(bpf_capable)"| LOOP["loop allowed —<br/>prove termination"]
  BE -->|"back-edge + unprivileged"| REJECT["REJECT:<br/>'back-edge from insn N to M'"]
  LOOP --> M1["bounded loop (5.3):<br/>simulate each iteration,<br/>track induction var range,<br/>prune when state converges"]
  LOOP --> M2["bpf_loop helper (5.17):<br/>kernel runs the callback N times,<br/>verifier checks body once,<br/>N bounded by BPF_MAX_LOOPS"]
  LOOP --> M3["open-coded iterator (6.4):<br/>bpf_iter_*_next() contract<br/>eventually returns NULL,<br/>state convergence proves exit"]
  M1 --> OK["program accepted"]
  M2 --> OK
  M3 --> OK

The decision flow for any loop in a BPF program. What it shows: the verifier’s first pass (check_cfg) does a depth-first search and classifies every jump; a jump back to an instruction still on the DFS stack is a back-edge, which means a loop. Unprivileged programs are rejected outright; privileged programs may keep the loop but must satisfy one of three termination mechanisms. The insight to take: “does this program have a loop?” and “will this loop terminate?” are answered in two completely different places — the cheap structural question (check_cfg, back-edge detection) in the first pass, the expensive semantic question (does the induction variable’s range force an exit?) in the second pass by simulating iterations or by trusting a runtime-enforced bound.

Mechanical Walk-through

Step 1 — check_cfg: detecting that a loop exists at all

Before the verifier simulates a single instruction, it runs check_cfg(), an iterative (non-recursive) depth-first search over the program’s instructions, treating each instruction as a graph node and each possible jump or fall-through as an edge (verifier.c, v6.12, check_cfg). The comment above the function is explicit about the goal:

/* non-recursive depth-first-search to detect loops in BPF program
 * loop == back-edge in directed graph
 */

Each instruction carries a state in insn_state[]: DISCOVERED (0x10, on the current DFS path / stack) or EXPLORED (0x20, fully processed and popped). The core of the search is push_insn(t, w, e, env), which considers an edge from instruction t to instruction w of type e (FALLTHROUGH or BRANCH). The classification of the edge falls out of w’s current state:

  • If insn_state[w] == 0 (never seen), this is a tree-edge: mark w discovered and push it onto the DFS stack.
  • If (insn_state[w] & 0xF0) == DISCOVERED (w is still on the current DFS path), the edge points backward into the path we are currently walking — this is a back-edge, and a back-edge in a directed graph is exactly the definition of a loop.
  • If insn_state[w] == EXPLORED, it is a harmless forward- or cross-edge.

What happens on a back-edge is the crux, and it is privilege-dependent in v6.12:

} else if ((insn_state[w] & 0xF0) == DISCOVERED) {
        if (env->bpf_capable)
                return DONE_EXPLORING;
        verbose_linfo(env, t, "%d: ", t);
        verbose_linfo(env, w, "%d: ", w);
        verbose(env, "back-edge from insn %d to %d\n", t, w);
        return -EINVAL;
}

For a privileged program (env->bpf_capable, i.e. holding CAP_BPF/CAP_SYS_ADMIN — see CAP_BPF and BPF Privilege Model), the back-edge is simply accepted at the CFG stage (DONE_EXPLORING) and the termination burden is deferred to the second pass. For an unprivileged program, the verifier emits the famous back-edge from insn N to M error and rejects with -EINVAL. This is the v6.12 incarnation of the “no loops at all” rule: it never went away, it became a privilege gate. Unprivileged BPF still cannot contain a back-edge-style loop in its raw control flow (see Unprivileged BPF and Its Restrictions).

Uncertain

Verify: the exact privilege boundary that flips env->bpf_capable for a given program type, and whether some unprivileged loop constructs (e.g. an unrolled loop, or a bpf_loop call) are nonetheless accepted because they contain no raw back-edge. Reason: bpf_capable is set from a combination of CAP_BPF, CAP_SYS_ADMIN, and the kernel.unprivileged_bpf_disabled sysctl, which interact; not fully traced here. To resolve: read bpf_capable() in include/linux/bpf.h and the per-program-type checks in bpf_check() at v6.12. #uncertain

check_cfg also catches programs with unreachable instructions (any instruction left non-EXPLORED after the DFS — verbose(env, "unreachable insn %d\n", i)), a property classic BPF allowed but eBPF forbids (verifier.rst, v6.12).

Step 2 — Bounded loops (5.3): prove termination by simulation

The bounded-loops feature, merged for Linux 5.3 from a patch set by Alexei Starovoitov (LWN 794934), is conceptually almost shockingly simple: the verifier does not analyze the loop, it runs it. During the second (path-walking) pass, when execution reaches a back-edge, the verifier just keeps simulating — it treats each loop iteration as another collection of register/stack states, “no different from any others” (LWN 794934). The loop terminates the verification when one of two things happens:

  1. The loop condition becomes false. Because the verifier tracks the value range of every register (see Verifier Register State Tracking), it knows that, say, r1 starts at 0 and the body does r1 += 1 with an exit test if r1 < 100 goto .... After simulating enough iterations the tracked range of r1 reaches 100, the branch is no longer taken, and the loop falls through to its exit. The induction variable’s bounds are what drives the exit — the verifier proves termination by watching that bound march toward the condition.
  2. State convergence (pruning). If the verifier reaches the loop head in a register/stack state it has already explored and proven safe, it prunes that path — there is nothing new to learn (see Verifier Complexity Limits and State Pruning). For loops whose iterations do not perturb the tracked state, this collapses the whole loop to a handful of simulated iterations.

The enabling change was raising the program-size ceiling. Classic BPF capped programs at BPF_MAXINSNS = 4096 instructions (bpf_common.h, v6.12), far too few to brute-force simulate a long loop. Linux 5.2 raised the effective bound for privileged programs to one million processed instructions, which made the brute-force-by-simulation approach viable (LWN 794934). This is why bounded loops and the million-instruction complexity limit are historically linked — see Verifier Complexity Limits and State Pruning for what that limit is and why a small loop with a large trip count can still blow it.

The catch with bounded loops is exactly that simulation cost. A loop with trip count 100 that touches state on each iteration may force the verifier to explore on the order of 100 distinct states per following branch; nested loops multiply. This is the state-explosion problem the later mechanisms were invented to dodge.

Step 3 — The bpf_loop helper (5.17): move the count into the runtime

The bpf_loop helper, merged in Linux 5.17 (work by Joanne Koong), inverts the relationship (LWN 877062; LWN 877170). Instead of writing a loop in BPF bytecode and asking the verifier to unroll/simulate it, you hand the kernel a callback and a trip count, and the kernel runs the loop:

long bpf_loop(u32 iterations,
              long (*loop_fn)(u32 index, void *ctx),
              void *ctx, u64 flags);

bpf_loop calls loop_fn(index, ctx) up to iterations times. The callback returns 0 to continue and 1 to break early (no other return values permitted) (LWN 877062). The verifier’s job collapses: it only has to verify the body once (a single invocation of loop_fn), because the actual iteration happens in trusted kernel C code outside the verified program. Termination is guaranteed because iterations is a concrete u32 upper bound and is itself capped at BPF_MAX_LOOPS = 8 * 1024 * 1024 (about 8 million) — defined as an enum precisely so it is discoverable through BTF (bpf.h, v6.12):

/* Maximum number of loops for bpf_loop and bpf_iter_num.
 * It's enum to expose it (and thus make it discoverable) through BTF.
 */
enum {
        BPF_MAX_LOOPS = 8 * 1024 * 1024,
};

The payoff is that verification cost becomes independent of the trip count: a bpf_loop of one iteration and a bpf_loop of a million iterations cost the verifier the same — one pass over the callback body (LWN 877062). This is the recommended way to write a long counted loop in modern BPF when the body is non-trivial.

Step 4 — Open-coded iterators and bpf_for (6.4): ergonomic in-program loops

bpf_loop’s callback style is awkward — the loop body lives in a separate function and shares state through a ctx struct. Open-coded iterators, merged in Linux 6.4 by Andrii Nakryiko, restore natural inline loop syntax while keeping a provable termination guarantee (LWN 925751; bpf_iterators.html). An iterator is a tightly-coupled trio of kfuncs following the naming contract bpf_iter_<type>_{new,next,destroy}() (bpf_iterators.html). The simplest is the numeric iterator: bpf_iter_num_new, bpf_iter_num_next, bpf_iter_num_destroy. libbpf wraps them in the bpf_for(i, start, end) and bpf_for_each(...) macros so you write:

int i;
bpf_for(i, 0, n) {
        /* ordinary inline loop body, i is the index */
}

The verifier proves termination from the iterator contract: bpf_iter_*_next() is required to eventually return a “sticky” NULL (once it returns NULL it keeps returning NULL), and the loop exits on that NULL (bpf_iterators.html). Mechanically the verifier still simulates the loop, but it uses iterator-aware state convergence: when it reaches the iter_next call in a state equivalent (within tracked ranges) to one already seen with the iterator still BPF_ITER_STATE_ACTIVE, it concludes the iteration will converge and stops — the v6.12 code handles this special-case in is_state_visited() via is_iter_next_insn() and update_loop_entry() (verifier.c, v6.12). The numeric iterator is itself bounded by BPF_MAX_LOOPS, the same 8-million ceiling as bpf_loop (bpf.h, v6.12).

Step 5 — may_goto / can_loop: a verifier-trusted runtime guard

The most recent mechanism visible in the v6.12 verifier is the may_goto instruction, exposed to programmers through the cond_break / can_loop macros. may_goto is a conditional jump backed by a hidden per-loop counter that the runtime decrements; when it hits zero the runtime forces the branch to fall through, guaranteeing the loop ends regardless of what the body does (LWN 1017116). The verifier trusts this runtime bound — it sees the may_goto and knows “the runtime will halt a loop that continues too long, so it doesn’t need to reject the loop” (LWN 1017116). In v6.12 the verifier handles it via is_may_goto_insn(), tracking a may_goto_depth in the state and using it during state convergence (verifier.c, is_state_visited, lines around the is_may_goto_insn_at check) (verifier.c, v6.12).

Uncertain

Verify: the exact kernel release that first merged the may_goto instruction (commonly cited as 6.11, sometimes conflated with the 6.4 iterator work). Reason: secondary sources describe it as “the eventual result of the may_goto work” without pinning a release; the v6.12 verifier code clearly contains is_may_goto_insn, so it is present by 6.12, but the introducing release is not confirmed against a primary commit here. To resolve: git log --oneline -- kernel/bpf/verifier.c | grep -i may_goto and check the merge tag, or find the LWN/commit announcing BPF_MAY_GOTO. #uncertain

Why Termination Is Non-Negotiable

A normal userspace program that loops forever is a nuisance; you kill -9 it. A BPF program that loops forever can be unkillable. BPF programs run in kernel context — an XDP program runs in the NIC driver’s receive path, a kprobe program runs at an arbitrary kernel function, often with preemption disabled or while holding a spinlock or RCU read lock. There is no scheduler tick that will preempt it and no signal that will interrupt it; a true infinite loop there hangs the CPU and, if it holds a lock other CPUs need, the whole machine. The BPF Design Q&A is blunt that the verifier “cannot solve the halting problem” and so must conservatively reject what it cannot prove (bpf_design_QA.html; LWN 1017116). The runtime-enforced ceilings — BPF_MAX_LOOPS for bpf_loop/iterators, the may_goto counter for can_loop — are belt-and-suspenders: even if a future verifier bug let a non-terminating loop through, these runtime bounds would still cap it.

Failure Modes and How They Read

  • back-edge from insn N to M — your (unprivileged) program contains a raw loop. Either gain CAP_BPF privilege, or restructure into a bpf_loop/bpf_for construct that has no back-edge in the program text.
  • infinite loop detected at insn N — emitted from is_state_visited() when the verifier re-reaches a loop head in a state exactly equal to a previous one with the loop variable unchanged: the loop makes no progress, so it can never exit. The classic cause is a loop whose induction variable the verifier cannot prove advances (e.g. it is incremented by a value the verifier only knows as an unbounded scalar) (verifier.c, v6.12).
  • BPF program is too large. Processed N insn — not strictly a termination failure but its constant companion: a bounded loop that does terminate but whose simulation cost exceeds the million-instruction budget. The fix is usually to switch from a bounded loop to bpf_loop/bpf_for, whose cost is trip-count-independent. This error is the subject of Verifier Complexity Limits and State Pruning.
  • Loop variable lost precision — a loop that the verifier accepted in a small form is rejected after a refactor because the induction variable became a non-constant scalar it can no longer bound. See Verifier Register State Tracking and Reading and Debugging Verifier Errors.

Alternatives and When to Choose Them

ConstructSinceVerifier costUse when
#pragma unroll (compiler unrolls to straight-line code, no back-edge)alwaysproportional to unrolled sizetiny, fixed trip count; no real loop reaches the verifier
Bounded loop (raw back-edge, simulated)5.3proportional to iterations × following stateshort loops, privileged programs, simple bodies
bpf_loop helper5.17one callback verification, trip-count-independentlarge counted loops, non-trivial body, awkward callback style acceptable
Open-coded iterator / bpf_for6.4iterator-aware convergence, lowthe modern default: natural inline syntax + cheap verification
may_goto / cond_break / can_loop~6.11 (flagged)trusts runtime boundopen-ended loops where you cannot state a static trip count

The progression is a clear trend: push the termination guarantee out of the verifier’s static simulation and into a runtime-enforced bound. Unrolling and bounded loops make the verifier do all the work; bpf_loop, iterators, and may_goto let the runtime guarantee the bound, so the verifier only checks the body once. For new code on a 6.12-era kernel, prefer bpf_for / open-coded iterators; reach for bpf_loop when a callback fits better, and can_loop/cond_break when the loop has no static count (LWN 1017116).

Production Notes

The one-million-instruction limit, originally chosen because it “felt big in 2019,” is now routinely hit by large real-world programs (Cilium’s datapath, complex tracing tools), and the recommended remedies are not to crank up loop counts but to restructure: use global functions (verified once, independently of context, counting once toward the limit) instead of static functions inlined into a loop, drop unnecessary __always_inline, and replace bounded loops with iterators or can_loop (LWN 1017116). A common production surprise is that __always_inline on a helper called inside a loop multiplies that helper’s whole body against the limit on every iteration; the guidance since 2017 is that it is no longer needed and often harmful (LWN 1017116). Tools like Cilium historically shipped extensively unrolled datapaths to avoid loops altogether; modern Cilium and bpftrace lean on bpf_loop/iterators where available to keep verification fast and portable across kernels (see Cilium).

See Also

Graph View

Backlinks