Presented by Greg Pettyjohn
Transcribed by Richard Cobbe
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:
ais in both processes' alphabets, then P1 can transition on
aif and only if P2 also transitions on
aat the same time.
bare both in both processes' alphabets, P1 can only transition on
a, and P2 can only transition on
b, then neither process can move.
ais in P1's alphabet but not P2's, then P1 may transition on
aindependently 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
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
a, it can still decide whether to go towards
P or Q. By this point, however, P1 has already committed to a specific
Now, consider the following example:
P1 = x -> a -> a -> P P2 = (x -> a -> a -> P) | (y -> a -> b -> Q) P3 = a -> a -> Pwhere
yare 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.
P1 = y -> a -> b -> Q P2 = (x -> a -> a -> P) | (y -> a -> a -> Q) P3 = a -> a -> Pwhere
yare still not in P3's alphabet. If we compose the three in parallel again, we will execute
y, athen deadlock.
From the point of view of P3, P2 will sometimes execute
P and other times
a, b, Q (modulo the deadlock),
and it cannot predict which way it will go. So, P3 essentially sees
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 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
P || Q denote the parallel composition of processes P
and Q. Consider the following two processes:
T = (a -> T1) | (b -> T2) U = a' -> U1Then
T || Uis 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:
a, U doesn't transition.
a', T doesn't transition.
b, U doesn't transition.
aand U transitions on
aand 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:
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
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)