oxymoron@waste.org (Oliver Xymoron) wrote on 24.04.00 in <Pine.LNX.4.10.10004240820290.1607-100000@waste.org>:
> On Mon, 24 Apr 2000, Jamie Lokier wrote:
>
> > Oliver Xymoron wrote:
> > > > > It's provably equivalent to the halting problem, assuming you even
> > > > > have enough info in the source to automatically identify things
> > > > > that need atomicity. Anything with recursion or coroutines is
> > > > > liable to make it very unhappy.
> > > > >
> > > > > That said, quite a bit can be done with runtime checks ala the
> > > > > spinlock debugging code that can't be done by static analysis.
> > > >
> > > > Everything that can be found using runtime tests can be found
> > > > statically in at most exponential time, except network protocols :-)
> > >
> > > Huh. So you can test for halt at runtime with atexit(), right?
> >
> > Everything you can test at runtime, yes. By simulation, and considering
> > all possible digital inputs as you go. (Hence exponential time).
>
> Exponential in the number of branches and possible inputs seen during
> execution, not lines of code. Since loops allow code to be visited an
> infinite number of times and have the context (memory, stack, input) be
> different every time, this gets out of hand very quickly.
>
> > That's not a complete proof -- and so does not solve the halting
> > problem. Neither does any runtime check.
>
> Waiting for exit is a runtime check for halt by definition and is O(1).
Sure, but it's *NOT* a solution to the halting problem.
It doesn't prove that the program halts for any input other than the one
given, and it cannot ever prove that the program does not halt. (Only that
it does not halt in X time.)
The situations it can prove, you can obviouysly also prove by simulation.
But with simulation, you can actually (try to) prove it for whole classes
of input, by following the decision paths "in parallel" (thus, exponential
time). That's actually more powerful than real runtime checks.
> There are runtime checks for deadlock that are O(number of locks^2) or
> better. But they're not speculative - they do the test each time you take
> a lock. Neither of these can be used for static analysis though.
You can, of course, trivially simulate those checks, too.
You can always prove that something halts or does not halt in a given
finite time. That's no big feat, and it's not the halting problem.
MfG Kai
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu
Please read the FAQ at http://www.tux.org/lkml/
This archive was generated by hypermail 2b29 : Sun Apr 30 2000 - 21:00:08 EST