Download The application of a resource logic to the non

2.3.4
Sequential composition
The sequential composition of program code is relatively straightforward to
define: one command is executed, which changes the state of the system, with
the rest of the program remaining. c shall range over single commands which
may be compound e.g., while loops. There are two cases to consider. Firstly,
the first command executes completely:
σ
(COMPTe ) :
R / JcK −→ R0 / JεK
σ
R / Jc; P2 K −→ R0 / JP2 K
If the command at the head executes to give an intermediate step, we place this
back in front:
σ
(COMPI ) :
2.3.5
R / JcK −→ R0 / JP10 K
σ
R / Jc; P2 K −→ R0 / JP10 ; P2 K
(P10 6≡ ε)
Parallel composition
We say that processes are acting in parallel or concurrently if more than one
process is ‘running’ at the same time. We shall use ·k· to represent parallel
composition of processes. Each parallel process, providing it is not blocked
(waiting for a resource not free in R), may be executed. At this stage, we
choose not to define a notion of fairness in execution — see §6.1.
One approach that may be adopted is to only allow one process to execute
one step in order to form a transition of the parallel system, forming a socalled asynchronous transition system. The choice of which process to execute
is arbitrary, or non-deterministic.
σ
(PARI,1 ) :
R / JP1 K −→ R0 / JP10 K
σ
R / JP1 kP2 K −→ R0 / JP10 kP2 K
σ
(PARI,2 ) :
R / JP2 K −→ R0 / JP20 K
σ
R / JP1 kP2 K −→ R0 / JP1 kP20 K
We must also consider the cases where one of the parallel processes terminates.
σ
(PARTe,1 ) :
R / JP1 K −→ R0 / JεK
σ
R / JP1 kP2 K −→ R0 / JP2 K
σ
(PARTe,2 ) :
R / JP2 K −→ R0 / JεK
σ
R / JP1 kP2 K −→ R0 / JP1 K
Alternatively, we may define a rule schema to allow easy access to parallel
processes. One may consider this to be a derived set of rules, or consider the
above to be specific instances of this; this is similar to the Expansion Law of
CCS.


σ
I = {1, . . . , n},
0
0
R
/
J
P
K
−→
R
/
J
P
K
i

rf
z
r fi
z
n > 1,
PARiI :
σ
0
0
R / j∈I Pj −→ R / Pi j∈I\{i} Pj
i∈I
34