Alexander Viro wrote:
>
> On Tue, 9 Jul 2002, Arnaldo Carvalho de Melo wrote:
>
>>Em Tue, Jul 09, 2002 at 02:47:49PM -0700, Robert Love escreveu:
>>
>>>On Tue, 2002-07-09 at 07:44, Dave Hansen wrote:
>>>
>>>>The Stanford Checker or something resembling it would be invaluable
>>>>here. It would be a hell of a lot better than my litle patch!
>>>
>>>The Stanford Checker would be infinitely invaluable here -- agreed.
>>>
>>>Anything that can graph call chains and do analysis... we can get it to
>>>tell us exactly who and what.
>
> Not anything. It can be used to find problems (and be very helpful at that)
> but it can't be used to verify anything.
>
> The problem is that checker doesn't (and cannot) cover all code paths -
> by the time when it comes into the game the source had already passed
> through through cpp. In other words, depending on the configuration
> you might get very different results.
I have the feeling that the filesystems' use of lots of function
pointers will add a large amount of complexity to whatever programming
any checker would require. Bill Irwin and I were discussing it and we
have ways of getting around most of them, but there are _lots_ of
special cases.
"Proving" correctness would obviously be ideal, but in an imperfect
world, what are your feelings on a runtime system for detecting
"magical/bad" BKL use? I'm not proposing my kludgy "printk if you're
bad" stuff, but something with much less impact. I would like to do
something somewhat like profile=2. During each lock_kernel(), the
program counter (any maybe more) could be stored in an internal kernel
structure and retrieved later via a /proc file, just like readprofile.
This wouldn't have intrusive printk messages, and would be able to
be activated by either a command-line parameter, or something else in
/proc. If we had this in our development kernel, interested
developers could pay attention to the output, while the normal kernel
developer could simply ignore it.
> Normally it's not that bad, but "can this function block?" is very nasty
> in that respect - changes of configuration can and do affect that in
> non-trivial ways.
I also wonder how it handles things like kmalloc(), which can block
depending on arguments.
-- Dave Hansen haveblue@us.ibm.com- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/
This archive was generated by hypermail 2b29 : Mon Jul 15 2002 - 22:00:16 EST