An Introduction to Communicating Sequential Processes

In my last post I touched upon the Communicating Sequential Processes calculus that inspired both my Communicating Haskell Processes library (including the name, of course) and the new Go language. This post serves as a brief introduction to CSP, and shows how it relates to CHP. For those interested in learning more about CSP, Hoare’s original book is available for free online, and is very readable, especially considering its formal subject matter. Hoare’s book is largely still accurate, but is superseded by Roscoe’s book, which is also freely available online. I’m going to quote from the two texts in this post; “quote”(H123) is a quote from page 123 of Hoare, and “quote”(R123) is from Roscoe.

Events

CSP is built on the idea of events. An event is a synchronisation that several concurrent processes can engage in. Events in CSP do not need to be pre-declared, and which processes synchronise together on events is determined by a notion of alphabets that I’m not going to cover here — because CHP doesn’t have alphabets, or events per se. CHP has barriers, which are a synchronisation that several concurrent processes can engage in, and thus they serve as a useful stand-in for events. The main difference is that barriers have the notion of membership, support dynamically enrolling on (and resigning from) the barrier at run-time — and they need to be allocated before use.

Events are written with lower-case names in CSP; Hoare’s book has lots of vending machine examples with events such as coin and choc.

Processes

CSP separates event synchronisations (the act of engaging in a single event) from processes (which can be composed of many synchronisations); in Haskell terms they should have different types. However, separating the types of an event synchronisation from a process would bring a whole load of pain — not least that I could not easily define a CHP monad — so I discard this in favour of everything being a process; an event synchronisation and a process are both of type CHP a, and thus there is no difference at the type-level between engaging in one event and engaging in many events.

Sequencing

The simplest form of sequencing in CSP is the prefix operator. “Given an event a and a process P, a -> P is the process which is initially willing to communicate a and will wait indefinitely for this a to happen. After a it behaves like P.”(R14). So in my CHP monad, this prefix operator is the standard monadic sequence operator, >>. CSP also has a semi-colon operator for sequencing two processes (which relies on notions of termination — a complex issue in formal systems of computation!), which also maps to >> in CHP.

As an example, here is Hoare’s vending machine (H6) that continually waits for a coin before dispensing a chocolate:

VMS = coin -> choc -> VMS

In CHP I might write this as:

vms = syncBarrier coin >> syncBarrier choc >> vms

Communication

Communication is central to CHP, and CSP. To perform a communication, we need a mechanism for performing an output to a channel, and a corresponding mechanism to input from the other end of the channel. We’ll start with output: “A process which first outputs v on the channel c and then behaves like P is defined (c!v -> P).”(H113). This translates to a call to writeChannel and monadic sequencing in CHP: writeChannel c x >> p.

Where I find the correspondence of CSP and CHP to be fascinating is in the definition of performing an input from a channel. “A process which is initially prepared to input any value x communicable on the channel c, and then behave like P(x), is defined (c?x -> P(x)).”(H114). To put it differently, this performs the action of reading a value from channel c, and binds the return value to x in the right-hand side of the arrow. This should sound familiar to Haskell programmers — this is monadic bind! Indeed, here is the CHP rendering: readChannel c >>= \x -> p(x), or more simply: readChannel c >>= p.

As an example, here is a CSP process (H115) that copies values from its left channel to its right channel:

COPY(left, right) = left?x -> right!x -> COPY(left, right)

This can be converted to CHP as follows:

copy :: Chanin a -> Chanout a -> CHP ()
copy left right = (readChannel left >>= writeChannel right) >> copy left right

Note that in CSP, a channel can be thought of as a (potentially infinite) set of events: one event for each value that could be communicated down the channel. So for some integer channel c, c.0 would be one event, c.1 another, etc). Thus channels in CSP are a sort of syntactic sugar on top of events — but in CHP we deal with actual channels that can communicate values, and they are distinct from barriers.

CSP is declarative, so it does not support the idea of assignment, or altering the value of a variable. Values are only introduced through the aforementioned binding of inputs, through constants, or by parameterisation of processes. Which means that slotting CSP into Haskell comes fairly naturally. We have seen that the sequencing of communications maps well to a monad (the CHP monad). The main other aspects of CSP are parallel composition and choice, which are process combinators in CHP (i.e. they have a type like CHP a -> CHP b -> CHP c).

