## Automatic Model Generation, part 1: Parallel

CHP is based on CSP, a formal process calculus. CSP has a model-checker, FDR (among other tools), that is free for academic use for dealing with CSP. It would be great if we could take our CHP programs and prove them correct using FDR, e.g. prove them deadlock free. To properly translate a CHP program into its CSP model requires full semantics-based processing of the program’s source code, including all the functional parts (including tackling things like `writeChannelStrict c undefined`). But what if, at least for simple programs, we didn’t need to go to these lengths?

In this multi-part guide, I will introduce a technique to generate CSP models from CHP programs without source code analysis. The programmer would make one small alteration to the imports of a program and then: instead of executing properly, the program would spit out its own CSP model which we could feed to FDR. This technique involves redefining the CHP monad and all the CHP primitives so that the program spits out its model rather than actually executing. The technique is very limited in some regards, and I’ll try to point out the limitations as we go along. But hopefully it will be interesting to show what you can do by redefining your monad (see also: the Concurrent Haskell Debugger, and the Beauty in the Beast paper). Explaining my technique will take several posts — for today, I will focus on the definition of the specification type, the CHP monad — and redefining the `runParallel` function.

#### Specification Type

We start by defining a type to represent a CSP model. An introduction to CSP can be found in a previous post, but if you know CHP then the CSP model type has a fairly straightforward correspondence to CHP code. The type of the specification is as follows:

data SpecItem' proc comm = Par [Spec' proc comm] | Alt [Spec' proc comm] | Call proc | Sync comm | Stop | Repeat (Spec' proc comm) deriving (Show) type Spec' proc comm = [SpecItem' proc comm]

The main `Spec'` list type is a chronological sequence of processes in the model. The types are parameterised by `proc` (the type that identifies a process) and `comm` (the type that identifies a communication/synchronisation). We will explain these types in a future part of the guide; for now, we will use the opaque types `ProcessId` and `CommId`:

type SpecItem = SpecItem' ProcessId CommId type Spec = Spec' ProcessId CommId type SpecMod = Spec -> Spec finalise :: SpecMod -> Spec finalise f = f []

The `SpecMod` type is a function that modifies a specification. We will compose several of these functions while building the model — and at the end, we can use the `finalise` function to turn a `SpecMod` function into an actual `Spec`, by applying the function to the empty sequence.

#### Redefining the CHP monad

These specification types are used in our redefinition of the CHP monad. The main part of the new CHP monad is a monad transformer `CHPSpecT` that permits building of specifications on top of an existing (book-keeping) monad. The monad is as follows:

newtype CHPSpecT m r = CHPSpecT {runSpecT :: forall b.(r -> m (b, SpecMod)) -> m (b, SpecMod) }

For those of you playing monad transformer bingo at home, `CHPSpecT` is effectively the unrolled version of `forall b. ContT b (WriterT SpecMod)`, and will later be used on top of `StateT`. As with `ContT`, the monad instance itself makes no reference to the underlying monad, so it is surprisingly simple:

instance Monad m => Monad (CHPSpecT m) where return x = CHPSpecT ($x) m>>=k = CHPSpecT$\c -> runSpecT m$\a -> runSpecT (k a) c

The road to hell is paved with monad explanations, but here goes. The `r -> m (b, SpecMod)` item takes a value of type “r” (for red) and gives back an item of type “b” (for blue) along with a specification modifying function. We can envisage that item as follows:

The values pass left to right in the top half (turning red to blue), while the model actually passes in the *opposite* direction. Our models are effectively built backwards, with each `SpecMod` function modifying all future specifications to produce a current specification. We can now diagram our CHP monad as follows:

Given a circled value of the aforementioned type `r -> m (b, SpecMod)` (the lambda is used to indicate that this is an argument), a CHP item will give back something of type `m (b, SpecMod)`; this is drawn on the right as a blue item with a straight left edge (to indicate it has no input), paired with a specification-modifying function. You can pick all sorts of holes in these diagrams, but I hope they will be useful in explaining various uses of this monad as the guide continues.

#### CHP Monad Helper Functions

The CHP monad itself has no real logic involved; all the logic is actually captured in other functions, two of which I will introduce here, beginning with `finSpecT`:

finSpecT :: Monad m => CHPSpecT m r -> m (r, Spec) finSpecT = liftM (second finalise).flip runSpecT (\x -> return (x, id))

The `finSpecT` function is used to run the `CHPSpecT` transformer; it returns a value and a model. Once it has the return value paired with the corresponding *model-changing function*, it makes the latter into a model by finalising it (applying it to the empty specification). The result of this latter operation can be visualised below; the composite item has an unmodified return value, but has its specification-modifying function applied to the empty specification (the empty list):

The second function is `addSpecT1`:

addSpecT1 :: forall m r.Monad m => m (r, SpecItem) -> CHPSpecT m r addSpecT1 m = CHPSpecT$\k -> m>>=apply k where apply :: (r -> m (b, SpecMod)) -> (r, SpecItem) -> m (b, SpecMod) apply k (x, s) = liftM (second ((s:).))$k x

The `addSpecT1` function encapsulates the logic for sequencing; it takes a monadic action that gives a return value paired with a corresponding single specification item, and turns all that into a `CHPSpecT` item that adds the item to the model. The diagram is below; the `addSpecT1` takes a parameter (the outermost lambda) and gives back a CHP item that takes an inner continuation parameter (the lambda inside the box). The value of the outer parameter is passed to the continuation, and the specification item of the outer parameter (a trapezoid named “s”) is adjoined to the front of the result of the specification-modifying function of the continuation:

#### Parallel Composition

For parallel composition, we take each branch of the parallel composition and finalise it into a specification (using `finSpecT`), then add the Par constructor and join it on to the front of future specifications:

runParallel :: [CHP a] -> CHP [a] runParallel = addSpecT1.liftM (second Par.unzip).mapM finSpecT

We can again diagram this:

Hmmm, *hopefully* that makes it clearer! The finalised parts of the parallel specification (which were run sequentially — no need for actual parallelism during model generation) are shown on the left: their return values are formed into a list of values (following the arrows at the top of the diagram) that is passed to the continuation, while their models are put into a list with a Par constructor (following the arrows at the bottom of the diagram), and this is prepended to the sequence from future models.

#### Example

We can now given an example of the model generated for a program with parallel composition. This example is particularly simple, as I don’t want to use features that I haven’t yet explained. Here is a plain CHP program, that synchronises on various barriers in parallel:

import Control.Concurrent.CHP syncOn :: [String] -> CHP () syncOn = mapM_ syncOnIndiv where syncOnIndiv :: String -> CHP () syncOnIndiv name = do b <- newBarrierWithLabel name enroll b syncBarrier p :: CHP () p = runParallel_ [syncOn ["a", "b"], syncOn ["c", "d"], syncOn ["e"]] main :: IO () main = runCHP_ p

This program will compile, and can be executed normally. To get a model of this program, rather than executing it, we only need change the top and bottom lines; we import a different module, and change the outermost-call to `runCHP_` to `specify`:

import Control.Concurrent.CHPSpec ... processes as before main :: IO () main = specify True p>>=putStrLn

The program will again compile (against a different library), but this time when it is executed it will output the following model, ready to be read into the FDR model-checker or another formal tool for CSP:

channel a channel b channel c channel d channel e main_1= (((a -> b -> SKIP) ||| ((c -> d -> SKIP) ||| ((e -> SKIP))))) main = main_0

In the next part of the guide, we will examine exactly how these models are printed — and after that we will cover model generation for CHP’s other primitives.

You can probably simplify, that is conceptually clarify, the definition of the new CHP monad by using an operational style as for example described in my article The Operational Monad Tutorial.

In fact, it should even be possible to use one and the same monad for both execution and model and delegate their differences to two interpretation functions.

“make one small alteration to the imports of a program” sounds like you are providing two shallow embeddings of the CHP DSL in different modules. Did you consider providing one deep embedding instead and implementing the two current (and possibly other) “semantics” on top of it? A concrete representation of the CHP combinators may also allow for optimizations being performed before execution.

Having quickly googled deep embedding a bit: how do you store or reify Haskell functions in a deep embedding? If I have the code “readChannel c >>= \x -> if prime x then p else q”, how do I represent that as a deep embedding, considering that any arbitrary Haskell function can be used in place of prime? I’m guessing it has to remain as a black box function, but doesn’t that break the usefulness of deep embedding? (That code is exactly of the kind that causes problems in this monad substitution technique; more on that in later parts — still writing them, I’m afraid!)

Hello Neil,

I’ve been following your blog for a while and I just want to give you

credit for introducing people to CSP and blogging about CHP.

You mention the use of ‘FDR (among other tools)’ and actually

I’m involved in two of the ‘other tools’ as part of my PhD thesis.

(The ProB tool of Prof Michael Leuschel and a complete-Haskell tool,

which does not have a fancy name yet.)

The CSP-M parser of the our CSP-M tools is also available on Hackage

(CSPM-Frontend) and I plan to put the rest of the source of

Haskell-CSP-tool on Hackage as soon as possible

(It is just too unpolished at the moment).

I have been thinking about using CHP as a plug-in for my tool

and also about implementing to GUI of my tool based on CHP.

It meight also be interesting to include some the functionality of

my tool in CHP.

So maybe we can start some cooperation.

Regards Marc

Hi Marc,

I am aware of your CSP-M package. Unfortunately I wrote this code over a year ago now, before you released the first version, so I have a simple pretty-printer to print the code rather than using your package — since I already had the code working, there wasn’t much call to change it. What does your Haskell-CSP tool do — does it convert CSP to executable Haskell, or is it for some other purpose?

Sorry, it took me some time to answer, but I thought, before going into long explications about my project, I’d rather upload the thing to Hackage.

Currently it consists of five packages.

CSPM-cspm is the package that clues everything together.

The other packages are

CSPM-Frontend

CSPM-CoreLanguage

CSPM-FiringRules

and

CSPM-Interpreter

The idea is to implement a FDR compatible csp-tool, while, at the same time, keeping a clean separation between a CSP core-language and all the details of the functional language that FDR implements.

One can use CSPM-cspm to trace processes

and compute a labeled transition system of a process.

IIRC, functions (like the second argument of monadic bind) are not reified even in deep embeddings. Yet deep embeddings seem useful (I never used one myself). The packages ‘control-monad-free’, ‘MonadPrompt’, and ‘operational’ may be interesting starting points. The latter is accompanied by a MonadReader article (Issue 15: The Operational Monad Tutorial) which explains how to implement different “interpreters” on top of a single representation of a DSL.