Halting problem [LWN.net]

Halting problem

Posted Dec 4, 2018 7:20 UTC (Tue) by corbet (editor, #1)
In reply to: Bounded loops in BPF programs by ringerc
Parent article: Bounded loops in BPF programs

Nobody is trying to solve the halting problem in any kind of general sense, so it's not really relevant here. After all, current BPF can guarantee that all programs it accepts will halt, no problem...

to post comments

Halting problem

Posted Dec 4, 2018 8:26 UTC (Tue) by vbabka (subscriber, #91706) [Link] (10 responses)

Exactly. Halting problem means that there will always exist programs where you can't prove that they will halt. That might also include programs that would actually halt (but you are not able to prove it). But when you can prove halting for some class of programs (e.g. because they are sufficiently constrained), then (modulo bugs in the prover itself :) you do have the guarantee, regardless of the general halting problem.

Halting problem

Posted Dec 4, 2018 8:52 UTC (Tue) by amacater (subscriber, #790) [Link]

Once, enigmatically
Alan Mathison Turing
Said to his colleagues
"It's now us or them.
Now, if you will
Help me hedge
Programatically
Goedel's insoluble
Entscheidungsproblem"

[If Turing machines are obsolete, when do you stop production? ]

Halting problem

Posted Dec 4, 2018 10:32 UTC (Tue) by excors (subscriber, #95769) [Link] (8 responses)

> 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.)

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.

Halting problem

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

Yeah. The problem here is not the halting problem: the problem here is always finding an approximation that lets useful stuff past but isn't too complex to be worth it. The high time- or sometimes space-complexity of many algorithms needed by compilers is a routine cause of foul curses in developers of normal ahead-of-time compilers that don't run in kernel space: the approximations needed by something that runs in the kernel seem likely to be even harder.

(Really, it's a shame the verifier and JITters have to run in kernel space: this sort of work seems like the sort of thing far better done by an upcall to something in userspace, unprivileged but only installable by root -- only that would stop BPF from being used to protect the system *from* root, and it wouldn't help with the time problem at all since the kernel would still have to block the process installing the BPF to wait for verification/JITing anyway...)

It just makes me icky seeing that people are basically writing compilers that run in kernelspace. Surely there must be a better way.

Halting problem

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

Maybe the kernel should use KVM to launch a minimal Linux distro, and use that as the userspace to run the compiler/JIT/verifier in, so it's unprivileged and not constrained by kernel programming requirements. The distro and applications can be encoded as a blob in a signed kernel module as part of the secure boot chain, so the VM is as secure as the kernel itself and can be protected against the root user.

Halting problem

Posted Dec 4, 2018 16:18 UTC (Tue) by farnz (subscriber, #17727) [Link] (3 responses)

This actually sounds like a potential application for proof-carrying code. The user-space verifier could attach a simple-to-verify proof to the program it's about to attach (even if it's an arbitrary program with loops and other such weirdnesses) that the kernel can check.

Halting problem

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

It really does. Heck the original Necula and Lee paper might as well have had 'BPF' written all over it in letters of fire ten miles high :)

Halting problem

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

It would be rather surprising if a researcher at Berkeley working on Packet Filters was completely unaware of BPF :-)

Halting problem

Posted Dec 11, 2018 17:45 UTC (Tue) by nix (subscriber, #2304) [Link]

Oh yeah, that's true. I had forgotten their affiliation. :)

Halting problem

Posted Dec 8, 2018 7:02 UTC (Sat) by marcH (subscriber, #57642) [Link]

> The problem here is not the halting problem:

Did anyone say it was?

> the problem here is always finding an approximation...

The "feat" was just to never mention once the name of what this approximates.

The misunderstanding and overreaction is even more interesting.