Strategic Directions
Concurrency research group
Unifying theories: a personal statement

C.A.R. Hoare

The progress of science involves a constant interplay between diversification and unification. Diversification extends the boundaries of science to cover new and wider ranges of phenomena; successful unification reveals that a range of experimentally validated theories are no more than particular cases of some more general principle. The cycle continues when the general principle suggests further specialisations for experimental investigation.

There is a lot of inherent diversity in the study of concurrency. There are major dichotomies between shared store and disjoint store approaches, between pairwise synchronisation and global lockstep synchronisation, between channelled and unchanelled communication, between isochronous and buffered input/output, and between hardware and software implementations. Further dichotomies can be introduced by varying the style of presentation of the theories, for example, in the form of operational, algebraic or denotational semantics.

The diversity of the phenomena gives scope for an equal diversity of the theories needed to explain and control them. It is unfortunate if one particular class of phenomenon becomes too fashionable; apart from distortion in the study of the subject as a whole, theories covering the same phenomena can engender unnecessary division between theoretical schools, particularly when there is no clear experimental criterion for choosing between them. Perhaps this has already happened, with at least three theories of synchronised channelled communication among processes with disjoint state. They differ primarily in their style of presentation.

I think that the time is ripe to make a start on the process of unification, which will show the relationship between many of the specialised theories of concurrency, and even apply to normal sequential programming. It is known that unification can be achieved at the level of operational semantics, for example by simulating the phenomena on a Turing machine. But this is not wholly illuminating: the structural similarities between theories tend to be obscured by their minor differences, which nevertheless have a major pervasive effect throughout the code of the simulation program. Algebraic presentations are much better for classifying theories by their many similarities and few differences.

But I recommend use of all the different styles of presentation because they each have value for differing purposes. A top-down approach may start with something like a denotational semantics, which provides a conceptual framework for specifying the requirements and intended effects of an engineering artifact, abstracting as far as possible from the technological details of its implementation. This has the practical benefit that the system may be later implemented in a mixture of paradigms, within a theory powerful enough to prove its overall correctness. But the scientific benefit is even greater: the alternative paradigms can be defined by just restricting the notations in which the details of an artifact are described. As a result, the structure of the discipline is embodied in the subset relation between paradigms, with the more complex of them revealed as subsets of the simpler ones. All the algebraic properties of the simpler theories are automatically inherited by the complex ones. An operational presentation is the most specific to a particular paradigm; its correctness can be established with the aid of algebraic reasoning.

That is the hope of unification which I am pursuing with the help of my valued colleague Jifeng He. Perhaps we will discover something of interest and of benefit; or even better, we will encourage the scientific community to collaborate in more effective pursuit of the same goal.