We first provide a “survival kit” introduction to the basic concept of the join-calculus: the join-definition. The JoCaml tutorial  presents join-definitions from a programming perspective in greater detail.
An OCaml program is a set of definitions. Definitions introduce
types, values or functions. JoCaml extends OCaml with
A join-definition is a list of reactions rules
that are processes guarded by join-patterns. A
join-pattern is a list of channel names with formal arguments. A
guarded process is fired when there are messages present on all the
channels of its join-pattern.
A typical process is the parallel composition
&”) of elementary processes.
In JoCaml there are two kind of channels: asynchronous and synchronous. Asynchronous channels are the classical channels of the join-calculus. Message sending on an asynchronous channel is an example of an elementary process. Synchronous channels can engage in any kind of join-pattern but the guarded process must send back a result to the emitter. In that aspect, sending a message on a synchronous channel can be seen as a function call.
Let us now consider an example of a join-definition: a concurrent buffer based on the two-lists implementation of functional FIFO queues.
Join-definitions are introduced by
reaction rules are separated by
or, and the channel names in
join-patterns are separated by “
The join-definition above defines one asynchronous channel
state) and two synchronous channels (
Asynchronous channels have type τ
Join.chan where τ is
the type of the message.
The idea of this buffer is to store the FIFO queue (implemented by a
pair of lists) as a message on the channel
state. By the
organization of join-patterns, which all include
exclusive access to the internal state of the buffer is granted to the
callers of synchronous
The first join-pattern
state(xs,ys) & put(x) is satisfied
whenever there are messages on both
behavior of the guarded process is to perform two actions in parallel:
(1) send a new message on
state where the value
x is added to
xs and (2) return the value
() to the caller
The second join-pattern
state(xs,y::ys) & get() is satisfied
when there are messages on both
that the message on
state matches the pattern
That is, the message is a pair whose second component is a
non-empty list. The process guarded by this join-pattern removes
one value from the buffer and returns it to the caller of
The last join-pattern
state(_::_ as xs,) & get() is satisfied
when there is a message on
get and a message on
that matches a pair whose first component is a non-empty list and second
component is an empty list.
The corresponding guarded process transfers elements from one end of the
queue to the other and performs
Notice that there is no join-pattern that satisfies
state(,) & get(). As a consequence, a call to
blocked when the buffer is empty.
To initialize the buffer, a message is sent on
An expression that performs such a sending is
spawn construct executes a process asynchronously.
spawn lifts a process into an expression.
It is to be noticed that
processes and expressions are distinct syntactical categories.
To be able to create several buffers, the previous definition is
encapsulated into a function
A buffer is in fact a record, whose fields are the
get synchronous channels.
That way, we make buffers first-class values and additionally
hide the internal channel