Date: Sun, 27 Jul 2003 13:59:13 +0200 From: Alexander Leidinger <Alexander@Leidinger.net> To: "Poul-Henning Kamp" <phk@phk.freebsd.dk> Cc: cvs-all@freebsd.org Subject: Re: 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 Message-ID: <20030727135913.0d2c3725.Alexander@Leidinger.net> In-Reply-To: <62633.1059304135@critter.freebsd.dk> References: <20030727121643.6daa5486.Alexander@Leidinger.net> <62633.1059304135@critter.freebsd.dk>
next in thread | previous in thread | raw e-mail | index | archive | help
On Sun, 27 Jul 2003 13:08:55 +0200 "Poul-Henning Kamp" <phk@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...). >=20 > Yes I think it would, but you would have to find a way to prove to=20 > 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=FCcken 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. --=20 0 and 1. Now what could be so hard about that? http://www.Leidinger.net Alexander @ Leidinger.net GPG fingerprint =3D C518 BC70 E67F 143F BE91 3365 79E2 9C60 B006 3FE7
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20030727135913.0d2c3725.Alexander>