Re: [9fans] linux stats in last year from linuxcon

[Tim Newsham <newsham@lava.net>]

>> 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/