|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?
Thanks for all the help,
On Mar 13, 2017, at 4:32 AM, David May <dave@xxxxxxxxxxxxxxxxxxxxx> wrote: