Editing Communicating sequential processes (section)

== 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|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 calculi|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 and primitive processes.

;Events

Events represent communications or interactions. They are assumed to be instantaneous, and their communication is all that an external ‘environment’ can know about processes. An event is communicated only if the environment allows it. If a process does offer an event and the environment allows it, then that event ''must'' be communicated. Events may be atomic names (e.g. {{mvar|on}}, {{mvar|off}}), compound names (e.g. {{mvar|valve.open}}, {{mvar|valve.close}}), or input/output events (e.g. {{mvar|mouse?xy}}, {{mvar|screen!bitmap}}). The set of all events is denoted <math>\Sigma</math>.<ref name="ucs">{{cite book |last1=Roscoe |first1=A.W. |date=2010 |title=Understanding Concurrent Systems |series=Texts in Computer Science |doi=10.1007/978-1-84882-258-0 |isbn=978-1-84882-257-3 }}</ref>

;Primitive processes

Primitive processes represent fundamental behaviors: examples include <math>\mathrm{STOP}</math> (the process that immediately deadlocks), and <math>\mathrm{SKIP}</math> (the process that immediately terminates successfully).<ref name="ucs"/>

=== Algebraic operators ===
CSP has a wide range of algebraic operators. The principal ones are informally given as follows.

; Prefix

The prefix operator combines an event and a process to produce a new process. For example, <math>a \to P</math> is the process that is willing to communicate event <math>a</math> with its environment and, after <math>a</math>, behaves like the process <math>P</math>.<ref name="ucs"/>

; Recursion

Processes can be defined using recursion. Where <math>F(P)</math> is any CSP term involving <math>P</math>, the process <math>\mu P. F(P)</math> defines a recursive process given by the equation
<math>P = F(P)</math>.
Recursions can also be defined mutually, such as
<math display="block">
\begin{align}
& P_u = up \to P_d\\
& P_d = down \to P_u\\
\end{align}
</math>
which defines a pair of mutually recursive processes that alternate between communcating <math>up</math> and <math>down</math>.<ref name="ucs"/>

; 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>(a \to P)\ \Box\ (b \to Q)</math> is the process that is willing to communicate the initial events <math>a</math> and <math>b</math> and subsequently behaves as either <math>P</math> or <math>Q</math>, depending on which initial event the environment chooses to communicate.<ref name="ucs"/>

; 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, <math>(a \to P) \sqcap (b \to Q)</math> can behave like either <math>a \to P</math> or <math>b \to Q</math>. It can refuse to accept <math>a</math> or <math>b</math> and is only obliged to communicate if the environment offers both <math>a</math> and <math>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 display=block>(a \to a \to \mathrm{STOP})\ \Box\ (a \to b \to \mathrm{STOP})</math> and
<math display="block">a \to \big((a \to \mathrm{STOP}) \sqcap (b \to \mathrm{STOP})\big)</math>
are equivalent.<ref name="ucs"/>

; Interleaving

The interleaving operator represents completely independent concurrent activity. The process <math>P \;|||\; Q</math> behaves as both <math>P</math> and <math>Q</math> simultaneously. The events from both processes are arbitrarily interleaved in time. Interleaving can introduce nondeterminism even if <math>P</math> and <math>Q</math> are both deterministic: if <math>P</math> and <math>Q</math> can both communicate the same event, then <math>P \;|||\; Q</math> nondeterministically chooses which of the two processes communicated that event.<ref name="ucs"/>

; Interface parallel

The interface parallel (or generalized parallel) operator represents concurrent activity that requires synchronization between the component processes: for <math>P \;|[X]|\; Q</math>, any event in the interface set <math>X \subseteq \Sigma</math> can only occur when both <math>P</math> and <math>Q</math> are able to engage in that event.<ref name="ucs"/>

For example, the process <math>P \;|[\{ a \}]|\; Q</math> requires that <math>P</math> and <math>Q</math> must both be able to perform event <math>a</math> before that event can occur. So, the process <math>(a \to P) \;|[\{ a \}]|\; (a \to Q)</math> is equivalent to <math>a \to (P \;|[\{ a \}]|\; Q)</math>, while <math>(a \to P ) \;|[\{ a, b \}]|\; (b \to Q)</math> is equivalent to <math>\mathrm{STOP}</math> (i.e. the process deadlocks).

; Hiding

The hiding operator provides a way to abstract processes by making some events unobservable by the environment. <math>P \setminus X</math> is the process <math>P</math> with the event set <math>X</math> hidden.

A trivial example of hiding is <math>(a \to P) \setminus \{ a \}</math> which, assuming that the event <math>a</math> doesn't appear in <math>P</math>, simply reduces to <math>P</math>. Hidden events are internalized as ''τ actions'', which are invisible to and uncontrollable by the environment. The existence of hiding introduces an additional behaviour called [[divergence (computer science)|divergence]], where an infinite sequence of τ actions is performed. This is captured by the process <math>\mathbf{div}</math>, whose behaviour is solely to perform τ actions forever.<ref name="ucs"/> For example, <math>(\mu P. a \to P) \setminus \{ a \}</math> is equivalent to <math>\mathbf{div}</math>.

=== Examples ===
{{unreferenced section|date=November 2024}}
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 (only in cash) before offering a chocolate can be written as:

<math display="block">\mathrm{VendingMachine} = \mathrm{coin} \rightarrow \mathrm{choc} \rightarrow \mathrm{STOP}</math>

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

<math display="block">\mathrm{Person} = (\mathrm{coin} \rightarrow \mathrm{STOP})\; \Box\; (\mathrm{card} \rightarrow \mathrm{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 display="block">\mathrm{VendingMachine} \left\vert\left[\left\{ \mathrm{coin}, \mathrm{card} \right\}\right]\right\vert \mathrm{Person} \equiv \mathrm{coin} \rightarrow \mathrm{choc} \rightarrow \mathrm{STOP}</math>

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

<math display="block">\mathrm{VendingMachine} \left\vert\left[\left\{ \mathrm{coin} \right\}\right]\right\vert \mathrm{Person} \equiv \left (\mathrm{coin} \rightarrow \mathrm{choc} \rightarrow \mathrm{STOP}\right ) \Box \left (\mathrm{card} \rightarrow \mathrm{STOP}\right )</math>

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

<math display="block">\left (\left (\mathrm{coin} \rightarrow \mathrm{choc} \rightarrow \mathrm{STOP}\right ) \Box \left (\mathrm{card} \rightarrow \mathrm{STOP}\right )\right ) \setminus \left\{\mathrm{coin, card}\right\}</math>

we get the nondeterministic process

<math display="block">\left (\mathrm{choc} \rightarrow \mathrm{STOP}\right ) \sqcap \mathrm{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), [[Nondeterministic algorithm|nondeterminism]] has been introduced.