[lkml]   [1998]   [Jul]   [30]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
Messages in this thread
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.


Nah, it's not hard.

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


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
Please read the FAQ at

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