Communicating sequential processes

From Wikipedia, the free encyclopedia

In computer science, Communicating Sequential Processes (CSP) is a formal language for describing patterns of interaction in concurrent systems.^[1] It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi. CSP was influential in the development of the occam programming language.^[2]^[1]

CSP was first described in a 1978 paper^[3] 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,^[4] and a secure ecommerce system. ^[5] Academic applications of CSP include using it as tool for research in concurrency theory^{[citation needed]}, much as abstract machines are used for studying sequential systems. 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^[6]).

1 History
2 Informal description
3 Formal definition
- 3.1 Syntax
- 3.2 Formal semantics
4 Applications
5 Tools
6 Related formalisms
7 See also
8 References
9 External links

[edit] History

The version of CSP presented in Hoare's original 1978 paper was essentially a concurrent programming language rather than a process calculus, and did not possess a mathematically defined semantics^[7]. It also suffered from a number of limitations, including an inability to represent unbounded nondeterminism. Subsequently, Hoare, Stephen Brookes, and A. W. Roscoe developed and refined the theory of CSP into its modern form^[8]. The approach taken in developing the theoretical version of CSP was heavily influenced by Robin Milner's work on the Calculus of Communicating Systems (CCS), and vice versa.

The theoretical version of CSP was presented in Hoare's book Communicating Sequential Processes^[7], which was published in 1985. In May 2005, 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. The definitive text on modern CSP is Roscoe's The Theory and Practice of Concurrency^[1].

[edit] Informal description

As its name suggests, CSP allows the description of systems in terms of component processes that operate independently, and interact with each other solely through message-passing communication. However, the "Sequential" part of the CSP name is now something of a misnomer, since modern CSP allows component processes to be defined both as sequential processes, and as the parallel composition of more primitive processes. The relationships between different processes, and the way each process communicates with its environment, are described using various process algebraic operators. Using this algebraic approach, quite complex process descriptions can be easily constructed from a few primitive elements.

[edit] 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. $o n$ , $o f f$ ), compound names (e.g. $v a l v e . o p e n$ , $v a l v e . c l o s e$ ), or input/output events (e.g. $m o u s e ? x y$ , $s c r e e n! b i t m a p$ ).
Primitive processes: Primitive processes represent fundamental behaviors. Examples include $S T O P$ (the process that communicates nothing, also called deadlock), and $S K I P$ (which represents successful termination).

[edit] 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,

$a \rightarrow P$

is the process which is willing to communicate

a

with its environment, and, after

a

, behaves like the process

P

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,

$\left(a \rightarrow P\right) \Box \left(b \rightarrow Q\right)$

is the process which is willing to communicate the initial events

a

and

b

, and subsequently behaves as either

P

Q

depending on which initial event the environment chooses to communicate. If both

a

and

b

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 of the component processes will be selected. For example,

$\left(a \rightarrow P\right) \sqcap \left(b \rightarrow Q\right)$

can behave like either $\left(a \rightarrow P\right)$ or $\left(b \rightarrow Q\right)$ . It can refuse to accept

a

b

, and is only obliged to communicate if the environment offers both

a

and

b

. 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,

$\left(a \rightarrow a \rightarrow STOP\right) \Box \left(a \rightarrow b \rightarrow STOP\right)$

is equivalent to

$a \rightarrow \left(\left(a \rightarrow STOP\right) \sqcap \left(b \rightarrow STOP\right)\right)$

Interleaving: The interleaving operator represents completely independent concurrent activity. The process

$P \left\vert\left\vert\right\vert\right. Q$

behaves as both

P

and

Q

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

$P \left\vert\left[ \left\{ a \right\} \right]\right\vert Q$

requires that

P

and

Q

must both be able to perform event

a

before that event can occur. So, for example, the process

$\left(a \rightarrow P\right) \left\vert\left[ \left\{ a \right\} \right]\right\vert \left(a \rightarrow Q\right)$

can engage in event

a

, and become the process

$P \left\vert\left[ \left\{ a \right\} \right]\right\vert Q$

while

$\left (a \rightarrow P\right ) \left\vert\left[ \left\{ a \right\} \right]\right\vert \left(b \rightarrow Q\right)$

will simply deadlock.

Hiding: The hiding operator provides a way to abstract processes, by making some events unobservable. A trivial example of hiding is

$\left(a \rightarrow P\right) \setminus \left\{ a \right\}$

which, assuming that the event

a

doesn't appear in

P

, simply reduces to

P

[edit] 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:

$VendingMachine = coin \rightarrow choc \rightarrow STOP$

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

$Person = (coin \rightarrow STOP) \Box (card \rightarrow STOP)$

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,

$VendingMachine \left\vert\left[\left\{ coin, card \right\}\right]\right\vert Person \equiv coin \rightarrow choc \rightarrow STOP$

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

$VendingMachine \left\vert\left[\left\{ coin \right\}\right]\right\vert Person \equiv \left (coin \rightarrow choc \rightarrow STOP\right ) \Box \left (card \rightarrow STOP\right )$

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

$\left (\left (coin \rightarrow choc \rightarrow STOP\right ) \Box \left (card \rightarrow STOP\right )\right ) \setminus \left\{coin, card\right\}$

