Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!think.com!samsung!crackers!m2c!risky.ecs.umass.edu!dime!chelm.cs.umass.edu!yodaiken
From: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Newsgroups: comp.lang.misc
Subject: Re: Will this *thread* ever halt?
Message-ID: <30835@dime.cs.umass.edu>
Date: 21 May 91 21:57:08 GMT
References: <3410@optima.cs.arizona.edu>
Sender: news@dime.cs.umass.edu
Organization: University of Massachusetts, Amherst
Lines: 80

In article <3410@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <30814@dime.cs.umass.edu> victor yodaiken writes:
>]... I argue that it is possible, in theory, for a C
>]compiler to detect all paths that lead to non-terminating loops and to
>]flag these paths.
>
>I argue that this is impossible in theory.  Infinite-loop detection
>state space of the algorithm in question.  Furthermore, in the general
>case this information must almost certainly require space on the order
>of the size of the set of all possible states at a given point in the
>program (see H1 below).
>
>If so, the amount of information needed for at least some classes of
>programs is huge.  So there are programs that would compile without
>this analysis that cannot be compiled with this analysis.
>Furthermore, due to the magnitude of the information that the
>algorithm has to keep around, I'll bet that _most_ nontrivial programs
>could not be analysed in this way.
>

Your argument is that the task is difficult, and would require
huge resources, possibly impractical resources, for most non-trivial
programs. No disagreement here. Impractical != impossible. You must
understand "in theory" in a nonstandard way. 


>Of course you can always reduce the amount of information you keep
>around by compacting many states into a single approximating state.
>If you do this you can greatly increase the set of programs you can
>analyse, but your analysis is only approximate.  You can make the
>approximation a safe one or a complete one: A safe approximation will
>recognize all programs that definitely will _not_ halt.  A complete
>approximation will recognize all programs that definitely _will_ halt.
>I expect that these approximations can be made good enough to be very
>useful.
>

I suspect that you are right. 

>Hypothesis H1:
>  any algorithm, HALT(p) that solves the halting problem for p must in
>general, for each point in p, encode at one time all the possible
>states that might occur at that point in p.
>
>Argument:
>  suppose HALT(p1) returns TRUE.  Create program p2 by adding
>somewhere the statement 
>
>  if (F()) exit(); else for(;;);
>
>where F is a function whose output depends on most of the current
>state.  Then HALT must be able to determine whether F can ever
>possibly answer 0 in order to tell if p2 halts.  To do this, in
>general HALT must be able to encode all possible states that might
>occur at this point.  It is possible to construct sets of states that
>cannot be encoded by anything much smaller than the entire set of
>states.
>
That's an interesting conjecture. For many cases it would be easy, even
if "F" looks at all of memory. For example, if F computes a checksum on
all of memory, then the possible state set of F would be huge, but it
would be easy to see that F does return 0 sometimes. Essentially, we
want to know if there is a path through F that terminates at some
"return 0" state, but we don't want to have to build the whole damn
state set of F.  People in hardware boolean circuit optimization and
in formal verification have been looking at this problem. I'll dig
up some references if anyone wants. Clarke and Burch recently reported that
in verification of bit-slice controllers, the state set of 10^20 elements
did not have to be completely unrolled, and that only 60,000 ( ?) or
so states had to be visited. But, your mileage may vary.


>Any HALT algorighm that attempts to avoid this by only doing one state
>at a time must in general deal with the possibility that HALT might
>not terminate, since it is simulating the program being analysed.  The
>same considerations apply to a program that works with subsets of the
>total set of possible states.

Yes. The HALT might not detect a loop, because it has thrown away the 
loop start state.  Is that your point?