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
P_{1} and P_{2} that are running concurrently must obey
the following three laws:

- Processes are synchronized on common symbols. That is, if
`a`

is in both processes' alphabets, then P_{1}can transition on`a`

if and only if P_{2}also transitions on`a`

at the same time. - Processes block on opposing guards. That is to say, if
`a`

and`b`

are both in both processes' alphabets, P_{1}can only transition on`a`

, and P_{2}can only transition on`b`

, then neither process can move. - Processes ignore foreign symbols. That is, if
`a`

is in P_{1}'s alphabet but not P_{2}'s, then P_{1}may transition on`a`

independently of P_{2}'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 -> Pwhere

`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 -> Pwhere

`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' -> U1Then

`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:

- T transitions on
`a`

, U doesn't transition. - U transitions on
`a'`

, T doesn't transition. - T transitions on
`b`

, U doesn't transition. - T transitions on
`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:

- If P transitions to P' via s, then there exists a Q' such that Q transitions to Q' via s.
- 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)