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?
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).
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