Archive
New chp-spec library released
I recently published a multi-part guide on how to provide a mirror implementation of (most of the API of) CHP that spits out a CSP specification of the program rather than execute it. You can go back and read:
- part 1: representing a specification and modelling parallelism,
- part 2: pretty-printing the CSP specification, and calculating parallel alphabets,
- part 3: modelling choice and lifted IO actions,
- part 4: modelling communication, and tracking communicated values, and
- part 5: modelling iteration — processes that repeat their behaviour.
This is the final post I plan to make on the matter (at least for a while)! This post is to announce the release of the work in the above guide as a new chp-spec-1.0.0 library. If you aren’t interested in formal specification, and just want to use CHP, you can ignore the chp-spec library. (And if you don’t use CHP, you can definitely ignore it!) It’s only useful if you want to try to generate a CSP model of your CHP program — and even then, the technique comes with a lot of caveats. But I’d rather release it than leave it sitting on my hard drive.
Instructions
To use the chp-spec library in place of chp, you must do the following:
- Change the library dependency from chp to chp-spec when you want to generate a specification. You may be able, in cabal, to have both dependencies listed all the time. Currently there is no chp-spec-plus; if you want this, let me know.
- Change the imports in all your modules from Control.Concurrent.CHP* to Control.Concurrent.CHPSpec* when you want to generate a specification; this can be automated somewhat using preprocessor macros if you want to switch between the two regularly.
- Make sure that all uses of the forever function in your process are changed to CHP’s foreverP (this is included in CHP 2.2.0 onwards so you can make this change permanent, even when using plain chp).
- Add the process annotation to all directly recursive processes (again, this is included in CHP 2.2.0 onwards, so you can make this change permanent, even when using plain CHP).
- When you want to generate a specification, change the top-level function from runCHP to specify.
Specify
The specify function mentioned in the last point is the top-level call that generates and post-processes the CSP specification. The generation has been mostly covered in previous posts; the generation part of specify is trivial; it annotates the top-level process to be called main, then runs the state transformer to get the altered state with all the processes recorded in it (among other things), which it passes to specify', the function that does all the post-processing:
specify :: Bool -> CHP () -> IO String specify showIO main = specify' showIO <$> execStateT (finSpecT $ process "main" main) emptyCHPState
That showIO parameter will be explained later in the post. The code for specify' is long-winded but not very exciting. It can be split into two aspects:
specify' :: Bool -> CHPState -> String specify' showIO st = render specs ++ declMain where ...
We’ll start with the first part of that concatenation. The render call uses the pretty-printing to print the specifications. The specs item is generated from the recorded process by two steps: first, it pulls up any Repeated processes to be top-level recursive processes — modern CSP has no iteration operator — and second, it transforms all the process-ids and communications into strings by uniquely numbering the processes and channel values.
The second part of the concatenation, declMain, declares a main process, named “main”. We know, because it’s the first process that is encountered, that our top-level process will end up named “main_1”, so at the most basic we end up with a line “main = main_1”, which wraps up all the numbering in a simpler name. But it can have different behaviour depending on that mysterious “unhideIO” parameter.
CSP’s semantics revolve around traces, which are records of the visible actions that a process takes. That visible qualifier is significant: CSP allows for hiding of events. This is particularly relevant in case of our dummy IO events. If we leave them as-is, they will show up in the trace of the process even though they are not really a part of its behaviour — but this does allow us to read traces produced by the FDR tool more easily, as we can see which IO events occurred. So the setting is useful for “debugging” any deadlocks, but these extra events can ruin refinement checks because the process appears to be taking extra events. If you’re doing a deadlock check, pass True to keep the IO events visible, otherwise pass False to hide them. That is done by the following code for declMain in the where clause of specify’:
declMain :: String
declMain = "\nmain = main_1 " ++ (if showIO then "" else
"\\ {" ++ intercalate "," (map getName $ Set.toList $ chpIOEvents st) ++ "}"
) ++ "\n"
where
getName = fromJust . flip Map.lookup events
If showIO is False, the main process will hide (backslash is the hide operator in CSP) all the IO events, to stop them being visible to the outside, and in traces of the main process.
Automatic Model Generation, part 5: Iteration
Previous parts of this guide have shown how to represent and print CSP models, and how to redefine the CHP monad and the primitives for choice, IO and communication in order to generate CSP models from CHP programs. This part deals with the final difficult item: iteration.
Most processes in CHP run in an infinite loop, terminated only by poison. Many are written using the helper function forever, which is defined: forever p = p >> forever p. Consider what happens when we try to generate the model for such a process, e.g. forever (syncBarrier b). We first encounter the syncBarrier and we store in the model that the process would engage in event “b”. Then in the forever function we loop round and reach the syncBarrier again, and add on to the model that the process would next engage in “b” again. And so on and so on. An infinite loop in our program would cause an infinite loop in our model generation, rendering it useless. We cannot observationally determine that the program is looping forever; think how our approach could possibly distinguish the above from replicateM_ 1000000 (syncBarrier b) >> syncBarrier c.
Forever in an Instant
To solve this particular problem, we supply a foreverP function in the CHP library and its redefinition. In the original CHP library, foreverP acts as forever. In the forthcoming chp-spec library, it is defined differently: it runs the code once to record the model, then makes a note in the model that this code should have run forever. It also stops further modelling; any code after a call to forever will be ignored in the normal library, and so it should be here, too:
foreverP :: CHP a -> CHP b foreverP p = stopSpecT . liftM (Repeat . snd) . finSpecT stopSpecT :: Monad m => m SpecItem -> CHPSpecT m a stopSpecT m = CHPSpecT $ const $ liftM (\sp -> (error "stopSpecT", (sp :))) m
The stopSpecT makes sure that no further specification is performed after this point. The crucial part is the const which ignores the continuation function — this is something that is easily done with our continuation-passing monad (and is like a short-circuiting error monad).
The above takes care of forever, which is used when the program carries no state around. But other processes have direct recursion and cannot use this function.
Process Annotations
To solve the recursion problem, we introduce a process annotation. The process annotation surrounds a process and captures the value of its arguments. The assumption is made (or rather, a condition is placed on the user) that the process will have the same behaviour (excluding any external input from channels and liftIO functions) when given the same arguments. In a pure language like Haskell, this is reasonable and will commonly be the case. The annotation should be added at the beginning of any process that recurses — when the recursion is performed, the process is modelled iff it has never been run before with these arguments; if it has been run before, its behaviour has already been modelled and recorded, so it is returned directly. Here is the annotation in action, on the security guard from the dining philosophers:
security :: [(Chanin (), Chanin ())] -> CHP ()
security chans = security' chans 0
where
security' :: [(Chanin (), Chanin ())] -> Int -> CHP ()
security' = process "security" $ \chans satDown ->
let (ups, downs) = unzip chans
maxSatDown = length chans - 1 in
(alt $
[readChannel c >> return (satDown - 1) | c <- ups, satDown > 0] ++
[readChannel c >> return (satDown + 1) | c <- downs, satDown < maxSatDown]
) >>= security' chans
It takes as its first parameter the name of the process — it is user-supplied, but should be unique in the program. The second parameter is the process itself. Here, the process has two arguments — but it could be any number. The process annotation is designed using type-classes so that it can be used with processes that take any number of arguments.
We need to store the arguments that each process took when it was modelled. So we need to store the models in a data structure like Map String (Map Args Model). But Args needs to be a set of differently-typed arguments for each process — we can’t statically assign a type to it. If we only supported self-recursion we could probably solve this with phantom type parameters in the monad and so forth, but sometimes, even in Haskell, it is appropriate to use dynamic typing. The Data.Dynamic module supports safe dynamic typing (in that casts from the Dynamic type have a run-time check).
In fact, we don’t actually need to store the arguments themselves. What we need to store with a previous model is a function like a -> Bool that says whether the latest parameter is the same as was used for generating the previous model:
type CheckArg = Dynamic -> Bool checkArgs :: [Dynamic] -> [CheckArg] -> Bool checkArgs ds fs | length ds /= length fs = False | otherwise = and $ zipWith ($) fs ds
We create a Process type-class to implement our process annotation:
process :: Process p => String -> p -> p process s = process' True s [] class Process p where process' :: Bool -> String -> [(Dynamic, CheckArg)] -> p -> p instance (Eq a, Typeable a, Process b) => Process (a -> b) where process' topLevel name args f x = process' topLevel name (args ++ [(toDyn x,(== Just x) . fromDynamic)]) (f x)
The process' function takes a Bool (ignore that for now), the process name, a list of arguments so far (each pair is the argument itself, and its function to check against a future value), and then wraps a process “p”. The instance shown above is the one that captures all a process’s parameters. Each parameter is appended to the list. toDyn turns a value into a Dynamic, and fromDynamic returns a Maybe value (Nothing if the type-cast is unsuccessful, Just if was successful). Comparing the result of fromDynamic to Just x checks both the type and the value at once. To support dynamic typing, parameters must have a Typeable instance (which GHC can derive for most types — and is supplied for all CHP library types) and an Eq instance to check for equality. The most notable types that cannot be used for a parameter are functions. This is a limitation of the approach — and indeed, CSP itself does not support any notion of functions being passed around. Any processes that take functions as parameters would have to be made first-order (Neil Mitchell’s Firstify comes to mind).
The base-case instance for Process is the one that actually uses the parameter list:
data CHPState = CHPState { ... ,
chpProcessMap :: Map.Map String (Map.Map Integer ([CheckArg], (Spec,Dynamic))),
chpFreeNames :: [(Dynamic, CheckArg)],
chpNextProcess :: !Integer }
instance (Typeable a, Eq a) => Process (CHP a) where
process' topLevel name immArgs p = addSpecT1 $ do
st <- get
let possibles = Map.toList <$> (Map.lookup name $ chpProcessMap st)
args = if topLevel then immArgs
else chpFreeNames st ++ immArgs
case possibles >>= L.find (checkArgs (map fst args) . fst . snd) of
Just (n, (_, (_, r)))
-> return (flip fromDyn (error "process-lookup") r, Call n)
Nothing ->
do let n = chpNextProcess st
put $ st { chpProcessMap = insertMapMap name n
(map snd args, (error "process", toDyn ()))
$ chpProcessMap st
, chpFreeNames = args
, chpNextProcess = succ n
}
(r, f) <- finSpecT p
modify $ \st' -> st' { chpProcessMap = insertMapMap name n
(map snd args, (f, toDyn r))
$ chpProcessMap st'
-- Restore original free names:
, chpFreeNames = chpFreeNames st }
return (r, Call n)
The case statement checks if any previously-modelled processes match. If one does (the Just case), its model and return value are returned. If Nothing is found, the process is modelled. It is crucial that the state is first updated with an entry for the process — that way, when the process recurses, it can find itself in the collection of recorded processes (if the recursion uses the same argument values). The dummy entry has the right parameters but an invalid model (that will never be accessed before it is later updated) and an incorrect return type; processes that recurse and then examine the value of the recursive call are not supported here. However, almost every recursive CHP process is tail-recursive, which can be modelled just fine (if they weren’t tail recursive, they would probably feature a space-leak). After the process has been modelled, its entry is updated with the real return value and real specification.
The model returned by the process annotation is always simply a Call item. Therefore, any process that recurses will simply have a Call item added to the end, stopping the model from extending forever — provided that at some point the same parameters are used to the process. A parameter with continually-changing parameters that never repeat — for example, one that outputs ascending integers — cannot be modelled here. This is yet another limitation of the approach.
Example
As an example, we’ll use the security guard shown earlier in this post, and how that is modelled with three philosophers (i.e. three sets of channels). Our approach produces a model for each different set of arguments to the process — the models for different arguments can potentially be completely different. Some effort could be put into collapsing them back down during post-processing, but here are the three models:
security_10=
(((security.up.phil0?x_14 -> security_9)
[]
(security.up.phil1?x_15 -> security_9)
[]
(security.up.phil2?x_16 -> security_9)
[]
(security.down.phil0?x_17 -> security_11)
[]
(security.down.phil1?x_21 -> security_11)
[]
(security.down.phil2?x_22 -> security_11)))
security_11=
(((security.up.phil0?x_18 -> security_10)
[]
(security.up.phil1?x_19 -> security_10)
[]
(security.up.phil2?x_20 -> security_10)))
security_9=
(((security.down.phil0?x_13 -> security_10)
[]
(security.down.phil1?x_23 -> security_10)
[]
(security.down.phil2?x_24 -> security_10)))
The top process, security_10, is the state where one philosopher is currently seated and thus all up and down events are offered. If an up event occurs, the next process is security_9, the state where no philosophers are seated, and thus only down events are offered. If a down event occurs in security_10, the next process is security_11, where two philosophers are seated and only up events are offered: this prevents a third philosopher sitting down (which could potentially lead to the classic deadlock in the dining philosophers).
That concludes all the in-depth technical parts of this guide. There’ll be one more post explaining the top-level specify method, which should also include the announcement of the release of the chp-spec library based on this guide.
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.
Example
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 main_1= (((leftIn?x_1 -> SKIP) ||| (rightIn?x_2 -> SKIP)) ; ((leftOut!x_2 -> SKIP) ||| (rightOut!x_1 -> SKIP)))
Limitations
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).
Automatic Model Generation, part 3: Choice and IO
This is the third part in a multi-part series describing a technique to generate formal CSP models of CHP programs by redefining the CHP monad and primitive actions to output the model of the program. In part 1 we saw the redefinition of the monad and the specification type; in part 2 we saw how to pretty-print the model, including the parallel composition alphabets. In this part, we look at choice and IO actions.
In part 1 of this guide, we saw how to define parallel composition. The specifications for each branch were generated, composed into a Par item, and added to the model. Choice is not so straightforward, because it can introduce branching execution paths. Consider this code:
alt [syncBarrier b >> return Nothing, syncBarrier c >> return (Just x)]
>>= maybe p q
The choice doesn’t return a single value — it returns one of two, and which value is returned will affect the code coming afterwards. So we need a different approach from just putting a choice on the front of the sequential execution of the model. In fact, there is quite a simple solution just by using one of the laws of CHP from the tutorial:
alt [p, q] >>= k = alt [p >>= k, q >>= k]
This rule is usually useful because you can use it to remove the code duplication on the right by transforming to the form on the left. Here, we will use the rule in the opposite way, to move the binding of the multiple results back into the alt and attach it to each branch.
Choice
The alt :: [CHP a] -> CHP a function chooses between several alternatives. We define it by using the Alt specification item:
alt :: [CHP a] -> CHP a
alt [] = stopSpecT $ return Stop
alt ps = altSpecT ps
altSpecT :: Monad m => [CHPSpecT m a] -> CHPSpecT m a
altSpecT ms = CHPSpecT $
\k -> do xfs <- mapM (flip runSpecT k) ms
return (error "alt return", \s -> [Alt $ map (($ s) . snd) xfs])
The key aspect of this code is that due to the continuation-passing style of the replacement CHP monad, we have a continuation (“k” in the above code) that represents all actions that would be taken after the alt. We pass this as the continuation when we run each of our branches of the alt (the first line of the do block). The specification-modifying functions from each branch are applied to future specifications, then returned as a specification containing a single Alt item. This can be depicted as follows:
Note that the eventual return values of all of the branches are discarded. This is not as bad as first appears, because the result values are only used if this choice is in a parallel composition and its result is needed (which is surprisingly rare in CHP code) or if the choice is in a recursive process where the result is needed (this again is surprisingly rare, and will be dealt with in a future part of the guide).
IO Actions
The real CHP monad is really a monad transformer on top of the IO monad, and supports IO actions being lifted into the CHP monad. An IO action may perform all sorts of actions, but these fall outside the scope of our modelling. The more significant problem for the modelling is that the IO actions may return a meaningful value (i.e. one other than a unit return). These values can then be used in the CHP program, and in particular they may be used to branch execution. If we simply return an error value in these cases, the code will fail. We can do slightly better than that, to allow partial support for IO actions when modelling.
In the case of an IO computation, we have some code (the code following the IO computation) that takes a value (the return value of the IO computation) and produces an output based on the value (the model of the code following the IO computation). This is, in effect, a testing problem, and we can borrow techniques from software testing to solve it. Haskell has several clever testing libraries: QuickCheck is one of the most well-known, but an even cleverer library is Lazy SmallCheck. Lazy SmallCheck allows for an efficient search of the input space to a function by starting off with undefined values, and partially defining them as necessary. Not only can this be efficient, but a particularly nice aspect is that it allows us to know if the search was complete or not.
The Lazy SmallCheck library doesn’t actually expose enough of its implementation as it currently stands, so I took it and modified it until I was able to produce a fuzz function:
fuzz :: (Serial a) => (a -> StateT s IO b) -> StateT s IO ([b], Bool)
This function takes an IO computation that sits inside a state monad transformer (I needed this, and it was much easier to embed this in the fuzz function than to do it any other way). The input space for this function is searched (with the stateful side-effects of any successful returns being kept) and a list of return values (the models) is produced. The boolean parameter indicates whether the search was complete: that is, whether it examined all possible values in the search space (either by exhaustion of all fully-defined values, or because it explored a complete set of partially defined values).
We can use the fuzz function on the continuation passed to the IO computation in order to explore the continuation’s possible models with different input values to the continuation. This will give us a collection of models, each of which represents a possible behaviour of the program from this point, based on an event (the IO action) that we must treat as unpredictable and out of our control. In CSP we can join these models together as an external choice between processes that are prefixed with non-synchronising events: that is, events that are not featured anywhere else in the model. The external choice between such events indicates that the process’s behaviour will depend on which event is offered by its environment, and that we must assume that any event might be offered (i.e. any input value might be returned). This code achieves that:
liftIO_CHP :: Serial a => IO a -> CHP a
liftIO_CHP _ = CHPSpecT $ \k ->
do (vals, complete) <- fuzz k
unless complete $
liftIO $ putStrLn "Incomplete fuzzing of IO computation"
nonces <- replicateM (length vals) newEvent
let firstLabel = "IO_" ++ show (head nonces)
zipWithM_ labelEvent nonces (map (firstLabel++) suffixes)
modify $ \st -> st { chpIOEvents = Set.union
(Set.fromList nonces) (chpIOEvents st) }
return (error "liftIO return",
\s -> [Alt $ zipWith (\n f -> Sync (Left n) : snd f s) nonces vals])
where
suffixes = map (:[]) ['A'..'Z'] ++ map show [(0::Integer)..]
As ever, this technique is limited: the search may be incomplete, in which case the model may be incomplete. We print a message in these cases to warn the user of the problem. The search will only be incomplete if the return value has a large flat domain (e.g. integers) and/or the subsequent computation makes full use of the domain. If the return value is ignored or if it is not used to make decisions about the control path, the search will be complete (because the value will never be defined). So if, for example, a String is returned and then passed to a different IO action to write to a file, this will not cause a problem in the modelling because the behaviour in terms of CSP processes is invariant to the return value. The only time this search above comes into play is when the return value is used to affect the execution path, for example if the process acts differently when the String is empty. (This is reminiscent of the different between monads and applicative functors: if CHP was only an applicative functor, IO actions could be completely ignored.)
Example
For an example, I will use a simple simulation example with a tick-tock barrier to divide time into time-steps. The simulation has six site processes wired up in a ring, with each site connected to its neighbours via a pair of barriers, representing incoming and outgoing movements. A site may be full or empty. If it is full (i.e. contains an agent), it makes a random choice as to which direction to send the agent in a time-step (and then ends the time-step). If it is empty, it offers to receive a new agent from either side, or to end the time-step. Here’s the diagram (the star indicates a full site) and the code:
site :: EnrolledBarrier -> (EnrolledBarrier, EnrolledBarrier)
-> (EnrolledBarrier, EnrolledBarrier) -> Bool -> CHP ()
site = process "site" $ \bar (inL, outL) (inR, outR) occupied ->
(if occupied
then do shouldMove <- liftIO_CHP' "shouldMove" $ getStdRandom random
if shouldMove
then do moveLeft <- liftIO_CHP' "moveLeft" $ getStdRandom random
if moveLeft
then syncBarrier outL
else syncBarrier outR
syncBarrier bar
return False
else syncBarrier bar >> return True
else alt [syncBarrier inL >> syncBarrier bar >> return True
,syncBarrier inR >> syncBarrier bar >> return True
,syncBarrier bar >> return False
]
) >>= site bar (inL, outL) (inR, outR)
main :: IO ()
main = specify True (runSiteRing [True, False, False, True, False, False])
>>= putStrLn
I’ve omitted a couple of uninteresting wiring functions. You can see that I’m using a version of liftIO_CHP that allows me to supply a label, which helps in reading the model. The program uses choice, and lifted IO actions to get random boolean values. It also has a potential deadlock, which we will find using the FDR model-checker.
One problem with this whole technique at the moment is that each site generates a separate model, even though they are all similar enough to be expressed in one model. So here are the processes that make up the behaviour of the first site — there are similar pairs for the other five sites:
site_2=
(((IO_shouldMove7A -> tock -> site_2)
[]
(IO_shouldMove7B
->
((IO_moveLeft5A -> right_0 -> tock -> site_3)
[]
(IO_moveLeft5B -> left_5 -> tock -> site_3)))))
site_3=
(((right_5 -> tock -> site_2)
[]
(left_0 -> tock -> site_2)
[]
(tock -> site_3)))
The site_2 process is the full process. It makes a choice between two events: IO_shouldMove7A and IO_shouldMove7B. These are the two possible outcomes of asking for a random boolean. In one case, it synchronises on the tock event and recurses — this must be the won’t-move case. In the other, it chooses between two other events: IO_moveLeft5A and IO_moveLeft5B. These are the decisions as to whether to go right or left: it next either synchronises on its right event or its left event, and then becomes site_3. The site_3 process is the empty process. It will agree to synchronise with its neighbours, end the timestep and become the full process — or to just end the timestep and remain the empty process.
There are six such pairs of processes in the model, one for each site in our model. The only difference between them is the names of the dummy IO events, and the numbers of the right and left events. They are all wired up in the main process:
main_1=
(((site_2)
[|{| left_0 , left_5 , right_0 , right_5 , tock |}|]
(((site_4)
[|{| left_4 , right_4 , tock |}|]
(((site_6)
[|{| left_3 , right_3 , tock |}|]
(((site_8)
[|{| left_2 , right_2 , tock |}|]
(((site_10) [|{| left_1 , right_1 , tock |}|] (site_12)))))))))))
We can add a single line at the end of the model: assert main_1 :[ deadlock free] and feed it to FDR, asking it to produce a trace if it finds a counter-example. FDR does find a counter-example for our assertion: a trace that ends in deadlock. Here it is:
IO_shouldMove7B IO_moveLeft5A right_0 IO_shouldMove25A tock IO_shouldMove35B IO_moveLeft33A right_1 IO_shouldMove25B IO_moveLeft23B
We can take this trace (a chronological list of events that occur) and relate it to the model. Here’s the short form: the agent in the first site moves right, while the agent in the fourth site stays put, and the time-step ends. Then the agent that is now in the second site moves right, and the agent in the fourth site decides to move left. At this point, one agent is in the third site (which is waiting to end the time-step) and the other is in the fourth site trying to move into the third site. Deadlock!
There are several ways to solve this problem, but I’m not really interested in them — the point here was to show that we took a simple example, we generated our model and fed it straight to the proof-checker which gave us a trace that produces deadlock. Reading the CSP and relating the trace to the model is straightforward, but can be long-winded. What might be nice in future is to have an option to somehow encode the source location in the event name, to then easily point back to the source and say “this bit of the source happened, then that bit happened, then deadlock”. In the next part of the guide I’ll show how we can deal with tracking communications when building the model.
Automatic Model Generation, part 2: Pretty-Printing the Model
In the first part of this guide, I explained part of a technique for generating CSP models from a CHP program — including the introduction of the specification type. In this second part of the guide I take a slight diversion to explain how to pretty-print the specifications. We will see in this part how parallel composition is rendered, which has particular importance in CSP.
After we’ve created the model of our program, we need to print it out to a file, ready to be fed to the proof-checker or other tool. I wanted the model to be as comprehensible as possible after printing, so that users (and I!) can read it. To that end, I used a pretty-printing library: pretty from Hackage, which is imported as PP throughout the code in this post. (After I wrote this code, Marc Fontaine uploaded a library to Hackage produced that supports CSP notation in an AST, but it’s easier for me to keep my original code rather than switch over.)
Sequence
CSP has two forms of sequencing. A semi-colon sequences two processes, whereas an arrow prefixes a process (right-hand side) with an event (left-hand side). My code for printing out a sequence of processes uses the arrow wherever possible, and a semi-colon otherwise:
type ProcEvents = Map.Map String (Set.Set String)
pprintCSP_Seq :: ProcEvents -> Spec' String String -> PP.Doc
pprintCSP_Seq m = PP.parens . PP.sep . p
where
p [] = [PP.text "SKIP"]
p (Sync c : xs) = [name c, PP.text "->"] ++ p xs
p [x] = [pprintCSP m x]
p (x:xs) = [pprintCSP m x, PP.text ";"] ++ p xs
The SKIP process does nothing, so it is used for blank lists and at the end of the list. Note that the singleton list [Sync x] will turn into x -> SKIP, whereas [Par xs] will not turn into xs ; SKIP (it will be merely xs). The ProcEvents parameter is used later on for printing out parallel composition and so must be passed around in case there are any nested parallel compositions.
Choice
External choice is handled by the first case of pprintCSP:
pprintCSP :: ProcEvents -> SpecItem' String String -> PP.Doc pprintCSP m (Alt s) = zeroOneMore m "STOP" (withOp m "[]") s
The helper functions are used to treat differently the case where the list is empty (in which case it uses the second parameter), has one item (in which case it is printed using pprintCSP_Seq), or has multiple items (in which case it is processed using the third parameter, which above joins the items with the external choice operator []):
withOp :: ProcEvents -> String -> [Spec' String String] -> PP.Doc withOp m op = PP.parens . PP.sep . intersperse (PP.text op) . map (pprintCSP_Seq m) zeroOneMore :: ProcEvents -> String -> ([Spec' String String] -> PP.Doc) -> [Spec' String String] -> PP.Doc zeroOneMore _ z _ [] = PP.text z zeroOneMore m _ _ [x] = pprintCSP_Seq m x zeroOneMore _ _ f xs = f xs
Parallel
When you compose two CSP processes in parallel, you must specify the events on which they synchronise. The process (a -> SKIP) [| {|a|} |] (a -> SKIP) will perform the event “a” once, with both sides of the parallel synchronising on event “a” together — that item in the middle is an infix parallel composition operator, parameterised by the singleton set containing “a”. In contrast, the process a -> SKIP [| {| |} |] a -> SKIP (which can be written more simply as: a -> SKIP ||| a -> SKIP) will perform the event “a” twice, with each side of the parallel doing it in turn — this is known as interleaving on an event.
In CHP, there is no support for interleaving; all events are synchronising. However, we cannot just put all events in the synchronising set. The process (a -> SKIP) [| {|a,b|} |] (b -> SKIP) will deadlock — each side tries to synchronise with the other on their respective events, which never happens. The solution is of course to use the intersection of the events that each side engages in:
pprintCSP m (Par xs) = zeroOneMore m "SKIP" joinPar xs
where
joinPar :: [Spec' String String] -> PP.Doc
joinPar [a] = pprintCSP_Seq m a
joinPar (a:bs) = PP.parens $ PP.sep $
[ pprintCSP_Seq m a
, pprintParOp (findAllComms eventName m a `Set.intersection`
unionAll (map (findAllComms eventName m) bs))
, joinPar bs
]
pprintCSP _ (Call p) = name p
pprintCSP _ x = error $ "pprintCSP: " ++ show x
pprintParOp :: Set.Set String -> PP.Doc
pprintParOp s
| Set.null s = PP.text "|||"
| otherwise = surround "[|{|" "|}|]" $ intersperse PP.comma $
map name (Set.toList s)
where
surround a b x = PP.sep $ [PP.text a] ++ x ++ [PP.text b]
The findAllComms does as its name suggests: it forms a set of all the communications performed anywhere in the process, using the supplied Map that we have been passing around to find out what communications are performed by named processes that are called. Note that as we compose parallel items together, we compose the head of the list using the intersection of all communications performed in the head, and all communications performed in the rest of the list (which will be the right-hand side of the parallel composition). So if you have three processes: [a -> b -> SKIP, b -> c -> SKIP, a -> c -> SKIP], they will get composed as:
(((a -> b -> SKIP)
[|{| a , b |}|]
((b -> c -> SKIP) [|{| c |}|] (a -> c -> SKIP))))
The first process synchronises on “a” and “b” with the others, as both feature somewhere later in the list. The second and third process only synchronise together on “c”; the events “a” and “b” are not shared, and thus occur separately, but synchronised with the first process.
Parallel Composition Omission
Basing the synchronisation sets on those events that are potentially performed has a problem. If a process is given a channel-end or barrier, but never uses it at all, the event will not show up in the model for that process, and thus will not be used in the synchronisation set. Let’s say you have a barrier, “b” with two processes enrolled, but one does not use it. Given those two processes, say “a ->SKIP” and “SKIP” they will be composed as “a ->SKIP ||| SKIP“, which will run fine — even though the original program would have deadlocked! The solution to this is to introduce extra code for tracking how many processes are involved in an event, and add dummy processes that have the events in their synchronisation set but never use them, thus reflecting the deadlock in the model. I haven’t yet implemented this just yet, though.
Summary
We have now seen how parallel composition is implemented, including determination of the synchronisation sets. In future parts of the guide, we will examine the remaining parts of CHP: channel communications, choice, and iteration, as well as how all these are put together.
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.
Processing without Buffering
While giving a talk last week, someone asked about obeying the arrow laws with CHP processes. The long and the short of it is that the arrow laws mean that arr id >>> arr id should be equivalent to arr id. But with the instance I have in chp-plus, the former is two processes and the latter one — and each process introduces one place of buffering. If you put in the same input you’ll get the same output with both, but with different buffering behaviour (this is already pointed out in the documentation). The same issue came up again later in the day with process fusion (more on that another time).
Extended Inputs
The way to resolve the problem of how much buffering to introduce is quite simple in retrospect: don’t introduce any buffering, anywhere. Then there is no issue of adding or removing it with the laws. We can easily eliminate buffering in CHP using extended input. Extended input means that when you read from a channel, you keep the writer waiting longer than usual, while the reader performs an extra action. The API in CHP is quite straightforward:
extReadChannel :: ReadableChannel r => r a -> (a -> CHP b) -> CHP b
The function takes an incoming channel end, an action to perform with the value, and then performs an extended input using your given action. Note that if you need the read value after the action, you’ll have to return it yourself as part of the “b” type.
Here is the relevant extended identity process, compared to the identity process (minus poison handling):
id, extReadId :: Chanin a -> Chanout a -> CHP () id = forever (readChannel input >>= writeChannel output) extReadId = forever (extReadChannel input (writeChannel output))
They share the same type but have slightly different behaviour. The key thing is that two of these extended identity processes composed next to each other have the same behaviour as one of these extended identity processes: extReadId <=> extReadId = extReadId. So if we build our arrow instance on these, we can avoid the buffering problem and fully obey the arrow laws.
Proof
This claim of identical behaviour can actually be proved using the FDR model checker for CSP. FDR doesn’t know about extended inputs, but an extended input can be formalised using a channel communication followed by an acknowledgement; the extended action takes place before the acknowledgement is sent. So here is the extended identity process from above in FDR script, parameterised by two pairs of data and ack channels:
EXTID(left, leftack, right, rightack)
= left?x -> right!x -> rightack?ack -> leftack!ack
-> EXTID(left, leftack, right, rightack)
FDR has an awkwardness that all its channels must be declared at the top-level, hence we declare the extra “middle” channels used to compose two of these processes at the top level:
datatype ACK = ack
channel midack2C : ACK
channel mid2C
EXTID2(left, leftack, right, rightack)
= EXTID(left, leftack, mid2C, midack2C)
[| {| mid2C, midack2C |} |]
EXTID(mid2C, midack2C, right, rightack)
\ {| mid2C, midack2C |}
The two composed processes synchronise together on mid2C and midack2C (but not the other channels). We then hide (backslash is hide) these events so that they are not visible outside. Without this hiding we would not have equivalence because some outside process could synchronise on mid2C and break everything; hiding makes sure these events are contained. All we then need are some more channel declarations and our assertions of equality:
channel leftackC, rightackC : ACK
channel leftC, rightC
assert EXTID(leftC, leftackC, rightC, rightackC)
[FD= EXTID2(leftC, leftackC, rightC, rightackC)
assert EXTID2(leftC, leftackC, rightC, rightackC)
[FD= EXTID(leftC, leftackC, rightC, rightackC)
The last two lines express refinement; you can think of this as expressing that one process is as general in its behaviour as another. The refinement operator is anti-symmetric, so expressing it twice in different directions like this is asserting equality of the two processes — a strong relationship. Putting all the above together we can run FDR and get the vital output:
This FDR release is for academic teaching and research purposes only. For any other use, please contact Formal Systems (Europe) Ltd at enquiries@fsel.com to obtain a commercial licence. Checking EXTID(leftC,leftackC,rightC,rightackC) [FD= EXTID2(leftC,leftackC,rightC,rightackC) ...snip true Checking EXTID2(leftC,leftackC,rightC,rightackC) [FD= EXTID(leftC,leftackC,rightC,rightackC) ...snip true
Inductively, if composing two extended identity processes together is the same as one extended identity process, any chain of N extended identity processes is equivalent to a single one. And the map process (on which the arrow instance is based) has the same communication pattern, so the result applies there too if we construct an extended map process: extMap f <=> extMap g = extMap (f.g)
Exploring a Communicating Sequential Processes EDSL
Translating Communicating Sequential Processes notation into program code
In my last post I showed the Communicating Sequential Processes (CSP) description of a pipeline of processes; here it is in full:
FULL(prev, next)
= FULL_WILLING(prev, next) |~| FULL_STATIONARY(prev, next)
FULL_WILLING(prev, next)
= prev.empty /\ next.move -> EMPTY (prev, next)
[] prev.move /\ next.move -> FULL (prev, next)
[] prev.empty /\ next.canstay -> FULL (prev, next)
[] prev.canstay /\ next.canstay -> FULL (prev, next)
[] prev.muststay /\ next.muststay -> FULL (prev, next)
FULL_STATIONARY(prev, next)
prev.empty /\ next.muststay -> FULL (prev, next)
[] prev.muststay /\ next.muststay -> FULL (prev, next)
[] prev.canstay /\ next.muststay -> FULL (prev, next)
EMPTY(prev, next)
= prev.empty /\ next.empty -> EMPTY (prev, next)
[] prev.muststay /\ next.empty -> EMPTY (prev, next)
[] prev.move /\ next.empty -> FULL (prev, next)
GENERATOR(next) = ON(next) ; OFF(next) ; OFF(next) ; GENERATOR(next)
ON(next) = next.move -> SKIP [] next.canstay -> SKIP
OFF(next) = next.empty -> SKIP
END(prev)
= prev.empty -> END(prev)
[] prev.muststay -> END(prev)
[] prev.move -> END(prev)
I can translate that into Haskell code that uses my CHP library fairly mechanically; here is a snippet:
site :: (Chanin Platelet, EnrolledBarrier, EnrolledBarrier, EnrolledBarrier)
-> (Chanout Platelet, EnrolledBarrier, EnrolledBarrier, EnrolledBarrier)
-> CHP ()
site (prevMove, prevEmpty, prevCanStay, prevMustStay)
(nextMove, nextEmpty, nextCanStay, nextMustStay)
= empty
where
fullWilling platelet = alt
[(syncBarrier prevEmpty <&> writeChannel nextMove platelet) >> empty
,(readChannel prevMove <&> writeChannel nextMove platelet) >>= full . fst
,(syncBarrier prevEmpty <&> syncBarrier nextCanStay) >> full platelet
,(syncBarrier prevCanStay <&> syncBarrier nextCanStay) >> full platelet
,(syncBarrier prevMustStay <&> syncBarrier nextMustStay) >> full platelet
]
Thankfully, CHP already allows us to get quite close to the original CSP, but it is still more verbose than the original. I wanted to see if I could get the code looking as much like the original CSP as possible, and this post details how I went about it.
Enter EDSLs
Many people have used Haskell as a host language for Embedded Domain Specific Languages. As far as I understand the term, an EDSL is where you craftily warp the host language to look like a completely different language with all sorts of frighteningly clever hacks. (I’m being very disingenuous to all the designers of very sensible and useful EDSLs, but for me the one that always springs to mind is Lennart Augustsson’s BASIC EDSL.) This post is my small foray into EDSLs, to get the CHP implementation looking as much like CSP as possible. I’m not sure that what I have is actually an EDSL, as it’s fairly specific to this particular piece of CSP, but these are at least EDSL-like techniques.
Cobbling together a CSP EDSL
I have a semantic hitch from the start. CSP’s “prev.move” can be viewed as a communication of the “move” value on the “prev” channel. If you take the latter view, the CSP code above is choosing between different messages on the same channel; something that is not possible in CHP (CML has it, but CML doesn’t have conjunction). So instead, we will have to implement the code as a group of events, where “prev.move” is a separate event to “prev.canStay”. There are four possible “sub-events” of prev and next (move, canStay, mustStay, empty) so we need a tuple of four events, with a different direction on the move channel for incoming platelets compared to outgoing platelets (CSP doesn’t have this notion of delineating direction); the remainder of the events can be symmetric two-party barriers:
type In = (Chanin Platelet, EnrolledBarrier, EnrolledBarrier, EnrolledBarrier) type Out = (Chanout Platelet, EnrolledBarrier, EnrolledBarrier, EnrolledBarrier)
Our implementation is going to add important features to the original CSP: we are going to keep track of information about the platelets (so if we are full, we know what we are full with) and we are going to report our status each time frame to a visualisation process. We will come back to that later, but this is why we have channels carrying the Platelet type. To access the latter three events of our quadruples, we use special accessor methods. We pick out the barriers and synchronise on them; CSP does not syntactically separate events and the synchronisation on them (we do in CHP to allow for poisoning, which CSP does not feature), so we shouldn’t here either:
canStay, mustStay, empty :: (a, EnrolledBarrier, EnrolledBarrier, EnrolledBarrier) -> CHP () empty (_, x, _, _) = syncBarrier x canStay (_, _, x, _) = syncBarrier x mustStay (_, _, _, x) = syncBarrier x
We want to be able to refer to the CSP event “next.canStay” using the identical CHP code “next.canStay”. If we look at the types, the first part, next, is our tuple of events, and canStay is an accessor on it. So we want to translate “next.canStay” into “canStay next”, effectively. So we hide the Prelude’s definition of the dot operator and redefine it to do just that:
(.) :: a -> (a -> b) -> b a . b = b a
These mechanisms work fine for the barriers; we will also need a way to use our channels. The difficulty here is that we want to refer to the channel (which will have a different type at each end) and in one the receiving instance access it as an implicitly-synchronising event (like the barriers above), and in the sending instance to leave it is some sort of value that we can then send a value on (borrowing CSP’s “!” operator for sending). So our accessor must be polymorphic both in its argument and return. Hence we need type-classes, with multiple parameters and functional dependencies:
class MoveConnector c r | c -> r where move :: (c, EnrolledBarrier, EnrolledBarrier, EnrolledBarrier) -> r instance MoveConnector (Chanin a) (CHP a) where move (c, _, _, _) = readChannel c instance MoveConnector (Chanout a) (Chanout a) where move (c, _, _, _) = c
This takes care of all that we need. “prev.move” will be of type CHP Platelet and “next.move” will be of type Chanout Platelet. Our ! operator is straightforward:
(!) :: Chanout a -> a -> CHP () (!) = writeChannel
The pieces of our jigsaw puzzle are almost there. Haskell’s >> sequence operator is already a close enough stand-in for CSP’s -> prefix operator, and the syntactic difficulties of using [] as the choice operator mean that CHP’s <-> will do instead. We will, however, use the CSPc /\ operator to mean the conjunction of the two events. We will return the value from the first of the two, because we only ever want to save the value we receive from the platelet before us (which always appears on the left-hand side of the conjunction in the CSP):
(/\) :: CHP a -> CHP b -> CHP a (/\) p q = fst <$> (p <&> q)
Now we can write our site process:
site :: Chanout (Maybe (Platelet, Bool)) -> In -> Out -> CHP ()
site obsOut prev next = emptySite
where
emptySite :: CHP ()
emptySite = obsOut!Nothing >>
((prev.empty /\ next.empty) >> emptySite)
<-> ((prev.mustStay /\ next.empty) >> emptySite)
<-> ((prev.move /\ next.empty) >>= full)
full :: Platelet -> CHP ()
full platelet
= do r <- liftIO $ randomRIO (0, 1::Double)
if r > 0.05
then obsOut!(Just (platelet, True)) >>
((prev.empty /\ next.move!platelet) >> emptySite)
<-> ((prev.move /\ next.move!platelet) >>= full)
<-> ((prev.empty /\ next.canStay) >> full platelet)
<-> ((prev.canStay /\ next.canStay) >> full platelet)
<-> ((prev.mustStay /\ next.mustStay) >> full platelet)
else obsOut!(Just (platelet, False)) >>
((prev.empty /\ next.mustStay) >> full platelet)
<-> ((prev.mustStay /\ next.mustStay) >> full platelet)
<-> ((prev.canStay /\ next.mustStay) >> full platelet)
The generator and end are also short:
plateletGenerator :: Out -> CHP ()
plateletGenerator out = forever $ on >> off >> off
where
on = do platelet <- Platelet <$> (liftIO $ randomRIO (0.5, 1))
(out.move!platelet) <-> (out.canStay)
off = out.empty
plateletEnd :: In -> CHP ()
plateletEnd prev = forever $ (prev.empty) <-> (prev.mustStay)
<-> (prev.move >> return ())
So we have implemented our CSP model, and made it look quite like the CSP itself. The behaviour is just as seen on previous videos, but now our sticky platelets are implemented tickless. There has been work before on compiling CSP by Fred Barnes, that supports a lot more features of CSP than the quick hacks shown here; this was just a fun exercise to get my code looking more like the CSP that it came from.
Sticky Platelet Pipeline — Finally Tickless
Tick and Tickless
A little while ago I posted an example of a simulation, with platelets moving down a pipeline together. When platelets bumped into each other, they stayed stuck together forever in a clot, and moved (or stayed put) together. The original code used a tick barrier, as many of my simulation examples do, to keep the simulation in lock-step. An alternative way to keep the simulation in lock-step is to make sure that every process in the pipeline communicates exactly once with its neighbours each timestep, which makes the tick barrier redundant. In this post I will show how to make my previous platelet example tickless, using this alternative method. I will be working in the formal Communicating Sequential Processes algebra, CSP (with a small extension); a Haskell implementation will follow in my next post.
The Ticking Version, in CSPc
We will start by looking at the ticking (original) version of the simulation in CSP. In fact, I will be using CSPc (CSP with conjunction); CSP doesn’t have the idea of conjunction in it, so I am using /\ as an added conjunction operator (akin to the logical conjunction operator) that conjoins two events into a single event that will occur when, and only when, both of its constituent events occur. All of the processes in this post are site processes: they represent a piece of space in the pipeline that does not move, and may or may not be occupied by a single platelet. A site that is occupied by a platelet is said to be full; otherwise it is empty. Let’s begin with the full site process:
FULL(prev, next) = FULL_WILLING(prev, next) |~| FULL_STATIONARY(prev, next)
The full process is making an internal choice between being willing to move this time-step and being stationary for the time-step. The internal choice means that FULL will make the decision itself and no other outside process (collectively referred to in CSP as its environment) can influence the decision. In our original Haskell implementation we made the choice randomly; a site would be stationary in 5% of the time-steps, and willing in the other 95% of time-steps. The stationary process refuses to do anything until the end of the time-step at which point it loops round to become the FULL process again:
FULL_STATIONARY(prev, next) = tick -> FULL(prev, next)
In contrast, the willing process offers two choices. It will move forwards if the process before it in the pipeline signals that is empty, or if the process before it in the pipeline is willing to move too. (So it will move if the process before it is empty, or full and willing, but not if the process before it is full and stationary.) We specify this using our conjunction operator:
FULL_WILLING(prev, next)
= prev.move /\ next.move -> tick -> FULL(prev, next)
[] prev.empty /\ next.move -> tick -> EMPTY(prev, next)
[] tick -> FULL(prev, next)
(/\ binds most tightly above, then ->, and [] binds least tightly.) This model is an accurate rendering of my original CHP program, but it contains a race hazard. It is possible that a site that is willing to move in a time-step does not do so and ticks instead; if all the sites in a clot (a contiguous group of full cells) were willing, they could just tick repeatedly and never move at all. The details of the CHP library’s implementation prevented this occurring in my original CHP program (and hence I did not realise there was a race hazard), but it is a sin to rely on a library’s implementation of synchronisation for your concurrent program to be correct. (If I had been able to model-check this code, I could have discovered this problem; see the summary at the end.) The problem could be removed if we gave priority to the movement event; see the previous discussion of priority on this blog and Gavin Lowe’s paper on implementing priority with a small extension to CSP.
The empty site is as long as the full site, but that is because it is repetitive:
EMPTY(prev, next)
= prev.move -> ((next.empty -> tick -> FULL(prev, next))
[] (tick -> FULL(prev, next)))
[] next.empty -> ((prev.move -> tick -> FULL(prev, next))
[] (tick -> EMPTY(prev, next)))
[] tick -> EMPTY(prev, next)
The empty site is willing to optionally accept a movement from behind it in the pipeline and/or signal to the process ahead of it that it is empty, before ticking. Like the full site, this again has the race hazard that it could tick without accepting the movement of a willing platelet from behind it.
To wire up our pipeline, we start with N EMPTY sites in a row (with the next event of each connected to the prev event of the following process as you would expect) synchronising on the tick event together with a GENERATOR at the beginning, but the END process does not need to synchronise on the tick event — the latter two processes being defined as follows:
GENERATOR(next) = ON(next) ; OFF(next) ; OFF(next) ; GENERATOR(next)
ON(next) = next.move -> tick -> SKIP
[] tick -> SKIP
OFF(next) = tick -> SKIP
END(prev) = prev.move -> END(prev)
The generator sends out a platelet every three steps (and again has the aforementioned problem that EMPTY and FULL have). The END process doesn’t need to synchronise on the tick event because it all it does is synchronise on move as frequently possible; the FULL process already rate-limits itself to one move event per time-step, so this is acceptable behaviour. In this ticking CSP version, we don’t really need this END process at all, but it’s instructive to include it because our tickless version will need one. The CSP up to this point makes up the full model of our original clotting program (minus the wiring, which isn’t very interesting).
The Tickless Version, in CSPc
The design of the tickless version is more complicated than the original version. In a simulation with a tick event, we can use implicit signalling. Each process will offer to perform some actions, then eventually it must agree to synchronise on the tick event (if all the processes didn’t eventually tick, we’d get deadlock!). So you can gain information if you offer a choice of event A with your neighbour, or tick with everyone, and the tick happens. This means that your neighbour did not choose to offer event A to you before it offered tick. We often use this implicit information in the simulation. In the previous platelets code, a full site not willing to move would not offer a movement, and would wait for a tick. A full site willing to move would offer to move with its neighbours, but if tick happened instead, it knew that one of its neighbours was not willing to move, and they had implicitly agreed to stay put by synchronising on tick instead. (The idea is good, but my use of it above led to the problem where willing platelets may not end up moving — this can be solved in the tickless version, though.)
If we want to remove the tick event from our pipeline, we therefore have to add more events between the processes, to allow them to explicitly communicate what they used to implicitly communicate. Peter Welch suggested a possible solution — but he saw that his suggestion had the problem now revealed in the original version, mentioned above. I was able to improve on his idea to remove the problem, and I describe my improvement to his solution here. The tickless version involves introducing two new events (besides move and empty) that indicate further information: canstay and muststay.
If there was only one stay value, then that is all that full stationary sites would offer. But willing full sites would also have to offer to stay, in order to synchronise with stationary neighbours (if one platelet in the clot stays they all must). So all willing sites would offer to stay, and this could allow a clot of willing platelets to agree to stay even though they were all willing to move. This is the same problem as we had in our ticking version. To remove the problem, we differentiate the events offered by a full stationary site (who will offer muststay) and a full willing site (who will offer canstay). Here is how they are used in the new FULL_WILLING process:
FULL_WILLING(prev, next)
= prev.empty /\ next.move -> EMPTY (prev, next)
[] prev.move /\ next.move -> FULL (prev, next)
[] prev.empty /\ next.canstay -> FULL (prev, next)
[] prev.canstay /\ next.canstay -> FULL (prev, next)
[] prev.muststay /\ next.muststay -> FULL (prev, next)
The first two cases are just as before, in the original version. The middle case is for when the process is at the beginning of the clot; it synchronises on empty with the process behind it, and canstay with the process ahead of it in the clot. The last two cases can be thought of as perpetuating the canstay/muststay event through the pipeline.
The new FULL_STATIONARY process is as follows:
FULL_STATIONARY(prev, next)
prev.empty /\ next.muststay -> FULL (prev, next)
[] prev.muststay /\ next.muststay -> FULL (prev, next)
[] prev.canstay /\ next.muststay -> FULL (prev, next)
The first case is for if this process is at the beginning of the clot; it synchronises on empty with the process behind it, and muststay with the process ahead of it. Looking up at the FULL_WILLING process, we can see that any FULL_WILLING process (from the last case) and any FULL_STATIONARY process (from the middle case immediately above) that synchronises on muststay with the process behind it will also synchronise on muststay with the process ahead of it. So if the process at the start of the clot synchronises on muststay, all processes ahead of it in the clot will also synchronise on muststay (by induction).
The third case of the FULL_STATIONARY process indicates that the processes behind the stationary one may offer canstay, and it will then offer muststay to all the processes ahead of it. The canstay event will only be offered from the previous process if it is in the FULL_WILLING state (FULL_STATIONARY only offers muststay to the process ahead of it, and we will see shortly that EMPTY only offers empty to the process ahead of it), which must then synchronise either on canstay with the process behind that (which, again, must be a FULL_WILLING process) or empty (which means it’s the start of the clot). All the full processes after FULL_STATIONARY, following the logic in the previous paragraph, will synchronise on muststay regardless of their state.
The new EMPTY process is as follows:
EMPTY(prev, next) = prev.empty /\ next.empty -> EMPTY (prev, next) [] prev.muststay /\ next.empty -> EMPTY (prev, next) [] prev.move /\ next.empty -> FULL (prev, next)
All cases offer the empty event to the process ahead of it. It will accept from behind: the empty case (when the previous site is empty), the move case (when the previous site is full and able to move forward) and the muststay event (when the previous site is part of a clot that cannot move). It does not accept the canstay event, which is crucial, for reasons explained in the next section.
The new ON, OFF and END processes are:
ON(next) = next.move -> SKIP [] next.canstay -> SKIP OFF(next) = next.empty -> SKIP END(prev) = prev.empty -> END(prev) [] prev.muststay -> END(prev) [] prev.move -> END(prev)
You can think of as ON as being the “forward half” of a FULL_WILLING site that is receiving empty from behind it; similarly, OFF is the forward half of an EMPTY site and END is the “backward half” of an EMPTY site.
Proofs
Since conjunction is an extra feature in CSP, there is no direct model-checking support for it. (We have designed a mapping from CSPc to CSP, but that causes a state space explosion and does not yet have automated tool support.) I will offer instead, inductive proofs about clots. By proving a statement for the beginning site, and optional middle/end sites based on the neighbour behind them, this should inductively cover all non-empty clots. This can be done by considering the pairings of prev and next events, to see when offering a set of events from the previous site, what might be offered to its next neighbour.
So, let us consider a clot of willing platelets. The site at the beginning of the clot can only synchronise on prev.empty (as that is all the empty site before it will offer). Therefore the site at the beginning of a clot will only offer move or canstay to the next site. Any middle site that synchronises on move or canstay with the previous site will offer the same thing to the next site. So inductively the last site of the clot will only offer move or canstay. We can see that the empty site following the clot will only accept move, not canstay, so a clot of willing processes may only move and may not stay put. This solves the problem that we had with the ticking version, and is why the EMPTY process does not offer to synchronise on canstay. (This result also shows that any line of sites at the beginning of a clot will only offer move or canstay to the sites ahead of it.)
Now let us consider a clot with one or more stationary platelets somewhere along its length (but not the beginning). We have seen in the previous paragraph that the willing sites at the beginning of the pipeline will offer move or canstay to the first stationary site in the clot. This stationary site appearing after these willing sites will only accept canstay, and will then offer muststay ahead of it. We can see that all full sites, stationary and willing, will only synchronise on prev.muststay with next.muststay, so regardless of the stationary/willing state of sites ahead of the first stationary site, muststay will be the event offered at the end of the clot. The empty site will accept this, and so a clot with one or more stationary sites after the beginning will all agree to stay. If a stationary site is at the beginning, it will synchronise on prev.empty and next.muststay, and then the rest of the clot will also synchronise on muststay, so again the clot will stay put. Thus any clot with one or more stationary sites will stay put.
Summary
So we have a system, expressed in a few lines of CSPc, of a sticky platelet simulation without a tick event. I will show a translation to CHP in the next post, which works the same as the original version (minus the potential problem). This work is interesting from a formal perspective because we have no direct support to model check this CSP, due to the conjunction extension. We have devised a mapping from CSPc to CSP, but it generates a large number of events; I believe it would be in the order of 4^N for this problem. We don’t have a tool to generate the CSP just yet, and even if we could, I suspect the model checker may choke on that size of problem. However, by taking advantage of conceptual features of the simulation, namely clots, I was able to perform some inductive reasoning about the problem. The reasoning was aided by the neat symmetry of the problem; each site in the pipeline offered a pair of (prev, next) events in conjunction, which could be thought as a sort of normal form.
From a practical perspective, it can be seen that this is not really a very concurrent simulation. The chained conjunction along the pipeline means that all processes must resolve their actions for the time-step together, and really the power of the simulation is in the resolution of all the choices (which could be written as a single sequential/functional piece of code: transforming the list of all platelets at time-step T to the list of all platelets at time-step T+1), not in the concurrency of the sites. The advantage of the way we constructed our solution is that we have encoded the behaviour of each site by only referring to the two neighbours of a site. These are local rules, that when resolved for all sites, produce the emergent behaviour of sticky platelets bumping, forming clots, and advancing down the pipeline together. There is no global visibility of the system in our code (only in the run-time system) to complicate things. This investigation of emergent behaviour is part of the ongoing CoSMoS research project that uses process-oriented technologies to produce this kind of simulation, and which builds on the original work of the TUNA project from which this blood clotting example is taken.
The Operators and Monoids of CHP
When we create binary operators, in mathematics or in programming, they often have certain common identifiable properties:
- If you can re-order the arguments, e.g. 1 + 2 is the same as 2 + 1, we say that it is commutative — in contrast, division is not commutative.
- If you have two applications of the operator and the order of evaluation/bracketing doesn’t matter, e.g. (1 + 2) + 3 is the same as 1 + (2 + 3), we say that it is associative — in contrast, subtraction is not associative.
- If one particular operand always leaves the other side unchanged, we can say that this is the unit of an operator, e.g. 1 * x is the same as x, so 1 is the unit of multiplication.
- If one particular operand always ignores/overrides the other, we can say that this is the zero of an operator, e.g. 0 * x is the same as 0, so 0 is the zero of multiplication.
- If an operator has a unit or zero that only works on one side of the operator, we name it accordingly. For example, we say that division has a right-unit of 1 (because x / 1 is the same as x), but it does not have a left-unit; there is no value k such that for all x, k / x is the same as x.
We can find these properties all over maths and programming. Set union is commutative, associative, and has a unit of the empty set, but no zero. The boolean AND operator is commutative, associative, has the unit “true” and the zero “false”. STM’s orElse combinator is associative, with the unit retry, and the left-zero of a return statement. Any operator that is associative and has a unit forms a monoid, which can be put into Haskell as an instance of the Monoid type-class (more on that below).
The operators in CHP also have some of the aforementioned properties. A full list is buried at the back of the tutorial, but I should probably pull them into the API documentation. (Note that the laws I discuss here are concerned with the behavioural semantics of the operators; the types of the expressions may differ trivially.) The parallel operator <||> is commutative and associative, with a unit of skip, the process that does nothing and returns successfully. The unprioritised choice operator <-> is commutative and associative, with a unit of stop, the process that is never ready in a choice. The implication of choice and parallelism being associative and commutative is that the order of the items in a call to alt or runParallel doesn’t make any difference to the behaviour. The operators for wiring up a pipeline in the Utils module are associative but lack the other properties.
Poison Handler Properties
We can view the poison handlers `onPoisonTrap` and `onPoisonRethrow` as binary operators. To recap: `onPoisonTrap` runs the left-hand side, but if a poison exception occurs then the right-hand side is run. `onPoisonRethrow` does the same, but after the right-hand side has finished, the poison exception is rethrown. They are not commutative — in exception terminology, the first argument is the try and the second the catch; they cannot be swapped freely!
To my surprise, `onPoisonTrap` is associative. Abbreviating it to `oPT`, consider p `oPT` q `oPT` r. If you bracket the first two items, (p `oPT` q) `oPT` r, q will only execute if p throws poison, and r will only execute if q then throws poison (because p’s poison is trapped, so the only poison that can escape the first bracket is from q). If you bracket the latter two, p `oPT` (q `oPT` r), the brackets will only execute if p throws poison, which will pass control to q, which will only pass control to r if poison is thrown by q. So the semantics are associative.
In contrast, `onPoisonRethrow` is not associative. Abbreviating it to `oPR`, consider: p `oPR` skip `oPR` r. If bracketed (p `oPR` skip) `oPR` r, r will be executed if p poisons, but if bracketed p `oPR` (skip `oPR` r), r will never be executed (because skip won’t throw poison).
`onPoisonTrap` has a left-unit of throwPoison (because throwing poison automatically transfers control to the other side, the handler), and a right-unit of throwPoison (because trapping poison then throwing poison has a null effect on the original code). `onPoisonRethrow` has no left-unit but has two right-units: throwPoison and the return statement. Any code that cannot throw poison (e.g. a return statement) is a left-zero of both `onPoisonTrap` and `onPoisonRethrow` because it will never trigger the handler. Neither operator has a right-zero; there is no handler that can cause the original code to always be ignored.
Monoids
The fact that some of the operators mentioned here are associative and have units mean that they could form a monoid. In fact, CHP blocks of code could form several monoids. In Haskell, there is the problem that the monoid instance must be uniquely identified by its type, even though it is really its operator that is distinctive. All the standard number types can form a Monoid in addition (unit: 0, operator: +) or multiplication (unit: 1, operator: *). Defining a Monoid instance for, say, Int would thus be ambigious: when you say 4 `mappend` 3, would you expect 7 or 12? To solve this, the Data.Monoid module defines newtype-wrappers around types to identify the monoid. Sum Int is a monoid in addition, whereas Product Int is a monoid in multiplication.
I could use the same trick for CHP; I could define several monoid instances. Here is a monoid that allows blocks of code (with no useful return) to be joined in parallel:
newtype Par = Par {runPar :: CHP ()}
instance Monoid Par where
mempty = Par skip
mappend p q = Par (runPar p <|*|> runPar q)
mconcat = Par . runParallel_ . map runPar
This could be made a little more useful by making a parallel monoid out of blocks of code that return a type that is itself a monoid; when the parallel blocks of code have all finished, their results are combined using the monoid instance:
newtype ParMonoid a = ParMonoid {runParMonoid :: CHP a}
instance Monoid a => Monoid (ParMonoid a) where
mempty = ParMonoid (return mempty)
mappend p q = ParMonoid
(liftM (uncurry mappend) $ runParMonoid p <||> runParMonoid q)
mconcat = ParMonoid . liftM mconcat . runParallel . map runParMonoid
There is also a straightforward monoid instance for choice between blocks:
newtype Alt a = Alt {runAlt :: CHP a}
instance Monoid (Alt a) where
mempty = Alt stop
mappend a b = Alt (runAlt a <-> runAlt b)
mconcat = Alt . alt . map runAlt
Finally, there is a monoid built around `onPoisonTrap`:
newtype PoisonTrap a = PoisonTrap {runPoisonTrap :: CHP a}
instance Monoid (PoisonTrap a) where
mempty = PoisonTrap throwPoison
mappend a b = PoisonTrap (runPoisonTrap a `onPoisonTrap` runPoisonTrap b)
Consider the meaning of mconcat (map PoisonTrap [p,q,r,s]). It says run p; if no poison is thrown, that’s done. If poison is thrown, run q. If q throws poison, run r, and if that throws a poison, run s. Obviously this is quite excessive, but I had never thought of constructing such a function until I realised that `onPoisonTrap` was associative and thus could form a monoid.
I can’t recall seeing monoid instances like these (involving monadic actions), so perhaps these sorts of monoid instances on monads don’t end up being very useful (if you know of a particular use, please add a comment below). I find it interesting to see how CHP code can form several different monoids just as an exercise.
Communicating Haskell Processes 