Regarding seL4 - I have no technical knowledge of what was done. However, some of the security community I had contact with within STMicroelectronics referred to the kennel as "formally proven”. The Wikipedia entry on L4 takes the same view. Of course, this is just hear-say……
David, the paper whose link you sent me waved its hands at the laws in question ;-)
However, I believe I figured out the essence. You reduce P to a big nesting of ALTs and IFs with each innermost payload being an assignment. For each such assignment, using 3.3 and 3.1 to imply x:=x = SKIP allows 4.7 (two cases) to imply law a of page 44, the SEQ reductions, and 5.5 with one component an empty assignment (3.1) implies law c of page 44, the PAR reduction.
And thank you, Adrian, for the copy of Bill Roscoe’s paper “The expressiveness of CSP with priority”. It will be a while before I can understand this, though I note that it is post-2013. One question is immediate: on p 5 it says
CSP provides two ways of getting one process to take over from another
without the first one terminating: interrupt P △ Q allows P to run, but at
any time offers the initial events of Q. If one of the latter happens then Q
Is it ever possible to go back to P, in the manner of actual interrupts in standard CPUs? And if so, doesn’t that give you all of priority?
My second question: do any of you have any comments on the claim of formal verifiability made for the microkernel seL4?
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika
Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon
Winwood. seL4: Formal Verification of an OS Kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating system principles. SOSP ’09, 2009.
Thanks for all the help,
The Laws you mention below are 'derived laws' - see the top of p. 44