3 ms·
eBPF is a real-world system that also refuses to accept programs that might not halt. You don't have to solve the halting problem, you just have to deny the p
by jrockway 3y ago
eBPF is a real-world system that also refuses to accept programs that might not halt. You don't have to solve the halting problem, you just have to deny the programmer loops (and loop-alikes, of course; recursive functions, jmp, etc).
- dragontamer 3y agoIIRC, some language model proved that one-layer of loops can be proven to halt vs not-halt. As soon as you add a 2nd layer of loops however, you reach Turing-completeness and suddenly the halting problem becomes unsolvable. ------- So you don't need to deny jmp/loops. You just need to deny _nested_ loops. And... find that old paper I read like 15 years ago to figure out the details to discriminate halt/not-halt in the single-layer loop language.
- napsterbr 3y agoYou could ask ChatGPT to find the paper for you! It told me the name of an old videogame I was trying to remember for years.
- jakear 3y agoThis is most assuredly false: while (state !== STOP): read = TAPE[index] [state, write, dir] = TABLE[read, state] TAPE[index] = write index = index + dir
- deleted 3y ago[deleted]
- vidarh 3y agoIt takes much more. You need to e.g. limit APIs you can call to ones that are also guaranteed to halt, and guarantee an exit condition that is guaranteed to occur, which means either seriously limiting input or adding additional implicit conditions. E.g. this Ruby program is undecidable: gets This one using a hypothetical gets guaranteed to eventually halt is still undecidable: while getsWithTimeout != "halt" end
- deleted 3y ago[deleted]
- insanitybit 3y agoMicrosoft's implementation of eBPF allows for loops :D https://vbpf.github.io/assets/prevail-paper.pdf https://vbpf.github.io/assets/prevail-paper.pdf
- deredede 3y agoFor loops (where the user is not allowed to change the value of the iterator mid-iteration) are guaranteed to terminate.
- insanitybit 3y agoYeah, I just wanted to point out that it's possible in ebpf.
- deredede 3y agoFair enough :) Although skimming the paper you linked, they say they don't check termination of loops, which surprises me.
- fardo 3y agoOr create more loops, since for example adding For (;;) { print(“hahaha you didn’t say the magic word!”); } In another loop would also prevent termination without program shutdowns.
- deredede 3y agoDon't let weird C syntax choices fool you, this is a while loop, not a for loop. To clarify, when I said "for loop", I meant what is sometimes called a "counted for loop" (or simply "counted loop"): there is an (maximum, if you allow early exit) iteration count that is computed before executing the loop and can't increase later. In C syntax, it is for (int i = 0, e = ...; i < e; ++i) { ... } and the body of the loop is not allowed to change the value of either i or e. Edit: actually I may have been unclear. When I said "for loops are guaranteed to terminate", in the context of the discussion, I meant "if the only kind of loops you allow are (counted) for loops in a language where loop-free expressions are guaranteed to terminate, you get a language where all expressions are guarantee to terminate". So loops can contain other loops, as long as they are all of the "counted for loop" kind.