One of my courses this term is titled Concurrency, which doesn't cover programming with multiple threads and synchronisation primitives, but instead covers a language called CSP, which isn't a programming language in the traditional sense, and is more of a language for modelling and verifying concurrent systems. This post is a brain-dump of my current understanding of machine readable CSP (called CSP/M), which is aimed at nobody in-particular.

Events

We shall be considering automata, and as such we first need a (possibly infinite) alphabet. The letters of this alphabet are called events, and a family of related events is given the term channel. In any given CSP/M script, the alphabet is defined by channel declarations. The simplest form of this declaration defines a finite number of events:

channel some_event, some_other_event, a_third_thing

In this simple form, the word channel is slightly misleading, as each family of events has just one event in it. The more complex form of the channel declaration defines a family of related events name.x where x runs over a set X:

channel name : X

Finally, you can conveniently define a family of related events where the set is a Cartesian product of other sets, so the following defines a family of events complex_name.x.y.z where x varies over X, y over Y and z over Z:

channel complex_name : X.Y.Z

Processes

We shall consider a process to be a (very-)non-deterministic non-finite automaton, where every state is an accepting one, and each transition is labelled with an event (or with epsilon or tau, which we'll get to) - the literature would call this a labelled transition system (LTS). The language accepted by this automaton is given the new term of the set of traces of the process, and two processes are called traces equivalent if they accept the same language. The whole of CSP can then be regarded as a language for defining these fancy automata. To build these automata, it is useful to have a few basic processes to start from, and while the literature presents quite a few, the only ones present in CSP/M are STOP and SKIP. For now, we shall ignore SKIP, and just consider STOP. The STOP process is the simplest possible automaton: it has a start state, but no outgoing edges whatsoever. The language accepted by STOP is the set containing the empty word, so we say that the set of traces of STOP is the set containing the empty trace. A state with no outgoing edges is called a deadlock state, and so the STOP process is always deadlocked.

Prefixing

One way of building up processes is called prefixing. In the most simple form, this creates a new automaton from an old one, with a new start state which is linked to the old start state by a single transition. In the following example, a process called press_me_once is defined, whose set of traces is the empty trace and the trace consisting of just the pressed event:

channel pressed
press_me_once = pressed -> STOP

A process can be parametrised by one or more variables, where each variable can be a simple scalar value, or more complex values like sets or sequences. Combined with defining processes in a recursive way, this allows for slightly more interesting processes. In the following example, the set of traces of the process press_me_n_times(n) are the empty trace and the traces made up of at most n pressed events:

channel pressed
press_me_n_times(0) = STOP
press_me_n_times(n) = pressed -> press_me_n_times(n - 1)

With parametrised processes and families of events, there emerge more complex forms of prefixing. The first of these allows for event to be specified from a family of events based on a parameter (or any other, possibly constant, expression). The following example uses the family!expression syntax to define five processes, where the set of traces of press_me_once(x) is the set containing the empty trace and the trace consisting of a single pressed.x event:

X = {1, 2, 3, 4, 5}
channel pressed : X
press_me_once(x) = pressed!x -> STOP

The second extended form of prefixing is different to prior forms in that it prefixes a set of automata into a single automaton rather than a prefixing a single automaton into a single automaton. The following example extends the previous one with the family?new_identifier syntax, so that the choice process prefixes all of the press_me_once(x) processes, with the set of traces of the choice process being the set containing the empty trace, the traces choose.x for any x in X, and the traces choose.x pressed.x for any x in X:

X = {1, 2, 3, 4, 5}
channel choose : X
channel pressed : X
press_me_once(x) = pressed!x -> STOP
choice = choose?x -> press_me_once(x)

This syntax can be extended to family?new_identifier:subset to restrict the prefixing to a subset of the family of events rather than the entire family. From this, we see that family!expression and family?dummy:{expression} have the same meaning, apart from the latter introducing a new dummy variable. For families of events constructed from the Cartesian product of multiple sets, this syntax extends to allow multiple "!" and "?" clauses, though these clauses should not be inter-mixed with "." clauses from simple prefixing (use a "!" clause with a constant expression where you want ".").

Internal and external choice

Prefixing is one way of constructing new processes from old ones, which involves added transitions labelled with events. On the other hand, choices construct new processes from old ones using epsilon (external) and tau (internal) transitions. External choice is the simpler of the two types of choice, and is similar to the union construction on NFAs. In its most basic form, the external choice operator (denoted []) takes two processes and constructs a new process whose initial transition is any of the initial transitions of the two original processes, and then proceeds like the chosen original process. For example, the traces of the following bebop process are the empty trace, and the singleton traces be and bop:

channel be, bop
bebop = (be -> STOP) [] (bop -> STOP)

This operator generalises to external choice between a set of processes rather than just two processes by the syntax []identifer:set@process(identifier) meaning that the following example defines the canonical RUN(X) process, which given a set of events X (not necessarily from the same family, hence precluding use of prefixing with a "?" clause), has a set of traces where each trace is made up of a finite non-negative number of (possibly repeated) members of X:

RUN(X) = [] x:X @ x -> RUN(X)

Internal choice is much more subtle than external choice, and the trace set concept is not sufficient for appreciating its semantics. Given two processes P and Q, the internal choice of P and Q is denoted P|~|Q, which is a process which behaves like P or like Q, but with the choice between the two taken immediately rather than delaying the choice until a subsequent properly-labelled transition is taken. The following bebop2 process is either an NFA which accepts the empty word and the word be, or an NFA which accepts the empty word and the word bop, but you do not know which until you actually simulate the NFA:

channel be, bop
bebop2 = (be -> STOP) |~| (bop -> STOP)

The set of traces of bebop2 is the same as the set of traces of bebop, as any given trace of bebop can be a trace of bebop2, just that sometimes it won't be. Like for external choice, there is a generalised internal choice operator which chooses between a set of processes rather than two processes, the syntax for this being |~|identifier:set@process(identifier).

Parallel processes

All the previous ways of combining processes are fairly sequential, and involve one process "running" at a time. The parallel operator spices things up a bit by allowing multiple processes to be combined into a single process which represents all of the original processes running in parallel, similar to the product construction on NFAs to allow one the simulation of multiple NFAs to be done by the simulation of their a single NFA representing their product. Given two processes P and Q, and a set of events ES, the syntax P[|ES|]Q denotes the parallel execution of P and Q, with the restriction that for every event E in ES, transitions labelled with E can only occur when P and Q perform them simultaneously. Like other process-combining operators, there is the generalised form [|ES|]identifier:set@process(identifier) which represents the parallel execution of all the involved processes, with the restriction that events in ES must occur in every process simultaneously.