4 ms·

We give up on automated program analysis far too easily - even for "Turing complete" languages. To be truly Turing complete requires infinite memory. That clea

by cjg 6y ago

We give up on automated program analysis far too easily - even for "Turing complete" languages. To be truly Turing complete requires infinite memory. That clearly doesn't hold for any current programming language. Mathematical proofs are only applicable where their assumptions are valid. So why would we believe that the where memory isn't infinite (everywhere in practice) that Turing's halting analysis is applicable? Sure, automated program analysis might not be easy, but that doesn't mean we should just give up. Indeed I have a simple algorithm (although relatively inefficient) to solve the halting problem where memory size is fixed and finite: enumerate every state until either a state is repeated or the program halts. This completes in O(2^N) time where N is the size of the memory. But I'm sure someone clever will come up with a more efficient algorithm than that. I already have several ideas that this margin is too small to contain. For me the tricky bits are where a loop terminates if and only if Goldbach's conjecture is true (or similar) - but perhaps a compiler could require an "unsafe" block for such code (in the vein of Rust).

Strilanc 6y ago
The halting problem proof will work fine on finite sizes, I think. Failing due to an infinite loop will just be replaced by going out of memory. The main caveat would be if the solver fills memory then the diagonalized solver (which is slightly larger) won't fit on the machine.
- Conlectus 6y ago
  For finite sized memory, the problem can be solved by recording every system state (registers, memory values etc.) and seeing if the same state is ever reached twice. If so, the program will never terminate, and vice versa.
  - Strilanc 6y ago
    For clarification: I was imagining the the solver machine had the same number of resources as the problem machine (e.g. same length of tape, same number of states). I of course agree that there is a Turing machine that decides the computability of LBAs. When I said the problem still existed I meant you'd need e.g. larger and larger LBAs to solve the LBA problem up to a given size and that an LBA of tape size K with M states could not solve the halting problem for all LBAs of that size.
- light_hue_1 6y ago
  It does not. A Turing machine with a finite tape is called a Linear Bounded Automaton. Halting is decidable for LBAs, but we don't know of any particularly fast algorithms for doing so.
  - Strilanc 6y ago
    For clarification: I was imagining the the solver machine had the same number of resources as the problem machine (e.g. same length of tape, same number of states). I of course agree that there is a Turing machine that decides the computability of LBAs.
jerf 6y ago
"Mathematical proofs are only applicable where their assumptions are valid. So why would we believe that the where memory isn't infinite (everywhere in practice) that Turing's halting analysis is applicable?" Because adding the assumption in that memory is finite doesn't make the analysis easier, it makes it harder. There's a reason the abstract mathematical model assumes infinite memory; it isn't because the abstract mathematical model can assume into existence, so, you know, why not, it's to simplify it. Now in addition to all the other things the mathematical proof has to worry about, it has to be constructed in such a way that if at any point memory is exceeded, it also "halts". That is way easier said than done. As a homework exercise, try to take the halting problem proof and update it to include the possibility that either the halting-detection machine or the machine it is simulating (within the boundaries of the halting-detection machine's resources!) runs out of memory. Pro-tip: If you think you cracked it in a couple of minutes, you did not. For instance, now rather than just waving at the fact the halting-detection machine is running a Universal Turing machine that simply has some "linear" factor of expansion in memory usage and/or runtime and not worrying since you have infinite amounts of both, now your proof is going to be intimately concerned with the details of exactly how the universal turing machine is encoded. What you end up with at the end won't be some neat claim about how the halting problem is impossible, you're going to end up with some rather complicated contingent claim with terms that will include specific details about the size of the encoding and the amount of memory given to the detection machine. If you do this work honestly and thoroughly, you'll quickly learn that adding finiteness of resource doesn't make the problem more tractable. Rather than a cute little statement about the halting problem, you'll end up with an incredibly complicated statement with dozens of terms in it about what the detection machine can and can not do, and the resulting mathematical statement will be much harder to use. "This completes in O(2^N) time where N is the size of the memory." In other words, our computers are finite state machines, which is basically true, so attack them with finite state machine tools. The problem is that even if your "finite state machine" you're modeling is, say, a Commodore 64, and even if you ignore external input and just simulate the machine itself, you have an intractable problem on your hands. The problem grows exponentially as you add each individual bit. Modern computers have a lot more bits than a Commodore 64. This turns out not to be a useful approach. If you're going to go this route, what you're looking for are sub-Turing programming languages [1] that allow you to write programs in a reduced-power environment that allows more useful assertions to be made. If you are legitimately interested in this, there's a lot of research occurring on the fun fringes of programming language research. But... I can tell you that they are certainly far from a magic wand either. At a minimum, it requires a huge mindset change, and it is very difficult to fit even some common problems/algorithms into the requisite constraints. And "completes in a finite period of time", even if you can prove it, can be a rather vague promise to make. [1]: Example from a quick google: http://ainfosec.github.io/crema/ http://ainfosec.github.io/crema/
teraflop 6y ago
> To be truly Turing complete requires infinite memory. That clearly doesn't hold for any current programming language. > Indeed I have a simple algorithm (although relatively inefficient) to solve the halting problem where memory size is fixed and finite: enumerate every state until either a state is repeated or the program halts. This completes in O(2^N) time where N is the size of the memory. "Relatively inefficient" is a colossal understatement. Anything that we would nowadays categorize as a "computer" has a state space so huge that, while technically finite, it is effectively infinite for all practical purposes. For example: the ATmega328 microcontroller in an Arduino has 2KB of RAM (assuming we ignore registers and the possibility of storing data in Flash). That's a total of 2^16384 possible states. If every cubic Planck length of the observable universe was capable of checking one of these states per Planck time, and did so from the Big Bang until the heat death of the universe (let's say 10^100 years in the future), they would still have enumerated only a googol'th of a googol'th of a googol'th of a googol'th [... repeat about 10 more times...] of the state space. We could of course imagine trying to find a better algorithm, but since this problem is easily shown to be NP-hard, it is very unlikely that we will find something that guarantees good enough performance to make this kind of analysis possible. We haven't "given up" on automated program analysis. It's just that the fully general case is intractable, and it takes a lot of hard work and ingenuity to find strategies that can separate the tractable problems we care about from the intractable ones.
josalhor 6y ago
> That clearly doesn't hold for any current programming language. To be fair, programming language != implementation. A language can be Turing complete without the implementation being complete. > to solve the halting problem where memory size is fixed and finite Just to clarify any lost reader: The halting problem describes halting on Turing Machines, the algorithm presented only works because Turing Machines that have finite memory are not Turing Machines. > For me the tricky bits are where a loop terminates if and only if Goldbach's conjecture is true (or similar) - but perhaps a compiler could require an "unsafe" block for such code (in the vein of Rust). This is for me the most interesting part of your comment and something I have also thought about. This lead me in an interesting rabbit hole: Most of the lines of code we write don't require Turing Completeness. i.e. When we do `for i in 0..10` we are iterating over a finite range of memory, we can prove we will finish (which appears to be easier than proving we will not finish). If you loop a finite set of times and do a finite set of work each time you will eventually finish. This made me realize that if you know your input, the only regions of code something like what you are proposing would work are `while True` loops, recursive code, stream consumption (which in reality is just a fancy version of a while True), and functions where you cannot prove if the number of loops is finite (i.e Some inner part of the loop may reset the outer loop), etc...(there are some other examples out of scope). From those, it looks to me like only the last group would truly benefit, the rest are relatively easy to spot. But notice the big caveat, all of this only works at runtime (when you know the amount of work you have to do per loop). At compile time, it only really works for really small regions of code. So as far as I can reason, this kind of static analysis would not be as beneficial as one may originally think.
- chriswarbo 6y ago
  > So as far as I can reason, this kind of static analysis would not be as beneficial as one may originally think. There are many advantages to total (terminating/coterminating) programming languages. It's not so much about throwing some random Java/C/whatever codebase at a tool and expecting useful results; it's more about making languages themselves more consistent, simpler, etc. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.364&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106...

by cjg 6y ago

Strilanc 6y ago

The halting problem proof will work fine on finite sizes, I think. Failing due to an infinite loop will just be replaced by going out of memory. The main caveat would be if the solver fills memory then the diagonalized solver (which is slightly larger) won't fit on the machine.

Conlectus 6y ago
For finite sized memory, the problem can be solved by recording every system state (registers, memory values etc.) and seeing if the same state is ever reached twice. If so, the program will never terminate, and vice versa.
- Strilanc 6y ago
  For clarification: I was imagining the the solver machine had the same number of resources as the problem machine (e.g. same length of tape, same number of states). I of course agree that there is a Turing machine that decides the computability of LBAs. When I said the problem still existed I meant you'd need e.g. larger and larger LBAs to solve the LBA problem up to a given size and that an LBA of tape size K with M states could not solve the halting problem for all LBAs of that size.
light_hue_1 6y ago
It does not. A Turing machine with a finite tape is called a Linear Bounded Automaton. Halting is decidable for LBAs, but we don't know of any particularly fast algorithms for doing so.
- Strilanc 6y ago
  For clarification: I was imagining the the solver machine had the same number of resources as the problem machine (e.g. same length of tape, same number of states). I of course agree that there is a Turing machine that decides the computability of LBAs.

jerf 6y ago

"Mathematical proofs are only applicable where their assumptions are valid. So why would we believe that the where memory isn't infinite (everywhere in practice) that Turing's halting analysis is applicable?" Because adding the assumption in that memory is finite doesn't make the analysis easier, it makes it harder. There's a reason the abstract mathematical model assumes infinite memory; it isn't because the abstract mathematical model can assume into existence, so, you know, why not, it's to simplify it. Now in addition to all the other things the mathematical proof has to worry about, it has to be constructed in such a way that if at any point memory is exceeded, it also "halts". That is way easier said than done. As a homework exercise, try to take the halting problem proof and update it to include the possibility that either the halting-detection machine or the machine it is simulating (within the boundaries of the halting-detection machine's resources!) runs out of memory. Pro-tip: If you think you cracked it in a couple of minutes, you did not. For instance, now rather than just waving at the fact the halting-detection machine is running a Universal Turing machine that simply has some "linear" factor of expansion in memory usage and/or runtime and not worrying since you have infinite amounts of both, now your proof is going to be intimately concerned with the details of exactly how the universal turing machine is encoded. What you end up with at the end won't be some neat claim about how the halting problem is impossible, you're going to end up with some rather complicated contingent claim with terms that will include specific details about the size of the encoding and the amount of memory given to the detection machine. If you do this work honestly and thoroughly, you'll quickly learn that adding finiteness of resource doesn't make the problem more tractable. Rather than a cute little statement about the halting problem, you'll end up with an incredibly complicated statement with dozens of terms in it about what the detection machine can and can not do, and the resulting mathematical statement will be much harder to use. "This completes in O(2^N) time where N is the size of the memory." In other words, our computers are finite state machines, which is basically true, so attack them with finite state machine tools. The problem is that even if your "finite state machine" you're modeling is, say, a Commodore 64, and even if you ignore external input and just simulate the machine itself, you have an intractable problem on your hands. The problem grows exponentially as you add each individual bit. Modern computers have a lot more bits than a Commodore 64. This turns out not to be a useful approach. If you're going to go this route, what you're looking for are sub-Turing programming languages [1] that allow you to write programs in a reduced-power environment that allows more useful assertions to be made. If you are legitimately interested in this, there's a lot of research occurring on the fun fringes of programming language research. But... I can tell you that they are certainly far from a magic wand either. At a minimum, it requires a huge mindset change, and it is very difficult to fit even some common problems/algorithms into the requisite constraints. And "completes in a finite period of time", even if you can prove it, can be a rather vague promise to make. [1]: Example from a quick google: http://ainfosec.github.io/crema/ http://ainfosec.github.io/crema/

teraflop 6y ago

> To be truly Turing complete requires infinite memory. That clearly doesn't hold for any current programming language. > Indeed I have a simple algorithm (although relatively inefficient) to solve the halting problem where memory size is fixed and finite: enumerate every state until either a state is repeated or the program halts. This completes in O(2^N) time where N is the size of the memory. "Relatively inefficient" is a colossal understatement. Anything that we would nowadays categorize as a "computer" has a state space so huge that, while technically finite, it is effectively infinite for all practical purposes. For example: the ATmega328 microcontroller in an Arduino has 2KB of RAM (assuming we ignore registers and the possibility of storing data in Flash). That's a total of 2^16384 possible states. If every cubic Planck length of the observable universe was capable of checking one of these states per Planck time, and did so from the Big Bang until the heat death of the universe (let's say 10^100 years in the future), they would still have enumerated only a googol'th of a googol'th of a googol'th of a googol'th [... repeat about 10 more times...] of the state space. We could of course imagine trying to find a better algorithm, but since this problem is easily shown to be NP-hard, it is very unlikely that we will find something that guarantees good enough performance to make this kind of analysis possible. We haven't "given up" on automated program analysis. It's just that the fully general case is intractable, and it takes a lot of hard work and ingenuity to find strategies that can separate the tractable problems we care about from the intractable ones.

josalhor 6y ago

> That clearly doesn't hold for any current programming language. To be fair, programming language != implementation. A language can be Turing complete without the implementation being complete. > to solve the halting problem where memory size is fixed and finite Just to clarify any lost reader: The halting problem describes halting on Turing Machines, the algorithm presented only works because Turing Machines that have finite memory are not Turing Machines. > For me the tricky bits are where a loop terminates if and only if Goldbach's conjecture is true (or similar) - but perhaps a compiler could require an "unsafe" block for such code (in the vein of Rust). This is for me the most interesting part of your comment and something I have also thought about. This lead me in an interesting rabbit hole: Most of the lines of code we write don't require Turing Completeness. i.e. When we do `for i in 0..10` we are iterating over a finite range of memory, we can prove we will finish (which appears to be easier than proving we will not finish). If you loop a finite set of times and do a finite set of work each time you will eventually finish. This made me realize that if you know your input, the only regions of code something like what you are proposing would work are `while True` loops, recursive code, stream consumption (which in reality is just a fancy version of a while True), and functions where you cannot prove if the number of loops is finite (i.e Some inner part of the loop may reset the outer loop), etc...(there are some other examples out of scope). From those, it looks to me like only the last group would truly benefit, the rest are relatively easy to spot. But notice the big caveat, all of this only works at runtime (when you know the amount of work you have to do per loop). At compile time, it only really works for really small regions of code. So as far as I can reason, this kind of static analysis would not be as beneficial as one may originally think.

chriswarbo 6y ago
> So as far as I can reason, this kind of static analysis would not be as beneficial as one may originally think. There are many advantages to total (terminating/coterminating) programming languages. It's not so much about throwing some random Java/C/whatever codebase at a tool and expecting useful results; it's more about making languages themselves more consistent, simpler, etc. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.364&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106...