From owner-cvs-all@FreeBSD.ORG Sun Jul 27 04:59:14 2003 Return-Path: Delivered-To: cvs-all@freebsd.org Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125]) by hub.freebsd.org (Postfix) with ESMTP id 059DB37B401; Sun, 27 Jul 2003 04:59:14 -0700 (PDT) Received: from mailout04.sul.t-online.com (mailout04.sul.t-online.com [194.25.134.18]) by mx1.FreeBSD.org (Postfix) with ESMTP id 8CB1343F85; Sun, 27 Jul 2003 04:59:12 -0700 (PDT) (envelope-from Alexander@Leidinger.net) Received: from fwd08.aul.t-online.de by mailout04.sul.t-online.com with smtp id 19gkBD-0007zU-04; Sun, 27 Jul 2003 13:59:11 +0200 Received: from Andro-Beta.Leidinger.net (Gt0vnqZrYeM7-4vMvTCBgMuKj7pLW5RBbwInou7V+jxadQsjGDaBoo@[217.83.18.165]) by fmrl08.sul.t-online.com with esmtp id 19gkBB-27mpEW0; Sun, 27 Jul 2003 13:59:09 +0200 Received: from Magelan.Leidinger.net (Magelan [192.168.1.1]) h6RBx79P047669; Sun, 27 Jul 2003 13:59:07 +0200 (CEST) (envelope-from Alexander@Leidinger.net) Received: from Magelan.Leidinger.net (netchild@localhost [127.0.0.1]) by Magelan.Leidinger.net (8.12.9/8.12.9) with SMTP id h6RBxDFs001632; Sun, 27 Jul 2003 13:59:13 +0200 (CEST) (envelope-from Alexander@Leidinger.net) Date: Sun, 27 Jul 2003 13:59:13 +0200 From: Alexander Leidinger To: "Poul-Henning Kamp" 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> X-Mailer: Sylpheed version 0.9.3claws (GTK+ 1.2.10; i386-portbld-freebsd5.1) Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Seen: false X-ID: Gt0vnqZrYeM7-4vMvTCBgMuKj7pLW5RBbwInou7V+jxadQsjGDaBoo@t-dialin.net cc: cvs-src@freebsd.org cc: src-committers@freebsd.org cc: dds@freebsd.org 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 X-BeenThere: cvs-all@freebsd.org X-Mailman-Version: 2.1.1 Precedence: list List-Id: CVS commit messages for the entire tree List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 27 Jul 2003 11:59:14 -0000 On Sun, 27 Jul 2003 13:08:55 +0200 "Poul-Henning Kamp" 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