Give up on proving termination [LWN.net]

Give up on proving termination

Posted Jun 19, 2026 23:34 UTC (Fri) by roc (subscriber, #30627)
Parent article: Suspending and resuming BPF programs

> For that matter, even with the verifier limiting BPF programs to less than one million verified instructions, there's nothing preventing a user from attaching a 999,999 instruction BPF program that makes lots of expensive kfunc calls to every available kernel hook and slowing the system to a crawl. The point of the limit is to prevent infinite loops that might cause deadlocks, so that the system can continue to make forward progress, not to prevent BPF programs from wasting CPU time.

This makes no sense to me. What is the value of "guaranteed forward progress" if in practice that progress can be made arbitrarily slow? You can't tell someone whose system has locked up that it's not a bug because their system will unfreeze in an hour.

It seems necessary and sufficient to have some kind of counter/timer that can reliably kill BPF programs that run too long, in a safe way that leaves the kernel in a good state. Once you have that, just give up on trying to verify termination.

to post comments

Give up on proving termination

Posted Jun 19, 2026 23:49 UTC (Fri) by Cyberax (✭ supporter ✭, #52523) [Link] (2 responses)

This means admitting that the verifier has been useless all along, and all the gratuitous complexity could have been avoided.

Give up on proving termination

Posted Jun 21, 2026 10:33 UTC (Sun) by summentier (subscriber, #100638) [Link] (1 responses)

Is that so? I thought the main point of the verifier was to check for illegal memory access, which, since BPF programs are AFAIK not sandboxed, could lead to crashes, corruption, and other calamaties.

The instruction limit stops the verifier from having to solve the halting problem. The guaranteed runtime limit seems to be a secondary benefit.

Give up on proving termination

Posted Jun 21, 2026 16:57 UTC (Sun) by Cyberax (✭ supporter ✭, #52523) [Link]

BPF is runtime-bounds-checked in practice. Eliding a few checks here and there is not significant.

> The instruction limit stops the verifier from having to solve the halting problem. The guaranteed runtime limit seems to be a secondary benefit.

BPF now has unlimited loops with the help of iterators. Even without them, it has access to string instructions, so you can easily make programs that take seconds to run. That's why BPF had to add asynchronous termination support.

As keep I saying, they should have just taken WASM instead of reinventing the wheel. Badly.

Give up on proving termination

Posted Jun 20, 2026 7:22 UTC (Sat) by kleptog (subscriber, #1183) [Link] (4 responses)

> What is the value of "guaranteed forward progress" if in practice that progress can be made arbitrarily slow?

You're not defending against a malicious actor here, it's (IMHO) to prevent people writing stupid BPF programs by accident. People don't write "make my system slow but not freeze" scripts by accident.

What you are basically suggesting is adding support for exceptions which would allow a BPF program to be aborted at any point. And every caller has to decide what to do with an OutOfInstructions exception. Given the opinion of exceptions in the rest of the kernel and the complexity isn't adds to e.g. C++, I can understand why they don't want to go that route.

Give up on proving termination

Posted Jun 20, 2026 11:24 UTC (Sat) by roc (subscriber, #30627) [Link]

> You're not defending against a malicious actor here, it's (IMHO) to prevent people writing stupid BPF programs by accident.

Then termination detection doesn't need to be in the kernel verifier, it can just be a lint that the compiler applies to warn you if your program might run too long.

> What you are basically suggesting is adding support for exceptions which would allow a BPF program to be aborted at any point. And every caller has to decide what to do with an OutOfInstructions exception. Given the opinion of exceptions in the rest of the kernel and the complexity isn't adds to e.g. C++, I can understand why they don't want to go that route.

One problem with that argument is that BPF programs already support aborts/exceptions: https://lpc.events/event/17/contributions/1578/attachment...
So the additional work that would be required would just be to define, for each context in which a BPF program can be called, where the BPF function's return value is not void, a default return value.

Give up on proving termination

Posted Jun 20, 2026 12:21 UTC (Sat) by jengelh (subscriber, #33263) [Link] (1 responses)

>People don't write "make my system slow but not freeze" scripts by accident.

If only. An unsuspecting writer might add a for loop in one function ("should be fine") and silently raising existing O(n^m) behavior into O(n^(m+1)). Works for his machine, and grinds on another with a sufficiently large dataset n.

Give up on proving termination

Posted Jun 21, 2026 10:28 UTC (Sun) by farnz (subscriber, #17727) [Link]

The variation I've seen on this is to write a loop with O(n^m) behaviour, where m is the number of CPU cores. Works fine on the small test EC2 instance with 1 or 2 vCPUs; blows up on production instances with 16 or 32 vCPUs.

Give up on proving termination

Posted Jun 22, 2026 8:29 UTC (Mon) by taladar (subscriber, #68407) [Link]

> People don't write "make my system slow but not freeze" scripts by accident.

Probably a lot more people than people who write "make the script not terminate" bugs by accident (where non-termination is defined as actually taking forever, not just taking a few years since that would technically fall into the slow category).

Give up on proving termination

Posted Jul 12, 2026 18:42 UTC (Sun) by yanjun.zhu (guest, #173290) [Link]

I am wondering if we can make eBPF program sleep. The eBPF program sleep when it is not needed, When it is needed, this eBPF program is waken up. Is it a solution to this resume problem?