> Oliver Xymoron wrote:
> > > I'd really like a tool that can check for missing locks, redundant
> > > locks, operations that should be atomic, missing memory barriers, that
> > > sort of thing. It's not easy is it? :-)
> >
> > 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? So you can
now solve the halting problem statically? Bzzt. It's more subtle than
that.
A problem that's closely related to the halting problem (and your proposed
lock checking tool) is the so called "busy beaver" problem. Simply put, a
busy beaver is a Turing machine that given no input, produces a maximally
long list of 1's on output before eventually halting.
Here's what the known best busy beavers are:
# of states length of output
1 1
2 4
3 6
4 13
5 >= 4098 (but still looking)
6 >= 95524079 (but still looking)
7 no one knows, but probably greater than the number of
particles in the universe
Considering that an n-state Turing machine can be coded in about n-squared
lines of switch statement (or an n-squared array declaration), it becomes
clear that even very simple programs can have incomprehensibly complex
behavior.
http://cis.csuohio.edu/~somos/beaver.ps
-- "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/