2.3 Overview of the pi-calculus

The pi-calculus [Mil91,Mil93,Tur95] is a process algebra developed by Milner as a successor to his very successful CCS language [Mil89]. It is very similar to Hoare's CSP language [Hoare86], differing largely in the way that communications are synchronised. Our use of (the polyadic) pi-calculus in this short paper is going to be rather pragmatic and hence we will give a users' description of it, referring the reader to [Mil91] for a full semantics of the language. In fact, we will introduce the pi-calculus through a series of examples, showing how processes are specified and how to understand their possible communication behaviours.

There are two basic actions: an output action denoted c!x and an input action denoted c?x. These respectively mean send value x on channel c and receive a value on channel c, binding that value to the name (variable) x. Sequences of actions can be composed so that the expression

c![3,d] . d?[x,y,z] . c!(x+y+z)

is the process whose behaviour is: send the tuple [3,d] on channel c, then receive a 3-tuple on channel d whose components are bound to the variables x, y and z, finally send the sum x+y+z on channel c.

For such a process to communicate, it must be running concurrently with other processes which do the matching half of the communication. For example if the above process runs in parallel with

c?[n,u] . u![n,n*n,n*n*n] . c?s

the net effect will be for the value n+n*n+n*n*n to be bound to s at the end of the second process expression.

Parallel composition of process expressions is denoted by P | Q. The essential semantic concept of communication is that two processes running in parallel may communicate with each other by sending values across channels. The interesting semantic aspect is when more than one communication is possible, which would arise for example in the context

( c!99 . P1 ) | ( c?x . P2(x) ) | ( c?y . P3(y))

where P1, P2(x) and P3(y) are themselves process expressions. The first of the three parallel processes can communicate with either the second or the third. In this case either, but not both, communications could happen and thus the possible successor states to this process state are P1 | P2(99) and P1 | P3(99)

Strictly, in pi-calculus, the values which are sent on channels are quite restricted, in order to be able to give a satisfactory mathematical definition. We will not restrict ourselves quite so rigidly in this short paper, nor will we justify the easing of the restriction. Rather, we will appeal to the readers' intuition about the rigour with which processes must be designed so as to not lead to stupid behaviour.

When we want to make a channel c local to a process expression P we use the construction $\hbox{{\bf new}}~c~.~P$, for example in

$$\hbox{{\bf new}}~c~.~((c!99~.~P1) \vert (c?x~.~P2(x)) \vert (c?y~.~P3(y)))$$

The only other pi-calculus construction we will make use of is non-deterministic (external) choice, denoted P + Q, which is a process which will behave as either P or as Q but not as both, the choice being determined by whichever of P or Q is able to communicate. For example, the expression

(c?x . P1(x))+(d?y . P2(y))

is waiting for communication on channels c or d. If a concurrent process communicates with c!99 then the above process moves to the state P1(99), whereas if it communicates with the d!77 then it moves to P2(77). If however the process is

(c?x . P1(x)) + (c?y . P2(y))

then the communication c!99 will cause an arbitrary choice between P1(99) and P2(99) as the successor state. The language does not prescribe the behaviour in this case. The user of the language must be prepared to cope with either choice. We will define more elaborate process behaviours using recursion equations.

Consider for example the definition

sink(c) = c?x . sink(c)

This defines a process sink(c) which will consume all values transmitted to it on channel c. Here c is a bound variable in a function definition which will be instantiated to an explicit channel for each actual use of the function. Consider also the following process

source(c) = (c!1 . c!2 . source(c)) + (c!3 . c!4 . source(c))

Readers should be able to convince themselves that

source(c1) | sink(c1)

runs forever, transmitting a sequence of integers on channel c1. An example of a sequence of values seen on c1 might begin $1\,2\,1\,2\,3\,4\,1\,2\,1\,2\,1\,2\,3\,4\,3\,4\,1\,2\,3\,4\,$.... Obviously, every 1 is followed immediately by a 2, and every 3 is followed immediately by a 4. But 1s and 3s can interleave arbitrarily. Similarly

source(c1) | source(c1) | sink(c1)

also runs forever, transmitting a sequence of integers on channel c1. Since there are two processes behaving as source(c1), either of them can transmit on c1 and in fact they will eventually both do so in an interleaved manner. An example of a sequence of values seen on c1 might begin $1\,\underline{1}\,2\,1\,\underline{2}\,\underline{1}\, \underline{2}\,2\,\underline{3}\,3\,4\,1\,\underline{4}\, \underline{1}\,2\,\underline{2}\,$...where the communications with one of the subprocesses have been underlined for clarity.

Suppose that we wished to define a source which was able to serve up values from a set $\{v1, v2, ..., vn\}$. What we want to write is

$$source(c) = (c!v1~.~source(c)) + (c!v2~.~source(c)) + \ldots + (c!vn~.~source(c))$$

We introduce a shorthand for this, giving ourselves a comprehension over sets. We write

$$\sum v:V~.~P(v)$$

to mean the sum over all values v in V of the processes P(v). Our source now becomes

$$source(c) = \sum v:\{v1, v2, ..., vn\}~ .~ (c!v~ .~ source(c))$$

With this short preparation, we are now in a position to show how such process components can be used to describe the behaviour of existing or proposed client-server systems.