Communicating sequential processes


In computer science, communicating sequential processes is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi, based on message passing via channels. CSP was highly influential in the design of the occam programming language and also influenced the design of programming languages such as Limbo, RaftLib, Go, Crystal, and Clojure's core.async.
CSP was first described in a 1978 article by Tony Hoare, but has since evolved substantially. CSP has been practically applied in industry as a tool for specifying and verifying the concurrent aspects of a variety of different systems, such as the T9000 Transputer, as well as a secure ecommerce system. The theory of CSP itself is also still the subject of active research, including work to increase its range of practical applicability.

History

The version of CSP presented in Hoare's original 1978 article was essentially a concurrent programming language rather than a process calculus. It had a substantially different syntax than later versions of CSP, did not possess mathematically defined semantics, and was unable to represent unbounded nondeterminism. Programs in the original CSP were written as a parallel composition of a fixed number of sequential processes communicating with each other strictly through synchronous message-passing. In contrast to later versions of CSP, each process was assigned an explicit name, and the source or destination of a message was defined by specifying the name of the intended sending or receiving process. For example, the process
COPY = *
repeatedly receives a character from the process named west and sends that character to process named east. The parallel composition

assigns the names west to the DISASSEMBLE process, X to the COPY process, and east to the ASSEMBLE process, and executes these three processes concurrently.
Following the publication of the original version of CSP, Hoare, Stephen Brookes, and A. W. Roscoe developed and refined the theory of CSP into its modern, process algebraic form. The approach taken in developing CSP into a process algebra was influenced by Robin Milner's work on the Calculus of Communicating Systems and conversely. The theoretical version of CSP was initially presented in a 1984 article by Brookes, Hoare, and Roscoe, and later in Hoare's book Communicating Sequential Processes, which was published in 1985. In September 2006, that book was still the computer science reference of all time according to Citeseer. The theory of CSP has undergone a few minor changes since the publication of Hoare's book. Most of these changes were motivated by the advent of automated tools for CSP process analysis and verification. Roscoe's The Theory and Practice of Concurrency describes this newer version of CSP.

Applications

An early and important application of CSP was its use for specification and verification of elements of the INMOS T9000 Transputer, a complex superscalar pipelined processor designed to support large-scale multiprocessing. CSP was employed in verifying the correctness of both the processor pipeline and the Virtual Channel Processor, which managed off-chip communications for the processor.
Industrial application of CSP to software design has usually focused on dependable and safety-critical systems. For example, the Bremen Institute for Safe Systems and Daimler-Benz Aerospace modeled a fault-management system and avionics interface intended for use on the International Space Station in CSP, and analyzed the model to confirm that their design was free of deadlock and livelock. The modeling and analysis process was able to uncover a number of errors that would have been difficult to detect using testing alone. Similarly, Praxis High Integrity Systems applied CSP modeling and analysis during the development of software for a secure smart-card certification authority to verify that their design was secure and free of deadlock. Praxis claims that the system has a much lower defect rate than comparable systems.
Since CSP is well-suited to modeling and analyzing systems that incorporate complex message exchanges, it has also been applied to the verification of communications and security protocols. A prominent example of this sort of application is Lowe’s use of CSP and the FDR refinement-checker to discover a previously unknown attack on the Needham–Schroeder public-key authentication protocol, and then to develop a corrected protocol able to defeat the attack.

Informal description

As its name suggests, CSP allows the description of systems in terms of component processes that operate independently, and interact with each other solely through message-passing communication. However, the "Sequential" part of the CSP name is now something of a misnomer, since modern CSP allows component processes to be defined both as sequential processes, and as the parallel composition of more primitive processes. The relationships between different processes, and the way each process communicates with its environment, are described using various process algebraic operators. Using this algebraic approach, quite complex process descriptions can be easily constructed from a few primitive elements.

Primitives

CSP provides two classes of primitives in its process algebra:
;Events
;Primitive processes:

Algebraic operators

CSP has a wide range of algebraic operators. The principal ones are:
; Prefix
; Deterministic choice
; Nondeterministic choice
; Interleaving
; Interface parallel
; Hiding

Examples

One of the archetypal CSP examples is an abstract representation of a chocolate vending machine and its interactions with a person wishing to buy some chocolate. This vending machine might be able to carry out two different events, “coin” and “choc” which represent the insertion of payment and the delivery of a chocolate respectively. A machine which demands payment before offering a chocolate can be written as:
A person who might choose to use a coin or card to make payments could be modelled as:
These two processes can be put in parallel, so that they can interact with each other. The behaviour of the composite process depends on the events that the two component processes must synchronise on. Thus,
whereas if synchronization was only required on “coin”, we would obtain
If we abstract this latter composite process by hiding the “coin” and “card” events, i.e.
we get the nondeterministic process
This is a process which either offers a “choc” event and then stops, or just stops. In other words, if we treat the abstraction as an external view of the system, nondeterminism has been introduced.