Parallel Composition

CSP allows for parallel composition of processes. Two processes composed in parallel run in parallel, and “a parallel combination terminates when all of the combined processes terminate… the best way of thinking about [this] is that all of the processes are allowed to terminate when they want to, and that the overall combination terminates when the last one does.”(R143). These semantics also apply to CHP’s parallel composition. CSP’s notation for composing P and Q in parallel: P || Q is near-identical to the CHP version: P <||> Q (they only differ because || is already used in the Prelude).

Choice

CSP has the notion of external choice. “If x and y are distinct events then (x -> P [] y -> Q) describes an object which initially engages in either of the events x or y. After the first event has occurred, the subsequent behaviour of the object is described by P if the first event was x, or by Q if the first event was y.”(H7). CSP has rules for what happens if the first events are not distinct; in CHP this is considered to be a programmer error. Note that the choice is only of the first events, not of later events in P and Q; this is also the case in CHP, although it requires a certain amount of wizardry underneath to pick out the leading event of a CHP code block. In CHP we use <-> as the choice operator.

As an example, Roscoe defines a counting process: “COUNT(n) is the process which will communicate any sequence of up’s and down’s, as long as there have never been n + 1 more down’s than up’s.”(R17):

COUNT(0) = up -> COUNT(1)
COUNT(n) = (up -> COUNT(n+1)) [] (down -> COUNT(n−1))

We can translate this into CHP fairly directly (using barriers for the up and down events):

count :: EnrolledBarrier -> EnrolledBarrier -> Int -> CHP ()
count up down 0 = syncBarrier up >> count up down 1
count up down n = (syncBarrier up >> count up down (n+1))
                     <-> (syncBarrier down >> count up down (n-1))

CSP also deals with nondeterministic choice, notated P |~| Q. “It is important to appreciate the difference between P [] Q and P |~| Q. The process (a -> STOP) [] (b > STOP) is obliged to communicate a or b if offered only one of them, whereas (a -> STOP) |~| (b -> STOP) may reject either. It is only obliged to communicate if the environment offers both a and b. In the first case, the choice of what happens is in the hands of the environment, in the second it is in the hands of the process.”(R24). I do not offer nondeterministic choice in CHP; “even though [nondeterministic choices] are not constructs one would be likely to use in any program written for execution in the usual sense, CSP contains… ways of presenting the nondeterministic choice of processes.”(R23). That is, nondeterministic choice is a modelling construct useful for capturing and reasoning about the behaviour of processes, but it is not something you would mean to write in a program (a bit like bottom in Haskell, perhaps).

Primitive Processes

CSP has two useful primitive processes: SKIP and STOP (skip and stop in CHP). SKIP is the process which is always ready in a choice, and always immediately terminates successfully. So in CHP it has the behaviour of return (), but with the special property that it can be used in a choice. STOP is the process which is never ready in a choice, and never terminates. In CHP it acts the same — it is primarily useful for not being ready in a choice (and thus for dummy items in a choice); running a process that has the sole purpose of doing nothing and not terminating is rarely useful!

Summary

CSP is a formal calculus underlying CHP, in much the same way that the lambda calculus underlies Haskell. It is useful for formal reasoning about programs, and expressing semantics, but just as you do not need to know the lambda calculus to program Haskell, you do not need to know CSP in order to program CHP. CSP does have a model checker, FDR, which is freely available for academic use, and I have done some work on turning simple CHP programs into CSP (and feeding them to FDR) automatically (which I will tidy up and release when I get time). CSP also provided the idea of traces, which feature in CHP, and were briefly described in a previous post on using traces for testing.

---

Note: I could use operators (including GHC’s postfix operators) to provide an interface for the channel operations. I could define:

(!) = writeChannel
(?) = readChannel

Then I could take this CSP process:

COPY(input,output) = input?x -> output!x -> COPY(input,output)

and write it in CHP as:

copy input output = (input?) >>= \x -> output!x >> copy input output

I didn’t want the code to end up too much like ASCII spaghetti so I decided against these operators, but feel free to define these in your own code if you prefer the operator version. Unfortunately you always need those brackets around the input, so the do version becomes:

copy input output = do x <- (input?)
                       output ! x
                       copy input output