From: A E Lawrence (adrian.lawrence_at_email.domain.hidden)
Date: 2001-08-22 22:16:50
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
This archive was generated by hypermail 2.1.7 on 2004-10-31 20:03:59 GMT
© Copyright WoTUG
All rights reserved