Previous Up Next

3  An introduction to join-definitions

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.

def state(xs,ys) & put(x) = state(x::xs,ys) & reply () to put or state(xs,y::ys) & get() = state(xs,ys) & reply y to get or state(_::_ as xs,[]) & get() = state([], List.rev xs) & reply get() to get val put : '_a -> unit val state : ('_a list * '_a list) Join.chan val get : unit -> '_a

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.

type 'a buffer = { put : 'a -> unit; get: unit -> 'a } let create_buffer () = … (* same definition of put/get/state as before *) spawn state([],[]) ; {put=put; get=get;} val create_buffer : unit -> 'a 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.

Previous Up Next