2 The objective join calculus

We first focus on a core calculus dealing with objects. This calculus is a variant of the join calculus [10]. We illustrate the operations of the calculus, then we define its syntax and semantics.

 2.1 Getting started
The basic operation of our calculus is asynchronous message passing. For instance, the process out.print_int(n) sends a message with label print_int and content n to an object named out, meant to print integers on the terminal. Accordingly, the definition of an object describes how messages received on some labels can trigger processes. For instance,
obj continuation = reply(n) |> out.print_int(n)

defines an object that reacts to messages on reply by printing their content on the terminal. Another example is the rendez-vous, or synchronous buffer:
obj sbuffer = get(r) & put(n,s) |> r.reply(n) & s.reply()

The object sbuffer has two labels get and put; it reacts to the simultaneous presence of one message on each of these labels by passing a message to the continuation r, with label reply and content n, and passing an empty message to s. (Object r may be the previously-defined continuation; object s is another continuation taking no argument on reply.) As regards the syntax, message synchronization and concurrent execution are expressed in a symmetric manner, on either side of |>, using the same infix operator &.

Some labels may convey messages representing the internal state of an object, rather than an external method call. This is the case of label Some in the following unbounded, unordered, asynchronous buffer:
obj abuffer =
or get(r) & Some(n) |> r.reply(n)

The object abuffer can react in two different ways: a message (n,r) on put may be consumed by storing the value n in a self-inflicted message on Some; alternatively, a message on get and a message on Some may be jointly consumed, and then the value stored on Some is sent to the continuation received on get. The indirection through Some makes abuffer behave asynchronously: messages on put are never blocked, even if no message is ever sent on get.

In the example above, the messages on label Some encode the state of abuffer. The following definition illustrates a tighter management of state that implements a one-place buffer:
obj buffer =
put(n,r) & Empty() |> r.reply() & buffer.Some(n)
or get(r)  & Some(n) |> r.reply(n) & buffer.Empty()
init buffer.Empty()

Such a buffer can either be empty or contain one element. The state is encoded as a message pending on Empty or Some, respectively. Object buffer is created empty, by sending a first message on Empty in the (optional) init part of the obj construct. As opposed to abuffer above, a put message is blocked when the buffer is not empty.

To keep the buffer object consistent, there should be a single message pending on either Empty or Some. This invariant holds as long as external users cannot send messages on these labels directly. In Section 6, we describe a refined semantics and a type system that distinguishes private labels (such as Empty and Some) from public labels and restricts access to private labels. In the examples, private labels conventionally bear an initial capital letter.

Once private labels are hidden, each of the three variants of buffer provides the same interface to the outside world (two methods labeled get and put) but their concurrent behaviors are very different.

 2.2 Syntax
We use two disjoint countable sets of identifiers for object names x, z, u Î O and labels l Î L. Tuples are written xii Î I or simply x. The grammar of the objective join calculus (without classes) is given in Figure 1; it has syntactic categories for processes P, definitions D, and patterns M. We abbreviate obj x = D \ init P1 in P2 by omitting init P1 when P1 is 0.
Figure 1: Syntax for the core objective join calculus
 P ::= Processes 0 null process x.M message sending P1 & P2 parallel composition obj x = D init P1 in P2 object definition D ::= Definitions M |> P reaction rule D1 or D2 disjunction M ::= Patterns l(u) message M1 & M2 synchronization

A reaction rule M |> P associates a pattern M with a guarded process P. Every message pattern l(u) in M binds the object names u with scope P. As in join calculus, we require that every pattern M guarding a reaction rule be linear, that is, labels and names appear at most once in M. In addition, the object definition obj x = D init P1 in P2 binds the name x to D. The scope of x is every guarded process in D (here x means self'') and the processes P1 and P2. Free names in processes and definitions, written fn( · ), are defined accordingly; a formal definition of free names appears in Figure 4. Terms are taken modulo renaming of bound names (or a-conversion).

 2.3 Chemical semantics
The operational semantics is given as a reflexive chemical abstract machine [10]. Each rewrite rule of the machine applies to configurations of objects and processes, called chemical solutions. A solution D ||- P consists of a set of named definitions  D (representing objects in solution) and of a multiset of processes P running in parallel. We write x.D for a named definition in D, and always assume that there is at most one definition for x in D. Chemical reductions are obtained by composing rewrite rules of two kinds: structural rules º represent the syntactical rearrangement of terms; reduction rules ¾® represent the basic computation steps.
Figure 2: Chemical semantics
Par
 ||- P   &   Q º ||- P,  Q

Nil
 ||- 0 º ||-

Obj
 ||- obj x = D init P in Q º x. D ||- P,  Q

Join
 ||- x.(M & M') º ||- x.M,  x.M'

Red
 x.[ M |> P] ||- x.Ms ¾® x.[ M |> P] ||- Ps

Chemistry
 D0 ||- P1 º stackrel ¾® D0 ||- P2
 D, D0 ||- P1, P º stackrel ¾® D, D0 ||- P2, P

Chemistry-Obj
 ||- P º x.D ||- P'      x Ïfn( D) È fn( P )
 D ||- P , P º D , x.D ||- P' , P

The rules for the objective join calculus are given in Figure 2, with side conditions for rule Red: [ M |> P] abbreviates a definition D that contains the reaction rule M |> P; s is a substitution with domain fn(M); the processes Ms and Ps denote the results of applying s to M and P, respectively.

Rules Par and Nil make parallel composition of processes associative and commutative, with unit 0. Rule Obj describes the introduction of an object. (Preliminary a-conversion may be required to pick a fresh name x.) Here, according to Obj and Par, expressions obj x = D \ init P in Q and obj x = D in P & Q are equivalent. However, P and Q have different meaning in the semantics with privacy, where Q cannot access private names of D (see Section 6.1). Rule Join gathers messages sent to the same object. Rule Red states how messages can be jointly consumed and replaced by a copy of a guarded process, in which the contents of these messages are substituted for the formal parameters of the pattern.

In chemical semantics, each rule usually mentions only the components that participate to the rewriting, while the rewriting applies to every chemical solution that contains them. More explicitly, we provide two context rules Chemistry and Chemistry-Obj. In rule Chemistry, the symbol º stackrel ¾® stands for either º or ¾®. In rule Chemistry-Obj, the side condition x Ï fn( D)È fn( P) prevents name capture when introducing new objects (the sets fn( D) and fn( P) are defined in Figure 4).