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.