Communicating sequential processes

From Free net encyclopedia

In computer science, Communicating Sequential Processes (CSP) is a formal language for describing patterns 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 first described in a 1978 paper by C. A. R. Hoare Template:Ref harvard, 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 (for examples, see Template:Ref harvard or Template:Ref harvard). The theory of CSP is still the subject of active research, including work to increase its range of practical applicability (e.g. Template:Ref harvard). CSP was influential in the development of the occam programming language Template:Ref harvard,Template:Ref harvard.

Contents

[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 Template:Ref harvard. 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 Template:Ref harvard. 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. Over the years there have been many fruitful exchanges of ideas between the researchers working on both CSP and CCS.

The theoretical version of CSP was presented in Hoare's book Communicating Sequential Processes, which was published in 1985 Template:Ref harvard. 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 Template:Ref harvard.

[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 – represent communications or interactions; assumed to be indivisible and instantaneous
    • May be atomic names (e.g. <math>\mathit{on}</math>, <math>\mathit{off}</math>), compound names (e.g. <math>valve.open</math>, <math>valve.close</math>), or input/output events (e.g. <math>mouse?xy</math>, <math>screen!bitmap</math>)
  • Primitive processes – represent fundamental behaviors
    • Examples include <math>\mathit{STOP}</math> (the process that communicates nothing, also called deadlock), and <math>\mathit{SKIP}</math> (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,
<math>a \rightarrow P</math>
is the process which is willing to communicate <math>\mathit{a}</math> with its environment, and, after <math>\mathit{a}</math>, behaves like the process <math>\mathit{P}</math>.
  • 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,
<math>\left(a \rightarrow P\right) \Box \left(b \rightarrow Q\right)</math>
is the process which is willing to communicate the initial events <math>\mathit{a}</math> and <math>\mathit{b}</math>, and subsequently behaves as either <math>\mathit{P}</math> or <math>\mathit{Q}</math> depending on which initial event the environment chooses to communicate. If both <math>\mathit{a}</math> and <math>\mathit{b}</math> 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,
<math>\left(a \rightarrow P\right) \sqcap \left(b \rightarrow Q\right)</math>
can behave like either <math>\left(a \rightarrow P\right)</math> or <math>\left(b \rightarrow Q\right)</math>. It can refuse to accept <math>\mathit{a}</math> or <math>\mathit{b}</math>, and is only obliged to communicate if the environment offers both <math>\mathit{a}</math> and <math>\mathit{b}</math>. 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,
<math>\left(a \rightarrow a \rightarrow STOP\right) \Box \left(a \rightarrow b \rightarrow STOP\right)</math>
is equivalent to
<math>a \rightarrow \left(\left(a \rightarrow STOP\right) \sqcap \left(b \rightarrow STOP\right)\right)</math>
  • Interleaving – the interleaving operator represents completely independent concurrent activity. The process
<math>P \left\vert\left\vert\right\vert\right. Q</math>
behaves as both <math>\mathit{P}</math> and <math>\mathit{Q}</math> 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
<math>P \left\vert\left[ \left\{ a \right\} \right]\right\vert Q</math>
requires that <math>\mathit{P}</math> and <math>\mathit{Q}</math> must both be able to perform event <math>\mathit{a}</math> before that event can occur. So, for example, the process
<math>\left(a \rightarrow P\right) \left\vert\left[ \left\{ a \right\} \right]\right\vert \left(a \rightarrow Q\right)</math>
can engage in event <math>\mathit{a}</math>, and become the process
<math>P \left\vert\left[ \left\{ a \right\} \right]\right\vert Q</math>
while
<math>\left (a \rightarrow P\right ) \left\vert\left[ \left\{ a \right\} \right]\right\vert \left(b \rightarrow Q\right)</math>
will simply deadlock.
  • Hiding – the hiding operator provides a way to abstract processes, by making some events unobservable. A trivial example of hiding is
<math>\left(a \rightarrow P\right) \setminus \left\{ a \right\}</math>
which, assuming that the event <math>\mathit{a}</math> doesn't appear in <math>\mathit{P}</math>, simply reduces to
<math>\mathit{P}</math>
[edit]

Formal definition

[edit]

Syntax

The syntax of CSP defines the “legal” ways in which processes and events may be combined. Let <math>\mathit{e}</math> be an event, <math>\mathit{X}</math> be a set of events, and <math>\mathit{P, Q, R}</math> be processes. Then the basic syntax of CSP can be defined as:

<math>

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

Note that, in the interests of brevity, the syntax presented above omits the <math>\mathbf{div}</math> 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]

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:

<math>VendingMachine = coin \rightarrow choc \rightarrow STOP</math>

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

<math>Person = (coin \rightarrow STOP) \Box (card \rightarrow STOP)</math>

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,

<math>VendingMachine \left\vert\left[\left\{ coin, choc \right\}\right]\right\vert Person \equiv coin \rightarrow choc \rightarrow STOP</math>

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

<math>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 )</math>

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

<math>\left (\left (coin \rightarrow choc \rightarrow STOP\right ) \Box \left (card \rightarrow STOP\right )\right ) \setminus \left\{coin, card\right\}</math>

we get the nondeterministic process

<math>\left (choc \rightarrow STOP\right ) \sqcap STOP</math>

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]

