I seem to have slided in an error there..(=
It’s of course it’s “combinable” not “composable”.
But “distributable” can’t be that easy to get wrong (since I got it right).
Sorry
An aside: XMOS and the laws of occam
I have now worked a while at home with the startKIT. Here’s a scenario:
I have used 27 chanends. I will try to see if I can use less. I haven’t inserted the WiFi lib yet. I have only three channels and the rest are interfaces. In the messages some are just RPC but some are sessions, guaranteed to be atomic. Some tasks are “composable” meaning they may share a select loop with other composite processes.
In two processes I have nested selects, so I am not allowed to make them composable. The compiler tells me. I move the nested select to become part of the outer select. Done? No! Because I had inserted a boolean only guard, with no triggering event. The compiler told me it can’t be composable, meaning it would have to be running by itself. I don’t need to, so I take that part and wrap it into a function call and then it’s ok composable.
As I do this I see that less chanends are needed. The compiler knows the rules and don’t need to use channels in some cases.
Then I try to place the processes at different logical cores and see that I can also jungle with this to get the chanend count down. Any XMOS slice has 32 chanends. Period. And a slice has shared memory between its logical cores.
I could also make a task “distributable” to allow the compiler to place the code on several logical cores. And from [1] “If a distributed task is connected to several tasks, they cannot safely change its state concurrently. In this case the compiler implicitly uses a lock to protect the state of the task”. Just impressing.
This comes in addition to the deterministic timing matters, possible for some code trails.
Disclaimer: I am not even remotely associated with XMOS, no money, no gifts. I just think this is so great! Well done David et al! Who else has anything remotely as elegant? (But I miss some, like [2])
I would never have thought the little blue-covered law-book (that I sent a snail mail with a check to have it sent to me) from 1986 would run on my desk, ever. It did, 30 years after. Even, at home. (Disclaimer: this mail is really about program transformations in practical use. I would have liked to see a mapping of the book (if possible) into XMOS internals. David?)
Øyvind Teig
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?
1. 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.
The Laws you mention below are 'derived laws' - see the top of p. 44
.
David
Thank you to everyone who communicated personally with me on the 14 Feb post. Here is an even more elementary question relating to Roscoe and Hoare, “The Laws of OCCAM Programming.”
Perhaps these are considered too trivial to require a law. But I searched and could not find the following, or anything that implied them:
Hello all,
We need to learn about formal verification, so I started with Martin and Jassim, “Technique for Checking the CSP sat Property”, WoTUG-21, poked at Roscoe, Theory and Practice of Concurrency, Prentice-Hall, and wound up at Roscoe and Hoare, “The Laws of OCCAM Programming,” Theoretical Computer Science 60 (1988) 177-229. A couple of questions on the last.
(1) In (5.6)* and (5.7)*, p 187, the c?x and x:=e instructions seem to share x across PAR members. Am I right that x is only a general symbol so that this illegal sharing does not really take place?
(2) The WHILE combination (W.2), p 221 and 228, seems incorrect: If I type v for OR, ^ for AND, and T for DIVERGENCE it claims
WHILE b1 (WHILE b2 P) = WHILE b1 v b2 IF(b2 P, true T)
But this clearly seems wrong if b1 is FALSE and b2 is TRUE. I thought at first that the v was a typo for ^ but ^ only works if you require b1 and b2 to be constant. If they both start TRUE and one turns FALSE in the course of P, the equality fails.
Is there further work on occam 2 or later occam along this line?