Microsoft did termination proof for Windows drivers in 2006. Termination proof does not require solving halting problem.

Termination proofs for systems code (PLDI 2006): https://dl.acm.org/doi/10.1145/1133255.1134029

As mentioned in a sibling reply, there goes my week. Thanks for the reference! Time to learn something I apparently did not know!

I think you can reason it like this.

Assuming certain constraints (what you can define bounded analysis rules for) you can prove that things terminate. These rules things are usually far more advanced than we suspect initially, but they're not still not fully unbounded.(And we can often come up with more rules to make things practical even if unwieldy)

Deciding termination for an arbitrarily large program in a turing complete system CAN require no less than execution of such a program thus we CANNOT guarantee to be able to verify termination for EVERY program. (This is the halting problem)

I spent a lot of time on my thesis learning about type inference systems and as many such systems for uncooperative languages(JS,Python,etc) need to do abstract interpretation they fall into the same kind of issues and this is why practical systems use JIT compilation instead of AOT even if there are exceptions (Shed Skin Python is quite impressive for example).

I thought any general system contain arithmetic (as the proof based on transformation) cannot be proved it will be halted. Termination ... can it be terminated without halting?

Halting is indeed the same as termination. The halting problem DOES allow you to prove that some programs terminate. The problem is that there will be other programs that do terminate, but you won't be able to prove that they terminate.

So there is no way to know, for EVERY possible program, whether that program will terminate or not. But there are still some programs that you can know for certain that those programs will terminate.

From my understanding eBPF is sufficiently constrained to where the halting problem is solvable for all representable programs (in eBPF).

BPF verifiers don't accept arbitrary programs.

Awww shit.

I knew this day would come. Be back in like a week. Gotta get my neurons warmed up and translating Theoretic CompSci/discrete math notation again.

If I don't come back send a search party. I'll probably be stuck somewhere around pumping lemmas screaming "This is arbitrary bullshit!"

It’s not magic, just constraints. there are some obvious tricks (which have since been relaxed).

No unbounded loops for one. I think no backward jumps was previously a rule? I think the ability to tail call another bpf program was added, so not sure if you can accidentally loop forever between individually terminating programs.

You can't; each program is verified independently, and there's a small limit to the number of tail calls you can do.

Being able to run an unbounded loop in eBPF would be a big deal (doesn't mean it can't be done; in fact: it almost surely can be) --- a serious vulnerability.