[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: More L4 hearsay



Roger and all,

Thanks for the research! This sounds like we may be converging. The little I know about Haskell indicates it has CSP elements but is a functional language. In Jeremy Martin’s thesis, p 66, it says “Deadlock Checker is implemented on top of FDR version 1.4, using the powerful functional programming language ML.” Since FDR is CSP, this appears to align. CSP is supposed to be declarative, not imperative, and functional avoids state questions - but occam has provable equivalences and is finite, avoiding the infinite recursions. Do we use an occam-like subset of Haskell, or an occam-to-Haskell translator? Does FDR or other CSP formal verifier accept Haskell input? I know a guy who has used Haskell.

Real stuff in the computer world is highly stateful, e.g. a hard drive.

Larry

On Apr 3, 2017, at 1:46 AM, rog@xxxxxxxx wrote:

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

Roger Shepherd

On 1 Apr 2017, at 17:50, Larry Dickson <tjoccam@xxxxxxxxxxx> wrote:

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

On Mar 30, 2017, at 8:43 PM, Larry Dickson <tjoccam@xxxxxxxxxxx> wrote:

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

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