Communicating Sequential Processes
📜 Abstract
Chapter 1 introduces the basic concept of a process as a mathematical abstraction of the interactions between a system and its environment. It shows how the familiar technique of recursion may be used to describe processes that last a long time, or forever. The concepts are explained first by example and then by pictures; a more complete explanation is given by algebraic laws, and by an implementation on a computer in a functional programming language. The second part of the chapter explains how the behaviour of a process can be recorded as a trace of the sequence of actions in which it engages. Many useful operations on traces are defined. A process can be specified in advance of implementation by describing the properties of its traces. Rules are given to help in implementation of processes which can be proved to meet their specifications. The second chapter describes how processes can be assembled together into systems, in which the components interact with each other and with their external environment. The introduction of concurrency does not by itself introduce any element of nondeterminism. The main example of this chapter is a treatment of the traditional tale of the five dining philosophers. The second part of Chapter 2 shows how processes can be conveniently adapted to new purposes by changing the names of the events in which they engage. The chapter concludes with an explanation of the mathematical theory of deterministic processes, including a simple account of the domain theory of recursion. The third chapter gives one of the simplest known solutions to the vexed problem of nondeterminism. Nondeterminism is shown to be a valuable technique for achieving abstraction, since it arises naturally from the decision to ignore or conceal those aspects of the behaviour of a systems in which we are no longer interested. It also preserves certain symmetries in the definition of the operators of the mathematical theory. Proof methods for nondeterministic processes are slightly more complicated than those for deterministic processes, since it is necessary to demonstrate that every possible nondeterministic choice will result in a behaviour which meets the given specification. Fortunately, there are techniques for avoiding nondeterminism, and these are used extensively in Chapters 4 and 5. Consequently the study or mastery of Chapter 3 can be postponed until just before Chapter 6, in which the introduction of nondeterminism can no longer be avoided. In the later sections of Chapter 3, there is given a complete mathematical definition of the concept of a nondeterministic process. This definition will be of interest to the pure mathematician, who wishes to explore the foundations of the subject, or to verify by proof the validity of the algebraic laws and other properties of processes. Applied mathematicians (including programmers) may choose to regard the laws as self-evident or justified by their utility; and they may safely omit the more theoretical sections. Chapter 4 at last introduces communication: it is a special case of interaction between two processes, one of which outputs a message at the same time as the other one inputs it. Thus communication is synchronised; if buffering is required on a channel, this is achieved by interposing a buffer process between the two processes. An important objective in the design of concurrent systems is to achieve greater speed of computation in the solution of practical problems. This is illustrated by the design of some simple systolic (or iterative) array algorithms. A simple case is a pipe, defined as a sequence of processes in which each process inputs only from its predecessor and outputs only to its successor. Pipes are useful for the implementation of a single direction of a communications protocol, structured as a hierarchy of layers. Finally, the important concept of an abstract data type is modelled a a subordinate process, each instance of which communicates only with the block in which it is declared. Chapter 5 shows how the conventional operators of sequential programming can be integrated within the framework of communicating sequential processes. It may be surprising to experienced programmers that these operators enjoy the same kind of elegant algebraic properties as the operators of familiar mathematical theories; and that sequential programs can be proved to meet their specifications in much the same way as concurrent programs. Even the externally triggered interrupt is defined and shown to be useful, and subject to elegant laws. Chapter 6 describes how to structure and implement a system in which a limited number of physical resources such as discs and line printers can be shared among a greater number of processes, whose resource requirements vary with time. Each resource is represented as a single process. On each occasion that a resource is required by a user process, a new virtual resource is created. A virtual resource is a process which behaves as if it were subordinate to the user process; but it also communicates with the real resource whenever required. Such communications are interleaved with those of other concurrently active virtual processes. So the real and virtual processes play the same roles as the monitors and envelopes of PASCAL PLUS. The chapter is illustrated by the modular development of a series of complete but very simple operating systems, which are the largest examples given in this book. Chapter 7 describes a number of alternative approaches to concurrency and communication, and explains the technical, historical, and personal motives which led to the theory expounded in the preceding chapters. Here I acknowledge my great debt to other authors, and give recommendations and an introduction to further reading in the field.
✨ Summary
Impact and influence.
Hoare’s CSP established a process-algebraic framework for describing concurrent systems through observable behaviour, including traces, refusals, and divergences. Oxford’s concurrency research group identifies CSP as the basis of a continuing research tradition in mathematical models of concurrency and refinement. (cs.ox.ac.uk)
The semantic ideas developed from CSP led to failures-divergences refinement and to the FDR model checker. FDR’s documentation describes the tool as being founded on CSP-based concurrency theory and using refinement to verify properties of state-machine models. (cs.ox.ac.uk) Subsequent CSP research connected these models to timed systems, operational semantics, data refinement, and mechanized verification. (cs.ox.ac.uk)
CSP-based refinement checking has also been applied to security-protocol analysis; Oxford describes the use of CSP and FDR to specify, analyze, and verify protocols in the presence of modeled adversaries. (cs.ox.ac.uk) A later retrospective reports industrial applications of CSP and FDR and characterizes the combination as a practical process-algebra approach. (cs.ox.ac.uk)