Incomputer science,communicating sequential processes (CSP) is aformal language for describingpatterns of interaction inconcurrent systems.^[1] It is a member of the family of mathematical theories of concurrency known as process algebras, orprocess calculi, based onmessage passing viachannels. CSP was highly influential in the design of theoccam programming language^[1][2] and also influenced the design of programming languages such asLimbo,^[3]RaftLib,Erlang,^[4]Go,^[5][3]Crystal, andClojure's core.async.^[6]

CSP was first described byTony Hoare in a 1978 article,^[7] and has since evolved substantially.^[8] CSP has been practically applied in industry as a tool forspecifying and verifying the concurrent aspects of a variety of different systems, such as the T9000Transputer,^[9] as well as a securee-commerce system.^[10] 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).^[11]

The version of CSP presented in Hoare's original 1978 article was essentially a concurrent programming language rather than aprocess calculus. It had a substantially differentsyntax than later versions of CSP, did not possess mathematically defined semantics,^[12] and was unable to representunbounded nondeterminism.^[13] 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 namedwest and sends that character to process namedeast. The parallel composition

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

assigns the nameswest to theDISASSEMBLE process,X to theCOPY process, andeast to theASSEMBLE process, and executes these three processes concurrently.^[7]

Following the publication of the original version of CSP, Hoare, Stephen Brookes, andA. W. Roscoe developed and refined thetheory of CSP into its modern, process algebraic form. The approach taken in developing CSP into a process algebra was influenced byRobin Milner's work on theCalculus of Communicating Systems (CCS) and conversely. The theoretical version of CSP was initially presented in a 1984 article by Brookes, Hoare, and Roscoe,^[14] and later in Hoare's bookCommunicating Sequential Processes,^[12] which was published in 1985. In September 2006, that book was still thethird-most citedcomputer science reference of all time according toCiteseer^{[citation needed]} (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'sThe Theory and Practice of Concurrency^[1] describes this newer version of CSP.

An early and important application of CSP was its use for specification and verification of elements of the INMOS T9000Transputer, 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.^[9]

Industrial application of CSP to software design has usually focused on dependable and safety-critical systems. For example, the Bremen Institute for Safe Systems andDaimler-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 ofdeadlock andlivelock.^[15][16] 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.^[10]

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 theFDR refinement-checker to discover a previously unknown attack on theNeedham–Schroeder public-key authentication protocol, and then to develop a corrected protocol able to defeat the attack.^[17]

As its name suggests, CSP allows the description of systems in terms of component processes that operate independently, and interact with each other solely throughmessage-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 variousprocess algebraic operators. Using this algebraic approach, quite complex process descriptions can be easily constructed from a few primitive elements.

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 eventmust be communicated. Events may be atomic names (e.g.on,off), compound names (e.g.valve.open,valve.close), or input/output events (e.g.mouse?xy,screen!bitmap). The set of all events is denoted${\displaystyle \mathrm{\Sigma }}$.^[18]

Primitive processes

Primitive processes represent fundamental behaviors: examples include${\displaystyle \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}}$ (the process that immediately deadlocks), and${\displaystyle \mathrm{S}\mathrm{K}\mathrm{I}\mathrm{P}}$ (the process that immediately terminates successfully).^[18]

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,${\displaystyle a\to P}$ is the process that is willing to communicate event${\displaystyle a}$ with its environment and, after${\displaystyle a}$, behaves like the process${\displaystyle P}$.^[18]

Recursion

