Date: Sun, 27 Jul 2003 13:08:55 +0200 From: "Poul-Henning Kamp" <phk@phk.freebsd.dk> To: Alexander Leidinger <Alexander@Leidinger.net> 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: <62633.1059304135@critter.freebsd.dk> In-Reply-To: Your message of "Sun, 27 Jul 2003 12:16:43 %2B0200." <20030727121643.6daa5486.Alexander@Leidinger.net>
next in thread | previous in thread | raw e-mail | index | archive | help
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.
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?62633.1059304135>