Criticisms

[edit]

Synchronous channels

Some people believe that the decision to use synchronous channels to represent communication in CSP introduces problems. Two specific objections to synchronous channels are typically raised:

  1. Implementing synchronous channels may introduce problems with starvation, livelock, and efficiency. For a description of this perspective see issues with synchronous channels. However:
    • CSP is intended as an abstract mathematical theory, rather than as an implementation model. Implementation problems are not a direct concern, while ease of reasoning is.
    • Despite these potential problems, several implementations based on CSP have been successfully used in practice. These include the occam and occam-π languages, the JCSP concurrency library for Java, and several languages from Bell Labs (including Alef and Limbo).
  2. The use of synchronous channels makes reasoning about fairness properties and guarantees of service difficult. However:
    • CSP was created for reasoning about properties other than fairness. CSP is a useful theory for analyzing systems that either don't depend on fairness properties to be “correct”, or need to operate “correctly” regardless of the fairness of the system components. Successful industrial uses of CSP (such as those reported in Template:Ref harvard or Template:Ref harvard) demonstrate that the inclusion of synchronous channels has not prevented CSP from being useful.
    • When it is necessary to do so, fairness can be represented (and thus reasoned about) using arbiter processes (pp. 263-270 of Template:Ref harvard), although there are limitations on the type of algebraic manipulations that can be performed. Thus, where large-scale reasoning about fairness is necessary, other formalisms which permit direct reasoning about fairness (such as the Actor model) may be a better choice.
[edit]

Lack of mobility

CSP does not provide a way to directly represent and reason about dynamic communications topologies and migrating computational agents, which are an important aspect of many modern systems. Some people see this as a major drawback of the CSP theory. However:

  • CSP is still extremely useful for reasoning about systems that have a static topology, as demonstrated by its wide use in industry.
  • Where necessary, dynamic topologies can be simulated within CSP's static topology (for example a CSP semantics for occam-π mobile channels). However, this can become cumbersome for complex systems, in which case other formalisms which permit direct reasoning about mobility (such as the π-calculus or the ambient calculus) may be a better choice.
[edit]

Related formalisms

Several other specification languages and formalisms have been derived from, or inspired by, the classic untimed CSP, including:

[edit]

See also

  • occam is a practical implementation of CSP as a concurrent imperative programming language.
  • JCSP is a blending of CSP & occam concepts in a Java thread support API.
  • C++CSP is an implementation of CSP/occam/JCSP ideas in C++, similar in style to JCSP.
  • 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.
[edit]

References

  • Template:Note label G. Barrett: “Model checking in practice: The T9000 Virtual Channel Processor”, IEEE Transactions on Software Engineering, vol. 21, no. 2, pp. 69–78, 1995 (DOI).
[edit]

External links

Retrieved from "http://www.netipedia.com/index.php/Communicating_sequential_processes"