It doesn't. Flip things around and you get something tractable, though incomplete.

Unsolvable problem: reject any loop that is provably infinite.

Solvable problem: reject any loop that isn't provably finite.

The trade off is that there will always be some loops that in fact always do terminate, but that the verifier can't prove do.

You need to slightly modify your code. Rather than:

while (condition) { … }

Do: #define MAX 1000 for n = 0; n < MAX; n++ { if !condition break; … }

Unroll all loops, don’t allow any backward jumps and limit to (say) 1m instructions.

Incidentally, iteration limits are a good idea for production code anyway. If you don't imagine any input needing more than 50 k iterations, throw a user-friendly exception after something like 10 M iterations. Prevents much more annoying problems than it causes.

> If you don't imagine any input needing more than 50 k iterations

What could possibly go wrong.

You get an error is the worst that happens.

Way better than running a denial of service attack on your own systems or those of your customer's.

> You get an error is the worst that happens.

That certainly depends on what eBPF is used for. If your load balancer errors out at [greatest number of connections envisioned] and an adversary manages to establish [greatest number of connections envisioned] then the result is a denial of service.

Not every operator is confident in making code changes in 3rd party software or might even be allowed to make such changes. Increasing resources o.t.o.h., e.g. adding RAM, is rarely banned. I sure would want a system to make best use of available resources.

I still think a denial of service due to tripping some sort of circuit breaker is preferable to one due to resource exhaustion.

If the code is intended to use as a library or the binary distributed to third parties one will have to handle it differently. For libraries taking a parameter indicating the maximum expected is common, for example. See e.g. man 3 read.

Nice. Be good if the language had an easy way to handle it, eg.:

while(condition)[1000 label]{…}