Event Synchronization by Lightweight Message Passing

arXiv:0805.4029v1 [] 27 May 2008

Avik Chaudhuri
Computer Science Department
University of California, Santa Cruz
avik@cs.ucsc.edu

Abstract. Concurrent ML’s events and event combinators facilitate modular concurrent programming with first-class synchronization abstractions. A standard
implementation of these abstractions relies on fairly complex manipulations of
first-class continuations in the underlying language. In this paper, we present a
lightweight implementation of these abstractions in Concurrent Haskell, a language that already provides first-order message passing. At the heart of our implementation is a new distributed synchronization protocol. In contrast with several
previous translations of event abstractions in concurrent languages, we remain
faithful to the standard semantics for events and event combinators; for example,
we retain the symmetry of choose for expressing selective communication.

1 First-class synchronization abstractions
In his doctoral thesis [12], Reppy invents the concept of first-class synchrony to facilitate modular concurrent programming in ML. He argues:
Unfortunately there is a fundamental conflict between the desire for abstraction and the
need for selective communication [in concurrent programs]. . . . To resolve the conflict
. . . requires introducing a new abstraction mechanism that preserves the synchronous
nature of the abstraction.

Thus, Reppy introduces a new type constructor event to type synchronous operations
in much the same way as → (“arrow”) types functional values.
This allows us to represent synchronous operations as first-class values, instead of
merely as functions . . . [and design] a collection of combinators for defining new event
values [from primitive ones]. . . . Selective communication is expressed as a choice among
event values, which means that user-defined abstractions can be used in a selective
communication without breaking the abstraction.

Reppy implements events in an extension of ML, called Concurrent ML (CML) [13],
and provides a formal semantics for synchronization of events [12]. While the implementation itself is fairly complex, it allows programmers to write sophisticated communication and synchronization protocols as first-class abstractions in the resulting language. Next, we provide a brief introduction to CML’s events and event combinators.
The interested reader can find a more detailed account of first-class synchrony and its
significance as a programming paradigm for concurrency in [13].
In particular, note that channel and event are polymorphic type constructors in
CML, as follows:

– The type channel τ is given to channels that carry values of type τ .
– The type event τ is given to events that return values of type τ on synchronization.
The combinators receive and transmit can build primitive events for synchronous
communication.
receive : channel τ → event τ
transmit : channel τ → τ → event ()
– receive c returns an event that, on synchronization, accepts a message M on channel c and returns M . Such an event must synchronize with transmit c M .
– transmit c M returns an event that, on synchronization, sends the message M on
channel c and returns () (“unit”). Such an event must synchronize with receive c.
The combinator choose can non-deterministically select an event from a list of events,
so that the selected event can be synchronized. In particular, choose can express any
selective communication.
The combinator wrapabort can specify an action that is spawned if an event is not
selected by a choose.
choose : [event τ ] → event τ
wrapabort : (() → ()) → event τ → event τ
– choose V returns an event that, on synchronization, synchronizes one of the events
in list V and “aborts” the other events.
– wrapabort f v returns an event that, on synchronization, synchronizes the event
v, and on abortion, spawns a thread that runs the code f (). Here, if v itself is of
the form choose V and one of the events in V is selected, then v is considered
selected, so f is not spawned.
The combinators guard and wrap can specify actions that are run before and after
synchronization, respectively.
guard : (() → event τ ) → event τ
wrap : event τ → (τ → τ ′ ) → event τ ′
– guard f returns an event that, on synchronization, synchronizes the event returned
by the code f (). Here, f () is run every time a thread tries to synchronize guard f .
– wrap v f returns an event that, on synchronization, synchronizes the event v and
applies function f to the result.
Finally, the function sync can synchronize an event and return the result.
sync : event τ → τ
Note that by construction, an event can synchronize at exactly one “commit point”,
where a message is either sent or accepted on a channel. This commit point may be
selected among several other, potential commit points. Some code may be run before
synchronization, as specified by guard functions throughout the event. Some more code
may be run after synchronization, as specified by wrap functions that surround the
commit point, and by wrapabort functions that do not surround the commit point.

