[tptacek]

The verifier is extremely fussy. Different forms of the exact same loop (as far as the programmer is concerned) will get different results, and my experience is that I spend time rewriting the same loop in different ways just to get programs to pass. A bona-fide non-unrolled loop in a BPF program right now is a special thing that takes extra time to implement, and you're probably not going to use them casually.

The answer to whether BPF effectively allows unbounded loops is "no". The verifier essentially emulates the instructions in your loop, iteration by iteration, and gives itself a fixed budget to do so. If it can't prove the loop invariably exits in that budget, it rejects the program. Allowing an unbounded loop would be an important security vulnerability, and is kind of the whole original point of the verifier.

Probably, this is just a terminology issue; what the verifier in fact cares about is indeed whether the program terminates.

[mehrdadn]

Thanks! Yeah that makes sense; it sounds like it's just the terminology then.