lkml.org 
[lkml]   [1998]   [Jul]   [30]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [patch] IDE problems on SMP, fixed? (fwd)


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
as

- 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.

Linus


-
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.altern.org/andrebalsa/doc/lkml-faq.html

\
 
 \ /
  Last update: 2005-03-22 13:43    [W:2.411 / U:0.012 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site