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

[Alexander Leidinger]

On Sun, 27 Jul 2003 12:02:36 +0200
"Poul-Henning Kamp" <phk at 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