Download Communicating Sequential Processes

2.2
Interaction
47
The stories that accompany these examples show a sad betrayal of proper
standards of scientific abstraction and objectivity. It is important to remember
that events are intended to be neutral transitions which could be observed and
recorded by some dispassionate visitor from another planet, who knows nothing of the pleasures of eating biscuits, or of the hunger suffered by the foolish
customer as he vainly tries to obtain sustenance. We have deliberately chosen
the alphabet of relevant events to exclude such internal emotional states; if
and when desired, further events can be introduced to model internal state
changes, as shown in 2.3 X1.
2.2.1
Laws
The laws governing the behaviour of (P || Q ) are exceptionally simple and
regular. The first law expresses the logical symmetry between a process and
its environment
L1 P || Q = Q || P
The next law shows that when three processes are assembled, it does not matter in which order they are put together
L2 P || (Q || R) = (P || Q ) || R
Thirdly, a deadlocked process infects the whole system with deadlock; but
composition with RUNαP (1.1.3 X8) makes no difference
L3A
P || STOPαP = STOPαP
L3B
P || RUNαP = P
The next laws show how a pair of processes either engage simultaneously in
the same action, or deadlock if they disagree on what the first action should
be
L4A
(c → P ) || (c → Q ) = (c → (P || Q ))
L4B
(c → P ) || (d → Q ) = STOP
if c ≠ d
These laws readily generalise to cases when one or both processes offer a choice
of initial event; only events which they both offer will remain possible when
the processes are combined
L4 (x : A → P (x)) || (y : B → Q (y)) = (z : (A ∩ B) → (P (z) || Q (z)))
It is this law which permits a system defined in terms of concurrency to be
given an alternative description without concurrency.