From owner-cvs-all@FreeBSD.ORG Sun Jul 27 03:16:53 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 845D537B401; Sun, 27 Jul 2003 03:16:53 -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 6C4B343F85; Sun, 27 Jul 2003 03:16:52 -0700 (PDT) (envelope-from Alexander@Leidinger.net) Received: from fwd03.aul.t-online.de by mailout04.sul.t-online.com with smtp id 19gia9-0005CJ-00; Sun, 27 Jul 2003 12:16:49 +0200 Received: from Andro-Beta.Leidinger.net (G5KGKTZTremfvWlB7act-3obklD4NvAopdnHDExcvGB2VV37GpmEE1@[217.83.18.165]) by fmrl03.sul.t-online.com with esmtp id 19giZw-2IbVWC0; Sun, 27 Jul 2003 12:16:36 +0200 Received: from Magelan.Leidinger.net (Magelan [192.168.1.1]) h6RAGa9P047456; Sun, 27 Jul 2003 12:16:37 +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 h6RAGhFs001121; Sun, 27 Jul 2003 12:16:43 +0200 (CEST) (envelope-from Alexander@Leidinger.net) Date: Sun, 27 Jul 2003 12:16:43 +0200 From: Alexander Leidinger To: "Poul-Henning Kamp" Message-Id: <20030727121643.6daa5486.Alexander@Leidinger.net> In-Reply-To: <62161.1059300156@critter.freebsd.dk> References: <20030727115457.553f1df7.Alexander@Leidinger.net> <62161.1059300156@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=US-ASCII Content-Transfer-Encoding: 7bit X-Seen: false X-ID: G5KGKTZTremfvWlB7act-3obklD4NvAopdnHDExcvGB2VV37GpmEE1@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 10:16:54 -0000 On Sun, 27 Jul 2003 12:02:36 +0200 "Poul-Henning Kamp" wrote: > >Are you talking about e.g. model checking? After Aug 2 I plan to look at > >porting 2 major open source model checkers. > > I don't think you could have gotten an accountant to explain what > a spread-sheet would do back in the days before VisiCalc, but once > the idea was out, everybody could see that it was brilliant. > > 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...). Bye, Alexander. -- The dark ages were caused by the Y1K problem. http://www.Leidinger.net Alexander @ Leidinger.net GPG fingerprint = C518 BC70 E67F 143F BE91 3365 79E2 9C60 B006 3FE7