A.4 Processes

Syntax

STOP	no actions
SKIP	successful termination
CHAOS(a)	the choatic process (on events in a)
c -> p	simple prefix
c ?x ?x':a !y -> p	complex prefix
p ; q	sequential composition
p /\ q	interrupt
p \ a	hiding
p [[ c <- c' ]]	renaming
p [] q	external choice
p [+ a +] q	delayed choice
p |~| q	internal choice
p [> q	untimed timeout
p [| e |> q	exception
b & q	boolean guard
p ||| q	interleaving
p [| a |] q	sharing
p [ a || a' ] q	alphabetised parallel
p [ c <-> c' ] q	linked parallel
; x:s @ p	replicated sequential composition
[] x:a @ p	replicated external choice
|~| x:a @ p	replicated internal choice (a must be non-empty)
||| x:a @ p	replicated interleave
[| a' |] x : a @ p	replicated sharing
|| x:a @ [a'] p	replicated alphabetised parallel
[ c <-> c' ] x:s @ p	replicated linked parallel (s must be non-empty)

Equivalences

As a consequence of the laws of CSP,

p ||| q ≡	p [| {} |] q
; x:<> @ p ≡	SKIP
[] x:{} @ p ≡	STOP
||| x:{} @ p ≡	SKIP
[| a |] x:{} @ p ≡	SKIP
|| x:{} @ [a] p ≡	SKIP

By definition

CHAOS(a) ≡

|~| x:a @ x -> CHAOS(a) |~| STOP

Remarks

The general form of the prefix operator is cf->p where c is a communication channel, f a number of communication fields and p is the process which is the scope of the prefix. A communication field can be

!x	output
?x:a	constrained input
?x	unconstrained input

Note that the set a in the constrained input must match the protocol, so it must be a subset of the values that would be permitted by the unconstrained input.

Fields are processed left to right with the binding produced by any input fields available to any subsequent fields. For example, we can write

channel ints : Int.Int
P = ints?x?y:{x-1..x+1} -> SKIP

Output fields behave as suggested by the equivalence

c !x f -> p ≡

c.x f -> p

The proportion of the channel matched by an input fields is based only on the input pattern. There is no lookahead, so if

channel c : {0..9}.{0..9}.Bool
P = c?x!true -> SKIP -- this will not work
Q = c?x.y!true -> SKIP -- but this will

then P is not correctly defined. The input pattern x will match the next complete value from the channel ({0..9}) and true will then fail to match the next copy of {0..9}. In the case of @@ patterns, the decomposition is based on the left-hand side of the pattern.

If an input occurs as the final communication field it will match any remaining values, as in

channel c : Bool.{0..9}.{0..9}
P = c!true?x -> SKIP -- this will work
Q = c!true?x.y -> SKIP -- this will also work

This special case allows for the construction of generic buffers.

BUFF(in,out) = in?x -> out!x -> BUFF(in, out)

is a one place buffer for any pair of channels.

Dots do not directly form part of a prefix: any which do occur are either part of the channel c, or the communication fields. (FDR1 took the approach that dots simply repeated the direction of the preceding communication field. This is a simplification which holds only in the absence of datatype tags.)

The guard construct ‘b & P’ is a convenient shorthand for

if b then P else STOP

and is commonly used with the external choice operator (‘[]’), as

COUNT(lo,n,hi) =
  lo < n & down -> COUNT(lo,n-1,hi)
[]
  n < hi & up -> COUNT(lo,n+1, hi)

This exploits the CSP law that p[]STOP=p.

The linked parallel and renaming operations both use the comprehension syntax for expressing complex linkages and renamings(15). For example,

p [ right.i<->left.((i+1)%n), send<->recv | i<-{0..n-1} ] q
p [[ left.i<-left.((i+1)%n), left.0<-send | i<-{0..n-1} ]]

Both the links (c<->c') and the renaming pairs (c<-c', read ‘becomes’) take channels of the same type on each side and extend these pointwise as required. For example,

p [[ c <- d ]]

is a process which behaves like p except all occurrences of channel c in p are replaced by channel d (so that c ‘becomes’ d). This is defined when extensions(c) is the same as extensions(d) and is then the same as

p [[ c.x <- d.x | x<-extensions(c) ]]

The replicated operators allow multiple generators between the operator and the ‘@’ sign in the same way as comprehensions. The terms are evaluated left-to-right, with the rightmost term varying most quickly. So

; x:<1..3>, y:<1..3>, x!=y @ c!x.y->SKIP

is the same as

c.1.2->c.1.3->c.2.1->c.2.3->c.3.1->c.3.2->SKIP

The linked parallel operator generalises the chaining operator (>>) of [Hoare85]. For example, if COPY implements a single place buffer,

COPY(in,out) =
  in?x -> out!x -> COPY(in,out)

then we can implement an n-place buffer by

BUFF(n,in,out) =
  [out<->in] i:<1..n> @ COPY(in, out)

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.