The Laboratory has been a centre for concurrency research since
Professor
(now Sir) Tony Hoare's arrival in 1977, and his development of CSP.
Though
there are a number of approaches to how to model the behaviours of
concurrent
systems mathematically, a characteristic "Oxford style" of semantic
modelling
was developed by Hoare and his students and collaborators.
In this style, a process is modelled primarily by all the behaviours
of one or more sorts that it could ever exhibit, such as finite (and
sometimes
infinite) traces, failures (a trace s and a set X of events refusable
after
s), and divergences (traces on which the process can enter an infinite
unbroken series of internal actions). These lead to models over which
the
mathematical theories of partial orders and metric spaces allow much
useful
analysis of process behaviour, and which in particular always come
equipped
with a natural theory of refinement. They can also be related naturally
to alternative approaches to semantics such as transition-system based
operational semantics and algebraic semantics.
Together with CCS, which was developed concurrently, CSP is a
founder
member of the club of "process algebras", namely mathematical-looking
notations
based on operators for describing patterns of parallel interaction, and
which often have little or no support for the data calculations which
form
the heart of most programming languages. Of course, in order to use it
in anything but toy examples, CSP had to have the capability for data
manipulation
built back in. There have been two important more-or-less direct
exercises
in doing this, alongside the influence CSP has had on the
communications
primitives included in other languages.
The first of these was the imperative programming language occam,
developed
as the language of the inmos transputer. occam is essentially CSP with
simple imerative features added, and had semantics derived directly
from
those of CSP.
While occam was given an appearance closer to traditional
programming
languages than to a process algebra, CSPM, a more recent development,
sticks
rigorously to the design philosophy of CSP. It uses a declarative
paradigm
for data, as opposed to the imperative one of occam, and is therefore,
essentially, a functional programming language in the style of Haskell,
with many additional features to support communication. CSPM has been
the
main vehicle for CSP tool development over the past decade, and for
many
practical uses of the language in specification and verification work,
but has also spawned theoretical work in itself such as Lazic's work on
data independence.
Theoretical work on CSP has encompassed unbounded nondeterminism,
leading
to novel fixed point theories, and has included extensive work on
incorporating
time, priority, probability etc.
The best source of further information on the theory of CSP is the
"The Theory and Practice" book by A. W. Roscoe (available
electronically in our books
section)
