Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!udel!haven!adm!cmcl2!kramden.acf.nyu.edu!brnstnd From: brnstnd@kramden.acf.nyu.edu (Dan Bernstein) Newsgroups: comp.lang.misc Subject: Re: Array references cannot be made optimal Message-ID: <3975:Nov1323:25:4390@kramden.acf.nyu.edu> Date: 13 Nov 90 23:25:43 GMT References: <23904:Nov905:22:5290@kramden.acf.nyu.edu> <11839@life.ai.mit.edu> Organization: IR Lines: 108 Here are two articles about the practical solution to the halting problem. The first, from February this year, is short and should give people an idea of the resources implied by ``practical solution.'' (Practical enough that it could reasonably be an option in Saber-C.) The second, from January 1989, was my first posting of the solution, on comp.theory. I remember having just finished reading an article in good old Dr. Dobbs about the halting problem. It gave the usual presentation of the theory, but went out on a limb and said that the halting problem wasn't solvable in practice. As happens so often in computer `science,' the limb wasn't connected to the tree's trunk. After seeing a similarly unjustified statement in a discussion in comp.lang.c and comp.theory, I was sufficiently annoyed to write the article. Several months ago someone from England seemed interested in implementing the method. I don't know what's come of it. Oh, well. ---Dan >From: brnstnd@stealth.acf.nyu.edu Newsgroups: comp.software-eng Subject: Re: Have *YOU* ever written a program which COULDN'T be proven correct? Message-ID: <3803:04:53:29@stealth.acf.nyu.edu> Date: 14 Feb 90 04:53:30 GMT Distribution: usa In article <793@arc.UUCP> steve@arc.UUCP (Steve Savitzky) writes: > I think you missed my point, which is that whether or not the halting > problem can be solved *in theory* for real programs on real computers, > it cannot be solved *in practice*. A year ago I posted a short note to comp.theory titled Finite Halting Problem Considered Solvable. The gist of it is that you can solve the halting problem for a program using just twice the memory and thrice the time. In practice, with language support, you designate certain variables to be tested for looping. Those variables are stored twice, and the program runs at a third of the speed. If those variables together enter a loop, the loop will be detected during its first period. For some programs this could be very useful. ---Dan >From: bernsten@phoenix.UUCP (Dan Bernstein) Newsgroups: comp.theory Subject: Finite Halting Problem Considered Solvable Message-ID: <8901162049.AA11027@jade.berkeley.edu> Date: 16 Jan 89 16:32:35 GMT Sender: daemon@ucbvax.BERKELEY.EDU Reply-To: TheoryNet List , Dan Bernstein Distribution: inet Organization: The Internet Lines: 52 The halting problem is to determine whether a given program loops forever. This is an uncomputable function of a program, as we all know. But if a program is restricted to a finite number of states then the problem is computable. The practical solution is that we run the program on two machines with that number of states, one machine exactly twice as fast as the other; if the program loops in time t to t+u, then we will see the machines in exactly the same state at time 3t to 3t+3u. Now consider modern, real computers. The space needed for this is practical. But the time is a trickier consideration. How do we compare the states of two computers? The solution is that in unit time a computer modifies a bounded-size portion of its state as expressed in bits. So we merely watch what registers, memory bytes, etc. are changed, incrementing a difference count when something is made different on the two machines and decrementing it when something is made the same. As a matter of fact, this (at least for memory) is already done by good caches. It would be a simple modification to those caches designed for multiprocessors to have them keep track of (1) registers and flags as well as memory and (2) a difference count. Of course, this eminently practical hardware solution is only appropriate if the entire machine is involved in a single computation that we don't want to have accidentally looping. But I'd say that the problem is practically solvable in software for many situations. For example, MACSYMA and similar programs could have a feature that a user-defined function be run three times slower and have it detect infinite loops of variables blah, blah, and blah in the function. I would expect that this be restricted to non-recursively written functions, and restricted to functions that don't use non-mathematical stuff like reading from a disk file---but it's still quite doable and would be a real, live, practical solution to the halting problem. More ambitiously, I can see how a C compiler could compile a function to detect infinite loops. The function would probably run somewhat slower than just three times, as most optimizations would go down the drain and dealing with the difference count would be a major speed factor relative to the speed of single expressions. And yes, it would take double the memory---which could be a problem if the function had an array taking an amount of space comparable to the space available on the machine. And I would expect the restriction that the function and everything it calls must use only built-in C, no system calls or anything else possibly external; and also that the function and everything it calls must only use variables local to themselves. But after all these caveats this still remains a valuable tool that I would have loved to have for testing many programs: the practical solution to the halting problem. ---Dan Bernstein, bernsten@phoenix.princeton.edu