3 ms·

The halting problem says that you cannot make this guarantee for ANY sufficiently complex program. Even a mere 9kloc L4 kernel (of intentionally not-so-dense C

by hajile 4y ago

The halting problem says that you cannot make this guarantee for ANY sufficiently complex program. Even a mere 9kloc L4 kernel (of intentionally not-so-dense C-code) took many man years to prove. EDIT: Has anyone ever offered such a proof for a program that is just 100kloc? What about 1mloc? Do people actually believe that most non-trivial "realtime" programs are provably realtime?

School-Cotton 4y ago
No it doesn’t. It says there are some programs for which you can’t make this guarantee.
willis936 4y ago
It's a high standard, but it is the standard for safety-critical systems. Nothing has changed about the problem, so the goal posts should stay where they are despite what new tools we have.
tralarpa 4y ago
That might be the reason why the JPL coding standard says: "All loops shall have a statically determinable upper-bound on the maximum number of loop iterations. It shall be possible for a static compliance checking tool to affirm the existence of the bound. An exception is allowed for the use of a single non-terminating loop per task or thread where requests are received and processed. Such a server loop shall be annotated with the C comment: /* @non-terminating@ */."
- hajile 4y ago
  It took around 5-10 man-years to verify the L4 kernel using a theorem prover and that's just 8700 LOC plus 600 lines of assembly. Without such a theorem solver, it is all just "best practices" then hoping for the best.
  - ducktective 4y ago
    Is there a tech stack or language that allows us to write formally proven and real-time (bounded-time tasks) for embedded systems? What if we can be lenient on these conditions (like soft real time, 500ms bounds)? I'm looking for something like shell scripting (easy and functional) + busybox set of utilities + language built-ins to write concurrent applications. Like an OS with a specialized shell scripting language. Does something like this exist?
    - psd1 4y ago
      cgi-bin
    - mbrodersen 4y ago
      I am currently playing around with Dafny and it is very promising. I have use it to generate proven correct high-performance C# code without too much efforts. It’s great fun actually. Like a really cool puzzle game.
deleted 4y ago
[deleted]
ablob 4y ago
Yet I can give you an estimate of the runtime of multiple programs I use to an accuracy within seconds (order of magnitude is hours). The halting problem itself is a good estimate for computational complexity (i.e. can my thing simulate a TM) and makes statements for the general case, but that's just it: the general case. There are a whole class of programs/languages that are decidable (i.e. they will terminate) and that can be proven as well by automated means. Now this does depend on what you mean with sufficiently complex, but for special programs you can prove a lot of things (by hand); the halting problem does not prevent that. However, a side effect is that you may not be able to prove that property for the program you want.
- hajile 4y ago
  > Yet I can give you an estimate of the runtime of multiple programs I use to an accuracy within seconds (order of magnitude is hours). Can you do this for all possible inputs? If not, then your informal pinky swear that it really will get things done on time isn't worth very much.
typon 4y ago
No, that's a misunderstanding. It says you can't come up with a general algorithm for arbitrary programs to detect whether they will halt, it says nothing about particular programs.
- hajile 4y ago
  That is true in theory, but not in practice. A large program is itself essentially composed of many subprograms. You must prove every single aspect of those subprograms (hard in and of itself) then you must prove that every possible combination of those subprograms is also provable. As there is no general formula for the halting problem, each combination must be uniquely proven. This essentially means that if you have N possible branches, then the difficulty proving for each unique case would be the factorial of N. Proving 9kloc of code for L4 took 5-10 man years. Adding just 1kloc of similarly dense code would likely add decades of man-years. What about 100kloc or 1mloc? Even if you could find tricks to optimize similar branches, the fundamental factorial problem doesn't go away (as making it go away would mean that you've solved the provably insolvable halting problem). In practice, only the most trivial of programs are completely provable before the heat death of the universe.
monocasa 4y ago
Part of why L4 took man years to prove is that the proof contains all sorts of stuff like the formal model of ARM machine code. Ideally we'd get to a point where those models can be shared across projects, just like for running software we don't start each project by writing a compiler. There's still work to get there for sure, but just wanted to add context as someone who wants to see more formally proven software.
- hajile 4y ago
  That's an even bigger problem. Running through every possible x86 instruction is out of the question. Even provably creating every possible instruction scenario would be all but impossible. Caching is a very hard problem. Add in a bunch of neural networks to control those caches and programmers aren't even sure what's actually happening (let alone actually having formal verification). Large, Out-of-order chips use millions of lines of code to implement their algorithms in hardware. They do lots of unit testing and some formal verification of the smaller bits, but the sum of the parts isn't formally verified. It takes a half-decade to create a chip without formal verification. With complete formal verification, we might not even have the first Pentium ready to ship yet (if ever). While we're on the topic, very few programming language implementations are formally verified. For example, L4 was verified using Isabelle which is written in StandardML and compiled using the PolyML compiler. I don't believe the PolyML compiler is formally verified. This means that Isabelle isn't formally verified when compiled which means that L4 isn't formally verified either (technically speaking). And of course, even if all of these were verified, there's the "trusting trust" issue and the fact that the compiler must be running on a formally verified CPU. I appreciate striving for formal verification, but code verifiable from the bottom-up is a very long way away from happening.
