From mboxrd@z Thu Jan 1 00:00:00 1970 MIME-Version: 1.0 In-Reply-To: References: Date: Tue, 22 Sep 2009 11:27:14 -0700 Message-ID: <3e1162e60909221127h7e275160pf8323ca1debc4df7@mail.gmail.com> From: David Leimbach To: Fans of the OS Plan 9 from Bell Labs <9fans@9fans.net> Content-Type: multipart/alternative; boundary=000e0cd5d01c612caf04742ebffa Subject: Re: [9fans] linux stats in last year from linuxcon Topicbox-Message-UUID: 754e1dd2-ead5-11e9-9d60-3106f5b1d025 --000e0cd5d01c612caf04742ebffa Content-Type: text/plain; charset=ISO-8859-1 On Tue, Sep 22, 2009 at 10:13 AM, erik quanstrom wrote: > > btw, there's even been one ukernel recently that has a formal > > proof of correctness (against its specification and some containment > > properties). Roughly a 10 man-year effort for about 7.5kloc. > > Not something you'd likely be able to do yet against something linux- > > sized. > > the other way of looking at this is all the complex and error > prone stuff is not prooved. > > i'm not clear on what all functional correctness entails. can > a functionally correct program suffer from deadlock or livelock? > > I'm not sure... I can tell you when I spawn threads in haskell that, while testing, the runtime seems to detect certain deadlock states, tells me about them, and then the program crashes. I like that a little better than deadlock :-) How that all works is a lit Dave > - erik > > --000e0cd5d01c612caf04742ebffa Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable

On Tue, Sep 22, 2009 at 10:13 AM, erik q= uanstrom <qua= nstro@quanstro.net> wrote:
> btw, there's even been one ukernel recently that= has a formal
> proof of correctness (against its specification and some containment > properties). =A0Roughly a 10 man-year effort for about 7.5kloc.
> Not something you'd likely be able to do yet against something lin= ux-
> sized.

the other way of looking at this is all the complex and error
prone stuff is not prooved.

i'm not clear on what all functional correctness entails. =A0can
a functionally correct program suffer from deadlock or livelock?


I'm= not sure... I can tell you when I spawn threads in haskell that, while tes= ting, the runtime seems to detect certain deadlock states, tells me about t= hem, and then the program crashes. =A0I like that a little better than dead= lock :-)

How that all works is a lit

Da= ve
=A0
- erik


--000e0cd5d01c612caf04742ebffa--