cvs commit: src/sys/kern init_main.c kern_malloc.c md5c.c subr_autoconf.c subr_mbuf.c subr_prf.c tty_subr.c vfs_cluster.c vfs_subr.c

[Poul-Henning Kamp]

In message <20030727121643.6daa5486.Alexander at Leidinger.net>, Alexander Leiding
er writes:

>> If I knew what the tools were, I would have been busy writing them
>> years ago, but unfortunately, I don't seem to be the one destined
>> to invent the programmers spread-sheet.
>
>http://www.uppaal.com/
>
>I think it would allow to test the locking assumptions (if you have a
>model of the kernel...).

Yes I think it would, but you would have to find a way to prove to 
yourself that your model was in fact precise and faithful relative to
the kernel source.

I'm still hoping that some day we will have tools which will read
source code and alert us to things which doesn't make sense or which
looks dubious.

-- 
Poul-Henning Kamp       | UNIX since Zilog Zeus 3.20
phk at FreeBSD.ORG         | TCP/IP since RFC 956
FreeBSD committer       | BSD since 4.3-tahoe    
Never attribute to malice what can adequately be explained by incompetence.