Date: Sun, 27 Jul 2003 12:16:43 +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: <20030727121643.6daa5486.Alexander@Leidinger.net> In-Reply-To: <62161.1059300156@critter.freebsd.dk> References: <20030727115457.553f1df7.Alexander@Leidinger.net> <62161.1059300156@critter.freebsd.dk>
next in thread | previous in thread | raw e-mail | index | archive | help
On Sun, 27 Jul 2003 12:02:36 +0200 "Poul-Henning Kamp" <phk@phk.freebsd.dk> 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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20030727121643.6daa5486.Alexander>