According to https://news.ycombinator.com/item?id=18496054, these programs have to halt? How does this system guarantee that the programs halt? Does this mean eBPF is not Turing complete?
The language itself is Turing complete, but the kernel will refuse to run a program that it cannot prove will halt.
There are three categories of programs; programs you can trivially prove will halt, programs you can trivially prove won't halt, and programs where it's difficult or impossible to prove whether or not will halt. The third category is what we call the halting problem. Only the first category will be run by the kernel.
The nitty gritty is that the only jumps which are allowed to go backwards are the end of a loop with a fixed number of iterations. All other jumps must jump forward.
This sounds like it's really limiting, but in practice there's not a whole lot of useful stuff you're unable to do.
Could you create an unbounded loop by scheduling another BPF execution on the end of each program? I imagine something like a WASM runtime that would be split into multiple BPF programs on loops. Which would practically achieve https://github.com/nebulet/nebulet, right?
From the accompanying video (17:11)[1] it's not Turing complete "because the verifier rejects unbounded loops and so there is some things that are not possible. We do have bounded loops in BPF now."
It's the definition of Turning complete that's the problem. A Turning complete machine must be able to process countably infinite inputs. The halting problem arises from same thing. There is no halting problem if we restrict ourselves to programs that will stop in a bounded time (obviously).
In practice that means a true Turning machine can compute things that aren't actually computable in our Universe, or at least not by the bits of the Universe we understand well. I doubt any engineer will think that "this architecture can't in theory compute things not computable in this Universe" is a strong argument against it.
