Re: CSP questions

[Larry Dickson <tjoccam@xxxxxxxxxxx>]

All,

I have been trying to teach myself CSP, and am looking at J. M. R. Martin’s PhD thesis

[MTh] http://www.wotug.org/docs/jeremy-martin/thesis.pdf

and the Martin and Jassim paper in WoTUG-21

[MJ] http://wotug.org/paperdb/send_file.php?num=45

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

On Mar 14, 2017, at 9:15 AM, Larry Dickson <tjoccam@xxxxxxxxxxx> wrote:

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

On Mar 13, 2017, at 3:15 PM, Larry Dickson <tjoccam@xxxxxxxxxxx> wrote:

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. 

Thanks for all the help,

Larry

On Mar 13, 2017, at 4:32 AM, David May <dave@xxxxxxxxxxxxxxxxxxxxx> wrote:

The original "Laws of Occam Programming" is a 1986 Oxford PRG monograph - there's a scan here https://www.cs.ox.ac.uk/files/3376/PRG53.pdf

The Laws you mention below are 'derived laws' - see the top of p. 44
.

David

On 7 March 2017 at 21:25, Larry Dickson <tjoccam@xxxxxxxxxxx> wrote:

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:

PAR(P, SKIP) = P

SEQ(SKIP, P) = P

SEQ(P, SKIP) = P

Larry

On Feb 14, 2017, at 4:42 PM, Larry Dickson <tjoccam@xxxxxxxxxxx> wrote:

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?

Larry Dickson