Home > Uncategorized > Automatic Model Generation, part 4: Communication

Automatic Model Generation, part 4: Communication

This is part of a multi-part guide on redefining the CHP monad and primitives to generate a CSP model rather than executing the program. In this relatively self-contained part, we examine the issue of tracking values as they are communicated around the process network.

Modelling the mere occurrence of communications and synchronisations themselves is quite straightforward. We just label each created channel/barrier with a unique identifier, and then every time it is used we record in the model which channel/barrier was used. We can, however, do a bit better than that. Consider this code:

do x <- readChannel input
   writeChannel output x

What if we could tell that the value sent on the output channel was the same value as the one received on the input channel — that would be much more powerful than simply recording that a communication took place on the input channel followed by a communication on the output channel.

Identifiable Bottoms

Haskell has a function, undefined :: a. This produces a “bottom” value of any type, and will give an error if evaluated. It has a counterpart, error :: String -> a that allows the error message to be customised to be something useful. The Control.Exception module provides a try function that can catch these messages, and an evaluate function to examine values. If we put all of these together, we can create dummy values of any type, and later on we can identify them (but see the limitations section at the end of this post). This is the same technique used by Lazy SmallCheck, which we used for modelling IO computations in the previous part of the guide.

Input and Output

When an input occurs, we use the identifier of the channel (which is passed to the fakeCommIn function below) to form a uniquely-identifiable bottom value, which we make a note of in our state and then return:

bottomPrefix :: String
bottomPrefix = "__CHP.bottom__"

fakeCommIn :: Integer -> CHP a
fakeCommIn n = addSpecT1 $ do
  st <- get
  put $ st { chpNextBottom = succ (chpNextBottom st) }
  return ( error $ bottomPrefix ++ show (chpNextBottom st)
         , Sync $ Right (n, DirInput, chpNextBottom st)

The Sync . Right item holds the identifier of the channel, “n”, the direction of the communication, and the identifier of the bottom value involved. In our corresponding output function, we watch out for these bottom values:

fakeCommOut :: Integer -> a -> CHP ()
fakeCommOut n x = addSpecT1 $ do
  possErr <- lift $ C.try $ C.evaluate x
  case possErr of
    Left (C.ErrorCall s) | bottomPrefix `isPrefixOf` s
      -> return ( (), Sync $ Right
           (n, DirOutput, read $ drop (length bottomPrefix) s))
    -- Wasn't one of our bottoms:
    _ -> return ((), Sync $ Left n)

That is all the core code we need. Our replacement channels just store the channel identifier, and delegate reading and writing on channels to the above two methods.


For an example, we will use a process that reads two values from one pair of channels, and sends them out, swapped, on another pair of channels:

import Control.Concurrent.CHPSpec
import Control.Monad (replicateM)

swap :: (Chanin a, Chanin b) -> (Chanout b, Chanout a) -> CHP ()
swap (inA, inB) (outB, outA)
  = do (a, b) <- readChannel inA <||> readChannel inB
       writeChannel outB b <|*|> writeChannel outA a

p :: CHP ()
p = do leftIn <- oneToOneChannel' $ chanLabel "leftIn"
       leftOut <- oneToOneChannel' $ chanLabel "leftOut"
       rightIn <- oneToOneChannel' $ chanLabel "rightIn"
       rightOut <- oneToOneChannel' $ chanLabel "rightOut"
       swap (reader leftIn :: Chanin Int, reader rightIn :: Chanin Int)
            (writer leftOut, writer rightOut)

main :: IO ()
main = specify True p >>= putStrLn

This program is able to generate the following model, that correctly follows the values through the process:

channel leftIn
channel leftOut
channel rightIn
channel rightOut
  (((leftIn?x_1 -> SKIP) ||| (rightIn?x_2 -> SKIP))
   ((leftOut!x_2 -> SKIP) ||| (rightOut!x_1 -> SKIP)))


The technique of identifying bottoms is far from foolproof. In particular, for Int, “1+x” will be identified as being the same as “x”. What we are really identifying is that the bottom value received is used somewhere prominent in the output. So the idea is nice, but the execution is imperfect. Tristan Allwood suggested looking at stable names — these may help to reduce the imperfection, but they do not provide a strong enough guarantee to make the technique water-tight either.

I have now covered most of the model-generation technique. In the next part I will tackle the complex matter of recursive processes, probably followed by a final part showing how the top-level specify method works — at which point I hope to release all of this as a library, alongside the next CHP release (with the mtl dependency removed).

Categories: Uncategorized Tags: ,

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 )

Google photo

You are commenting using your Google 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 )

Connecting to %s

%d bloggers like this: