The Laboratory has been a centre for concurrency research since
(now Sir) Tony Hoare's arrival in 1977, and his development of CSP.
there are a number of approaches to how to model the behaviours of
systems mathematically, a characteristic "Oxford style" of semantic
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
infinite) traces, failures (a trace s and a set X of events refusable
s), and divergences (traces on which the process can enter an infinite
unbroken series of internal actions). These lead to models over which
mathematical theories of partial orders and metric spaces allow much
analysis of process behaviour, and which in particular always come
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
member of the club of "process algebras", namely mathematical-looking
based on operators for describing patterns of parallel interaction, and
which often have little or no support for the data calculations which
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
built back in. There have been two important more-or-less direct
in doing this, alongside the influence CSP has had on the
primitives included in other languages.
The first of these was the imperative programming language occam,
as the language of the inmos transputer. occam is essentially CSP with
simple imerative features added, and had semantics derived directly
those of CSP.
While occam was given an appearance closer to traditional
languages than to a process algebra, CSPM, a more recent development,
rigorously to the design philosophy of CSP. It uses a declarative
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
main vehicle for CSP tool development over the past decade, and for
practical uses of the language in specification and verification work,
but has also spawned theoretical work in itself such as Lazic's work on
Theoretical work on CSP has encompassed unbounded nondeterminism,
to novel fixed point theories, and has included extensive work on
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