🚀 go-pugleaf

(for those of you who feel that there's a little too much CSP in your
 very own Z newsgroup... relax, it'll be over by Christmas)

In article <...> brendan@cs.uq.oz.au (Brendan Mahony) writes:

   I find it quite natural (as perhaps do other state based people) to
   think of event related notations as being fundamentally algorithmic in
   nature. 

Depends upon what you mean by "event".  

In standard CSP, events are instantaneous happenings in the history of a
system. This is why we don't have any problem with "true" vs. "interleaving"
concurrency, by the way... events don't describe states or actions with
duration, although a limited amount of state information may be inferred from
a record of external events.

   An event is after all something that is done, either by a system
   or to a system. Of course at the most abstract level there is nothing to
   distinguish event from state, except the language we throw at them,

I disagree, politely. Events are best seen as marker points in time, they may
delimit actions or mark state changes, but they should not be identified with
states (or actions with duration).

   it is hard to argue that CSP is not about describing how something is to
   be done. 

The theory of CSP consists of the language of processes (abstract programs)
and a series of semantic models, which are used for specification and
refinement.  These specifications need not be algorithmic; in fact, in five
years of producing CSP specifications I have yet to come up with an
useful algorithmic one.  But that may just be me :-)

             The specification language of traces and refusals has very
   little to tell us about what we are discussing, without some mechanism
   for interpretting the "meaning" of the event names, such as described
   above.

Surely this is true for any formal notation: if you don't give an intuitive
interpretation for your formal symbols, then you can't infer very much about
the "real" world.  

Returning to the point, however... what do I have to say about the hybrid
models of CSP, the models which include system state in their semantics?  The
answer is: not very much.  Some of these models are custom jobs, tailored to a
specific task---such as compiler verification---and some of them are excellent
pieces of work, but they shouldn't be confused with standard CSP.

That's not an "Oxford knows best" sort of comment.  Most of the hybrid models
have originated around here, for a start.  But a large number of complementary
design decisions have been incorporated into CSP.  These were pretty much
undocumented by the people who made them (Brookes, Hoare, Roscoe)... at least
never in the form where they were isolated or made obvious.

If you change the notion of "event", then you've got a different theory.  The
assumptions of your model of computation may not be so complementary, and you
may have to address such issues as "true" vs. "false" concurrency.  Just
because it still looks like good old CSP notation, it's not necessarily the
same animal.  For similar reasons, CSP is very different from CCS or ACP.

Jim

p.s.  to avoid any global misunderstandings, I should emphasise that 
      there's no conflict between Brendan's research and mine... we're 
      working in different areas, and any disagreement in our postings 
      is probably about terminology. 
--