we get the nondeterministic process

$\left (choc \rightarrow STOP\right ) \sqcap STOP$

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.

[edit] Formal definition

[edit] Syntax

The syntax of CSP defines the “legal” ways in which processes and events may be combined. Let $e$ be an event, and $X$ be a set of events. Then the basic syntax of CSP can be defined as:

$\begin{matrix} Proc & ::= & STOP & \; \\ &|& SKIP & \; \\ &|& e \rightarrow Proc & (prefixing)\\ &|& Proc \;\Box\; Proc & (external \; choice)\\ &|& Proc \;\sqcap\; Proc & (nondeterministic \; choice)\\ &|& Proc \;|||\; Proc & (interleaving) \\ &|& Proc \;|[ \{ X \} ]| \;Proc & (interface \; parallel)\\ &|& Proc \setminus X & (hiding)\\ &|& Proc ; Proc & (sequential \; composition)\\ &|& \mathrm{if} \; b \; \mathrm{then} \; Proc\; \mathrm{else}\; Proc & (boolean \; conditional)\\ &|& Proc \;\triangleright\; Proc & (timeout)\\ &|& Proc \;\triangle\; Proc & (interrupt) \end{matrix}$

Note that, in the interests of brevity, the syntax presented above omits the $\mathbf{div}$ process, which represents divergence, as well as various operators such as alphabetized parallel, piping, and indexed choices.

[edit] 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 semantics, algebraic semantics, and operational semantics.

[edit] Applications

This section is a stub. You can help by expanding it.

Software design
Hardware design
Security protocol analysis

[edit] Tools

This section is a stub. You can help by expanding it.

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^[9]. The CSP_M dialect of CSP possesses a formally defined operational semantics, which includes an embedded functional programming language.

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, and then determines whether one of the processes is a refinement of the other within some specified semantic model (traces, failures, or failures/divergence)^[10].

Other CSP tools include

ProBE
ARC
Casper

[edit] 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
Wright, 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 Programming
CspCASL, an extension of CASL that integrates CSP

[edit] See also

Ease programming language - same lead designer as Occam, uses CSP as its formal basis.
JCSP is a blending of CSP & occam concepts in a Java thread support API.
Limbo is a language that implements concurrency inside the Inferno operating system, in a style inspired by CSP.
Plan 9 from Bell Labs and Plan 9 from User Space include the libthread library which allows the use of a CSP-inspired concurrency model from C.
VerilogCSP is a set of macros added to Verilog HDL to support Communicating Sequential Processes channel communications.

[edit] References

^ ^a ^b ^c Roscoe, A. W. (1997). The Theory and Practice of Concurrency. Prentice Hall. ISBN 0-13-674409-5.
- Some links relating to this book are available here. The full text is available for download as a PS or PDF file from Bill Roscoe's list of academic publications.
^ INMOS (1995-05-12). occam 2.1 Reference Manual. SGS-THOMSON Microelectronics Ltd.. , INMOS document 72 occ 45 03
^ Hoare, C. A. R. (1978). "Communicating sequential processes". Communications of the ACM 21 (8): 666–677. DOI:10.1145/359576.359585.
^ Barrett, G. (1995). "Model checking in practice: The T9000 Virtual Channel Processor". IEEE Transactions on Software Engineering 21 (2): 69–78. DOI:10.1109/32.345823.
^ Hall, A; R. Chapman (2002). "Correctness by construction: Developing a commercial secure system". IEEE Software 19 (1): 18–25.
^ Creese, S. (2001). "Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks". D. Phil.. Oxford University.
^ ^a ^b Hoare, C. A. R.. Communicating Sequential Processes. Prentice Hall. ISBN 0-13-153289-8.
- This book has been updated by Jim Davies at the Oxford University Computing Laboratory and the new edition is available for download as a PDF file at the Using CSP website.
^ Brookes, Stephen; C. A. R. Hoare and A. W. Roscoe (1984). "A Theory of Communicating Sequential Processes". Journal of the ACM 31 (3): 560–599. DOI:10.1145/828.833.
^ Scattergood, J.B. (1998). "The Semantics and Implementation of Machine-Readable CSP". D.Phil.. Oxford University Computing Laboratory.
^ A.W. Roscoe (1994). "Model-checking CSP". In A Classical Mind: essays in Honour of C.A.R. Hoare. Prentice Hall.

[edit] External links

The CSP Archive
WoTUG, a User Group for CSP and occam style systems, contains some information about CSP and useful links.
Formal Systems Europe, Ltd. develop CSP tools, some of which are freely downloadable.
CSP Citations from CiteSeer
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.
CSP.NET is an implementation of a CSP style library for Microsoft .NET 2.0.
CSP++ is a software synthesis tool for making specifications written in CSPm executable via C++.
csp is a Common Lisp library which allows use of a CSP-inspired concurrency model from SBCL and other multi-threaded Common Lisp implementations.

Retrieved from "http://en.wikipedia.org../../../c/o/m/Communicating_sequential_processes.html"

Categories: Articles with unsourced statements since February 2007 | All articles with unsourced statements | Articles with sections needing expansion | Process calculi