Communicating sequential processes

In computer science, communicating sequential processes (CSP) 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, INMOS document 72 occ 45 03. and also influenced the design of programming languages such as Limbo, RaftLib, Erlang, Go, Crystal, and Clojure's core.async.

CSP was first described by Tony Hoare in a 1978 article, and 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 e-commerce system. The theory of CSP itself is also still the subject of active research, including work to increase its range of practical applicability (e.g., increasing the scale of the systems that can be tractably analyzed).

History Original version 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 = *[c:character; west?c → east!c]

repeatedly receives a character from the process named west and sends that character to process named east. The parallel composition

[west::DISASSEMBLE || X::COPY || east::ASSEMBLE]

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.

Development into process algebra 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 (CCS) 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 third-most cited computer science reference of all time according to Citeseer (albeit an unreliable source due to the nature of its sampling). 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 (consisting of about 23,000 lines of code) 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 (approximately 100,000 lines of code) 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 and primitive processes.

Events

Events represent communications or interactions. They are assumed to be instantaneous, and their communication is all that an external 'environment' can know about processes. An event is communicated only if the environment allows it. If a process does offer an event and the environment allows it, then that event must be communicated. Events may be atomic names (e.g., , ), compound names (e.g. , ), or input/output events (e.g., , ). The set of all events is denoted .

Primitive processes

Primitive processes represent fundamental behaviors: examples include (the process that immediately deadlocks), and (the process that immediately terminates successfully).

Algebraic operators CSP has a wide range of algebraic operators. The principal ones are informally given as follows.

Prefix

The prefix operator combines an event and a process to produce a new process. For example, is the process that is willing to communicate event with its environment and, after , behaves like the process .

Recursion

Processes can be defined using recursion. Where is any CSP term involving , the process defines a recursive process given by the equation . Recursions can also be defined mutually, such as

which defines a pair of mutually recursive processes that alternate between communicating and .

Deterministic choice

The deterministic (or external) choice operator allows the future evolution of a process to be defined as a choice between two component processes and allows the environment to resolve the choice by communicating an initial event for one of the processes. For example, is the process that is willing to communicate the initial events and and subsequently behaves as either or , depending on which initial event the environment chooses to communicate.

Nondeterministic choice

The nondeterministic (or internal) choice operator allows the future evolution of a process to be defined as a choice between two component processes, but does not allow the environment any control over which one of the component processes will be selected. For example, can behave like either or . It can refuse to accept or and is only obliged to communicate if the environment offers both and .

Nondeterminism can be inadvertently introduced into an ostensibly deterministic choice if the initial events of both sides of the choice are identical. So, for example, and

are equivalent.

Interleaving

The interleaving operator represents completely independent concurrent activity. The process behaves as both and simultaneously. The events from both processes are arbitrarily interleaved in time. Interleaving can introduce nondeterminism even if and are both deterministic: if and can both communicate the same event, then nondeterministically chooses which of the two processes communicated that event.

Interface parallel

The interface parallel (or generalized parallel) operator represents concurrent activity that requires synchronization between the component processes: for , any event in the interface set can only occur when both and are able to engage in that event.

For example, the process requires that and must both be able to perform event before that event can occur. So, the process is equivalent to , while is equivalent to (i.e. the process deadlocks).

Hiding

The hiding operator provides a way to abstract processes by making some events unobservable by the environment. is the process with the event set hidden.

A trivial example of hiding is which, assuming that the event doesn't appear in , simply reduces to . Hidden events are internalized as τ actions, which are invisible to and uncontrollable by the environment. The existence of hiding introduces an additional behaviour called divergence, where an infinite sequence of τ actions is performed. This is captured by the process , whose behaviour is solely to perform τ actions forever. For example, is equivalent to .

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 that demands payment (only in cash) 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 were only required on "coin", we would obtain

If we abstract this latter composite process by hiding the "coin" and "card" events, i.e.,

we obtain the nondeterministic process

This is a process that 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 (e.g., someone who does not see the decision reached by the person), 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, be a boolean, 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.