We first provide a “survival kit” introduction to the basic concept of the join-calculus: the join-definition. The JoCaml tutorial [14] 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
join-definitions.
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
(operator “&”) 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 def,
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 (put and get).
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 state,
exclusive access to the internal state of the buffer is granted to the
callers of synchronous put and get.
The first join-pattern state(xs,ys) & put(x) is satisfied
whenever there are messages on both state and put. The
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
the list xs and (2) return the value () to the caller
of put.
The second join-pattern state(xs,y::ys) & get() is satisfied
when there are messages on both state and put and
that the message on state matches the pattern (xs,y::ys).
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 get.
The last join-pattern state(_::_ as xs,[]) & get() is satisfied
when there is a message on get and a message on state
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 get again.
Notice that there is no join-pattern that satisfies
state([],[]) & get(). As a consequence, a call to get is
blocked when the buffer is empty.
To initialize the buffer, a message is sent on state.
An expression that performs such a sending is spawn state([],[]).
The spawn construct executes a process asynchronously.
Syntactically, 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 create_buffer.
A buffer is in fact a record, whose fields are the put
and get synchronous channels.
That way, we make buffers first-class values and additionally
hide the internal channel state.