Communicating sequential processes
Encyclopedia
In computer science
, Communicating Sequential Processes (CSP) is a formal language
for describing pattern
s of interaction
in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi
. CSP was highly influential in the design of the occam
programming language, and also influenced the design of programming languages such as Limbo and Go
.
CSP was first described in a 1978 paper by C. A. R. Hoare
, but 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 ecommerce 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).
. 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::DISASSEMBLE || X::COPY || east::ASSEMBLE]
assigns the names
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 vice versa. 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.
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 some 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.
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.
Events
Primitive processes:
Prefix
Deterministic Choice
Nondeterministic Choice
Interleaving
Interface Parallel
Hiding
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 was only required on “coin”, we would obtain
If we abstract this latter composite process by hiding the “coin” and “card” events, i.e.
we get the nondeterministic process
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.
be an event, 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.
, algebraic semantics
, and operational semantics
.
The traces 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,
More formally, the meaning of a process
in the traces model is defined as 
such that:
where
is the set of all possible finite sequences of events.
The stable failures model extends the traces model with refusal sets, which are sets of events
that a process can refuse to perform. A failure is a pair 
, consisting of a trace 
, and a refusal set 
which identifies the events that a process may refuse once it has executed the trace 
. The observed behavior of a process in the stable failures model is described by the pair 
. For example,
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, Communicating Sequential Processes (CSP) is a formal language
Specification language
A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis, requirements analysis and systems design.Specification...
for describing pattern
Pattern
A pattern, from the French patron, is a type of theme of recurring events or objects, sometimes referred to as elements of a set of objects.These elements repeat in a predictable manner...
s of interaction
Interaction
Interaction is a kind of action that occurs as two or more objects have an effect upon one another. The idea of a two-way effect is essential in the concept of interaction, as opposed to a one-way causal effect...
in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi
Process calculus
In computer science, the process calculi are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes...
. CSP was highly influential in the design of the occam
Occam (programming language)
occam is a concurrent programming language that builds on the Communicating Sequential Processes process algebra, and shares many of its features. It is named after William of Ockham of Occam's Razor fame....
programming language, and also influenced the design of programming languages such as Limbo and Go
Go (programming language)
Go is a compiled, garbage-collected, concurrent programming language developed by Google Inc.The initial design of Go was started in September 2007 by Robert Griesemer, Rob Pike, and Ken Thompson. Go was officially announced in November 2009. In May 2010, Rob Pike publicly stated that Go was being...
.
CSP was first described in a 1978 paper by C. A. R. Hoare
C. A. R. Hoare
Sir Charles Antony Richard Hoare , commonly known as Tony Hoare or C. A. R. Hoare, is a British computer scientist best known for the development of Quicksort, one of the world's most widely used sorting algorithms...
, but has since evolved substantially. CSP has been practically applied in industry as a tool for specifying and verifying
Formal specification
In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
the concurrent aspects of a variety of different systems, such as the T9000 Transputer, as well as a secure ecommerce 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
The version of CSP presented in Hoare's original 1978 paper was essentially a concurrent programming language rather than a process calculusProcess calculus
In computer science, the process calculi are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes...
. It had a substantially different syntax
Syntax
In linguistics, syntax is the study of the principles and rules for constructing phrases and sentences in natural languages....
than later versions of CSP, did not possess mathematically defined semantics, and was unable to represent unbounded nondeterminism
Unbounded nondeterminism
In computer science, unbounded nondeterminism or unbounded indeterminacy is a property of concurrency by which the amount of delay in servicing a request can become unbounded as a result of arbitration of contention for shared resources while still guaranteeing that the request will eventually be...
. 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 then 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.Following the publication of the original version of CSP, Hoare, Stephen Brookes, and A. W. Roscoe
Bill Roscoe
A. William "Bill" Roscoe is a Scottish computer scientist. He is Head of the Department of Computer Science, University of Oxford and a Professor of Computing Science...
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
Robin Milner
Arthur John Robin Gorell Milner FRS FRSE was a prominent British computer scientist.-Life, education and career:...
's work on the Calculus of Communicating Systems
Calculus of Communicating Systems
The Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...
(CCS), and vice versa. 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
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
reference of all time according to Citeseer
CiteSeer
CiteSeer was a public search engine and digital library for scientific and academic papers. It is often considered to be the first automated citation indexing system and was considered a predecessor of academic search tools such as Google Scholar and Microsoft Academic Search. It was replaced by...
(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 some 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
Praxis High Integrity Systems
Altran Praxis is a British software house that specialises in critical 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
Needham-Schroeder protocol
The term Needham–Schroeder protocol can refer to one of two communication protocols intended for use over an insecure network, both proposed by Roger Needham and Michael Schroeder. These are:...
, 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-passingMessage passing
Message passing in computer science is a form of communication used in parallel computing, object-oriented programming, and interprocess communication. In this model, processes or objects can send and receive messages to other processes...
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
- Events represent communications or interactions. They are assumed to be indivisible and instantaneous. They may be atomic names (e.g.
, 
), compound names (e.g. 
, 
), or input/output events (e.g. 
, 
).
Primitive processes:
- Primitive processes represent fundamental behaviors: examples include
(the process that communicates nothing, also called deadlockDeadlockA deadlock is a situation where in two or more competing actions are each waiting for the other to finish, and thus neither ever does. It is often seen in a paradox like the "chicken or the egg"...
), and
(which represents successful termination)
Algebraic operators
CSP has a wide range of algebraic operators. The principal ones are:Prefix
- The prefix operator combines an event and a process to produce a new process. For example,
- is the process which is willing to communicate
with its environment, and, after 
, behaves like the process 
.
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 which is willing to communicate the initial events
and 
, and subsequently behaves as either 
or 
depending on which initial event the environment chooses to communicate. If both 
and 
were communicated simultaneously the choice would be resolved nondeterministically.
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 a nominally deterministic choice if the initial events of both sides of the choice are identical. So, for example,
- is equivalent to
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.
Interface Parallel
- The interface parallel operator represents concurrent activity that requires synchronization between the component processes – any event in the interface set can only occur when all component processes 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, for example, the process
- can engage in event
, and become the process
- while
- will simply deadlock.
Hiding
- The hiding operator provides a way to abstract processes, by making some events unobservable. A trivial example of hiding is
- which, assuming that the event
doesn't appear in 
, simply reduces 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 which demands payment 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 was only required on “coin”, we would obtain
If we abstract this latter composite process by hiding the “coin” and “card” events, i.e.
we get the nondeterministic process
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
Nondeterministic algorithm
In computer science, a nondeterministic algorithm is an algorithm that can exhibit different behaviors on different runs, as opposed to a deterministic algorithm. There are several ways an algorithm may behave differently from run to run. A concurrent algorithm can perform differently on different...
has been introduced.
Syntax
The syntax of CSP defines the “legal” ways in which processes and events may be combined. Let be an event, and be a set of events. Then the basic syntaxSyntax
In linguistics, syntax is the study of the principles and rules for constructing phrases and sentences in natural languages....
of CSP can be defined as:
Note that, in the interests of brevity, the syntax presented above omits the
process, which represents divergenceDivergence (computer science)
In computer science, a computation is said to diverge if it does not terminate or terminates in an exceptional state. Otherwise it is said to converge...
, 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 semanticsDenotational semantics
In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
, algebraic semantics
Algebraic semantics
An programming language theory, the algebraic semantics of a programming language is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program semantics in a formal manner....
, and operational semantics
Operational semantics
In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...
.
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.The traces 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,
-
since 
performs no events -
since the process 
can be observed to have performed no events, the event 
, or the sequence of events 
followed by 
More formally, the meaning of a process
in the traces model is defined as such that:
-
(i.e. 
contains the empty sequence) -
(i.e. 
is prefix-closed)
where
is the set of all possible finite sequences of events.The stable failures model extends the traces model with refusal sets, which are sets of events
that a process can refuse to perform. A failure is a pair , consisting of a trace , and a refusal set which identifies the events that a process may refuse once it has executed the trace . The observed behavior of a process in the stable failures model is described by the pair . For example,-
-
The failures/divergence model further extends the failures model to handle divergenceDivergence (computer science)In computer science, a computation is said to diverge if it does not terminate or terminates in an exceptional state. Otherwise it is said to converge...
. A process in the failures/divergences model is a pair
where 
is defined as the set of all traces that can lead to divergent behavior and 
.
Tools
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 CSPM. The CSPM dialect of CSP possesses a formally defined operational semanticsOperational semanticsIn computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...
, which includes an embedded functional programming language.
The most well-known CSP tool is probably Failures/Divergence Refinement 2 (FDR2FDR2FDR and subsequently FDR2 are refinement checking software tools, designed to check formal models expressed in Communicating sequential processes . The tools have been developed by Formal Systems Ltd...
), 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). FDR2 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.
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 DiagramBinary decision diagramIn the field of computer science, a binary decision diagram or branching program, like a negation normal form or a propositional directed acyclic graph , is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed...
s (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.
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 LTLLinear temporal logicIn logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...
model-checking. ProB can also be used to verify properties of combined CSP and B specifications.
The Process Analysis Toolkit (PAT)
is a CSP analysis tool developed in the School of Computing at the National University of SingaporeNational University of SingaporeThe National University of Singapore is Singapore's oldest university. It is the largest university in the country in terms of student enrollment and curriculum offered....
. 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 asdeadlineandwaituntil. 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 sugarSyntactic sugarSyntactic sugar is a computer science term that refers to syntax within a programming language that is designed to make things easier to read or to express....
for well-known process modelling patterns used in standard CSP. The PAT syntax is similar, but not identical, to CSPM. The principal differences between the PAT syntax and standard CSPM 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.
CSPsim is a lazy simulator. It does not model check CSP, but is useful for exploring very large (potentially infinite) systems.
Related formalisms
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
- WrightWright (ADL)In software architecture, Wright is an architecture description language developed at Carnegie Mellon University. Wright formalizes a software architecture in terms of concepts such as components, connectors, roles, and ports. The dynamic behavior of different ports of an individual component is...
, an architecture description language - TCOZ, an integration of Timed CSP and Object Z
- Circus, an integration of CSP and Z based on the Unifying Theories of ProgrammingUnifying Theories of ProgrammingUnifying Theories of Programming deals with program semantics. It shows how denotational semantics, operational semantics and algebraic semantics can be combined in a unified framework for the formal specification, design and implementation of programs and computer systems.The book of this title by...
- CspCASL, an extension of CASLCommon Algebraic Specification LanguageThe Common Algebraic Specification Language is a general-purpose specification languagebased on first-order logic with induction. Partial functionsand subsorting are also supported....
that integrates CSP - LOTOSLanguage Of Temporal Ordering SpecificationLanguage Of Temporal Ordering Specification is a formal specification language based on temporal ordering used for protocol specification in ISO OSI standards....
, an international standard that incorporates the best features of CSP and CCSCalculus of Communicating SystemsThe Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...
.
Comparison with the Actor Model
In as much as it is concerned with concurrent processes that exchange messages, the Actor modelActor modelIn computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions, create more actors, send more messages, and...
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 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 same time, and senders may transmit messages before receivers are ready to accept them. These approaches may 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.
- CSP uses explicit channels for message passing, whereas actor systems transmit messages to named destination actors. These approaches may also 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.
See also
- occam was the first language implementing a CSP model.
- Ease programming languageEase programming languageEase is a general purpose parallel programming language, designed by Steven Ericsson-Zenith of Yale University. It combines the process constructs of CSP with logically shared data structures called contexts...
- combines the process constructs of CSP with logically shared data structures. - JCSPJCSPIn computer science and software engineering, JCSP is an implementation of Communicating Sequential Processes for the Java programming language....
is a blending of CSP & occam concepts in a JavaJava (programming language)Java is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer low-level facilities...
thread support API. - XCXC Programming LanguageThe XC Programming Language is a computer programming language developed by XMOS.XC is an imperative programming language with a computational framework based on C. XC programs consist of functions that execute statements that act upon values stored in variables...
is a language developed by XMOSXMOSXMOS is a fabless semiconductor company that develops multi-core multi-threaded processors designed to execute several real-time tasks, DSP, and control flow all at once.-Company history:...
which was heavily influenced by CSP and occam - Limbo is a language that implements concurrency inside the InfernoInferno (operating system)Inferno is a distributed operating system started at Bell Labs, but is now developed and maintained by Vita Nuova Holdings as free software. Inferno was based on the experience gained with Plan 9 from Bell Labs, and the further research of Bell Labs into operating systems, languages, on-the-fly...
operating system, in a style inspired by CSP. - Plan 9 from Bell LabsPlan 9 from Bell LabsPlan 9 from Bell Labs is a distributed operating system. It was developed primarily for research purposes as the successor to Unix by the Computing Sciences Research Center at Bell Labs between the mid-1980s and 2002...
and Plan 9 from User SpacePlan 9 from User SpacePlan 9 from User Space is a port of many Plan 9 from Bell Labs libraries and applications to Unix-like operating systems...
include the libthread library which allows the use of a CSP-inspired concurrency model from CC (programming language)C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
. - VerilogCSPVerilogCSPIn integrated circuit design, VerilogCSP is a set of macros added to Verilog HDL to support Communicating Sequential Processes channel communications...
is a set of macros added to Verilog HDL to support Communicating Sequential Processes channel communications. - Trace monoidTrace monoidIn mathematics and computer science, a trace is a set of strings, wherein certain letters in the string are allowed to commute, but others are not. It generalizes the concept of a string, by not forcing the letters to always be in a fixed order, but allowing certain reshufflings to take place...
and history monoidHistory monoidIn mathematics and computer science, a history monoid is a way of representing the histories of concurrently running computer processes as a collection of strings, each string representing the individual history of a process...
, the mathematical formalism of which CSP is an example. - Trace theoryTrace theoryIn mathematics and computer science, trace theory aims to provide a concrete mathematical underpinning for the study of concurrent computation and process calculi...
, the general theory of traces. - Go is a programming language by GoogleGoogleGoogle Inc. is an American multinational public corporation invested in Internet search, cloud computing, and advertising technologies. Google hosts and develops a number of Internet-based services and products, and generates profit primarily from advertising through its AdWords program...
incorporating ideas from CSP. - JoyceJoyce (programming language)Joyce is a secure, concurrent programming language designed by Per Brinch Hansen in the 1980s. It is based on the sequential language Pascal and the principles of Communicating Sequential Processes...
is a programming language based on the principles of CSP, developed by Brinch Hansen around 1989. - SuperPascalSuperPascalSuper Pascal is an imperative, concurrent computing programming language developed by Brinch Hansen. It was designed as a publication language: a thinking tool to enable the clear and concise expression of concepts in parallel programming. This is in contrast with implementation languages which are...
is a programming language also developed by Brinch Hansen, influenced by CSP and his earlier work with JoyceJoyce (programming language)Joyce is a secure, concurrent programming language designed by Per Brinch Hansen in the 1980s. It is based on the sequential language Pascal and the principles of Communicating Sequential Processes...
. - AdaAda (programming language)Ada is a structured, statically typed, imperative, wide-spectrum, and object-oriented high-level computer programming language, extended from Pascal and other languages...
implements features of CSP such as the rendezvous.
Further reading
-
- This book has been updated by Jim Davies at the Oxford University Computing LaboratoryOxford University Computing LaboratoryThe Department of Computer Science, until 2011 named the Computing Laboratory , is a department of Oxford University in England...
and the new edition is available for download as a PDF file at the Using CSP website.
- This book has been updated by Jim Davies at the Oxford University Computing Laboratory
General
- A PDF version of Hoare's CSP book - Copyright restriction apply, see the page text before downloading.
- The CSP Archive
- WoTUG, a User Group for CSP and occam style systems, contains some information about CSP and useful links.
- CSP Citations from CiteSeer
Analysis tools
- Formal Systems Europe, Ltd. develop CSP tools, some of which are freely downloadable.
- ARC, the Adelaide Refinement Checker, is a CSP verification tool.
- ProB is an animator and model-checker for the B method, but also support refinement checking and LTL model-checking of CSP.
- PAT is a model checker, simulator and refinement checker for CSP and various extensions of CSP (e.g. shared variables, arrays, fairness).
Implementation support
- CTJ is a Java implementation of CSP with network/distributed support.
- C++CSP is an implementation of CSP/occam/JCSP ideas in C++, similar in style to JCSP.
- Jibu (previously known as CSP.NET) is an implementation of a CSP style library for Microsoft .NET.
- CSP++ is a software synthesis tool for making specifications written in CSPm executable via C++.
- csp is a Common LispCommon LispCommon Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers...
library which allows use of a CSP-inspired concurrency model from SBCL and other multi-threaded Common LispCommon LispCommon Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers...
implementations. CHP is a Haskell library featuring a concurrency model inspired by CSP. - PyCSP is a Python implementation of CSP with network/distributed support.
- jCSP is a (100% pure) Java class library providing a base range of CSP primitives plus a rich set of extensions.
- Agent is a pure Ruby implementation of CSP primitives.