🚀 go-pugleaf

In article <6591@ecs.soton.ac.uk> igl@ecs.soton.ac.uk (Ian Glendinning) writes:

>> (Hoare's definition of parallel composition is inadequate.)
>
>Please explain.  Why is it inadequate?

A sequential process as defined by Hoare is essentially an automaton that 
defines a language of events (which correspond to messages) in which the
process is capable of interacting.  The parallel composition operator (||)
transforms a pair of sequential processes into an equivalent single sequential
process, defining a language of events in which both processes are capable of
interacting.  Consider the following example from Hoare's book:

  VMCT = coin -> (choc -> VMCT | toffee -> VMCT)
    (a vending machine with chocolate and toffe)
  GRCUST = (toffee -> GRCUST | choc -> GRCUST | coin -> choc -> GRCUST)
    (a greedy customer who tries to get something without paying)

  (GRCUST||VMCT) = coin -> choc -> (GRCUST||VMCT)
    
Note that the parallel composition of the two is, itself, a sequential
process.  Furthermore, together, the greedy customer and the vending machine
can only 'agree' to interact with a sequence of coin, chocolate, coin,
chocolate, ...  However, the parallel composition of these two processes
does not cause an interaction to take place.  (It does not cause the events to
happen.)  It simply defines a new language of interactions.  Hoare's
definition of parallel composition is based upon a 'broadcast' synchronization.
That is if we perform another parallel composition with the example,

  ((GRCUST||VMCT)||VMCT)

then we get the same sequential process defined above. (The name is changed,
the process definition is identical.  Hoare uses a notation that I cannot 
duplicate here, using mu, in order to avoid concern about the names.)

The sequential processes that result are still ready to interact, but Hoare
never introduces an additional notion of parallel composition that allows
these events to ever take place.  As a result, Hoare's parallel composition
of processes defines processes that exist in a vacuum, and can't actually
do anything (except to describe a possible set of events).

>>(Note that, ignoring the procedural/functional differences, the main 
>>conceptual difference between CSP and occam involves the action of parallel 
>>composition.)
>
>Again, please explain.  I always thought they were the same.

If you are familiar with occam, it should be clear that the definition of
the parallel composition operator (PAR) is quite different.  Consider two
occam processes,

  SEQ
    <interact in event>
    x := 1

and

  SEQ
    <interact in event>
    y := 2

(Let us use an <event>, without worrying about channels, communication, and 
other concepts that are not relevant to this discussion 
of parallel composition.)

Now consider the parallel composition of these:

  PAR
    SEQ
      <interact in event>
      x := 1
    SEQ
      <interact in event>
      y := 2

which is equivalent to the occam process:

  x, y := 1, 2

because the <event> actually takes place.  It is an internal event that
is invisible outside of the scope of the PAR operator.  One may prefer
to view this as:

  SEQ
    <event takes place>
    x, y := 1, 2

Notably, the parallel composition is NOT equivalent to:

  SEQ
    <interact in event>
    x, y := 1, 2

which is what one would expect based upon Hoare's notion of parallel
composition.

Fundamentally, when two processes share an event in occam, the event takes
place.  In CSP, it does not.


Jonathan