Halting problem [LWN.net]

Halting problem

Posted Dec 4, 2018 10:32 UTC (Tue) by excors (subscriber, #95769)
In reply to: Halting problem by vbabka
Parent article: Bounded loops in BPF programs

> Halting problem means that there will always exist programs where you can't prove that they will halt.

And by "programs", it specifically means programs in a system equivalent to a Turing machine, which has infinite memory and infinite time. That means it doesn't apply to any practical computer - they will have limited memory, so it's trivial to prove whether a program will halt by just enumerating all possible states. (Of course that's also a practically useless thing to prove - the BPF verifier wouldn't want to accept a program that definitely halts but might take a million years to do so.)

to post comments

Halting problem

Posted Dec 4, 2018 12:35 UTC (Tue) by nix (subscriber, #2304) [Link] (6 responses)

Only a million years? We have an upper bound for all-possible-states enumeration, the busy beaver problem. I'm fairly sure a six-symbol program would exceed any likely bound for a mere million-year verification, and that's *way* below the likely size of BPF programs. (Hell, the max size of BPF programs has *always* been above the limit at which Aaronson et al hav shown that finding the busy beaver becomes noncomputable, though most BPF programs are probably much smaller than that.)

Halting problem

Posted Dec 4, 2018 14:27 UTC (Tue) by excors (subscriber, #95769) [Link] (5 responses)

I think the busy beaver problem assumes infinite tape (i.e. memory). When you have finite memory, you can consider the contents of memory (including registers etc) to be the machine's state, and then it's just a finite state machine. If it has N bits of memory, then after 2^N cycles it must have either halted or found a cycle from one state back to itself (in which case it will never halt). From a theoretician's perspective, that solves the halting problem for this machine.

Halting problem

Posted Dec 4, 2018 16:31 UTC (Tue) by dskoll (subscriber, #1630) [Link] (4 responses)

Well, you know that N is so large that 2^N might as well be infinite for all practical purposes. Also, you assume that the computation is deterministic. In real-world situations where external events can change the state (a network packet arriving, for example), a program might terminate even if it repeats a state it has been in before.

Actually, it's trivial to prove that all programs on computers on earth will eventually halt, becuase the Sun will eventually expand and destroy the earth, thereby halting the program. That's the ultimate example of an external event affecting the state.

Halting problem

Posted Dec 4, 2018 17:40 UTC (Tue) by excors (subscriber, #95769) [Link] (3 responses)

Oh, sure - I think what I'm trying to get at is that there are two completely separate realms, one of theoretical computer science (which is really just computer-themed mathematics) where the halting problem and busy beavers and Turing machines are relevant, and most finite things are trivial; and one of practical reality where the difference between "1 msec" and "after the heat death of the universe" is an important distinction. Applying theoretical tools to practical problems doesn't give useful results, and that's why the halting problem isn't relevant to BPF.

Halting problem

Posted Dec 4, 2018 19:35 UTC (Tue) by dskoll (subscriber, #1630) [Link]

I wouldn't say the halting problem isn't relevant at all to BPF, but it's not the only problem with trying to make it work practically.

But yeah, mostly it's just fun to point out weird edge cases that distinguish theory from practice. :)

Halting problem

Posted Dec 4, 2018 23:53 UTC (Tue) by nix (subscriber, #2304) [Link]

Yes, except that this stuff is also tied up with complexity theory, and that *is* extremely relevant (a lot of algorithms exist that would be really nice to use in compilers except that their time or space complexity is in very much the wrong class, should we say... so one uses approximations, or a less optimal algorithm, and wishes we lived in a perfect world.)

Halting problem

Posted Dec 5, 2018 10:46 UTC (Wed) by farnz (subscriber, #17727) [Link]

It's also not relevant because the halting problem says that you can't sort all programs into "does not halt" and "does halt". If you accept a third bucket - "may or may not halt", then the problem falls away; you can sort all programs into those three buckets in theory, and then it's just a practical problem.

This is not a new insight - it's basically a conservative approximation to the halting problem (where you treat "may or may not halt" as "does not halt", and accept that you are rejecting some programs that do halt), and is a common process in compilers.

Halting problem

Posted Dec 5, 2018 14:16 UTC (Wed) by mina86 (guest, #68442) [Link]

Million years? You can do it in constant time! Just precompute all possible states of the machine and stash all that terminate to a hash set. As added bonus the computation can be used to replace bogomips loop.