From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 22 Sep 2009 12:25:55 -1000 From: Tim Newsham To: Fans of the OS Plan 9 from Bell Labs <9fans@9fans.net> In-Reply-To: Message-ID: References: <> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Subject: Re: [9fans] linux stats in last year from linuxcon Topicbox-Message-UUID: 75c99fc0-ead5-11e9-9d60-3106f5b1d025 >> i'm not clear on what all functional correctness entails. can I thought I'd go into a little more detail about what they did since my last email probably doesnt clear it up very much. They wrote a model of their operating system in a high level language (Haskell). They then translated the model into a language suitable for theorem proving (Isabelle/HOL) and they proved certain properties about the model. I don't know specifics on what all was proven, but they did mention that they processes are properly isolated (one process cannot write to the memory of another process except through certain specific and controlled message passing primitives). They then manually translated the spec into C and made proofs that the model and the C implementation behave the same way. There were no proofs about the behavior of the C compiler or the underlying cpu. So there should be no defects relating to the properties they proved unless they are hardware or compiler bugs. There can still be bugs for properties which they did not prove. Also the proof is over the microkernel only, its obviously still possible to write an OS on top of the kernel that has its own bugs. You can find out a lot more from their papers and websites: http://ertos.nicta.com.au/research/sel4/ http://ertos.nicta.com.au/research/l4.verified/ http://ertos.nicta.com.au/research/l4.verified/proof.pml Tim Newsham http://www.thenewsh.com/~newsham/