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.