There's a subtlety being missed here. Proven termination of BPF programs far predates the adversarial threat model you and the WASM person are thinking about. It was a property of the original 1991 McCanne BPF. It's a safeguard for the programmer against themselves. eBPF shims in all over the place in the kernel; it would not be OK for the guarantee to simply be "there's a worst case maximum cycle budget for programs". eBPF programs are bounded, so they can be installed in hot places in the kernel.
The solved problem you're referring to is a much simpler problem.
Comments
Program termination is a solved problem with gas metering. Ethereum popularized the idea, but the idea itself is as old as hills.
There's a subtlety being missed here. Proven termination of BPF programs far predates the adversarial threat model you and the WASM person are thinking about. It was a property of the original 1991 McCanne BPF. It's a safeguard for the programmer against themselves. eBPF shims in all over the place in the kernel; it would not be OK for the guarantee to simply be "there's a worst case maximum cycle budget for programs". eBPF programs are bounded, so they can be installed in hot places in the kernel.
The solved problem you're referring to is a much simpler problem.
What is the difference between "there's a worst case maximum cycle budget for programs" and bounded? and why it would not be OK?