Processes can be defined using recursion. Where${\displaystyle F(P)}$ is any CSP term involving${\displaystyle P}$, the process${\displaystyle \mu P.F(P)}$ defines a recursive process given by the equation${\displaystyle P=F(P)}$.Recursions can also be defined mutually, such aswhich defines a pair of mutually recursive processes that alternate between communicating${\displaystyle up}$ and${\displaystyle down}$.^[18]

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,${\displaystyle (a\to P)◻(b\to Q)}$ is the process that is willing to communicate the initial events${\displaystyle a}$ and${\displaystyle b}$ and subsequently behaves as either${\displaystyle P}$ or${\displaystyle Q}$, depending on which initial event the environment chooses to communicate.^[18]

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,${\displaystyle (a\to P)\sqcap (b\to Q)}$ can behave like either${\displaystyle a\to P}$ or${\displaystyle b\to Q}$. It can refuse to accept${\displaystyle a}$ or${\displaystyle b}$ and is only obliged to communicate if the environment offers both${\displaystyle a}$ and${\displaystyle b}$.

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,$${\displaystyle (a\to a\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P})◻(a\to b\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P})}$$ and$${\displaystyle a\to ((a\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P})\sqcap (b\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}))}$$are equivalent.^[18]

Interleaving

The interleaving operator represents completely independent concurrent activity. The process${\displaystyle P|||Q}$ behaves as both${\displaystyle P}$ and${\displaystyle Q}$ simultaneously. The events from both processes are arbitrarily interleaved in time. Interleaving can introduce nondeterminism even if${\displaystyle P}$ and${\displaystyle Q}$ are both deterministic: if${\displaystyle P}$ and${\displaystyle Q}$ can both communicate the same event, then${\displaystyle P|||Q}$ nondeterministically chooses which of the two processes communicated that event.^[18]

Interface parallel

The interface parallel (or generalized parallel) operator represents concurrent activity that requires synchronization between the component processes: for${\displaystyle P|[X]|Q}$, any event in the interface set${\displaystyle X\subseteq \mathrm{\Sigma }}$ can only occur when both${\displaystyle P}$ and${\displaystyle Q}$ are able to engage in that event.^[18]

For example, the process${\displaystyle P|[\{a\}]|Q}$ requires that${\displaystyle P}$ and${\displaystyle Q}$ must both be able to perform event${\displaystyle a}$ before that event can occur. So, the process${\displaystyle (a\to P)|[\{a\}]|(a\to Q)}$ is equivalent to${\displaystyle a\to (P|[\{a\}]|Q)}$, while${\displaystyle (a\to P)|[\{a,b\}]|(b\to Q)}$ is equivalent to${\displaystyle \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}}$ (i.e. the process deadlocks).

Hiding

The hiding operator provides a way to abstract processes by making some events unobservable by the environment.${\displaystyle P\setminus X}$ is the process${\displaystyle P}$ with the event set${\displaystyle X}$ hidden.

A trivial example of hiding is${\displaystyle (a\to P)\setminus \{a\}}$ which, assuming that the event${\displaystyle a}$ doesn't appear in${\displaystyle P}$, simply reduces to${\displaystyle P}$. Hidden events are internalized asτ actions, which are invisible to and uncontrollable by the environment. The existence of hiding introduces an additional behaviour calleddivergence, where an infinite sequence of τ actions is performed. This is captured by the process${\displaystyle \mathbf{d}\mathbf{i}\mathbf{v}}$, whose behaviour is solely to perform τ actions forever.^[18] For example,${\displaystyle (\mu P.a\to P)\setminus \{a\}}$ is equivalent to${\displaystyle \mathbf{d}\mathbf{i}\mathbf{v}}$.

This sectiondoes notcite anysources. Please helpimprove this section byadding citations to reliable sources. Unsourced material may be challenged andremoved.(November 2024) (Learn how and when to remove this message)

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 (only in cash) before offering a chocolate can be written as:

$${\displaystyle \mathrm{V}\mathrm{e}\mathrm{n}\mathrm{d}\mathrm{i}\mathrm{n}\mathrm{g}\mathrm{M}\mathrm{a}\mathrm{c}\mathrm{h}\mathrm{i}\mathrm{n}\mathrm{e}=\mathrm{c}\mathrm{o}\mathrm{i}\mathrm{n}\to \mathrm{c}\mathrm{h}\mathrm{o}\mathrm{c}\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}}$$

A person who might choose to use a coin or card to make payments could be modelled as:

