Communicating sequential processes

CSPCommunicating Sequential Processes (CSP)channelcooperating sequential processes
In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems.wikipedia
140 Related Articles

Occam (programming language)

occamoccam programming languageoccam 2
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.
occam is a programming language which is concurrent and builds on the communicating sequential processes (CSP) process algebra, and shares many of its features.

Go (programming language)

GoGo programming languageGolang
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.
Go is syntactically similar to C, but with memory safety, garbage collection, structural typing, and CSP-style concurrency.

Tony Hoare

C. A. R. HoareC.A.R. HoareHoare
CSP was first described in a 1978 paper by Tony Hoare, but has since evolved substantially.
He also developed Hoare logic for verifying program correctness, and the formal language communicating sequential processes (CSP) to specify the interactions of concurrent processes (including the dining philosophers problem) and the inspiration for the occam programming language.

Channel (programming)

channelschannelcommunication channels
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.
Channels are fundamental to the process calculus approach to concurrency, and originated in communicating sequential processes (CSP), a formal model for concurrency, and has been used in many derived languages, such as occam, and Limbo programming language (via Newsqueak and the Alef programming language).

Limbo (programming language)

LimboDis virtual machineDis
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.
Limbo's approach to concurrency was inspired by Hoare's communicating sequential processes (CSP), as implemented and amended in Pike's earlier Newsqueak language and Winterbottom's Alef.

Concurrency (computer science)

concurrencyconcurrentconcurrently
In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems.

Process calculus

process calculiprocess algebracalculus
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.
Leading examples of process calculi include CSP, CCS, ACP, and LOTOS.

Clojure

Rich HickeyClojureScriptClojure programming language
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.
For parallel and concurrent programming Clojure provides software transactional memory, a reactive agent system, and channel-based concurrent programming.

Crystal (programming language)

Crystal
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.
Crystal's concurrency model is inspired by communicating sequential processes (CSP) and implements light-weight fibers and channels (for communicating between fibers) inspired by the language Go.

Calculus of communicating systems

CCSCCS-Calculus
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 vice versa.

Transputer

INMOS Transputer TRAM TRAnsputer Module
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.
Transputers were intended to be programmed using the programming language occam, based on the communicating sequential processes (CSP) process calculus.

Bill Roscoe

A. W. RoscoeRoscoe, A.W.
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.
Professor Roscoe works in the area of concurrency theory, in particular the semantic underpinning of Communicating Sequential Processes (CSP) and the associated occam programming language with Sir Tony Hoare.

FDR (software)

FDR2Failures-Divergence RefinementFDR
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. The most well-known CSP tool is probably Failures/Divergence Refinement 2 (FDR2), which is a commercial product developed by Formal Systems (Europe) 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 (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 (Failures-Divergences Refinement) and subsequently FDR2 are refinement checking software tools, designed to check formal models expressed in Communicating sequential processes (CSP).

Message passing

message-passingmessagesmessage
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.

Denotational semantics

denotationalfully abstractHistory of denotational semantics
The theory of CSP includes mutually consistent denotational semantics, algebraic semantics, and operational semantics.
Denotational semantics have been developed for modern programming languages that use capabilities like concurrency and exceptions, e.g., Concurrent ML, CSP, and Haskell.

Formal specification

specificationsoftware specificationspecifications
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.

Model checking

model checkermodel checkerssymbolic model checking
The most well-known CSP tool is probably Failures/Divergence Refinement 2 (FDR2), which is a commercial product developed by Formal Systems (Europe) 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 (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).

History monoid

Distribution (concurrency)
History monoids occur in the theory of concurrent computation, and provide a low-level mathematical foundation for process calculi, such as CSP the language of communicating sequential processes, or CCS, the calculus of communicating systems.

Divergence (computer science)

terminatingdivergencenon-termination
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.
In the calculus of communicating sequential processes, divergence is a drastic situation where a process performs an endless series of hidden actions.

Joyce (programming language)

Joyce
It is based on the sequential language Pascal and the principles of Communicating Sequential Processes (CSP).

Actor model

actorsactorActor programming
In as much as it is concerned with concurrent processes that exchange messages, the Actor model is broadly similar to CSP.
The original communicating sequential processes (CSP) model published by Tony Hoare differed from the actor model because it was based on the parallel composition of a fixed number of sequential processes connected in a fixed topology, and communicating using synchronous message-passing based on process names (see Actor model and process calculi history).

Parallel programming model

parallelParallel programmingprogramming model
The Communicating sequential processes (CSP) formalisation of message passing uses synchronous communication channels to connect processes, and led to important languages such as Occam, Limbo and Go.

VerilogCSP

In integrated circuit design, VerilogCSP is a set of macros added to Verilog HDL to support Communicating Sequential Processes (CSP) channel communications.

XC (programming language)

XCXC Programming Language
Occam was developed by David May and built on the Communicating Sequential Processes formalism, a process algebra developed by Tony Hoare.