Re: rewriting CSP processes

[Michael Goldsmith <michael@xxxxxxxx>]

John,

> I've a CSP question. The words around the mathematics
> talk about "events" being instantaneous transactions that
> are handshaken (both the Roscoe and Schneider books 
> use those terms).  In real life, that's not possible.  Handshaking 
> protocols don't execute in zero time, and signals don't
> propagate instantly.  Is there anything in the CSP literature
> that deals with this problem?

That is perhaps overstating the case: when I depress the key to type this X,
my finger, the X key-cap and the contacts beneath it perform a three-way
synchronisation which involves no complicated protocol.  We would describe the
event as taking place at the instant when sufficient voltage or current is
released to allow and commit the rest of the circuitry to recognise that I
have pressed it.

The "instantaneity" supposed in CSP does not necessarily imply that the events
model zero-time transactions.  It is much more a simplifying assumption (which
is sufficiently often valid to make it worthwhile) that if two events can
happen in either order, with the possibility of no other event intervening,
then there is nothing useful that can be added by considering the possibility
that they in fact happen simultaneously.  (In the jargon, it is part of the
avoidance of "true concurrency".)  The fact that there is a measurable amount
of analogue activity involved in the key-press is irrelevant to our interest
in it.  If we're not writing keyboard drivers, then we probably work on the
basis that the physically distinct events of depressing the key and delivering
the keystroke to the application can be identified as a single abstract event,
key.X, say.  This abstraction is a Good Thing: it allows us to understand and
reason about systems which would be completely intractable if we had to deal
with every little bit of detail all the time. 

> It seems that you could re-write any set of CSP processes
> in terms of lower level processes.  For example, a shared
> event at the macro level would be re-written as a set of
> events at the micro level, where the hand shaking would be 
> implemented as micro-processes (Ignore that pun).  At some
> point you get to logic gates that intrinsically respond to
> "events" at their input terminals.

In principle, that is true, except that the world is not all built of logic
gates.  You could probably go down to the quantum level (Adrian?) if you
really wanted to, but I'm not sure what you would hope to gain.  It
won't be just a set of micro-events, but some recognisable protocol among
them, that constitutes the occurrence of the abstract version.  The shared
event should probably be one of the events of one of the micro-processes, in
order to tie the rewritten form in with more abstract specifications.

> My question is, what are the minimum properties of the
> micro-level and the re-writing process to guarantee that
> CSP properties hold at the macro level?  Its the kind of
> thing that seems likely to have been dealt with in the
> theoretical literature, but I haven't seen it.  Any light
> would be appreciated. -jc

The general topic to look up is probably "event refinement".  Essentially what
you need to establish is that the more abstract events are made atomic with
regard to one another.  That is something that you lose by looking inside
them, unless you use appropriate protocols.
									     M