> I don't know what you would do in the case of like, livelock though.
The idea is we never allow this to happen by enforcing your use of locks and memory through helpers. Helpers are really the secret sauce to how we are able to enforce memory barriers, etc. without having the author think about them too much. Helpers are essentially the new syscall layer for the kernel with the advantage that they are far less expensive to add, and there's less complaining when it's later decided they were a bad decision... :) Of course, there will be bugs in eBPF, just as their are bugs in any other part of the kernel that will cause unexpected behavior.
You are right in that a different design might have been easier to verify and less error prone, but I think that eBPF overall has been very robust, and is still far better than what we had with loading kernel modules and letting people do whatever they want, or trying to create really rigid policies through syscalls and exposing internals through VFS.
It's sort of hard to solve right now in the "Will this arbitrary C program work or not" sense, because the underlying toolchain and kernel implementation is evolving. I know there's a userspace verifier. What would be excellent is something like the ability to compile the kernel implementation of the verifier, but in userspace, so you could use it in CI. Does this already work, maybe?
There are two issues with loading - the first is as you described, which is that the verifier sometimes reject programs that clang can build. The second is that sometimes there are issues resolving BTF and fixing up programs to run against the target ABI. Both of these problems are hard to solve and I have personally seen users run into this as a major pain point. It needs improvement. Verification in userland is definitely one way to improve this. No matter what though, the nature of sitting inside the kernel is that it's very hard to keep any sort of userland step in lockstep with the kernel, and so I think this will always be a hard problem to solve.
I don't know what you would do in the case of like, livelock though. But I also don't know what the failure mode is if, say, the program I ran today always ran and hit some dynamic error, either e.g. in the case of livelock you have to eventually just kill the program to make any further forward progress, but this seems no different than if an eBPF program simply always failed due to dynamic constraints. If the program just keeps exploding you eventually have to back off... Another downside I guess is that it's probably hard to implement transactional models in raw RTL, like this project :)
But this is all just an idea. The thrust of it is to turn small exposures of the underlying processor semantics into higher-level compiler problems. I think this would work because you don't need to solve every compiler problem perfectly, just a small subset of them for a small set of domains. It doesn't really matter for Linux today because it just picked a common subset of the memory model for eBPF, but if anyone was to design a newer language for things like this in some new system, maybe some ideas like that are worthwhile. After all, CO-RE and related projects are about bringing "portability" to BPF programs. This is just an (somewhat logical) extension of that idea to the concurrent programming model. I don't need to worry about processor consistency models when I type "COMMIT TRANSACTION" in a SQL prompt, after all.
> To your second point about verification, yes this is something that is actively being worked on.
It's sort of hard to solve right now in the "Will this arbitrary C program work or not" sense, because the underlying toolchain and kernel implementation is evolving. I know there's a userspace verifier. What would be excellent is something like the ability to compile the kernel implementation of the verifier, but in userspace, so you could use it in CI. Does this already work, maybe?