Re: [patch] IDE problems on SMP, fixed? (fwd)

Linus Torvalds (
Thu, 30 Jul 1998 09:43:28 -0700 (PDT)

On Thu, 30 Jul 1998, David S. Miller wrote:
> Well, if we had a static analysis tool we'd obviously be able to track a
> lot of things that we can't currently track. You could build a tree of all
> calling sequences, and statically verify quite a few rules. You might not
> prove correctness, but you could find a lot of things like this.
> Dreaming? Yes.
> Actually, inside SunSoft there is such a tool for debugging locking
> rule violations in the solaris kernel.

If anybody feels like doing something like this, it shouldn't be
inherently hard to do at least a simplistic one. You may not be able to
follow function pointers etc, but essentially the only thing you need is a
"extended C" parser to parse "calling conventions" (the "extended" part
comes from the fact that macros and inline functions would be counted as
"calls" - and the fact that you have to "linearize" the functions to take
care of all conditionals and go through all combinations: the latter part
is the hard one).

That, together with certain rules (attach "attributes" to important call
points) and a simple algorithm to expand the attributes downwards to the
caller (and taking ordering and attribute merging and cancelation into
account) would make it possible to fairly reliably answer such questions

- do we ever call "lock_kernel()" or touch user mode pages with a
spinlock held or interrupts disabled?
- do we ever aquire certain semaphores or spinlocks in the wrong order.

etc etc.

It's a big project, but it could actually be fairly interesting (it would
certainly fit somebody looking for an academic project for a thesis or
similar: it is fairly theoretically oriented). It might be useful even in
a more limited form.


To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to
Please read the FAQ at