From adrian.lawrence@computing-services.oxford.ac.uk Sun Oct 31 15:49:11 2004 From: A E Lawrence To: Lawrence Dickson Cc: CSPUG@JISCMAIL.AC.UK, gordon_hutchison@uk.ibm.com, java-threads@ukc.ac.uk, occam-com@ukc.ac.uk Date: Wed, 22 Aug 2001 22:16:50 +0100 Subject: Re: The future of CSP? Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=us-ascii MIME-Version: 1.0 X-Mailer: Mozilla 4.77 [en] (X11; U; Linux 2.4.9 i686) Message-ID: <3B842142.1A05A498@computing-services.oxford.ac.uk> Lawrence Dickson wrote: > > All, > > I want to express my sympathy with Gordon Hutchison's > point of view. I too am just programming, trying > to get things to work, and finding occam concepts > and emulation indispensable to this. Absolutely. That's how most of us work from day to day. You don't have to understand Acceptance semantics to use CSPP. Everyone in the occam community has been using parts of it for years, presumably since 1983ish. We have all had an intuitive understanding of PRI ALT and used it successfully. But we couldn't give definite answers to questions like priority conflict: we didn't even notice the possibility until it was thrown up by trying to set up a proper semantics. We wouldn't have occam or all the other wonderful things based on CSP without the rigorous theory. I am just trying to lay secure foundations for existing stuff like PRI ALT and taking it further, especially for hardware compilation. The relation of Handel circuits to CSP is actually a little problematical: a Handel circuit has true concurrency. But CSP serializes all events. So long as clocks are implicit, you can live with that. But make the clocks explicit, and there are real issues thrown up. Which are addressed in HCSP. So please don't think that I propose that everyone understand acceptances. But *I* need them, for example, to prove that PRI ALT really is a valid implementation of ALT. Most programmers just need to use their existing intuition about, say, PRI ALT. If that was all Gordon was saying then I agree with him. But he seemed to be saying that an approach based on firing rules and ready sets - pretty much an operational semantics - would be easier in establishing, say algebraic laws. Maybe. Although I rather doubt it. Especially if Gordon looks at some of the examples of laws of CSPP that I have established in various papers. In passing, someone very eminent once said that the transputer ALT was not an implementation of []. I was very new to things then and would not have dared to ask why not, and I doubt that I would have understood the answer if I had asked. But in the light of my work on CSPP, I now think that I understand why he said that. But in CSPP PRI ALT is an implementation (ie refinement) of []. I think that the intuition about [] was that it should be compliant. And the transputer ALT isn't. But the work on CSPP shows that a more abstract version of [] maps onto CSP syntax just as well as a compliant version. It is a distinction with Failures cannot draw, so that doesn't provide an answer. I really wouldn't want even to try to formulate the question using an operational approach. But I haven't tried. And it probably just demonstrates that I only have a rather superficial knowledge of that method. That said, I did play with a sort of operational semantics based on Acceptances a long time ago, and it seemed to work. I must look it out sometime. I think it was just a LTS decorated with extra stuff representing particular offers. Adrian -- Dr A E Lawrence