Department of Computer Science
University of Oxford

Theory of Concurrency

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)

Random Image
Random Image
Random Image