Process calculus
|
In the first half of the 20th century, various formalisms were proposed to capture the informal concept of computable function, μ-recursive functions, Turing Machines and the λ-calculus possibly being the most well-known examples today. The surprising fact that they are essentially equivalent in the sense that they are all encodable into each other is the content of the Church-Turing thesis. Another shared feature is more rarely commented on: they all are most readily understood as models of sequential computation.
The subsequent consolidation of computer science required a more subtle formulation of the notion of computation, in particular explicit representations of concurrency and communication. Petri-Nets and calculi such as Tony Hoare's CSP, Robin Milner's CCS and the π-calculus by Milner, Joachim Parrow and David Walker are currently the most prominent calculi to have emerged from this line of enquiry.
The process calculus approach gathered momentum in the 1970s when it became increasingly clear that the then dominant approaches to modelling computation were unlikely to yield satisfactory accounts of non-deterministic, non-terminating and interacting agents. Instead, early pioneers such as Milner and Hoare decided to make interaction between agents executing in parallel the basic computational primitive. This can be done in several ways that can be characterised by three core design decisions.
- Computing agents have zero or more discrete points of connection and interaction called, interchangeably, names, channels or interaction points. Parallel composition of two agents involves connecting their interaction points by links, whenever they share a name. Crucially, a link does not preclude further connections at a name. The Internet is a good source of analogies here: names correspond roughly to IP addresses (plus port numbers, but let's ignore this detail for simplicity).
- Computation itself is binary, point-to-point interaction between independent agents. Interaction happens along names by handshaking or synchronisation between a sender and a receiver. This handshaking may or may not involve passing data from the sender to the receiver. In the Internet, interaction happens by sending IP packets between computers.
- Interaction is an atemporal event in the sense that it does not have a duration. Interactions may be ordered in time. Here the Internet analogy breaks down because the duration of packet delivery from sender to receiver has important semantic consequences.
To define a process calculus, one starts with a set of names, the discrete interaction points. Names have no internal structure apart from what is required to distinguish names from one another. Hence names are pure. Their only purpose is to denote interaction points. In many implementations, names have rich internal structure to improve efficiency, but this is abstracted away in most theoretic models. In addition to names, one needs a means to form new processes from old: the crucial operators, always present in some form or other, allow
- the parallel composition of processes,
- to specify which channels to use for sending and receiving data,
- sequentialisation of interactions,
- hiding of interaction points and
- recursion or replication.
Parallel composition of two processes P and Q, usually written P | Q is the key primitive distinguishing sequential models of computation from process calculi. It allows computation in P and Q to proceed simultaneously and independently. But it also allows interaction, that is synchronisation and flow of information from P to Q on a channel shared by both (or vice versa). Channels are created by shared names in parallel composition.
Interaction is a directed flow of information. That means, input and output are distinguished as dual interaction primitives. We have an input operator x(v) and an output operator x<y>, both of which name an interaction point (here x) that is used to synchronise with a dual interaction primitive. Should information be exchanged, it will flow from the outputting to the inputting process. The output primitive will specify the data to be sent. In x<y>, this data is y. Similarly, if an input expects to receive data, one or more bound variables will act as place-holders to be substituted by data, when it arrives. In x(v), v plays that role. But what kind of data is exchanged in an interaction? There are various choices. It will turn out that this choice is a key distinguishing feature between process calculi.
Sometimes interactions must be temporally ordered, because we might want to specify algorithms like: first receive some data on x and then send that data on y. Sequential composition can be used for such purposes. It is well-known from other models of computation. In process calculi, the sequentialisation operator is usually integrated with input or output or both. For example the process x(v).P will wait for an input on x. Only when this input occurs, P will be activated with the received data substituted for v.
The key operational rule, containing the computational essence of process calculi, can be given solely in terms of parallel composition, sequentialisation, input and output: although the details vary, it always looks something like this.
The process x<y>.P sends a message, here y, along the channel x. Once that message has been sent, x<y>.P becomes the process P. Dually, the process x(v).Q receives that message on channel x to become Q[y/v], which is Q with the place-holder v substituted by y, the data received on x. The class of processes that P is allowed to range over as the continuation of the output operation substantially influences the properties of the calculus.
Processes do not limit the number of connection that can be made at a given interaction point. But interaction points allow interference (i.e. interaction). For the synthesis of compact, minimal and compositional systems, the ability to restrict interference is crucial. Hiding operations allow to control the connections made between interaction points when composing agents in parallel. In sequential models of computation, scoping rules, procedures and objects facilitate hiding (but they might have other uses, too: functional features in the case of procedures and subtyping with its associated dispatch mechanisms for objects). We denote the hiding of a name x in P by (ν x)P. Figure shows the effect of going from P to (ν x)P. The process P on the left can interact with the outside world on x, y and z. In contrast, (ν x)P on the right can only use y and z for this purpose. The restriction does not prevent usage of x inside P. But what happens if x gets sent to a process outside of (ν x)P, as may happen in (ν x)(y<x> | Q), provided x \neq y? Whether or not it is possible to communicate a name hidden this way is another important point of divergence between different calculi.
The operations presented so far allow to describe only finite interaction and are consequently insufficient for full computability, which includes non-terminating behaviour. Recursion or replication are operations that allow finite descriptions of infinite behaviour. Recursion is well-known from the sequential world. Replication !P can be understood as abbreviating the parallel composition of a countably infinite number of P 's.
Finally, we mention the null process which has no interaction points. It is utterly inactive and its sole purpose is to act as the inductive anchor on top of which we can generate more interesting processes.
Many different variants of process calculi have been studied and not all of them fit the paradigm sketched here. The most prominent example may be the Ambient calculus. This is to be expected as process calculi are an active field of study. Currently research on process calculi focuses on the following problems.
- Development of new process calculi for better modelling of computational phenomena.
- Finding well behaved subcalculi of a given process calculus. This is valuable because (1) most calculi are fairly wild in the sense that they are rather general and not much can be said about arbitrary processes; and (2) computational application rarely exhaust the whole of a calculus. Rather they use only processes that are very constrained in form. Constraining the shape of processes is mustly studied by way of Datatype.
- Logics for processes that allow to reason about (essentially) arbitrary properties of processes, following the ideas of Hoare logic.
- Behavioural theory: what does it mean for two processes to be the same? How can we decide whether two processes are different or not? Can we find representatives for equivalence classes of processes. Generally, processes are considered to be the same if no context, that is other processes running in parallel, can detect a difference. Unfortunately, making this intuition precises is subtle and mostly yields unwieldy characterisations of equality (which must also be undecidable, as a consequence of the Halting Problem in most cases). Bisimulations are a technical tool that aids reasoning about process equivalences.
- Expressivity of calculi. Programming experience shows that certain problems are easier to solve in some languages than in others. This phenomenon calls for a more precise characterisation of the expressivity of calculi modelling computation than that afforded by the Church-Turing thesis. One way of doing this is to consider encodings between two formalisms and see what properties encodings can potentially preserve. The more properties can be preserved, the more expressive the target of the encoding is said to be. For process calculi, the celebrated results are that the synchronous π-calculus is more expressive than its asynchronous variant, has the same expressive power as the higher-order π-calculus, but less than the Ambient calculus.
- Using process calculus to model biological systems. It is thought by some that the compositionality offered by process-theoretic tools can help biologists to organise their knowledge more formally.