| 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.
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 =
put(n,r) |> r.reply() & abuffer.Some(n)
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.
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).
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
| 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).