Larry
Asking around about L4. It seems L4 is well known in the Haskell community (because a Haskell specification was used in the proof) and is considered to have been formally proven
Roger All,
We seem to have gotten to a point where progress can be made, and I am going to open a view of it to the group. Some guidance from Jeremy Martin got me past my difficulty of March 30 Re: CSP questions (20:43 PDT). The key is that the n-th step from pre-normalization to normalization identifies n steps to follow that look the same from the point of view of the outside world. So a fixed point means forever. Jeremy also pointed out a paper (Bryan Scattergood and Karen Siedel, “Translating occam 2 into CSP”) which, together with Jeremy’s thesis, is suggestive of a route to a practical tool.
The Scattergood-Siedel approach mostly turns imperative assignment stuff into SKIP. However, it hints at a distinction that I want to make explicit. They refer (p 3) to “those places where the value of an _expression_ alters the flow of control or the unrolling of a replicated construct” as special. I’d like to extend this distinction on stateful imperative stuff - dividing it into STRUCTURE and CONTENT. The former is key to flow, the latter just takes up time (from the flow point of view). This fits the very robust development practice of replacing complex content (not yet written) with busy loops that last the same time and use the same resources, and debugging the program before its content is written.
My feeling is that you can catch the structure in the occam and do an occam-to-occam equivalence (or formally finite restriction) to get less efficient but more ”CSP-friendly” occam that lets you prove a lot more using the Scattergood-Siedel translation or similar translation. Example - and I did not plan this - the two FIFOs I posted March 28 Re: [External] CSP questions (8:06 PDT): going backward from FIFO to rawFIFO goes from a FIFO indexed circular buffer to a FIFO of multiple parallel buffers. Do this sort of thing until all the imperative content that is left is CPU-busy filler (a time-consuming SKIP?).
The ultimate goal would be a complete description of program behavior from an external point of view.
Larry All,
I have been trying to teach myself CSP, and am looking at J. M. R. Martin’s PhD thesis
and the Martin and Jassim paper in WoTUG-21
Starting from VM = coin -> tea -> VM |~| coin -> VM ([MJ] p 95), and applying the method of [MTh] p 63-66, I do not get the normal form NF(VM) shown in [MJ] Figure 1 p 98. The pre-normalization of State 0 is more like the top of left side of Figure 3.2 in [MTh] p 65, and leads to two coin arrows, of which one is a loop-back.
Can someone show where I am going wrong, or is this a real error?
Larry
All,
Here is a follow-up question for the CSP experts. On priority and the P delta Q interrupt: Since it says that P did not terminate, is it possible that Q can pass control back to P by executing half a communication (i.e. blocking)? This is what actually happens in the case of Transputer occam high-priority processes - they keep going until they block. If we get that, we get all of Transputer occam, it seems - and more (because you could have more than two levels of priority).
Larry 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
takes over.
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,
Larry The Laws you mention below are 'derived laws' - see the top of p. 44 . David
|