Home > Uncategorized > Automatic Model Generation, part 1: Parallel

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.

About these ads
Categories: Uncategorized Tags: ,
  1. April 13, 2010 at 12:54 pm

    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.

  2. Sebastian Fischer
    April 13, 2010 at 2:56 pm

    “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.

  3. April 13, 2010 at 3:18 pm

    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!)

  4. April 13, 2010 at 5:59 pm

    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

    • April 13, 2010 at 9:06 pm

      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?

      • May 6, 2010 at 1:46 pm

        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.

  5. Sebastian Fischer
    April 14, 2010 at 12:51 pm

    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.

  1. April 15, 2010 at 11:22 am
  2. April 20, 2010 at 12:31 pm
  3. May 1, 2010 at 5:49 pm
  4. May 3, 2010 at 5:28 pm

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: