On Tue, Sep 22, 2009 at 10:13 AM, erik quanstrom <quans...@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). 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 > >
