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

[Alexander Leidinger]

On Sun, 27 Jul 2003 13:08:55 +0200
"Poul-Henning Kamp" <phk at phk.freebsd.dk> wrote:

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

Sort of... you need an abstract (high level) model of what you want to
achieve. There you can check the model if it fulfills some constraints
(no deadlocks, mutual exclusion, ...). This way you can check for design
errors. To verify that the actual implementation is an instance of thos
high level model, you need a model of what your source does (partially
autogenerated). This model is far more complex than the abstract one.
Now you let the model checker compare both models (uppaal generates a
minimal state machine out of the models and compares them).

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

I don't know if uppaal is able to generate models out of source already
(I hadn't time to investigate it that deep), but there's definitively
active research happening in this direction (as far as I know the german
government sponsors some researchers (3 groups) here in Saarbrücken
which actually work on trying to prove everything from a CPU upto the
OS/programs; if someone is interested I can provide some URLs).

Bye,
Alexander.

-- 
            0 and 1. Now what could be so hard about that?

http://www.Leidinger.net                       Alexander @ Leidinger.net
  GPG fingerprint = C518 BC70 E67F 143F BE91  3365 79E2 9C60 B006 3FE7