A rapid tour of the join-calculus

2 A rapid tour of the join-calculus

2.1 Syntax

We here rephrase the traditional presentation of the core join-calculus [4], where names are the only value. Thus, we ignore the issue of system primitives and constants, since names provide sufficient expressive power for our purpose of describing our implementation of pattern-matching (However we use primitives and constants in our examples). We slightly change the syntax of [4], in order to match the one of the join programming language.

We use x to denote a name in general.

P	::=	x(x_i^{i ∈ 1… p})
	∣	`let` D `in` P
	∣	P \| P

D	::=	J `=` P
	∣	D `and` D
J	::=	x(x_i^{i ∈ 1… p})
	∣	J \| J

A process P is either a message, a defining process, or a parallel composition of processes (note that names are polyadic, meaning that messages may be made of several values); a definition D consists of one or several clauses J = P that associate a guarded process P to a specific message pattern J; a join-pattern J consists of one or several messages in parallel. We say that the pattern J = … x(x_i ^{i ∈ 1… p})… defines the name x and that a definition defines the set of the names defined by its patterns. Moreover, patterns are linear, i.e. names may appear at most once in a given pattern.

Processes and definitions are known modulo renaming of bound variables, as substitution performs α-conversion to avoid captures.

2.2 Semantics

This semantics is specified as a reflexive chemical abstract machine (RCHAM) (see [3]). The state of the computation is a chemical soup D ⊩ P that consists of two multisets: active definitions D and running processes P.

The chemical soup evolves according to two families of rules: Structural rules ↔ are reversible (→ is heating, ← is cooling); they represent the syntactical rearrangement of terms (heating breaks terms into smaller ones, cooling builds larger terms from their components). Reduction rules ⇒ consume specific processes present in the soup, replacing them by some others; they are the basic computation steps.

We present simplified chemical rules (see [4, 5] for the complete set of rules). Following the chemical tradition, every rule applies on any matching sub-part of the soup, non-matching sub-parts of the soup being left implicit.

	⊩ P₁ \| P₂	↔		⊩ P₁, P₂	S-Par
D₁ `and` D₂	⊩	↔	D₁, D₂	⊩	S-And
	⊩ `let` D `in` P	↔	D	⊩ P	S-Def
J `=` P	⊩ ϕ (J)	⇒	J `=` P	⊩ ϕ (P)	R-β

Two of the rules above have side conditions:

(S-Def) the names defined in D must not appear anywhere in solution but in the reacting process and definition D and P. This condition is global; in combination with α-renaming it enforces lexical scoping.
(R-β) ϕ (·) substitute actual names for the received variables in J and P.

Additionally, we only consider well-typed terms and reductions. See [6] for details on a rich polymorphic type system for the join calculus. Here, this mostly amounts to assuming that message and name arity always agree.

In this paper, we take particular interest in the reduction (R-β). Informally, when there are messages pending on all the names defined in a given join-pattern, then the process guarded by this join-pattern may be fired. When firing is performed, we say that a matching occurs. On the semantics level, there is a message (x_i^{i ∈ 1… p}) pending on a name x when there is an active molecule x(x_i^{i ∈ 1… p}) in the chemical soup.

Thus, we may define the reactivity status of a given chemical soup as the multiset of the active molecules in it. Later on in this paper, we shall consider various abstractions of this reactivity status.

2.3 The join programming languages

Apart from primitives, join-languages support synchronous names, which the core join-calculus does not provide directly. Synchronous names send back results, a bit like functions. However synchronous names may engage in any kind of join-synchronization, just as asynchronous names do. A program written using synchronous names can be translated into the core join-calculus alone. The translation is analogous to continuation passing style transformation in the λ-calculus. In our implementation, as far as pattern-matching is concerned, a synchronous name behave like it was asynchronous and carried one additional continuation argument. All implementation difficulties concentrate in managing this extra argument, whose presence had no effect on pattern-matching itself.

The join language [7] is our first prototype. All examples in this paper are in join syntax. The system consists in a bytecode compiler and a bytecode interpreter. Both compiler and interpreter are Objective Caml [9] programs and it is easy to lift Objective Caml data types and functions into join abstract data types and primitives. For instance, join programs easily draw graphics, using the graphics Objective Caml library. As a consequence, join can be seen either as a language of its own, featuring many primitives, or as a distributed layer on top of Objective Caml. Continuations are encoded using ad hoc threads, which are created and scheduled by the join bytecode interpreter.

The jocaml system is our second implementation. In jocaml, all join-calculus constructs for concurrency, communication, synchronization and process mobility are directly available as syntactical extensions to Objective Caml. On the runtime environment side, we have supplemented the original Objective Caml runtime system (which already provides a thread library) with a special “join” library and a distributed garbage collector [14]. On the compiler side, the Objective Caml compiler has been extended to translate join-calculus source code into functions calls to the “join” library. However, we also introduced a few new instructions to Objective Caml bytecode, but only to handle code mobility, a feature orthogonal to pattern-matching. The jocaml system is currently available as a prototype version [8].