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).
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.
-- "Love the dolphins," she advised him. "Write by W.A.S.T.E.."- 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:07 EST