61–65 of 65 posts
Can anyone comment as to how feasible/practical it would be to extend these proofs to a multicore chip?
Earlier quoted context omitted.
Source: I have worked at NICTA, with the seL4 team, on the seL4 project, I've seen the seL4 source code and am (was?) a primary author of the user manual. What they mean by this is that they have specified certain properties at a high level in a logical reasoning language they call HOL. These properties are things like the kernel will never reference a null pointer, or, the kernel will always run the next runable thr…
Man, I have so many questions :) Why not just use the haskell version? What did you use to check the haskell version? What did you use to check that C implements what haskell implements? Edit: I have read http://ertos.nicta.com.au/research/l4.verified/proof.pml , but I'd like to know more about tooling. Like, did you use agda, e.t.c?
1) Why not use the Haskell version? The Haskell version was (is?) "executable", but it ran only against a hardware simulator, never against real hardware. Haskell has a complex runtime which is not (easily) suitable to run directly on Hardware (although one student I worked with did port a subset of the Haskell runtime to work on top of seL4). Using Haskell directly would be slow, and would require the researchers to prove the correctness of the Haskell runtime implementation as well which would be a huge amount of work.
2) What did you use to check the haskell version? I was not directly involved in this. I believe the Haskell used to write the kernel was a subset of the language, they call "literate haskell" which was used to both implement and specify the kernel. This was somehow minimally translated into a dialect of Isabelle called HOL.
3) What did you use to check that C implements what haskell implements? A similar process was used for checking that the C implementation was a refinement of the Haskell. Again, a restrictive subset of the C language a tool was written to translate the C code into HOL (I think). I remember the team lead arguing that the way the C implementation was checked, both the code itself and the translator could be checked for bugs.
AFAIK, The tooling was almost all custom except for relying on Haskell and the Isabel theorem prover. The group had a lot of experience for building and releasing the OKL4 kernel so a lot of the dirty work was already done as well as an excellent "Advanced Operating Systems Course" which whips and tortures undergraduates into systems engineers and ideally PhD students. :-)
This will be pretty exciting for anyone learning operating systems. More source to read. https://en.wikipedia.org/wiki/L4_microkernel_family
Beware, since the source is a translation of Haskell into C, this is not an entry level source tree and is not straightforward to read/understand despite it's small (LOC) size.
Can anyone comment as to how feasible/practical it would be to extend these proofs to a multicore chip?
Very, very hard, if you mean kernel threads running in parallel. However, if the other cores run separate kernel instances (machine partitioning, separate memory and everything) that would be more achieveable. UNSW call this the clustered micokernel approach.
Earlier quoted context omitted.
Man, I have so many questions :) Why not just use the haskell version? What did you use to check the haskell version? What did you use to check that C implements what haskell implements? Edit: I have read http://ertos.nicta.com.au/research/l4.verified/proof.pml , but I'd like to know more about tooling. Like, did you use agda, e.t.c?
I can't answer all of these questions authoritatively, as I have more of a systems focus than a formal methods focus, but I can hopefully point you in the right directions. The various published papers and final release will be the right places to find all the authoritative answers. 1) Why not use the Haskell version? The Haskell version was (is?) "executable", but it ran only against a hardware simulator, never agai…
I have already seen the approach "Lets design this in haskell and write production code in C" for http://cryptol.net/, but due to limited scope (mostly functions of several hundered bits input and output as customary in crypto-primitives), they were able to check that the implementation adheres to specification automatically. The aim was to allways know that the c code does what it is supposed to, so that programmer can focus on mitigating side-channel attacks :)
I wonder if something similar would be applicable to writing the micro-kernell.