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:
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.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.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 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:
a, U doesn't transition.a', T doesn't transition.b, U doesn't transition.a and U transitions on
a'.
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:
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)