From owner-cvs-src@FreeBSD.ORG  Sun Jul 27 04:09:04 2003
Return-Path: <owner-cvs-src@FreeBSD.ORG>
Delivered-To: cvs-src@freebsd.org
Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125])
	by hub.freebsd.org (Postfix) with ESMTP
	id 9092537B401; Sun, 27 Jul 2003 04:09:04 -0700 (PDT)
Received: from phk.freebsd.dk (phk.freebsd.dk [212.242.86.175])
	by mx1.FreeBSD.org (Postfix) with ESMTP
	id 6962F43F93; Sun, 27 Jul 2003 04:09:03 -0700 (PDT)
	(envelope-from phk@phk.freebsd.dk)
Received: from critter.freebsd.dk (critter.freebsd.dk [212.242.86.163])
	by phk.freebsd.dk (8.12.8/8.12.8) with ESMTP id h6RB8uV3023281;
	Sun, 27 Jul 2003 11:08:56 GMT
	(envelope-from phk@phk.freebsd.dk)
Received: from critter.freebsd.dk (localhost [127.0.0.1])
	by critter.freebsd.dk (8.12.9/8.12.9) with ESMTP id h6RB8t5H062634;
	Sun, 27 Jul 2003 13:08:55 +0200 (CEST)
	(envelope-from phk@phk.freebsd.dk)
To: Alexander Leidinger <Alexander@Leidinger.net>
From: "Poul-Henning Kamp" <phk@phk.freebsd.dk>
In-Reply-To: Your message of "Sun, 27 Jul 2003 12:16:43 +0200."
             <20030727121643.6daa5486.Alexander@Leidinger.net> 
Date: Sun, 27 Jul 2003 13:08:55 +0200
Message-ID: <62633.1059304135@critter.freebsd.dk>
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-src@freebsd.org
X-Mailman-Version: 2.1.1
Precedence: list
List-Id: CVS commit messages for the src tree <cvs-src.freebsd.org>
List-Unsubscribe: <http://lists.freebsd.org/mailman/listinfo/cvs-src>,
	<mailto:cvs-src-request@freebsd.org?subject=unsubscribe>
List-Archive: <http://lists.freebsd.org/pipermail/cvs-src>
List-Post: <mailto:cvs-src@freebsd.org>
List-Help: <mailto:cvs-src-request@freebsd.org?subject=help>
List-Subscribe: <http://lists.freebsd.org/mailman/listinfo/cvs-src>,
	<mailto:cvs-src-request@freebsd.org?subject=subscribe>
X-List-Received-Date: Sun, 27 Jul 2003 11:09:05 -0000

In message <20030727121643.6daa5486.Alexander@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@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.