Reppy’s implementation of synchronization involves fairly complex manipulations
of first-class continuations in phases [13]. Even the channel communication functions
accept : channel τ → τ
send : channel τ → τ → ()
are derived by synchronization on the respective base events.
accept c = sync (receive c)
send c M = sync (transmit c M )
In contrast, in this paper we show how to implement first-class event synchronization
in a language that already provides first-order synchronous communication. Our implementation relies on a new distributed synchronization protocol, which we formalize as
an abstract state machine and prove correct (Section 2). We concretely implement this
protocol by message passing in Concurrent Haskell [8], a language that is quite close to
the pi calculus [11]. Building on this implementation, we present an encoding of CML
events and event combinators in Concurrent Haskell (Sections 3 and 4).
We are certainly not the first to encode CML-style concurrency primitives in another
language. However, a lightweight implementation of first-class event synchronization
by message passing, in the exact sense of Reppy [12], has not appeared before. We defer
a more detailed discussion on related work to Section 6.
Before we present our protocol, we introduce its main ideas through the following
(fictional) narrative, which describes an analogous protocol for arranging marriages.
In the Land of Frı̄g, there are many young inhabitants who are eager to get
married. At the same time, the rivalry among siblings is so fierce that if a
young man or woman gets married, his or her siblings commit suicide. There
are many priests, who serve as matchmakers. Eager young inhabitants flock to
these matchmakers to meet prospective partners of the opposite sex. When two
such partners meet, they reserve the priest who matches them, and then inform
their parents. Meanwhile, the priest stops matching other couples.
Parents select the first child to inform them about meeting a partner, and
send their approval to the concerned priest. For all other children who are too
late, on the other hand, they send back their refusal. If a priest receives approval
from both parties, he confirms the marriage date to both sides; following this
information, the couple weds. If one party refuses and the other approves, the
priest alerts the approving side that the impending marriage must be canceled;
following this information, the young members of that family begin searching
for partners once again. The priest now resumes matching other couples.
Obviously, we would like to have progress in the Land of Frı̄g—weddings should be
possible as long as there remain eligible couples. Can we prove this property? Yes. We
first prove the following lemma: if there remain two inhabitants of opposite sex who are
looking for partners, a priest can eventually match them. Indeed, pick any priest. Either
that priest is free, or two partners who have already met have reserved that priest. In the
latter case, both partners inform their parents; both parents send their decisions to the
priest; therefore, the priest is eventually free.

Now, suppose that there remain two inhabitants A and B of opposite sex who are
looking for partners. Then (by the lemma above) a priest eventually matches them. Next,
A and B inform their parents. Now, if both A and B are the first among their siblings to
inform their parents, they eventually get married and we are done. On the other hand,
suppose that one of A’s siblings informs A’s parent first. (Clearly, that sibling could not
have been married when A was looking for partners, since otherwise, A would have
been dead, not looking for partners.) Now, either that sibling gets married, and we are
done; or, that sibling does not get married, and A tries again. Similarly, either one of B’s
siblings gets married and we are done, or B tries again. Now, if A and B both try again,
they can be the first among their siblings to inform their parents; so, they eventually get
married, and we are done.

2 A distributed event synchronization protocol
We now present a distributed protocol for synchronizing events, that is based on the
protocol for arranging marriages in the Land of Frı̄g. Specifically, we interpret
– young inhabitants as potential commit points, or simply, points;
– priests as channels;
– parents as synchronization sites, or simply, synchronizers.
In other words, points, channels, and synchronizers are principals in our protocol. A
point is a site of pending input or output on a channel—every receive or transmit
event contains a point. Every application of sync contains a synchronizer.
We focus on synchronization of events that are built with the combinators receive,
transmit, and choose. The other combinators do not fundamentally affect the protocol; we consider them only in the concrete implementation in Section 3.
A source language For brevity, we simplify the syntax of the source language.
– Actions α, β are of the form c or c (input or output on channel c).
– Programs are of the form S1 | . . . | Sn (parallel composition of S1 , . . . , Sn ), where
→
each Si is either an action α, or a synchronization of a choice of actions select(−
α ).
Further, we consider only the following local reduction rule, which models selective
→
−
communication:
→
c∈−
α
c∈ β
→
−
→
select(−
α ) | select( β ) → c | c
besides the usual structural rules for parallel composition. In particular, we ignore reduction of actions at this level of abstraction.
A distributed abstract state machine for synchronization We formalize our protocol
as a distributed abstract state machine that implements the above semantics of selective
communication. Let σ range over states of the machine. These states may be of the
form σ | σ ′ (parallel composition), (νp) σ (name restriction), or ς (sub-state of some
principal in the protocol). Sub-states may be of the following forms.

ςp ::=
sub-states of points
p 7→ α
unmatched
Candidatep
matched
α
married
ςc ::=
sub-states of channels
⊙c
free
Matchc (p, q)
busy

ςs ::=
sub-states of synchronizers
s
open
⊠s
closed
Selects (p)
approved
Reject(p)
refused
Dones (p)
confirmed
Retrys
canceled

Here p, c, and s range over points, channels, and synchronizers. A synchronizer is a partial function from points to actions; we represent this function as a parallel composition
of bindings of the form p 7→ α. Further, we require that each point belongs to exactly
one synchronizer, that is, for any s and s′ , s 6= s′ ⇒ dom(s) ∩ dom(s′ ) = ∅. The
semantics of the machine is described by the following local transition rules, plus the
usual structural rules for parallel composition and name restriction (cf. the pi calculus [11], for example). In Section 3, these rules are implemented by message passing
between appropriate processes run at points, channels, and synchronizers.
p 7→ c | q 7→ c | ⊙c → Candidatep | Candidateq | Matchc (p, q)
p ∈ dom(s)
(II.i)
Candidatep | s → ⊠s | Selects (p)

(I)

p ∈ dom(s)
(II.ii)
Candidatep | ⊠s → ⊠s | Reject(p)

Selects (p) | Selects′ (q) | Matchc (p, q) → Dones (p) | Dones′ (q) | ⊙c
Selects (p) | Reject(q) | Matchc (p, q) → Retrys | ⊙c

(III.ii)

Reject(p) | Selects (q) | Matchc (p, q) → Retrys | ⊙c