$${\displaystyle \mathrm{P}\mathrm{e}\mathrm{r}\mathrm{s}\mathrm{o}\mathrm{n}=(\mathrm{c}\mathrm{o}\mathrm{i}\mathrm{n}\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P})◻(\mathrm{c}\mathrm{a}\mathrm{r}\mathrm{d}\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P})}$$

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,

$${\displaystyle \mathrm{V}\mathrm{e}\mathrm{n}\mathrm{d}\mathrm{i}\mathrm{n}\mathrm{g}\mathrm{M}\mathrm{a}\mathrm{c}\mathrm{h}\mathrm{i}\mathrm{n}\mathrm{e}\left|\left[\left\{\mathrm{c}\mathrm{o}\mathrm{i}\mathrm{n},\mathrm{c}\mathrm{a}\mathrm{r}\mathrm{d}\right\}\right]\right|\mathrm{P}\mathrm{e}\mathrm{r}\mathrm{s}\mathrm{o}\mathrm{n}\equiv \mathrm{c}\mathrm{o}\mathrm{i}\mathrm{n}\to \mathrm{c}\mathrm{h}\mathrm{o}\mathrm{c}\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}}$$

whereas if synchronization was only required on “coin”, we would obtain

$${\displaystyle \mathrm{V}\mathrm{e}\mathrm{n}\mathrm{d}\mathrm{i}\mathrm{n}\mathrm{g}\mathrm{M}\mathrm{a}\mathrm{c}\mathrm{h}\mathrm{i}\mathrm{n}\mathrm{e}\left|\left[\left\{\mathrm{c}\mathrm{o}\mathrm{i}\mathrm{n}\right\}\right]\right|\mathrm{P}\mathrm{e}\mathrm{r}\mathrm{s}\mathrm{o}\mathrm{n}\equiv \left(\mathrm{c}\mathrm{o}\mathrm{i}\mathrm{n}\to \mathrm{c}\mathrm{h}\mathrm{o}\mathrm{c}\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)◻\left(\mathrm{c}\mathrm{a}\mathrm{r}\mathrm{d}\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)}$$

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

$${\displaystyle \left(\left(\mathrm{c}\mathrm{o}\mathrm{i}\mathrm{n}\to \mathrm{c}\mathrm{h}\mathrm{o}\mathrm{c}\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)◻\left(\mathrm{c}\mathrm{a}\mathrm{r}\mathrm{d}\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)\right)\setminus \left\{\mathrm{c}\mathrm{o}\mathrm{i}\mathrm{n},\mathrm{c}\mathrm{a}\mathrm{r}\mathrm{d}\right\}}$$

we get the nondeterministic process

$${\displaystyle \left(\mathrm{c}\mathrm{h}\mathrm{o}\mathrm{c}\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)\sqcap \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}}$$

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 (e.g., someone who does not see the decision reached by the person),nondeterminism has been introduced.

This sectiondoes notcite anysources. Please helpimprove this section byadding citations to reliable sources. Unsourced material may be challenged andremoved.(November 2024) (Learn how and when to remove this message)

The syntax of CSP defines the “legal” ways in which processes and events may be combined. Lete be an event,b be a boolean andX be a set of events. Then the basicsyntax of CSP can be defined as:

Note that, in the interests of brevity, the syntax presented above omits the${\displaystyle \mathbf{d}\mathbf{i}\mathbf{v}}$ process, which representsdivergence, as well as various operators such as alphabetized parallel, piping, and indexed choices.

This sectionneeds expansion. You can help byadding to it.(June 2008)

CSP has been imbued with several differentformal semantics, which define themeaning of syntactically correct CSP expressions. The theory of CSP includes mutually consistentdenotational semantics,algebraic semantics, andoperational semantics.

The three major denotational models of CSP are thetraces model, thestable failures model, and thefailures/divergences model. Semantic mappings from process expressions to each of these three models provide the denotational semantics for CSP.^[1]

Denotational semantics allows several definitions of apartial order ofrefinement on processes, which in turn can be used to elegantly represent several properties on processes. Generally,${\displaystyle P⊑Q}$ denotes${\displaystyle Q}$refines${\displaystyle P}$.

Thetraces model defines the meaning of a process expression as the set of sequences of events (traces) that the process can be observed to perform. For example,

• ${\displaystyle \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}\left(\mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)=\left\{⟨⟩\right\}}$ since${\displaystyle \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}}$ performs no events
• ${\displaystyle \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}\left(a\to b\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)=\left\{⟨⟩,⟨a⟩,⟨a,b⟩\right\}}$ since the process${\displaystyle (a\to b\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P})}$ can be observed to have performed no events, the eventa, or the sequence of eventsa followed byb

More formally, the traces model${\displaystyle \mathcal{T}}$ is defined as the set of non-empty prefix-closed subsets of${\displaystyle {\mathrm{\Sigma }}^{\ast }}$. The meaning of a processP in the traces model is defined as${\displaystyle \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}\left(P\right)\subseteq {\mathrm{\Sigma }}^{\ast }}$ such that:

1. ${\displaystyle ⟨⟩\in \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}\left(P\right)}$ (i.e.${\displaystyle \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}\left(P\right)}$ contains the empty sequence)
2. ${\displaystyle s_1⌢s_2\in \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}\left(P\right)⟹s_1\in \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}\left(P\right)}$ (i.e.${\displaystyle \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}\left(P\right)}$ is prefix-closed)

where${\displaystyle {\mathrm{\Sigma }}^{\ast }}$ is the set of all possible finite sequences of events.

A process${\displaystyle P}$ is said totrace-refine another${\displaystyle Q}$ if and only if${\displaystyle \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}(P)\supseteq \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}(Q)}$.${\displaystyle P}$trace-refines${\displaystyle Q}$ is denoted${\displaystyle Q{⊑}_{\mathrm{T}}P}$.^[18]

Thestable failures model${\displaystyle \mathcal{F}}$ extends the traces model with refusal sets, which are sets of events${\displaystyle X\subseteq \mathrm{\Sigma }}$ that a process can refuse to perform. Afailure is a pair${\displaystyle \left(s,X\right)}$, consisting of a traces, and a refusal setX which identifies the events that a process may refuse once it has executed the traces. The observed behavior of a process in the stable failures model is described by the pair${\displaystyle \left(\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}\left(P\right),\mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}\left(P\right)\right)}$. For example,

$${\displaystyle \mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}\left(\left(a\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)◻\left(b\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)\right)=\left\{\left(⟨⟩,\mathrm{\varnothing }\right),\left(⟨a⟩,\left\{a,b\right\}\right),\left(⟨b⟩,\left\{a,b\right\}\right)\right\}}$$$${\displaystyle \mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}\left(\left(a\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)\sqcap \left(b\to \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}\right)\right)=\left\{\left(⟨⟩,\left\{a\right\}\right),\left(⟨⟩,\left\{b\right\}\right),\left(⟨a⟩,\left\{a,b\right\}\right),\left(⟨b⟩,\left\{a,b\right\}\right)\right\}}$$

A process${\displaystyle P}$stable-failures-refines${\displaystyle Q}$ if and only if${\displaystyle \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}(P)\supseteq \mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}\mathrm{s}(Q)\wedge \mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}(P)\supseteq \mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}(Q)}$.${\displaystyle P}$stable-failures-refines${\displaystyle Q}$ is denoted${\displaystyle Q{⊑}_{\mathrm{F}}P}$.^[18]

Thefailures/divergence model${\displaystyle \mathcal{N}}$ further extends the failures model to handledivergence. The semantics of a process in the failures/divergences model is a pair${\displaystyle \left({\mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}}_{\perp }\left(P\right),\mathrm{d}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}\mathrm{s}\left(P\right)\right)}$ where${\displaystyle \mathrm{d}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}\mathrm{s}\left(P\right)}$ is defined as the extension-closure of the set of all traces after which the process can immediately diverge, and${\displaystyle {\mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}}_{\perp }\left(P\right)=\mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}\left(P\right)\cup \left\{\left(s,X\right)\mid s\in \mathrm{d}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}\mathrm{s}\left(P\right),X\subseteq {\mathrm{\Sigma }}^{\ast }\right\}}$, which is the extension of${\displaystyle \mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}(P)}$ with all divergent traces.

A process${\displaystyle P}$failures-divergences-refines${\displaystyle Q}$ if and only if${\displaystyle {\mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}}_{\mathrm{\perp }}(P)\supseteq {\mathrm{f}\mathrm{a}\mathrm{i}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{e}\mathrm{s}}_{\mathrm{\perp }}(Q)\wedge \mathrm{d}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}\mathrm{s}(P)\supseteq \mathrm{d}\mathrm{i}\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{g}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}\mathrm{s}(Q)}$.${\displaystyle P}$failures-divergences refines${\displaystyle Q}$ is denoted${\displaystyle Q{⊑}_{\mathrm{F}\mathrm{D}}P}$.^[18]

One of the most important principles in CSP is theunique fixed points (UFP) rule. Generally, it states that a process which satisfies certain nice properties has a single semantic interpretation. It can be used to conclude algebraic proofs that two processes are equal in a model of CSP. A version for single recursions in the traces model is outlined here.

Consider processes as their trace sets. The operator${\displaystyle \downarrow }$ is defined for all processes${\displaystyle P}$, all${\displaystyle n\in \mathbb{N}}$ so that${\displaystyle P\downarrow n=\{s\in P:\mathrm{\#}s\le n\}}$, where${\displaystyle \mathrm{\#}s}$ denotes the length of string${\displaystyle s}$: the set of traces in${\displaystyle P}$ of length at most${\displaystyle n}$. This allows ametric to be defined on${\displaystyle \mathcal{T}}$. For each${\displaystyle P}$,${\displaystyle Q}$, let${\displaystyle d(P,Q)=\mathrm{i}\mathrm{n}\mathrm{f}\{2^{-n}:P\downarrow n=Q\downarrow n\}}$. Informally, a process which agrees on traces with another up to some length is ‘more distant’ from it than one which agrees with it up to a greater length. It can be shown that this forms acomplete metric space.

A function on trace sets${\displaystyle F:\mathcal{T}\to \mathcal{T}}$ is calledconstructive if and only if for all processes${\displaystyle P}$,${\displaystyle Q}$, all${\displaystyle n\in \mathbb{N}}$, if${\displaystyle P\downarrow n=Q\downarrow n}$ then${\displaystyle F(P)\downarrow (n+1)=F(Q)\downarrow (n+1)}$. This means that a function is constructive if and only if it is acontraction mapping with respect to the metric on trace sets.

By theBanach fixed-point theorem, if${\displaystyle F}$ is a constructive function, it has a uniquefixed point. This means that if${\displaystyle X}$ and${\displaystyle Y}$ are processes defined recursively as${\displaystyle X=F(X)}$ and${\displaystyle Y=F(Y)}$, then they are equivalent in the traces model. UFP can also be extended to mutual recursions (by using vectors of processes) and other models of CSP (e.g. in${\displaystyle \mathcal{F}}$ by defining the metric as in${\displaystyle \mathcal{T}}$, with respect to the trace parts of a process's trace-failure pair).

It can be derived using UFP (andTarski's fixed point theorem), that formonotonic${\displaystyle F}$, a recursive term defined as${\displaystyle X=F(X)}$ has the semantic interpretation${\displaystyle {\sqcap }_{n=0}^{\mathrm{\infty }}{F}^n(\mathrm{\perp })}$, where${\displaystyle \mathrm{\perp }}$ is the least element of the model. In the traces, stable failures and failures/divergences models,${\displaystyle \mathrm{\perp }=\mathbf{d}\mathbf{i}\mathbf{v}}$ (equivalent to${\displaystyle \mathrm{S}\mathrm{T}\mathrm{O}\mathrm{P}}$ in the traces model).^[1][18]

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 CSP_M.^[19] The CSP_M dialect of CSP possesses a formally definedoperational semantics, which includes an embeddedfunctional programming language.

The most well-known CSP tool is probablyFailures-Divergences Refinement, which is a commercial product originally developed by Formal Systems (Europe) Ltd. FDR is often described as amodel checker, but is technically arefinement checker, in that it converts two CSP process expressions intolabelled 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).^[20] 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.^[21]

TheAdelaide Refinement Checker (ARC)^[22] is a CSP refinement checker developed by the Formal Modelling and Verification Group atThe University of Adelaide. ARC differs from FDR2 in that it internally represents CSP processes as orderedbinary 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.

TheProB project,^[23] 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 theB method. However, it also includes support for analysis of CSP processes both through refinement checking, andLTL model-checking. ProB can also be used to verify properties of combined CSP and B specifications. A ProBE CSP Animator is integrated in FDR3.

TheProcess Analysis Toolkit (PAT)^[24][25] is a CSP analysis tool developed in the School of Computing at theNational 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 asdeadline andwaituntil. 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 convenientsyntactic sugar for well-known process modelling patterns used in standard CSP. The PAT syntax is similar, but not identical, to CSP_M.^[26] The principal differences between the PAT syntax and standard CSP_M 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^[27] produces animated visualisations of CSP systems from specifications, and supports timed CSP.

CSPsim^[28] 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 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.

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 andObject Z
• Circus, an integration of CSP andZ based on theUnifying Theories of Programming
• CMLArchived 2020-02-19 at theWayback Machine (COMPASS Modelling Language), a combination ofCircus andVDM developed for the modelling ofSystems of Systems (SoS)
• CspCASL, an extension ofCASL that integrates CSP
• LOTOS, an international standard^[29] that incorporates features of CSP andCCS.
• PALPS, a probabilistic extension with locations for ecological models developed by Anna Philippou and Mauricio Toro Bermúdez

This sectiondoes notcite anysources. Please helpimprove this section byadding citations to reliable sources. Unsourced material may be challenged andremoved.(November 2024) (Learn how and when to remove this message)

In as much as it is concerned with concurrent processes that exchange messages, theactor 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 receiving 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.

In 1990, “AQueen’s Award for Technological Achievement [was] conferred ... on[Oxford University] Computing Laboratory. The award recognises a successful collaboration between the laboratory andInmos Ltd. … Inmos’ flagship product is the ‘transputer’, amicroprocessor with many of the parts that would normally be needed in addition built into the same singlecomponent.”^[30] According to Tony Hoare,^[31]“The INMOS Transputer was as 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 theCSP ideas were ripe for industrial exploitation, and he made that the basis of the language for programming Transputers, which was calledOccam. … 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.”

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

• Hoare, C. A. R. (2004) [1985].Communicating Sequential Processes. Prentice Hall International.ISBN 978-0-13-153271-7.
  • This book has been updated byJim Davies at theOxford University Computing Laboratory and the new edition is available for download as a PDF file at theUsing CSP website.
• Roscoe, A. W. (1997).The Theory and Practice of Concurrency.Prentice Hall.ISBN 978-0-13-674409-2.
  • Some links relating to this book are availablehere. The full text is available for download as aPS orPDF file from Bill Roscoe'slist of academic publications.

• A PDF version of Hoare's CSP book – copyright restriction apply, see the page text before downloading.
• 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" fromCiteSeer

• Computer-related introductions in 1978
• 1978 in computing
• Process calculi
• Concurrent computing

• Articles with short description
• Short description is different from Wikidata
• All articles with unsourced statements
• Articles with unsourced statements from November 2018
• Articles needing additional references from November 2024
• All articles needing additional references
• Articles to be expanded from June 2008
• All articles to be expanded
• Webarchive template wayback links