A Tutorial for Session Types, Part 3
This is the third part of this multi-part tutorial in which I hope to explain quite how my Session Types implementation can be used.
Contents
- Part 1: Making Session Types
- Part 2: Using Session Types
- Part 3: Advanced Functionality; you are here!
Pids, forking, creating channels and multi-receive
It's pretty limiting if all you can do is create new threads to run implementations of single (or perfectly nested) Session Types. It really won't be very long before you want a single thread that's able to handle a number of channels and interleave actions across them. Furthermore, you really want to be able to communicate Pids or Process IDs and then use a Pid to create a new channel between you and that Pid. Finally, once you've got a set of open channels, you really want some kind of receive construct that is capable taking a subset of those channels and blocking until one of them has some value ready for you to receive, thus allowing you to respond to the first available channel.
All of these features are catered for and these are the subject of this installment.
Pids
A Pid contains a number of pieces of information about another process. Firstly it contains a unique ID. If you're at all familiar with Erlang, then the IDs will be at least slightly familiar to you. However, the actual ID is of very little use so I'll move on. The main piece of information that a Pid contains is a list of all the Session Types that the process indicated by the Pid is prepared to take part in. Now sadly, this is not a perfect piece of information, as the list can change dynamically (it can shrink), for the following reasons.
If you have the Pid of another process, you don't really know what that process is up to. You may have some information about it, but its true state is dependent on many things, for example, the scheduler. It may actually be that that process has already died, or it may be that it's been created but not yet run at all, you really don't know, and there's no way for that process to change the type of the Pid you hold in order to make you more aware.
Thus the list of Session Types that the Pid contains is the biggest that the list could be. I.e. it's the list of Session Types that the process is aware of at the point at which the process is created. It may well be that if you try to create a channel with that process that it will never answer your call as it's already gone down some path which prevents it from ever agreeing to your request. But if you try to create a channel to a process, then you can only do so if that process knows about the Session Type you're trying to use for the new channel. So you get some guarantees, but certainly further analysis beyond what I can do with GHC is necessary to give stronger guarantees.
Finally, note that every Pid uses the same Session Type - there is simply one large Session Type which is propagated everywhere. What actually varies are the indexes of the fragments that a Pid is prepared to start a channel at. We'll come back to Pids in little while.
Interleaving
Before we get as far as throwing Pids about and creating new channels to existing Pids, let me show you how to interleave actions on channels. Put simply, you have an SMonad wrapping around a list of SMonads. Then you choose which inner SMonad (i.e. channel) you want to work on and do so. So how do you build up this list?
fork takes four arguments:
- The index of the fragment within the Session Type that you want
the channel to start at. Recall that
runat the end of tutorial 2 took an index to the fragment to start at, well it's all the same idea as that. - To dual or not to dual. Are you going to implement the
fragment as it's defined (and thus the child will implement the dual),
or are you going to implement the dual and the child will implement
the fragment as defined? Use
TTif you're going to implement the dual andFFif you're going to implement as written. - The index list. The child has a Pid. That Pid must contain some
sort of list of Session Types that the Pid is willing to take part in
(or as is actually the case, a list of indexes into the
Session Type). If an index isn't in this list then the child cannot
create a channel at the given index. Note that this is solely for the
use of
createSession, covered below, and not for the use offork. Also, the indexes are actually tuples containing the index and theTTorFFto indicate whether the Pid is willing to deal with the fragment as written, or the dual of the fragment. - The child implementation. This is the function which will be run in a new thread. It receives two arguments: firstly the channel to its parent and secondly the Pid of its parent.
fork returns to you a tuple containing the channel to
the child and the Pid of the child. So, let's see this in action!
test = runInterleaved nil st master
where
st = cons (SendInt ~> SendInt ~> RecvBool ~> end) $
cons (SendBool ~> RecvBool ~> end)
nil
childA parentCh parentPid
= (sliftIO . putStrLn $ "ChildA is alive!") ~>>
withChannel parentCh srecv ~>>= \x ->
withChannel parentCh srecv ~>>= \y ->
withChannel parentCh (ssend (x == y))
childB parentCh parentPid
= (sliftIO . putStrLn $ "ChildB is alive!") ~>>
withChannel parentCh (ssend True ~>>
srecv ~>>=
sliftIO . putStrLn . (++) "ChildB received a Bool: " . show
)
master
= fork (D0 E) FF nil childA ~>>= \(aCh, aPid) ->
fork (D1 E) TT nil childB ~>>= \(bCh, bPid) ->
withChannel aCh (ssend 5) ~>>
withChannel bCh srecv ~>>= \boolB ->
(if boolB
then withChannel aCh (ssend 6 ~>> srecv)
else withChannel aCh (ssend 5 ~>> srecv)
) ~>>= \boolA ->
withChannel bCh (ssend (boolA && boolB)) ~>>
(sliftIO . putStrLn $ "Master has finished. Bye bye.")
This demonstrates all of the above. Firstly we have the Session
Type itself, st. We have definitions for two children,
and we have the definition of the master, or root process. Finally, we
have test which runs the whole thing. In a very similar
way to fork, runInterleaved takes a list of
(index, dual) tuples which sets the list of fragments in the Pid of
the root process. This explains what the nil is doing
there. It also takes the Session Type for the entire tree of processes
and the function that is the root process.
master starts by creating two children. Note that for
childA, master states that
master will do the (D0 E) fragment as
written which means childA will do the dual. However, for
childB, master states that it will do the
dual of the (D1 E) fragment, thus childB
must do the fragment as written.
master then just continues to use the two channels to
the two children, interleaving actions through the use of
withChannel. Note that both inside and outside
withChannel we're in SMonad instances
(though different ones), so the combinators are the same, and
sliftIO (and the rest) all work as expected.
childA starts up receiving the channel to the parent
(parameterised by the dual of the (D0 E) fragment) and
the Pid of its parent and then does some work. Note that
childA could have been written as: withChannel
parentCh (srecv ~>>= \x -> srecv ~>>= \y -> ssend (x
== y)) - it makes no difference at all.
childB similarly makes use of its channel to the
parent.
So hopefully, it should be clear how interleaving works and you're getting more comfortable with the idea that there is one global Session Type and it's referred to by an index and a weird sort of boolean value indicating whether you're working on the fragment as written or its dual. This still has limitations though, in particular, how can you send Pids around and use them to create new channels? Without this, all you can do is create trees of processes where communications can only flow up and down the trees.
Working with Pids
Sadly, Pids are a little bit of a special case. When specifying
sending or receiving a Pid in a Session Type you can't just use
Send or Recv. If you do (and you manage to
get the type of the Pid right!), you'll get GHC exploding with an
infinite type problem. So, there are a couple of "special" functions
for specifying the communication of Pids: sendPid and
recvPid. Note that this only exists when specifying
Session Types - in the implementation you use ssend and
srecv as normal.
By now you've probably been able to predict that
sendPid and recvPid are going to take lists
of (index, dual) tuples. You're right. So, we could specify a Session
Type as follows:
st = cons (sendPid (cons ((D1 E), FF) nil) ~> end) $
cons (SendInt ~> end)
nil
Thus the fragment at (D0 E) says that a Pid must be
sent, and that the process indicated by the Pid may be willing to take
part in a channel parameterised by the fragment at (D1 E)
as written. Which means that if you receive that Pid, you may use it
to try and create a channel where you are using the dual of the
fragment at (D1 E): i.e. RecvInt ~> end. So
let's implement that:
test = runInterleaved (cons ((D1 E), TT) nil) st master
where
st = cons (sendPid (cons ((D1 E), FF) nil) ~> end) $
cons (SendInt ~> end)
nil
master
= fork (D0 E) TT (cons ((D1 E), FF) nil) child ~>>= \(childCh, childPid) ->
withChannel childCh srecv ~>>= \childPid' ->
createSession (D1 E) TT childPid' ~>>= \chA ->
createSession (D1 E) TT childPid ~>>= \chB ->
withChannel chA (srecv ~>>= sliftIO . putStrLn . (++) "Received on chA: " . show) ~>>
withChannel chB (srecv ~>>= sliftIO . putStrLn . (++) "Received on chB: " . show) ~>>
sreturn ()
child parentCh parentPid
= myPid ~>>= \me ->
withChannel parentCh (ssend me) ~>>
createSession (D1 E) FF parentPid ~>>= \chA ->
createSession (D1 E) FF parentPid ~>>= \chB ->
withChannel chA (ssend 10) ~>>
withChannel chB (ssend 20)
So, runInterleaved specifies that the Pid of
master will contain ((D1 E), TT). That's
good news, because it means that master can call
createSession (D1 E) TT somePid provided that
somePid contains ((D1 E), FF). Now the Pid of
child just happens to be that way inclined as you can see
from the call to fork in master.
So what actually happens here is that master forks off
child. Child then gets its own Pid (myPid is
provided for this purpose) and sends its own Pid to its parent. Note
that the call to fork says that master is
doing the dual of (D0 E) - i.e. it will receive a Pid
parameterised by ((D1 E), FF) (note that the library is
very careful about making sure these dual booleans always refer to the
original Session Type as written), which is exactly what it gets. Of
course, master already has the Pid of child,
but it gets a second copy anyway. Just to prove they are both the
same, it uses each one in calls to createSession. This is
really the same idea as fork except instead of suppling a
list of indexes and an implementation, you just specify the
Pid. Because we know that the child will do the
((D1 E), FF) side of things, the master must
do the ((D1 E), TT) side of things which is exactly what
happens. The child mirrors the creation of the two new
channels and sends two numbers to the master which are
received and printed out.
Note that createSession is a synchronous operation. It
will block until the process indicated by the supplied Pid performs
the reciprocal call.
Also note that the ability to specify indexes in the Session Type for the communication of Pids is very useful when Pids refer to each other. Consider:
st = cons (sendPid (cons (D1 E, FF) nil) ~> end) $
cons (sendPid (cons (D0 E, FF) nil) ~> end)
nil
I.e. the Pid that will be sent in D0 E will
participate in sessions in which it will send the Pid indicated in
D1 E. And that Pid is prepared to participate in
sessions in which it will send the Pid indicated in D0
E. And that Pid... Yes, stuff like this will slowly
break your head, and you really need to draw out what points to
what. But it is actually pretty useful.
Multi-receive
Finally, we get to multi-receive. It is often the case that you
have a set of channels open and the next action on all of them is some
sort of Recv. You don't know which one will be ready
first, and you know that if you block waiting on the wrong one then
you can get a deadlock. So you want a multi-receive construct which
will block until any of those channels becomes ready to
srecv on.
multiReceive is just like soffer in that
it takes a list of continuations. In this case, each list element is a
tuple, where the left hand side is a channel and the right hand side
is a function. The function will be called if that channel is the
first channel to become ready. Let's see it in action:
test aDelay bDelay = runInterleaved nil st master
where
st = cons (SendInt ~> end) nil
master
= fork (D0 E) TT nil (child aDelay) ~>>= \(aCh, _) ->
fork (D0 E) TT nil (child bDelay) ~>>= \(bCh, _) ->
multiReceive ( (aCh, receive "A" aCh ~>> receive "B" bCh)
~|||~
(bCh, receive "B" bCh ~>> receive "A" aCh)
~|||~
MultiReceiveNil
)
receive str ch
= withChannel ch (srecv ~>>=
sliftIO . putStrLn .
(++) ("Master received from child " ++ str ++ ": ") . show)
child delay parentCh _
= (sliftIO . threadDelay $ delay) ~>>
withChannel parentCh (ssend delay)
Yes, we now have (~|||~) as well as
(~||~) and (~|~)! So master
creates two children which are both parameterised by different values,
supplied through test. They sleep for that number of
microseconds before replying. master just wants to get
the responses as quickly as possible so it uses
multiReceive. If the aCh becomes ready
first, it receives on aCh first and then on
bCh. Otherwise the other way round. So the values to
aDelay and bDelay will control the order in
which the print expressions get executed:
*Tests> test 1000000 100
Master received from child B: 100
Master received from child A: 1000000
*Tests> test 100 1000000
Master received from child A: 100
Master received from child B: 1000000
Again, every function in the list to multiReceive must
perform the same actions, just they can do it in different orders: the
state of all the channels must be the same at the end of every
function in the multiReceive list.
Some conclusions
Hopefully, these three articles have gone some way to explaining how to use this library. One of the problems with abusing the Haskell type system to this extent is that the type signatures become huge: there's a reason why there are no type sigs in these articles. The other problem is that when you make a mistake, the error messages are enormous and often fairly unhelpful: you're normally much better off thinking for a few seconds about what might be wrong rather than trying to parse a few thousand lines of error message.
I am very keen to receive feedback. You probably already know my
email address, given this domain, and my name's Matthew, you should
hopefully be able to put the two together and contact me. Otherwise, I
tend to sit on #haskell on freenode.net. If
you have problems, thoughts, comments etc, I'd be very happy to
receive them. Many thanks.