(III.iii)

(III.i)

Reject(p) | Reject(q) | Matchc (p, q) → ⊙c
(III.iv)
→
−
dom(s) = p
s(p) = α
(IV.i)
(IV.ii)
→
Dones (p) → α
Retrys → (ν −
p ) (s | s)
The rules may be read as follows.
(I) Two points p and q, bound to complementary actions on channel c, react with c if it
is free (⊙c ), so that p and q become candidates and the channel becomes busy.
(II.i–ii) Next, p (and likewise, q) reacts with its synchronizer s. If the synchronizer
is open (s ), it now becomes closed (⊠s ), and p is declared selected by s. If the
synchronizer is already closed, then p is rejected.
(III.i–iv) If both p and q are selected, c confirms the selections to both parties. If only
one of them is selected, c cancels that selection. The channel now becomes free.
(IV.i–ii) If the selection of p is confirmed, the action bound to p is released. Otherwise,
the synchronizer “reboots” with fresh names for the points in its domain.
Compilation We compile the source language to this machine. Let the symbol Π denote finite parallel composition. Suppose that the set of channels in a program Πi∈1..n Si
is C. We compile this program to the state Πc∈C ⊙c | Πi∈1..n Sbi , where

α
if S = α
b
S=
→
→), where s = Π (p 7→ α ) for fresh names −
→
(ν −
pj ) (s | s) if S = select(−
α
pj
j
j
j
j

Correctness We prove that our protocol is correct, that is, the abstract machine correctly implements selective communication, by showing that the compilation from programs to states preserves progress and safety. Let a denotation be a list of actions. The
denotations of programs and states are derived by the function p·q, as follows.
pS1 | . . . | Sn q = pS1 q ⊎ · · · ⊎ pSn q
pαq = [α]
→
−
pselect( α )q = []

pσ | σ ′ q = pσq ⊎ pσ ′ q
p(νp) σq = pσq

[α] if ς = α
pςq =
[] otherwise

Now, if a program is compiled to some state, then the denotations of the program and
the state coincide. Further, we have the following theorem, proved in the appendix.
Theorem 1 (Correctness). Let C be the set of channels in a program Πi∈1..n Si . Then
Πi∈1..n Si ∼ Πc∈C ⊙c | Πi∈1..n Sbi , where ∼ is the largest relation such that P ∼ σ iff

(Correspondence) σ →⋆ σ ′ for some σ ′ such that pPq = pσ ′ q;
(Safety) if σ → σ ′ for some σ ′ , then P →⋆ P ′ for some P ′ such that P ′ ∼ σ ′ ;
(Progress) if P → , then σ →+ σ ′ and P → P ′ for some σ ′ and P ′ such that P ′ ∼ σ ′ .

Example Consider the program select(x, y) | select(y, z) | select(z) | select(x). The
program can reduce either to x | z | z | x, or to y | y | select(z) | select(x). The
denotations of these reduced programs are {x, x, z, z} and {y, y}, respectively. The
original program is compiled to the state
⊙x | ⊙y | ⊙z | (νpx̄ pȳ ) ((px̄ 7→x | pȳ 7→y) | px̄ 7→ x | pȳ 7→ y) |
(νpy pz ) ((py 7→y | pz 7→z) | py 7→ y | pz 7→ z) |
(νpz̄ ) ((pz̄ 7→z) | pz̄ 7→ z) |
(νpx ) ((px 7→x) | px 7→ x)
This state can transition in multiple steps to either of the following states, with denotations {x, x, z, z} and {y, y}, respectively. (In these states, σjunk can be garbagecollected, and is separated out for readability.)
– x | z | z | x | ⊙x | ⊙y | ⊙z | σjunk
– y | y | (νpz̄ ) ((pz̄ 7→z) | pz̄ 7→ z) | (νpx ) ((px 7→x) | px 7→ x) | ⊙x | ⊙y | ⊙z | σjunk
σjunk , (νpx̄ pȳ py pz pz̄ px ) (⊠(px̄ 7→x | pȳ 7→y) | ⊠(py 7→y | pz 7→z) | ⊠(pz̄ 7→z) | ⊠(px 7→x) )

3 A concrete implementation in Concurrent Haskell
The abstract machine of the previous section can be concretely implemented by a system of communicating processes. Indeed, we now present a complete implementation
of a CML-style event library in a fragment of Concurrent Haskell with first-order message passing. This fragment is rather close to the pi calculus. Thus, we ensure that our
implementation can be ported without difficulty to languages that support first-order
communication. At the same time, we take advantage of Haskell’s type system to show
how events and event combinators can be typed under the IO monad [7,9].

Before we proceed, we briefly review some of the concurrency primitives in Concurrent Haskell. Note that MVar and IO are polymorphic type constructors, as follows:
– The type MVar τ is given to a communication cell that carries values of type τ .
– The type IO τ is given to a computation that yields results of type τ , with possible
side effects via communication.
We rely on the following semantics of MVar cells.
– A cell can carry at most one value at a time.
– The function New :: IO (MVar τ ) returns a fresh, empty cell.
– The function Get :: MVar τ → IO τ is used to read from a cell; Get m blocks if
the cell m is empty, else gets the content of m (thereby emptying it).
– The function Put :: MVar τ → τ → IO () is used to write to a cell; Put m M
puts the term M in cell m if it is empty, else blocks.
Further, we rely on the following semantics of IO computations.
– The function fork :: IO () → IO () is used to spawn a concurrent computation.
– The function return :: τ → IO τ is used to inject a value into a computation.
– Computations can be sequentially composed by “piping”. We use Haskell’s convenient do{. . . ; . . . } notation for this purpose, instead of applying the de jure function
>>= :: IO τ → (τ → IO τ ′ ) → IO τ ′ .
Implementing synchronization by message passing We implement the following
functions for programming with first-class events in Concurrent Haskell. (Note the differences between ML and Haskell types for these functions. Since Haskell is purely
functional, we must embed types for computations with possible side-effects via communication, within the IO monad. Further, since evaluation in Haskell is lazy, we can
discard abstractions that only serve to “delay” evaluation.)
new :: IO (channel τ )
receive :: channel τ → event τ
transmit :: channel τ → τ → event ()
guard :: IO (event τ ) → event τ
wrap :: event τ → (τ → IO τ ′ ) → event τ ′
choose :: [event τ ] → event τ
wrapabort :: IO () → event τ → event τ
sync :: event τ → IO τ
For now, we focus on events that are built without wrapabort (i.e., we focus on programs without abort actions); the full implementation appears in Section 4.
We begin by concretizing the abstract state machine in Section 2. Specifically, we
run some protocol code at points, channels, and synchronizers, which reduce by simple
message passing on MVar cells. In this implementation:
– Each point is identified with a fresh name p :: Point.

– Each channel c is identified with a pair of fresh cells in [c] :: In and out [c] :: Out
on which it receives messages from points that are bound to actions on c.
– Each synchronizer is identified with a fresh cell s :: Synchronizer on which it
receives messages from points in its domain.
Before we present protocol code, let us describe the sequence of messages exchanged
in a typical session of the protocol, and mention the involved sub-states. On the way, we
develop type definitions for the MVar cells on which those messages are exchanged.
– A point p (at state p 7→ c or p 7→ c) begins by sending a message to c on its
respective input or output cell in [c] or out [c] ; the message contains a fresh cell
candidate [p] :: Candidate on which p expects a reply from c.
type In = MVar Candidate
type Out = MVar Candidate
– When c (at state ⊙c ) gets a pair of messages on in [c] and out [c] , say from p and
another point q, it replies by sending fresh cells decision [p] :: Decision and
decision [q] :: Decision on candidate [p] and candidate [q] respectively (reaching
state Matchc (p, q)), and expects the synchronizers for p and q to reply on them.
type Candidate = MVar Decision
– On receiving a message from c on candidate [p] , p (reaching state Candidatep ) tags
the message with its name and forwards it to its synchronizer on the cell s.
type Synchronizer = MVar (Point, Decision)
– If p is the first point to send such a message on s (that is, s is at state s ), a fresh cell
commit [p] :: Commit is sent back on decision [p] (reaching state ⊠s | Selects (p));
for each subsequent message received on s, say from p′ , a blank message is sent
′
back on decision [p ] (reaching state ⊠s | Reject(p′ )).
type Decision = MVar (Maybe Commit)1
– On receiving messages from the respective synchronizers of p and q on decision [p]
and decision [q] , c inspects the messages and responds (reaching state ⊙c ).
• If both commit [p] and commit [q] have come in, a positive signal is sent back
on commit [P ] and commit [Q] .
• If only commit [p] has come in, a negative signal is sent back on commit [p] ; if
only commit [q] has come in, a negative signal is sent back on commit [q] .
type Commit = MVar Bool
– If s receives a positive signal on commit [p] (reaching state Dones (p)), it signals
on p to continue. If, instead, a negative signal is received (reaching state Retrys ),
another session ensues.
type Point = MVar ()
1

Recall that the Haskell type Maybe τ is given to a value that is either Nothing, or of the
form Just v where v is of type τ . The function maybe :: τ ′ → (τ → τ ′ ) → Maybe τ → τ ′
is the associated case analyzer. For instance, the function isJust :: Maybe τ → Bool is
defined as maybe False (λ . True).

Protocol code for points The protocol code run by points abstracts on a cell s for the
associated synchronizer, and a name p for the point itself. Depending on whether the
point is for input or output, the code additionally abstracts on an input cell i or output
cell o, and an input or output action α.
@PointI :: Synchronizer → Point → In → IO τ → IO τ
@PointI s p i α = do {candidate ← New; Put i candidate;
decision ← Get candidate; Put s (p, decision );
Get t; α}
@PointO :: Synchronizer → Point → Out → IO () → IO ()
@PointO s p o α = do {candidate ← New; Put o candidate;
decision ← Get candidate; Put s (p, decision );
Get t; α}
Protocol code for channels The protocol code run by channels abstracts on an input
cell i and an output cell o for the channel.
@Chan :: In → Out → IO ()
@Chan i o = do {candidate i ← Get i; candidate o ← Get o;
decision i ← New; Put candidate i decision i ; xi ← Get decision i ;
decision o ← New; Put candidate o decision o ; xo ← Get decision o ;
maybe (return ()) (λcommit i . Put commit i (isJust xo )) xi ;
maybe (return ()) (λcommit o . Put commit o (isJust xi )) xo }
Protocol code for synchronizers The protocol code run by synchronizers abstracts on
a cell s for that synchronizer and some “rebooting code” X. (Here, we encode a loop
with the function fix :: (τ → τ ) → τ ; recall that fix f reduces to f (fix f ).)
@Sync :: Synchronizer → IO () → IO ()
@Sync s X = do {(p, decision) ← Get s;
fork (fix (λiter . do {
(p′ , decision ′ ) ← Get s; Put decision ′ Nothing; iter }));
commit ← New; Put decision (Just commit );
done ← Get commit ; if done then (Put p ()) else X}
We instantiate these processes in the translation of new, receive, transmit, and sync
below. But first, let us translate types for channels and events.
Translation of types The Haskell types for ML channel and event values are:
channel τ = (In, Out, MVar τ )
event τ = Synchronizer → IO τ
An ML channel is a Haskell MVar tagged with a pair of input and output cells. An
ML event is a Haskell IO function that abstracts on a synchronizer cell.

Translation of functions We now translate functions for programming with events.
We begin by compiling the ML function for creating channels.
new :: IO (channel τ )
new = do {i ← New; o ← New;
fork (fix (λiter . do {@Chan i o; iter }));
m ← New; return (i, o, m)}
– The term new spawns a looping instance of @Chan with a fresh pair of input and
output cells, and returns that pair along with a fresh MVar cell that carries messages for the channel.
Next, we compile the ML combinators for building base communication events. Recall
that a Haskell event is an IO function that abstracts on the cell of its synchronizer.
receive :: channel τ → event τ
receive (i, o, m) = λs. do {p ← New; @PointI s p i (Get m)}
transmit :: channel τ → τ → event ()
transmit (i, o, m) M = λs. do {p ← New; @PointO s p o (Put m M )}
– The term receive c s runs an instance of @PointI with the synchronizer s, a
fresh name for the point, the input cell for channel c, and an action that inputs on c.
– The term transmit c M s is symmetric; it runs an instance of @PointO with
the synchronizer s, a fresh name for the point, the output cell for channel c, and an
action that outputs term M on c.
Next, we compile the ML event combinators for specifying actions that are run before
and after synchronization.
guard :: IO (event τ ) → event τ
guard f = λs. do {v ← f ; v s}
wrap :: event τ → (τ → IO τ ′ ) → event τ ′
wrap v f = λs. do {x ← v s; f x}
– The term guard f s runs the computation f and passes the synchronizer cell s to
the event returned by the computation.
– The term wrap v f s passes the synchronizer cell s to the event v and pipes the
returned value to function f .
Next, we compile the ML combinator for choosing among a list of events. (Here, we
encode recursion over a list with the function fold :: (τ ′ → τ → τ ′ ) → τ ′ → [τ ] →
τ ′ ; recall that fold f x [] reduces to x and fold f x [v, V ] reduces to fold f (f x v) V .)
choose :: [event τ ] → event τ
choose V = λs. do {temp ← New;
fold (λ v. fork (do {x ← v s; Put temp x})) () V ;
Get temp}

– The term choose V s spawns a thread for each event v in V , passing the synchronizer s to v; any value returned by one of these threads is collected in a fresh cell
temp and returned.
Finally, we compile the ML function for event synchronization.
sync :: event τ → IO τ
sync v = do {temp ← New;
fork (fix (λiter . do {
s ← New; fork (@Sync s iter ); x ← v s; Put temp x}));
Get temp}
– The term sync v recursively spawns an instance of @Sync with a fresh synchronizer s and passes s to the event v; any value returned by one of these instances is
collected in a fresh cell temp and returned.

4 Compiling abort actions
The implementation of the previous section does not account for wrapabort. We now
show how wrapabort can be handled by slightly extending our notion of event.
Recall that abort actions (such as those specified by wrapabort) are spawned only
at events that do not enclose the commit point. Therefore, in an implementation of
wrapabort, it makes sense to name events with the sets of points they enclose. However, computing the set of points that an event encloses should not interfere with the dynamic semantics. In particular, for an event built with guard, we cannot run the guard
functions to compute the set of points that the event encloses. Thus, we refrain from
naming events at compile time. Instead, we introduce events as principals in our protocol; each event is named in situ by computing the list of points it encloses at runtime.
This list is carried on a fresh cell name :: Name for the event.
type Name = MVar [Point]
Further, each synchronizer carries a fresh cell abort :: Abort on which it receives
wrapabort functions from events, tagged with the list of points they enclose.
type Abort = MVar ([Point], IO ())
Protocol code run by points and channels remain the same. We add a handler for
wrapabort functions to the protocol code run by synchronizers. Accordingly, the code
now abstracts on an abort cell.
@Sync :: Synchronizer → Abort → IO () → IO ()
@Sync s abort X = do {. . . ;
if done then do {. . . ;
fix (λiter . do {
(P, f ) ← Get abort ; fork iter ;
if p ∈ P then return () else f })}
else . . . }

Here, after signaling the commit point p to continue (as earlier), the synchronizer continues to accept abort code f on abort ; such code is spawned only if the list of points
P , enclosed by the event that sends that code, does not include p.
The extended Haskell type for event values is as follows.
event τ = Synchronizer → Name → Abort → IO τ
Now, an ML event is a Haskell IO function that abstracts on a synchronizer, an abort
cell, and a name cell that carries the list of points the event encloses.
The Haskell function new does not change. We highlight minor changes in the remaining translations. We begin with the functions transmit and receive. An event
built with either function is named by a singleton containing the name of that point.
transmit (i, o, m) M = λs name abort . do {. . . ; fork (Put name [p]); . . . }
receive (i, o, m) = λs name abort . do {. . . ; fork (Put name [p]); . . . }
The function choose becomes slightly lengthy. A fresh name ′ cell is passed to each
event in the list; the names of those events are concatenated to name the choose event.
choose V = λs name abort . do {. . . ;
P ← fold (λP v. do {
name ′ ← New;
fork (do {x ← v s name ′ abort ; . . . });
P ′ ← Get name ′ ; Put name ′ P ′ ;
return (P ′ ⊎ P )}) [] V ;
fork (Put name P );
...}
We now compile the ML event combinator for specifying abort actions.
wrapabort :: IO () → event τ → event τ
wrapabort f v = λs name abort . do {
fork (do {P ← Get name; Put name P ; Put abort (P, f )});
v s name abort }
– The term wrapabort f v s name abort spawns a thread that reads the list of
enclosed events P on the cell name and sends the function f along with P on the
cell abort ; the synchronizer s is passed to the event v along with name and abort .
The functions guard and wrap remain similar.
guard f = λs name abort . do {v ← f ; v s name abort }
wrap v f = λs name abort . do {x ← v s name abort ; f x}
Finally, in the function sync, a fresh abort cell is now passed to @Sync, and a fresh
name cell is created for the event to be synchronized.

sync v = do {. . . ;
fork (fix (λiter . do {
. . . ; name ← New; abort ← New;
fork (@Sync s abort iter ); x ← v s name abort ; . . . }));
...}

5 Implementing communication guards
Beyond the standard primitives for communication in CML, some previous implementations of events further consider guarded communication. We discuss how our implementation can be easily extended to handle such communication. Specifically, we
require the following receive combinator, that can carry a communication guard.
receive :: channel τ → (τ → Bool) → event τ
Intuitively, receive c cond synchronizes with transmit c M only if cond M is true.
In our implementation, we make some slight adjustments to the types of some MVar
cells.
type In τ = MVar (Candidate, τ → Bool)
type Out τ = MVar (Candidate, τ )
type Candidate = MVar (Maybe Decision)
Next, we adjust the protocol code run by points and channels. Input and output points
that are bound to actions on c respectively send their conditions and messages to c. A
pair of points is matched only if the message of one satisfies the condition of the other.
@Chan :: In τ → Out τ → IO ()
@Chan i o = do {(candidate i , cond ) ← Get i; (candidate o , M ) ← Get o;
if (cond M ) then do {
. . . ; Put candidate i (Just decision i ); . . . ;
. . . ; Put candidate o (Just decision o ); . . . ;
...}
else do {Put candidate i Nothing; Put candidate i Nothing}}
@PointI :: Synchronizer → Point → In τ → (τ → Bool) → IO τ → IO τ
@PointI s p i cond α = do {. . . ; Put i (candidate, cond );
x ← Get candidate;
maybe (@PointI s p i cond α)
(λdecision . do {Put s (p, decision ); . . . }) x}
@PointO :: Synchronizer → Point → Out τ → τ → IO () → IO ()
@PointO s p o M α = do {. . . ; Put o (candidate, M );
x ← Get candidate;
maybe (@PointO s p o M α)
(λdecision . do {Put s (p, decision ); . . . }) x}

Finally, we make the following trivial adjustments to the type constructor channel,
and the functions receive and transmit.
type channel τ = (In τ, Out τ, MVar τ )
receive (i, o, m) cond = λs name abort . do {. . . ; @PointI s p i cond (Get m)}
transmit (i, o, m) M = λs name abort . do {. . . ; @PointO s p o M (Put m M )}

6 Related work
We are not the first to implement CML-style concurrency primitives in another language. In particular, Russell presents an implementation of events in Concurrent Haskell
in [14]. The implementation provides guarded channels, which filter communication
based on conditions on message values (as in Section 5). Unfortunately, the implementation requires a rather complex Haskell type for event values. In particular, a value of
type event τ must carry (among other things) a continuation of type IO τ → IO ().
An important difference between Russell’s implementation and ours is that Russell’s
choose combinator is asymmetric. In contrast, we implement a symmetric choose
combinator, following the standard CML semantics. While it is difficult to compare
other aspects of our implementations, we should point out that Russell’s event library is
more than 1300 lines of Haskell code (without comments), compared to our 150. Yet,
guarded communication in the sense of Russell can be readily implemented in our setting, as shown in Section 5. In the end, we believe that this difference in complexity is
largely due to the elegance of our synchronization protocol.
Recently, Donnelly and Fluet [5] introduce transactional events and implement
them over the software transactional memory (STM) module in Concurrent Haskell.
Their key observation is that combining all-or-nothing transactions with CML-style
concurrency recovers a monad. Unfortunately, implementing transactional events requires solving NP-hard problems [5]. In contrast, our direct implementation of CMLstyle concurrency remains rather lightweight.
Other implementations of events include those of Flatt and Findler in Scheme [6]
and of Demaine in Java [4]. While Flatt and Findler focus on kill-safety, Demaine focuses on efficiency by exploiting communication patterns that involve either single receivers or single senders. Demaine does not consider event combinators—in particular,
it is not clear whether his implementation can accommodate abort actions.
Distributed protocols for implementing selective communication date back to the
1980s. The protocols of Buckley and Silberschatz [3] and Bagrodia [1] seem to be
among the earliest in this line of work. Unfortunately, those protocols are prone to
deadlock. Bornat [2] proposes a protocol that is deadlock-free assuming communication between single receivers and single senders. Finally in [10], Knabe presents the
first deadlock-free protocol to implement selective communication for arbitrary channel communication. Knabe’s protocol appears to be the closest to ours. Channels are
considered as sites of control, and messages are exchanged between communication
points and channels to negotiate synchronization. However, Knabe assumes a global
ordering on processes and maintains queues for matching points; we do not require either of these facilities in our protocol. Moreover, as in [4], it is not clear whether the
protocol can accommodate event combinators such as guard and wrapabort.

7 Conclusion
In this paper, we show how to implement first-class event synchronization in Concurrent Haskell, a language with first-order message passing. We appear to be the first to
implement the standard semantics for events and event combinators in this setting. An
interesting consequence of our work is that implementing distributed selective communication is reduced to implementing distributed message-passing in Concurrent Haskell.
At the heart of our implementation is a new deadlock-free protocol that is run among
communication points, channels, and synchronization sites. This protocol seems to be
robust enough to allow implementations of sophisticated synchronization primitives.
All the code presented in this paper is available online at
http://www.soe.ucsc.edu/˜avik/projects/CML
Acknowledgments This work started off as a class project for Cormac Flanagan’s course
on Concurrent Programming and Transactional Memory at UC Santa Cruz in Spring
2007. Thanks to him, Martı́n Abadi, and Andy Gordon for their enthusiasm and curiosity, which encouraged further development of this work since that course.

References
1. R. Bagrodia. A distributed algorithm to implement the generalized alternative command of
CSP. In ICDCS ’86: Distributed Computing Systems, pages 422–427. IEEE, 1986.
2. R. Bornat. A protocol for generalized Occam. Software Practice and Experience, 16(9):783–
799, 1986.
3. G. N. Buckley and A. Silberschatz. An effective implementation for the generalized inputoutput construct of CSP. ACM Transactions on Programming Languages and Systems,
5(2):223–235, 1983.
4. E. D. Demaine. Protocols for non-deterministic communication over synchronous channels.
In IPPS/SPDP ’98: Parallel and Distributed Processing, pages 24–30. IEEE, 1998.
5. K. Donnelly and M. Fluet. Transactional events. SIGPLAN Notices, 41(9):124–135, 2006.
6. M. Flatt and R. B. Findler. Kill-safe synchronization abstractions. In PLDI ’04: Programming Language Design and Implementation, pages 47–58. ACM, 2004.
7. A. D. Gordon. Functional programming and input/output. Cambridge University, 1994.
8. S. L. P. Jones, A. D. Gordon, and S. Finne. Concurrent Haskell. In POPL ’96: Principles of
Programming Languages, pages 295–308. ACM, 1996.
9. S. L. P. Jones and P. Wadler. Imperative functional programming. In POPL ’93: Principles
of programming languages, pages 71–84. ACM, 1993.
10. F. Knabe. A distributed protocol for channel-based communication with choice. In PARLE
’92: Parallel Architectures and Languages, Europe, pages 947–948. Springer-Verlag, 1992.
11. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts I and II. Information and Computation, 100(1):1–77, 1992.
12. J. H. Reppy. Higher-order concurrency. PhD thesis, Cornell University, 1992. Available as
Technical Report 92-1852.
13. J. H. Reppy. Concurrent programming in ML. Cambridge University, 1999.
14. G. Russell. Events in Haskell, and how to implement them. In ICFP ’01: Functional Programming, pages 157–168. ACM, 2001.

A

Correctness proof for the synchronization protocol

In this appendix, we prove correctness of the synchronization protocol (Theorem 1).
This proof closely follows the informal proof of progress in the Land of Frı̄g.
Consider any state σ. We begin by defining some invariants that σ must satisfy;
→
the satisfaction of these invariants is written as ⊢ σ. Let σ be in the form (νP ) Π −
ς.
→
−
→
−
We assume that the set of points in ς is P , the set of channels in ς is C, the set of
→
synchronizers in −
ς is S, and C ∩ P = ∅. Then ⊢ σ if:
1. For any p ∈ P, there is a unique s ∈ S such that p ∈ dom(s). Further, let s(p) = α.
→
Then at most one of the following sub-states is in −
ς:
{p 7→ α, Candidatep , Selects (p), Reject(p), Dones (p), Retrys }
→
and exactly one of the following sub-states is in −
ς:
{s , ⊠s }
→
2. For every c ∈ C, exactly one of the following sub-states is in −
ς:
{⊙c , Matchc ( , )}
3. Let p ∈ P and s ∈ S such that p ∈ dom(s). Then, if one of the following sub-states
→
is in −
ς:
{Selects (p), Reject(p), Dones (p), Retrys }
→
→
then ⊠s is in −
ς . On the other hand, if ⊠s is in −
ς then there is at most one p such
→
that p ∈ dom(s) and one of the following sub-states is in −
ς:
{Selects (p), Dones (p), Retrys }
→
4. Let c ∈ C and p, q ∈ P . Then Matchc (p, q) is in −
ς iff there are (not necessarily
′
′
distinct) s, s ∈ S such that s(p) = c, s (q) = c, one of the following sub-states is
→
in −
ς:
{Candidatep , Selects (p), Reject(p)}
→
and one of the following sub-states is in −
ς:
{Candidateq , Selects′ (q), Reject(q)}
It is easy to see that (1–4) are invariants for any state compiled from a program.
Lemma 1. Let C be the set of channels in a program Πi∈1..n Si . Now, suppose that
Πc∈C ⊙c | Πi∈1..n Sbi →⋆ σ. Then ⊢ σ.
Next, we prove the analog of the lemma in Section 1.

→
Lemma 2. Suppose that ⊢ (νP ) Π −
ς . Let p, q ∈ P , and let p 7→ c and q 7→ c be in
→
−
→
−
→
−
→
−
⋆
′
ς . Then (νP ) Π ς −→ (νP )Π ς such that ⊙c is in ς ′ .

→
Proof. If ⊙c is in −
ς , we are done. Otherwise, by (2) it follows that Matchc (p′ , q ′ ) in
→
−
′ ′
in ς for some p , q ∈ P . Now, by (1) and (4), p′ 6= p and q ′ 6= q. Further, by (4),
→
there are s and s′ in the set of synchronizers in −
ς such that p′ ∈ dom(s), q ′ ∈ dom(s′ ),
→
−
′
′
Candidatep′ or Selects (p ) or Reject(p ) is in ς , and Candidateq′ or Selects′ (q ′ ) or
→
→
→
ς . Now,
Reject(q ′ ) is in −
ς . Further, by (1), s or ⊠s is in −
ς , and s′ or ⊠s′ is in −
→
−
′′
′
(II.i–ii) can be applied to move to a state (νP )Π ς such that Selects (p ) or Reject(p′ )
→
−
→
−
is in ς ′′ , and Selects′ (q ′ ) or Reject(q ′ ) is in ς ′′ . Finally, (III.i–iv) can be applied to move
→
−
to the required state (νP )Π ς ′ .
We are now ready to prove the main theorem.
Restatement of Theorem 1. Let C be the set of channels in a program Πi∈1..n Si . Then
Πi∈1..n Si ∼ Πc∈C ⊙c | Πi∈1..n Sbi , where ∼ is the largest relation such that P ∼ σ iff
(Correspondence) σ →⋆ σ ′ for some σ ′ such that pPq = pσ ′ q;
(Safety) if σ → σ ′ for some σ ′ , then P →⋆ P ′ for some P ′ such that P ′ ∼ σ ′ ;
(Progress) if P → , then σ →+ σ ′ and P → P ′ for some σ ′ and P ′ such that P ′ ∼ σ ′ .

Proof. The proof of (Safety) is fairly easy. (Progress) follows from Lemmas 1 and 2, as
follows. By Lemma 1, we can consider only a subset ≃ of ∼ such that ≃ σ ⇒ ⊢ σ.
→
Now, suppose that P ≃ (νP ) −
ς and P → .
→
ς . Then, by Lemma 2
We first assume that there are some p 7→ c and q 7→ c in −
→
−
→
−
→
−
⋆
′
and (I), (νP ) ς → (νP ) ς such that Candidatep and Candidateq are in ς ′ . It can be
shown, following the reasoning of Section 1, that eventually: either c and c are released;
or, some α is released such that for some point p′ and synchronizer s, we have s(p′ ) = α
and either p ∈ dom(s) or q ∈ dom(s). In the former case, P makes the corresponding
reduction, and we are done. In the latter case, the action complementary to α is released
in the next step; then P makes the corresponding reduction, and we are done.
→
On the other hand, if there are no p 7→ c and q 7→ c in −
ς , then by (1) there must
′
′
be some p and q, and s and s , such that s(p) = c, s (q) = c, and one of the following
→
sub-states is in −
ς:
{Candidatep , Selects (p), Reject(p), Dones (p), Retrys }
→
and one of the following sub-states is in −
ς:
{Candidateq , Selects′ (q), Reject(q), Dones′ (q), Retrys′ }
→
So either Candidatep and Candidateq are in −
ς , or p and q are in sub-states reachable
from Candidatep and Candidateq ; in either case, we proceed as before.

