Review of the pi-calculus: a theory of mobile processes

With the rise of computer networks in the past decades, the sp read of distributed applications with components across multiple machines, and with new notions such as mobile code, there has been a need for formal methods to model and reason about concurrency and mobility. The study of sequ ential computations has been based on notions such as Turing machines, recursive functions, the -calculus, all equivalent formalisms capturing the essenc e of sequential computations. Unfortunately, for concurrent programs, th eories for sequential computation are not enough. Many programs are not simply programs that compute a result and re turn it to the user, but rather interact with other programs, and even move from machine to machine. Process calculi are an attempt at getting a formal foundatio n based on such ideas. They emerged from the work of Hoare [4] and Milner  on models of concurrency. These calc uli are meant to model systems made up of processes communicating by exchanging values across channels. They a llow for the dynamic creation and removal of processes, allowing the modelling of dynamic systems. A typical proces s calculus in that vein is CCS [6, 7]. The -calculus extends CCS with the ability to create and remove communicat ion links between processes, a new form of dynamic behaviour. By allowing links to be created and deleted, it is po sible to model a form of mobility, by identifying the position of a process by its communication links. This book, “The -calculus: A Theory of Mobile Processes”, by Davide Sangior gi and David Walker, is a in-depth study of the properties of the -calculus and its variants. In a sense, it is the logical foll owup to the recent introduction to concurrency and the -calculus by Milner , reviewed in SIGACT News, 31(4), Dec ember 2000. What follows is a whirlwind introduction to CCS and the -calculus. It is meant as a way to introduce the notions discussed in much more depth by the book under review. Let us s tart with the basics. CCS provides a syntax for writing processes. The syntax is minimalist, in the grand tradition of foundational calculi such as the -calculus. Processes perform actions, which can be of three forms: the sending of a message over channel x (written x), the receiving of a message over channel x (written x), and internal actions (written ), the details of which are unobservable. Send and receive actions are called synchronizationactions, since communication occurs when the correspondin g processes synchronize. Let stand for actions, including the internal action , while we reserve ;  for synchronization actions. 1 Processes are written using the following syntax: P ::= Ahx1; : : : ; xki jXi2I i:Pi j P1jP2 j x:P We write 0 for the empty summation (when I = ;). The idea behind process expressions is simple. The proces s 0 represents the process that does nothing and simply termina tes. A process of the form :P awaits to synchronize with a process of the form :Q, after which the processes continue as process P andQ respectively. A generalization 1In the literature, the actions of CCS are often given a much mo re abstract interpretation, as simply names and co-names. T he send/receive interpretation is useful when one moves to the -calculus.