Formal definition

Syntax

The syntax of CSP defines the “legal” ways in which processes and events may be combined. Let be an event, and be a set of events. Then the basic syntax of CSP can be defined as:
Note that, in the interests of brevity, the syntax presented above omits the process, which represents divergence, as well as various operators such as alphabetized parallel, piping, and indexed choices.

Formal semantics

CSP has been imbued with several different formal semantics, which define the meaning of syntactically correct CSP expressions. The theory of CSP includes mutually consistent denotational semantics, algebraic semantics, and operational semantics.

Denotational semantics

The three major denotational models of CSP are the traces model, the stable failures model, and the failures/divergences model. Semantic mappings from process expressions to each of these three models provide the denotational semantics for CSP.
The traces model defines the meaning of a process expression as the set of sequences of events that the process can be observed to perform. For example,
More formally, the meaning of a process in the traces model is defined as such that:
where is the set of all possible finite sequences of events.
The stable failures model extends the traces model with refusal sets, which are sets of events that a process can refuse to perform. A failure is a pair, consisting of a trace, and a refusal set which identifies the events that a process may refuse once it has executed the trace. The observed behavior of a process in the stable failures model is described by the pair. For example,
The failures/divergence model further extends the failures model to handle divergence. The semantics of a process in the failures/divergences model is a pair where is defined as the set of all traces that can lead to divergent behavior and.

Tools

Over the years, a number of tools for analyzing and understanding systems described using CSP have been produced. Early tool implementations used a variety of machine-readable syntaxes for CSP, making input files written for different tools incompatible. However, most CSP tools have now standardized on the machine-readable dialect of CSP devised by Bryan Scattergood, sometimes referred to as CSPM. The CSPM dialect of CSP possesses a formally defined operational semantics, which includes an embedded functional programming language.
The most well-known CSP tool is probably Failures/Divergence Refinement 2, which is a commercial product developed by Formal Systems Ltd. FDR2 is often described as a model checker, but is technically a refinement checker, in that it converts two CSP process expressions into Labelled Transition Systems, and then determines whether one of the processes is a refinement of the other within some specified semantic model. FDR2 applies various state-space compression algorithms to the process LTSs in order to reduce the size of the state-space that must be explored during a refinement check. FDR2 has been succeeded by FDR3, a completely re-written version incorporating amongst other things parallel execution and an integrated type checker. It is released by the University of Oxford, which also released FDR2 in the period 2008-12.
The Adelaide Refinement Checker is a CSP refinement checker developed by the Formal Modelling and Verification Group at The University of Adelaide. ARC differs from FDR2 in that it internally represents CSP processes as Ordered Binary Decision Diagrams, which alleviates the state explosion problem of explicit LTS representations without requiring the use of state-space compression algorithms such as those used in FDR2.
The ProB project, which is hosted by the Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, was originally created to support analysis of specifications constructed in the B method. However, it also includes support for analysis of CSP processes both through refinement checking, and LTL model-checking. ProB can also be used to verify properties of combined CSP and B specifications. A ProBE CSP Animator is integrated in FDR3.
The Process Analysis Toolkit
is a CSP analysis tool developed in the School of Computing at the National University of Singapore. PAT is able to perform refinement checking, LTL model-checking, and simulation of CSP and Timed CSP processes. The PAT process language extends CSP with support for mutable shared variables, asynchronous message passing, and a variety of fairness and quantitative time related process constructs such as deadline and waituntil. The underlying design principle of the PAT process language is to combine a high-level specification language with procedural programs for greater expressiveness. Mutable shared variables and asynchronous channels provide a convenient syntactic sugar for well-known process modelling patterns used in standard CSP. The PAT syntax is similar, but not identical, to CSPM. The principal differences between the PAT syntax and standard CSPM are the use of semicolons to terminate process expressions, the inclusion of syntactic sugar for variables and assignments, and the use of slightly different syntax for internal choice and parallel composition.
VisualNets produces animated visualisations of CSP systems from specifications, and supports timed CSP.
CSPsim is a lazy simulator. It does not model check CSP, but is useful for exploring very large systems.
is a CSP refinement checker with interactive modeling and analyzing environment. It has a graphical state-transition diagram editor. The user can model the behavior of processes as not only CSP expressions but also state-transition diagrams. The result of checking are also reported graphically as computation-trees and can be analyzed interactively with peripheral inspecting tools. In addition to refinement checks, It can perform deadlock check and livelock check.

Related formalisms

Several other specification languages and formalisms have been derived from, or inspired by, the classic untimed CSP, including:
In as much as it is concerned with concurrent processes that exchange messages, the Actor model is broadly similar to CSP. However, the two models make some fundamentally different choices with regard to the primitives they provide: