CSP

CSP, short for Communicating Sequential Processes, is two things that share a name. In 1978 it was a small programming language, proposed by Tony Hoare in a twelve-page paper, in which independent processes share no variables and cooperate only by sending each other messages. By 1985 it had become a mathematical theory, a process algebra, for describing how concurrent systems interact and for proving that they behave correctly. The first CSP gave programming languages the idea that ! and ? on a synchronous channel can replace locks and shared memory. That idea reached occam and the transputer within five years and Go three decades later. The second CSP gave engineers a notation and a tool, FDR, that can check a design for deadlock before any code exists.

CSP is not something you download and run. There is no CSP compiler in the usual sense and no single implementation. What exists is the notation, the theory behind it, a machine-readable dialect called CSP_M, and the programming languages that borrowed its model.

History & Origins

The 1978 paper

“Communicating Sequential Processes” appeared in Communications of the ACM in August 1978 (volume 21, number 8, pages 666–677). The paper records that it was received in March 1977 and revised in August 1977. Its title page gives Hoare’s affiliation as the Queen’s University of Belfast and his present address as the Programming Research Group in Oxford. He made that move in 1977, to succeed Christopher Strachey.

The paper’s claim fits in its abstract: “input and output are basic primitives of programming and … parallel composition of communicating sequential processes is a fundamental program structuring method.” Hoare observed that assignment was well understood but that input and output “are often added to a programming language only as an afterthought”. He also noted that languages had collected a long list of structuring devices, including subroutines, coroutines, classes, monitors and actors, with little agreement on which were fundamental. His proposal was that a few primitives could express all of them.

Those primitives were:

• a parallel command that runs a fixed set of named processes concurrently, with no shared variables;
• input and output commands, source?variable and destination!expression, which happen only when both processes are ready, so that communication is also synchronization;
• Dijkstra’s guarded commands, extended so that an input command can appear in a guard and a process can wait for whichever of several messages arrives first.

Hoare credits “the technical inspiration” to Edsger Dijkstra, and thanks IFIP Working Group 2.3 as the forum where the ideas were discussed.

A language shown by example

Most of the paper is worked examples. They cover coroutines (copying and reformatting a stream of punched cards, including Conway’s problem), subroutines and data representations (division, factorial, a small set of integers), monitors and scheduling (a bounded buffer, a semaphore, the dining philosophers), and two arrays of processes: a sieve of Eratosthenes that prints the primes below 10,000 using a pipeline, and a matrix multiplier that the paper calls an “iterative array”.

The simplest example copies characters from one process to another:

1

X :: *[c:character; west?c → east!c]

*[ … ] repeats its body. The guard west?c inputs a character from the process named west, and east!c outputs it to the process named east. When west terminates, the input fails and the loop ends. Three such processes are joined by the parallel command:

1

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

A subroutine is just a process that waits for its arguments and sends back its results. This is the paper’s division routine:

1
2
3
4
5
6
7

[DIV :: *[x,y:integer; X?(x,y) →
          quot,rem:integer; quot := 0; rem := x;
          *[rem ≥ y → rem := rem − y; quot := quot + 1];
          X!(quot,rem)
        ]
|| X :: USER
]

What the paper left open

Hoare called the proposal partial and gave a whole section to its doubts. He chose explicit process names over named ports, which he called “an attractive alternative”. He rejected automatic buffering of messages. He asked whether an implementation should be required to be fair and answered “I am fairly sure that the answer is NO”. He considered allowing output commands in guards and left them out. The paper ends by warning that these primitives should not “wholly replace the other concepts in a programming language”.

The 1978 language also had no formal semantics. Hoare’s later book says so directly: “The early design of Communicating Sequential Processes had no mathematical semantics, and it left open a number of important design questions.”

From Language to Algebra

Answering those questions took the next seven years at Oxford. Hoare worked with Stephen Brookes and Bill Roscoe (whose 1982 doctoral thesis was titled A Mathematical Theory of Communicating Processes). Their paper “A Theory of Communicating Sequential Processes” appeared in the Journal of the ACM in 1984. Hoare’s book Communicating Sequential Processes followed from Prentice Hall International in 1985, with a foreword by Dijkstra.

The book is a different CSP. Hoare describes the 1978 paper as “an early version of the design propounded in this book” and names two significant changes. First, communication moved from named processes to named channels. Second, the notation got a mathematical model, in which a process is defined by what an observer could see it do. With that model in place, the open questions from 1978 (nested parallelism, recursion that spawns parallel copies, output guards) could all be answered “yes”.

The book openly acknowledges Robin Milner, whose Calculus of Communicating Systems (CCS) was published in 1980. Hoare writes of Milner’s “original insights, his personal friendship and his professional rivalry” as “a constant source of inspiration”. CSP and CCS grew up together and influenced each other. The main difference is that CCS compares processes by bisimulation, while CSP compares them by what they can be observed to do and refuse.

Design Philosophy

A few convictions run through both versions of CSP:

• Communication is a primitive. Input and output belong beside assignment as basic operations, not in a library.
• No shared state. Processes interact only by communicating. Anything that looks like shared data is a process that other processes talk to.
• Synchronous by default. A message passes only when sender and receiver are both ready. Hoare argued in 1978 and again in 1985 that buffering should not be built in, because a buffer is easy to write as a process when one is wanted.
• Few concepts, short notation. Hoare defended ! and ? on the grounds that mathematics uses brief symbols for common ideas. He also confessed “a distaste for the pronunciation of words like fi, od, or esac”.
• Laws before implementation. In the algebraic CSP, operators are chosen so that they obey simple laws, and those laws are what make proofs possible.

Key Features

Processes and events

In the 1985 notation, a process is described by the events it is willing to engage in. Hoare’s running example is a vending machine. The simple one takes a coin and gives a chocolate, forever:

1

VMS = (coin → (choc → VMS))

A machine that offers a choice after each coin uses the choice bar and the recursion operator μ:

1

VMCT = μ X • coin → (choc → X | toffee → X)

The operators

Two primitive processes anchor the algebra: STOP, which does nothing and so represents deadlock, and SKIP, which terminates successfully. Channel input and output survive from 1978 as c?x and c!v.

Traces, failures and divergences

The meaning of a process is given by sets of observations, in three levels of detail:

• Traces: the finite sequences of events the process can perform. Traces capture safety (nothing bad happens).
• Failures: pairs of a trace and a set of events the process may refuse after that trace. Failures capture deadlock and nondeterminism, which traces alone cannot see.
• Divergences: traces after which the process may do internal work forever. Divergences capture livelock.

Refinement

A process Q refines a process P if every behaviour of Q is also a behaviour of P in the chosen model. Refinement is how CSP states requirements. The specification is itself a process, usually a simple and obviously correct one, and the design is correct if it refines the specification. Deadlock freedom, livelock freedom and determinism can all be expressed this way.

Tools: FDR and CSP_M

Refinement between finite-state processes can be checked mechanically. The best-known tool is FDR (Failures-Divergences Refinement). According to its manual, the original FDR was written in 1991 by Formal Systems (Europe) Ltd, a company Roscoe co-founded, and a completely revised FDR2 followed in the mid-1990s. The University of Oxford released FDR2 versions from 2.90 in 2008–12, then FDR3 in 2013 and FDR4 in October 2016. FDR3 was a complete rewrite of FDR2, and the manual lists what the new line added: multi-core refinement checking, an integrated type checker and a redesigned debugger. FDR4 continues it. FDR 4.2.7, dated 11 May 2020, is the current release on the FDR site, which is now hosted by Cocotec. FDR is proprietary, with free licences for academic teaching and research, although its CSP_M front end has been open-sourced.

FDR reads CSP_M, the machine-readable dialect defined in Bryan Scattergood’s 1998 Oxford thesis. CSP_M combines the CSP operators with a small functional language. The vending machines above look like this in CSP_M, with two assertions for the checker:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

channel coin, choc, toffee

VMS  = coin -> choc -> VMS
VMCT = coin -> (choc -> VMCT [] toffee -> VMCT)

-- every trace of VMS is also a trace of VMCT
assert VMCT [T= VMS

-- VMS can never reach a state where it refuses everything
assert VMS :[deadlock free [F]]

Other tools work on CSP as well. The University of Adelaide built ARC, a refinement checker based on binary decision diagrams. ProB, from Heinrich-Heine-Universität Düsseldorf, was written for the B method and also animates and checks CSP_M. PAT, the Process Analysis Toolkit from the National University of Singapore, checks a CSP-based language extended with shared variables.

Evolution

Variants and extensions

• Timed CSP began with Reed and Roscoe’s “A timed model for communicating sequential processes” (1986; journal version 1988) and adds real time to the theory.
• Circus combines CSP with the Z notation, and CSP‖B and related work combine it with the B method.
• LOTOS, the ISO specification language standardized as ISO 8807, incorporates features of both CSP and CCS.
• Roscoe’s two textbooks, The Theory and Practice of Concurrency (1997) and Understanding Concurrent Systems (2010), document the version of CSP that the tools actually implement. It differs in small ways from the 1985 book.

CSP in programming languages

The 1978 paper was a language proposal, and language designers took it up quickly.

occam (Inmos, 1983) is the most direct descendant. Hoare’s 1985 book says it “very closely follows the principles expounded in this book” and shows how SEQ, PAR and ALT correspond to CSP’s sequential composition, parallel composition and choice.

Joyce, designed by Per Brinch Hansen and published in 1987, is a Pascal subset extended with CSP-style channels, ? and !.

The Bell Labs line is traced in Russ Cox’s essay “Bell Labs and CSP Threads”. In 1980 Gerard Holzmann and Rob Pike wrote a protocol analyser, pan, whose input language was a CSP dialect; Cox notes that it developed into the Spin model checker and Promela. Luca Cardelli and Pike’s Squeak (1985) and Pike’s Newsqueak applied CSP to user-interface programming. Newsqueak made channels first-class values, which the original CSP did not allow, so they could be stored, passed and sent over other channels. That idea passed through Alef and Limbo to Go. The Go FAQ says its concurrency primitives “derive from a different part of the family tree whose main contribution is the powerful notion of channels as first class objects”.

A Go program in this style reads like the 1978 COPY example with named channels:

1
2
3
4
5
6

func copyChars(west <-chan rune, east chan<- rune) {
	for c := range west {
		east <- c
	}
	close(east)
}

Erlang is sometimes listed as a CSP language, and the Go FAQ describes it as stemming from CSP. The connection is looser than that suggests. Erlang’s own FAQ says only that “! as the send-message operator comes from CSP”. Its asynchronous mailboxes and named processes are closer to the actor model.

Libraries carry the model into languages that lack it. JCSP for Java and C++CSP came out of the occam community, and Clojure’s core.async, announced in June 2013, provides CSP-style channels as a library.

CSP versus actors

The comparison comes up often. In CSP, processes are anonymous and channels have names. Communication is a synchronous rendezvous. In the actor model, actors have identities, messages are sent to an actor instead of a channel, and sending is asynchronous. Each can simulate the other, which is why the two are often described as duals. The 1978 paper sits partly on the actor side of that line, since its processes were named and it had no channels. Named channels arrived with the 1985 theory.

Industrial Use

CSP’s industrial record is concentrated in hardware, protocols and safety-critical software.

• Inmos. Beyond basing occam on CSP, Inmos used CSP and FDR to verify the T9000 transputer’s Virtual Channel Processor, as reported by Barrett in 1995. Earlier, in 1990, Oxford University Computing Laboratory and Inmos shared a Queen’s Award for Technological Achievement for their collaboration on the transputer. In a 2009 interview in Communications of the ACM, Hoare recalled that Inmos estimated the work let it deliver the hardware a year sooner. That is the company’s own estimate as Hoare remembered it nearly two decades later, not a measured comparison, and the page has not traced it to an Inmos document.
• Security protocols. Lowe’s attack on the Needham–Schroeder public-key protocol, published in Information Processing Letters in November 1995, was found by modelling the protocol and an intruder as CSP processes. His 1996 TACAS paper showed FDR finding the attack automatically and checking the fix. The protocol had been in the literature since 1978.
• Space systems. Buth, Kouvaras, Peleska and Shi’s “Deadlock analysis for a fault-tolerant system” (AMAST ‘97) and Buth, Peleska and Shi’s “Combining methods for the livelock analysis of a fault-tolerant system” (AMAST ‘98, a conference held in January 1999) describe CSP models of a fault-tolerant system intended for the International Space Station.
• Secure systems. Hall and Chapman’s 2002 IEEE Software article “Correctness by construction: developing a commercial secure system” describes Praxis using CSP for the concurrency design of a certification authority.

Hoare was candid about the limits of this record. In a paper published in 1996 he wrote that researchers into formal methods, “and I was the most mistaken among them”, had predicted that the programming world would embrace formalisation far more readily than it did.

Current Relevance

The encyclopedia lists CSP as Historical, and for the 1978 language that is accurate. Nobody writes programs in it, and it was superseded by its own descendants within a decade.

The algebra and its model are still in use. FDR is still distributed and still used in teaching and research, though its last release was in 2020. Hoare’s book has been freely available in an electronic edition, edited by Jim Davies at Oxford and carrying a 1985–2004 copyright notice, since about 2004. Every Go programmer who writes ch <- v is using a channel discipline that Hoare proposed in 1978. Tony Hoare died on 5 March 2026, aged 92.

Why It Matters

CSP changed how programmers think about concurrency in two ways.

The first is practical. Before CSP, concurrent programs were mostly built from shared memory guarded by semaphores, critical regions and monitors, the last of which Hoare himself had helped to define. CSP showed that processes which share nothing and communicate synchronously can express coroutines, subroutines, monitors and data abstractions with one mechanism. occam, Newsqueak, Limbo and Go each made that model usable in a real language.

The second is mathematical. The step from the 1978 language to the 1985 algebra made concurrency something that could be calculated with. Deadlock, livelock and nondeterminism became properties with exact definitions, and refinement gave a single relation for saying that one design correctly implements another. Much of the later work on verifying concurrent systems builds on that foundation.

Sources

• C. A. R. Hoare, “Communicating Sequential Processes”, Communications of the ACM 21(8), August 1978, pp. 666–677
• S. D. Brookes, C. A. R. Hoare and A. W. Roscoe, “A Theory of Communicating Sequential Processes”, Journal of the ACM 31(3), 1984, pp. 560–599
• C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall International, 1985; electronic edition edited by Jim Davies, usingcsp.com
• A. W. Roscoe, The Theory and Practice of Concurrency, Prentice Hall, 1997; Understanding Concurrent Systems, Springer, 2010
• G. Barrett, “Model checking in practice: the T9000 Virtual Channel Processor”, IEEE Transactions on Software Engineering 21(2), 1995
• G. Lowe, “An attack on the Needham-Schroeder public-key authentication protocol”, Information Processing Letters 56(3), November 1995; “Breaking and fixing the Needham-Schroeder public-key protocol using FDR”, TACAS 1996
• A. E. Abdallah, C. B. Jones and J. W. Sanders (eds.), Communicating Sequential Processes: The First 25 Years, LNCS 3525, Springer, 2005
• C. A. R. Hoare, “An interview with C.A.R. Hoare” (with Len Shustek), Communications of the ACM 52(3), March 2009, pp. 38–41, as quoted in Wikipedia’s CSP article
• B. Buth, M. Kouvaras, J. Peleska and H. Shi, “Deadlock analysis for a fault-tolerant system”, AMAST ‘97, LNCS 1349; B. Buth, J. Peleska and H. Shi, “Combining methods for the livelock analysis of a fault-tolerant system”, AMAST ‘98, LNCS 1548 (titles and authors checked; the papers themselves were not read)
• A. Hall and R. Chapman, “Correctness by construction: developing a commercial secure system”, IEEE Software 19(1), 2002, pp. 18–25
• FDR manual and release notes, cocotec.io/fdr
• Russ Cox, “Bell Labs and CSP Threads”, swtch.com/~rsc/thread/
• The Go FAQ, “Why build concurrency on the ideas of CSP?”; the Erlang FAQ, “Academic and Historical Questions”