Early Process Calculi

Presented by Greg Pettyjohn
Transcribed by Richard Cobbe

Hoare: Concurrent Sequential Processes, 1978

In Hoare's formalism of concurrent sequential processes, a process is a set of execution traces, where each trace is represented as a (possibly infinite) string from some particular alphabet. The symbols in the alphabet represent particular events in the process's execution. He defines an algebra on processes with operations that allow us to prefix an event onto a process, make a choice between two events, construct recursive processes via a fixed-point operator, and compose two or more processes in parallel execution.

With multiple processes running concurrently, we need some means of communication between the processes. In CSP, two processes P1 and P2 that are running concurrently must obey the following three laws:

  1. Processes are synchronized on common symbols. That is, if a is in both processes' alphabets, then P1 can transition on a if and only if P2 also transitions on a at the same time.
  2. Processes block on opposing guards. That is to say, if a and b are both in both processes' alphabets, P1 can only transition on a, and P2 can only transition on b, then neither process can move.
  3. Processes ignore foreign symbols. That is, if a is in P1's alphabet but not P2's, then P1 may transition on a independently of P2's actions.

A useful way to think about processes is as labeled directed graphs: nodes represent process states, edges represent possible transitions, and the labels on the edges represent the events from the process's alphabet that happen with each transition.

Hoare also adds nondeterminism: in our graph model, this corresponds to multiple edges with the same label leaving a particular node. This leads to interesting problems. For instance, consider the following two processes (where P and Q are arbitrary processes):

        P1 = (a -> a -> P) | (a -> b -> Q)
        P2 = a -> (a -> P | b -> Q)

The processes have the same traces; should they be identified?

There was some discussion on this, but the conclusion was that we should not identify them. After P2 has made a single transition on a, it can still decide whether to go towards P or Q. By this point, however, P1 has already committed to a specific execution path.

Now, consider the following example:

        P1 = x -> a -> a -> P
        P2 = (x -> a -> a -> P) | (y -> a -> b -> Q)
        P3 = a -> a -> P
where x and y are not in P3's alphabet. If we compose all three processes in parallel, the only possible choice of execution is the sequence of events x, a, a, P; otherwise things will deadlock.

Another example:

        P1 = y -> a -> b -> Q
        P2 = (x -> a -> a -> P) | (y -> a -> a -> Q)
        P3 = a -> a -> P
where x and y are still not in P3's alphabet. If we compose the three in parallel again, we will execute y, a then deadlock.

From the point of view of P3, P2 will sometimes execute a, a, P and other times a, b, Q (modulo the deadlock), and it cannot predict which way it will go. So, P3 essentially sees the following:

        P2 = (_ -> a -> a -> P) | (_ -> a -> b -> Q)
where _ denotes an unlabeled transition. In other words, as far as P3 can tell, P2 behaves nondeterministically.

Two important conclusions to draw. First, nondeterminism models hidden actions. Second, the environment in which we run a process (specifically, those processes with which we compose a process) can distinguish between two different processes with the same traces. This leads to a notion of process equivalence.

Sam asked what we could express in this calculus; Greg responded that this was just the core of Hoare's system. Hoare also added a communication mechanism and a complete imperative sequential language to describe actual straight-line processing.

Milner: A Calculus of Communicating Systems, 1979

Milner starts with the same deterministic core; the primary difference is in how they handle parallel composition. Milner introduces the idea of names (a) and conames (a'). (Milner actually uses an overbar, but I'm using a prime in this summary because I don't want to take the time to figure out how to make HTML do this right.) So, two processes running in parallel synchronize when one executes a transition marked with a name and the other executes a transition marked with its coname.

So, for an example, let T1, T2, and U1 be arbitrary processes, and let P || Q denote the parallel composition of processes P and Q. Consider the following two processes:

            T = (a -> T1) | (b -> T2)
            U = a' -> U1
Then T || U is given by the following:
            T || U = (a -> T1 || U) | (a' -> T || U1) | (b -> T2 || U) | (t -> T1 || U1)
In other words, there are four possible executions. From left to right:
  1. T transitions on a, U doesn't transition.
  2. U transitions on a', T doesn't transition.
  3. T transitions on b, U doesn't transition.
  4. T transitions on a and U transitions on a'.
In the final case, the name a and its coname cancel each other out, leaving a transition with no label. Milner uses the label tau (here rendered as t) to indicate the lack of a label. Essentially, in this case, nondeterminism has essentially hidden this "internal" transition from outside observers. Also, note that Milner has moved his definition of nondeterminism into his definition of parallel composition.

Milner also develops a new method of identifying two processes, that of a bisimulation. Two processes P and Q are bisimilar if and only if, for any trace s in the (combined?) alphabet, the following conditions hold:

  1. If P transitions to P' via s, then there exists a Q' such that Q transitions to Q' via s.
  2. If Q transitions to Q' via s, then there exists a P' such that P transitions to P' via s.

Sam asked if Greg could demonstrate two processes that are equivalent according to Hoare but not bisimilar; Greg provided the following example. (Again, the label t, pronounced `tau', indicates an empty transition.)

            p1 = (t -> P) | (t -> Q) | (t -> R)
            p2 = (t -> (t -> P) | (t -> Q)) | (t -> R)
Thus we can conclude that bisimulation is a finer-grained definition of equality than Hoare's notion of equivalence.

Another example of processes that Milner can distinguish and Hoare cannot:

            p1 = (a -> P) | (a -> Q)
            p2 = a -> ((t -> P) | (t -> Q))
            p3 = (t -> a -> P) | (t -> a -> Q)