mbrodersen 4y ago
> The halting problem says that you cannot make this guarantee for ANY sufficiently complex program. That is correct but also completely irrelevant. In practice all software we actually use and need can be written in languages that are slightly less powerfully than Turing complete languages. Look at CompCert, seL4, Dafny, Coq, LEAN, F-Star etc. etc.

by hajile 4y ago

School-Cotton 4y ago

No it doesn’t. It says there are some programs for which you can’t make this guarantee.

willis936 4y ago

It's a high standard, but it is the standard for safety-critical systems. Nothing has changed about the problem, so the goal posts should stay where they are despite what new tools we have.

tralarpa 4y ago

That might be the reason why the JPL coding standard says: "All loops shall have a statically determinable upper-bound on the maximum number of loop iterations. It shall be possible for a static compliance checking tool to affirm the existence of the bound. An exception is allowed for the use of a single non-terminating loop per task or thread where requests are received and processed. Such a server loop shall be annotated with the C comment: /* @non-terminating@ */."

hajile 4y ago
It took around 5-10 man-years to verify the L4 kernel using a theorem prover and that's just 8700 LOC plus 600 lines of assembly. Without such a theorem solver, it is all just "best practices" then hoping for the best.
- ducktective 4y ago
  Is there a tech stack or language that allows us to write formally proven and real-time (bounded-time tasks) for embedded systems? What if we can be lenient on these conditions (like soft real time, 500ms bounds)? I'm looking for something like shell scripting (easy and functional) + busybox set of utilities + language built-ins to write concurrent applications. Like an OS with a specialized shell scripting language. Does something like this exist?
  - psd1 4y ago
    cgi-bin
  - mbrodersen 4y ago
    I am currently playing around with Dafny and it is very promising. I have use it to generate proven correct high-performance C# code without too much efforts. It’s great fun actually. Like a really cool puzzle game.

deleted 4y ago

[deleted]

ablob 4y ago

Yet I can give you an estimate of the runtime of multiple programs I use to an accuracy within seconds (order of magnitude is hours). The halting problem itself is a good estimate for computational complexity (i.e. can my thing simulate a TM) and makes statements for the general case, but that's just it: the general case. There are a whole class of programs/languages that are decidable (i.e. they will terminate) and that can be proven as well by automated means. Now this does depend on what you mean with sufficiently complex, but for special programs you can prove a lot of things (by hand); the halting problem does not prevent that. However, a side effect is that you may not be able to prove that property for the program you want.

hajile 4y ago
> Yet I can give you an estimate of the runtime of multiple programs I use to an accuracy within seconds (order of magnitude is hours). Can you do this for all possible inputs? If not, then your informal pinky swear that it really will get things done on time isn't worth very much.

typon 4y ago

No, that's a misunderstanding. It says you can't come up with a general algorithm for arbitrary programs to detect whether they will halt, it says nothing about particular programs.

hajile 4y ago
That is true in theory, but not in practice. A large program is itself essentially composed of many subprograms. You must prove every single aspect of those subprograms (hard in and of itself) then you must prove that every possible combination of those subprograms is also provable. As there is no general formula for the halting problem, each combination must be uniquely proven. This essentially means that if you have N possible branches, then the difficulty proving for each unique case would be the factorial of N. Proving 9kloc of code for L4 took 5-10 man years. Adding just 1kloc of similarly dense code would likely add decades of man-years. What about 100kloc or 1mloc? Even if you could find tricks to optimize similar branches, the fundamental factorial problem doesn't go away (as making it go away would mean that you've solved the provably insolvable halting problem). In practice, only the most trivial of programs are completely provable before the heat death of the universe.

monocasa 4y ago

Part of why L4 took man years to prove is that the proof contains all sorts of stuff like the formal model of ARM machine code. Ideally we'd get to a point where those models can be shared across projects, just like for running software we don't start each project by writing a compiler. There's still work to get there for sure, but just wanted to add context as someone who wants to see more formally proven software.

hajile 4y ago
That's an even bigger problem. Running through every possible x86 instruction is out of the question. Even provably creating every possible instruction scenario would be all but impossible. Caching is a very hard problem. Add in a bunch of neural networks to control those caches and programmers aren't even sure what's actually happening (let alone actually having formal verification). Large, Out-of-order chips use millions of lines of code to implement their algorithms in hardware. They do lots of unit testing and some formal verification of the smaller bits, but the sum of the parts isn't formally verified. It takes a half-decade to create a chip without formal verification. With complete formal verification, we might not even have the first Pentium ready to ship yet (if ever). While we're on the topic, very few programming language implementations are formally verified. For example, L4 was verified using Isabelle which is written in StandardML and compiled using the PolyML compiler. I don't believe the PolyML compiler is formally verified. This means that Isabelle isn't formally verified when compiled which means that L4 isn't formally verified either (technically speaking). And of course, even if all of these were verified, there's the "trusting trust" issue and the fact that the compiler must be running on a formally verified CPU. I appreciate striving for formal verification, but code verifiable from the bottom-up is a very long way away from happening.

mbrodersen 4y ago

> The halting problem says that you cannot make this guarantee for ANY sufficiently complex program. That is correct but also completely irrelevant. In practice all software we actually use and need can be written in languages that are slightly less powerfully than Turing complete languages. Look at CompCert, seL4, Dafny, Coq, LEAN, F-Star etc. etc.