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 and also influenced the design of programming languages such as Limbo, RaftLib, Erlang, Go,

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 <code>west</code> and sends that character to process named <code>east</code>. The parallel composition

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

assigns the names <code>west</code> to the <code>DISASSEMBLE</code> process, <code>X</code> to the <code>COPY</code> process, and <code>east</code> to the <code>ASSEMBLE</code> process, and executes these three processes concurrently. and later in Hoare's book Communicating Sequential Processes, 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.

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 <math>\Sigma</math>.

;Primitive processes

Primitive processes represent fundamental behaviors: examples include <math>\mathrm{STOP}</math> (the process that immediately deadlocks), and <math>\mathrm{SKIP}</math> (the process that immediately terminates successfully). The CSP<sub>M</sub> dialect of CSP possesses a formally defined operational semantics, which includes an embedded functional programming language.

FDR

The most well-known CSP tool is probably Failures–Divergences Refinement, which is a commercial product originally developed by Formal Systems (Europe) Ltd. FDR 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 (LTSs), and then determines whether one of the processes is a refinement of the other within some specified semantic model (traces, failures, or failures/divergence). FDR 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. FDR was succeeded by FDR2, FDR3 and FDR4.

ARC

The Adelaide Refinement Checker (ARC) 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 (OBDDs), 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.

ProB

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.

PAT

The Process Analysis Toolkit (PAT) 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 <code>deadline</code> and <code>waituntil</code>. The underlying design principle of the PAT process language is to combine a high-level specification language with procedural programs (e.g. an event in PAT may be a sequential program or even an external C# library call) 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 CSP<sub>M</sub>. The principal differences between the PAT syntax and standard CSP<sub>M</sub> 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.

Others

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 (potentially infinite) systems.

SyncStitch is a CSP refinement checker with an 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 results of checking are also reported graphically as computation trees and can be analyzed interactively with peripheral inspection tools. In addition to refinement checks, it can perform deadlock checks and livelock checks.

Several other specification languages and formalisms have been derived from, or inspired by, the classic untimed CSP, including:

  • Timed CSP, which incorporates timing information for reasoning about real-time systems
  • Receptive Process Theory, a specialization of CSP that assumes an asynchronous (i.e., nonblocking) send operation
  • CSPP
  • HCSP
  • TCOZ, an integration of Timed CSP and Object Z
  • Circus, an integration of CSP and Z based on the Unifying Theories of Programming
  • CML (COMPASS Modelling Language), a combination of Circus and VDM developed for the modelling of Systems of Systems (SoS)
  • CspCASL, an extension of CASL that integrates CSP
  • LOTOS, an international standard that incorporates features of CSP and CCS.
  • PALPS, a probabilistic extension with locations for ecological models developed by Anna Philippou and Mauricio Toro Bermúdez

Comparison with the actor model

Inasmuch 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:

  • CSP processes are anonymous, while actors have identities.
  • CSP uses explicit channels for message passing, whereas actor systems transmit messages to named destination actors. These approaches may be considered duals of each other, in the sense that processes received through a single channel effectively have an identity corresponding to that channel, while the name-based coupling between actors may be broken by constructing actors that behave as channels.
  • CSP message-passing fundamentally involves a rendezvous between the processes involved in sending and receiving the message, i.e., the sender cannot transmit a message until the receiver is ready to accept it. In contrast, message-passing in actor systems is fundamentally asynchronous, i.e., message transmission and reception do not have to happen at the same time, and senders may transmit messages before receivers are ready to accept them. These approaches may also be considered duals of each other, in the sense that rendezvous-based systems can be used to construct buffered communications that behave as asynchronous messaging systems, while asynchronous systems can be used to construct rendezvous-style communications by using a message/acknowledgement protocol to synchronize senders and receivers.

Note that the aforementioned properties do not necessarily refer to the original CSP paper by Hoare, but rather the modern incarnation of the idea as seen in implementations such as Go and Clojure's core.async. In the original paper, channels were not a central part of the specification, and the sender and receiver processes actually identify each other by name.

Award

In 1990, “A Queen’s Award for Technological Achievement [was] conferred ... on [[Oxford University Computing Laboratory|[Oxford University] Computing Laboratory]]. The award recognises a successful collaboration between the laboratory and Inmos Ltd. … Inmos’ flagship product is the ‘transputer’, a microprocessor with many of the parts that would normally be needed in addition built into the same single component.”

According to Tony Hoare,

“The INMOS Transputer was an embodiment of the ideas … of building microprocessors that could communicate with each other along wires that would stretch between their terminals. The founder had the vision that the CSP ideas were ripe for industrial exploitation, and he made that the basis of the language for programming Transputers, which was called Occam. … The company estimated it enabled them to deliver the hardware one year earlier than would otherwise have happened. They applied for and won a Queen’s award for technological achievement, in conjunction with Oxford University Computing Laboratory.”

See also

  • Trace theory, the general theory of traces.
  • Trace monoid and history monoid
  • Ease programming language
  • XC programming language
  • VerilogCSP is a set of macros added to Verilog HDL to support communicating sequential processes channel communications.
  • Joyce is a programming language based on the principles of CSP, developed by Brinch Hansen around 1989.
  • SuperPascal is a programming language also developed by Brinch Hansen, influenced by CSP and his earlier work with Joyce.
  • Ada implements features of CSP such as the rendezvous.
  • DirectShow is the video framework inside DirectX, it uses the CSP concepts to implement the audio and video filters.
  • OpenComRTOS is a formally developed network-centric distributed RTOS based on a pragmatic superset of CSP.
  • Input/output automaton
  • Parallel programming model
  • TLA<sup>+</sup> is another formal language for modelling and verifying concurrent systems.

References

Further reading

  • This book has been updated by Jim Davies at the Oxford University Computing Laboratory and the new edition is available for download as a PDF file at the Using CSP website (link above).
  • Some links relating to this book are available here. The full text is available for download as a PS or PDF file from Bill Roscoe's list of academic publications.
  • The Annotation of CSP (Chinese version), non-profit translation and annotation work based on Prentice-Hall book (1985), Chaochen Zhou's Chinese version (1988), and Jim Davies's online version (2015).
  • WoTUG, a user group for CSP and occam-style systems, contains some information about CSP and useful links.
  • "CSP Citations" from CiteSeer