lkml.org 
[lkml]   [1998]   [Jul]   [30]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
From
Date
SubjectRe: [patch] IDE problems on SMP, fixed? (fwd)
Linus Torvalds writes:
> 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.

<troll>

Nah, it's not hard.

First, you rewrite the kernel in ML... ;)

</troll>

But this has set me wondering. Is it remotely possible to do something
like this? An assertion-checking tool like GNU nana could help, but
that particular tool - and, probably, all similar tools - have the
disadvantage that they render your source almost illegible :(

Strictly speaking if we wanted a generic tool we'd need to verify a
lot more than calling sequences. There's calling thru function
pointers, for a start (does that go on to any significant degree
within the kernel, though? For context switches it obviously has to
but that's accompanied by ring transitions &c so it hardly counts;
we're not trying to validate user-level too)...

I shall have to think about this.

--
`It is inelegant and it was hacked on. But it was hacked on with
careful consideration.' - PLA on perl and OO

-
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    [from the cache]
©2003-2011 Jasper Spaans