3 |
Inheritance and concurrency |
|
We now extend the calculus of concurrent objects with classes
and inheritance.
The behavior of objects in the join calculus is statically defined:
once an object is created, it cannot be extended with new labels or
with new reaction rules synchronizing existing labels. Instead, we
provide this flexibility at the level of classes.
Our operators on classes can express various object paradigms, such
as method overriding (with late binding) or method extension. As
regards concurrency, these operators are also suitable to define
synchronization policies in a modular manner.
3.1 |
Refining synchronization |
|
We introduce the syntax for classes in a series of simple examples.
We begin with a class buffer defining the one-place buffer of
Section 2.1:
class buffer = self(z)
get(r) & Some(n) |> r.reply(n) & z.Empty()
or put(n,r) & Empty() |> r.reply() & z.Some(n)
As regards the syntax, the prefix
self(z) explicitly binds the name z
to
self. The class buffer can be used to create objects:
obj b = buffer init b.Empty()
Assume that, for debugging purposes, we want to log the buffer content
on the terminal. We first add an explicit log method:
class logged_buffer = self(z)
buffer
or log() & Some(n) |> out.print_int(n) & z.Some(n)
or log() & Empty() |> out.print_string("Empty") & z.Empty()
The class above is a disjunction of an inherited class and of
additional reaction rules.
The intended meaning of disjunction is that reaction rules are
cumulated, yielding competing behaviors for messages on labels
that appear in several disjuncts. The order of the disjuncts does not
matter.
The programmer who writes logged_buffer must have some
knowledge of the parent class buffer, namely the use of
private labels Some and Empty for representing the
state.
Some other useful debugging information is the synchronous
log of all messages that are consumed on put. This log
can be produced by selecting the patterns in which put occurs and
adding a
printing message to the corresponding guarded processes:
class logged_buffer_bis =
match buffer with
put(n,r) => put(n,r) |> out.print_int(n)
end
The match construct can be understood by analogy with
pattern matching à la ML, applied to the reaction rules of
the parent class.
In this example, every reaction rule from the parent buffer
whose synchronization pattern contains the label put is
replaced in the derived logged_buffer_bis by a rule with
the same synchronization pattern (since put appears on both
sides of Þ) and with the original guarded process in
parallel with the new printing message (the original guarded process
is left implicit in the match syntax). Every
other parent rule is kept unchanged. Hence, the class above
behaves as the definition:
class logged_buffer_bis = self(z)
get(r) & Some(n) |> r.reply(n) & z.Empty()
or put(n,r) & Empty() |> r.reply() & z.Some(n) & out.print_int(n)
Yet another kind of debugging information is a log of put
attempts:
class logged_buffer_ter = self(z)
match buffer with
put(n,r) => Parent_put(n,r) |> nil
end
or put(n,r) |> out.print_int(n) & z.Parent_put(n,r)
In this case, the match construct performs a renaming of
put into Parent_put in every pattern of class
buffer, without affecting their guarded processes.
The overall effect is similar to the overriding of the method put
of buffer
with a late-binding semantics.
Namely, should there be a message z.put(u) in a guarded process
of the parent class, then, at runtime, z.put(u) would reach the new
definition of put.
The examples above illustrate that the very idea of class refinement
is less abstract in a concurrent setting than in a sequential one. In
the first logged_buffer example, logging the buffer state
requires knowledge of how this state is encoded; otherwise, some states
might be forgotten or logging might lead the buffer into
deadlock. The other two examples expose another subtlety: in a
sequential language, the distinction between logging put
attempts and put successes is irrelevant.
Thinking in terms of sequential object invocations, one may be unaware
of the concurrent behavior of the object, and thus write
logged_buffer_ter instead of logged_buffer_bis.
The language with classes extends the core calculus of
Section 2; its grammar is given in
Figure 3.
We refer to
Sections 2.1, 3.1,
and 4 for explanations and examples.
Classes are taken up to the associative-commutative laws for
disjunction.
We use two additional sets of identifiers for class names c Î
C and for sets of labels L Î 2 L. Such sets L are
used to represent abstract classes that declare the labels in L but
do not necessarily define them.
Figure 3: Syntax for the objective join calculus
|
|
P ::= |
|
|
|
|
|
Processes |
|
|
|
|
|
|
|
0 |
|
|
|
null process |
|
|
|
|
|
x.M |
|
|
|
message sending |
|
|
|
|
|
P1 & P2 |
|
|
|
parallel composition |
|
|
|
|
|
obj x = C init P1 in P2 |
|
|
|
object definition |
|
|
|
|
|
class c = C in P |
|
|
|
class definition |
|
|
|
C ::= |
|
|
|
|
|
Classes |
|
|
|
|
|
|
|
c |
|
|
|
class variable |
|
|
|
|
|
|
|
L |
|
|
|
abstract class |
|
|
|
|
|
|
|
J |> P |
|
|
|
reaction rule |
|
|
|
|
|
C1 or C2 |
|
|
|
disjunction |
|
|
|
|
|
self(x) C |
|
|
|
self binding |
|
|
|
|
|
match C with S end |
|
|
|
selective refinement |
|
|
|
S ::= |
|
|
|
|
|
Refinement clauses |
|
|
|
|
|
|
|
(K1 Þ K2 |> P) | S |
|
|
|
refinement sequence |
|
|
|
|
|
Ø |
|
|
|
empty refinement |
|
|
|
J ::= |
|
|
|
|
|
Join patterns |
|
|
|
|
|
|
|
l(u) |
|
|
|
message |
|
|
|
|
|
|
|
J1 & J2 |
|
|
|
synchronization |
|
|
|
|
|
|
|
J1 or J2 |
|
|
|
alternative |
|
|
|
|
|
K ::= |
|
|
|
|
|
Selection patterns |
|
|
|
|
|
|
|
0 |
|
|
|
empty pattern |
|
|
|
|
|
|
|
J |
|
|
|
join pattern |
|
|
Join patterns J generalize the syntactic category of patterns M
given in Figure 1 with an or operator that
represents alternative synchronization patterns.
Selection patterns K are either join patterns or the empty
pattern 0.
All patterns are taken up to equivalence laws:
& and or are associative-commutative, & distributes over or,
and 0 is the unit for &.
Hence, every pattern K can be written as an
alternative of patterns ori Î I Mi. We sometimes use the notation K1 & K2 for decomposing patterns
M.
Figure 4: Free names fn(·) and declared labels dl(·)
In patterns M, join patterns J, and selection patterns K: |
|
|
fn(0) |
|
= |
Ø |
|
|
|
fn( l(u)) |
|
= |
u |
|
|
|
fn( J & J' ) |
|
= |
fn( J ) È fn( J' ) |
|
|
|
fn( J or J' ) |
|
= |
fn( J )
(also = fn( J' )) |
|
|
|
dl(0) |
|
= |
Ø |
|
|
|
dl( l(u) ) |
|
= |
{ l } |
|
|
|
dl( J & J' ) |
|
= |
dl( J ) + dl( J' ) |
|
|
|
dl( J or J' ) |
|
= |
dl( J ) È dl( J' ) |
|
In refinement clauses S: |
|
|
fn(|i Î I (Ki Þ Ki' |> Pi)) |
|
= |
Èi Î I fn(Pi) \ fn(Ki') |
|
|
|
dl(|i Î I (Ki Þ Ki' |> Pi)) |
|
= |
Èi Î I dl(Ki') \ dl(Ki) |
|
In classes C: |
|
|
fn( c ) |
|
= |
{ c } |
|
|
|
fn( L ) |
|
= |
Ø |
|
|
|
fn( J |> P) |
|
= |
fn( P ) \ fn( J ) |
|
|
|
fn( C1 or C2 ) |
|
= |
fn(C1) È fn(C2) |
|
|
|
fn( self(z) C ) |
|
= |
fn(C) \ { z } |
|
|
|
fn( match C with S end ) |
|
= |
fn(C) È fn(S) |
|
|
|
dl( c ) |
|
= |
Ø |
|
|
|
dl( L ) |
|
= |
L |
|
|
|
dl( J |> P ) |
|
= |
dl( J ) |
|
|
|
dl( C1 or C2 ) |
|
= |
dl( C1 ) È dl( C2) |
|
|
|
dl( self(z) C ) |
|
= |
dl( C ) |
|
|
|
dl( match C with S end ) |
|
= |
dl(C) È dl(S) |
|
In processes P: |
|
|
fn( 0 ) |
|
= |
Ø |
|
|
|
fn( x. M ) |
|
= |
{x} È fn(M) |
|
|
|
fn( P & Q ) |
|
= |
fn(P) È fn(Q) |
|
|
|
fn( obj x = C init P in Q ) |
|
= |
(fn(C) È fn(P) È fn(Q)) \ { x } |
|
|
|
fn( class c = C in P ) |
|
= |
fn(C) È (fn(P) \ { c }) |
|
In solutions: |
|
|
fn( D ) |
|
= |
Èx.D Î D ({x} È fn(D)) |
|
|
|
fn( P ) |
|
= |
ÈP Î P fn(P) |
|
|
We always assume that processes meet the following
well-formedness conditions:
- All conjuncts Mi in the normal form of K are linear
(as defined in Section 2.2) and binds the same names
(i.e. have the same set of free names, as defined in Figure 4). By extension, we say that K binds the names fn(Mi)
bound in each Mi, and write fn(K) for these names.
- In a refinement clause K1 Þ K2 |> P, the pattern K1
is either M or 0, the pattern K2 binds at least the
names of K1 (fn(K1)Í fn(K2)), and
K1 is empty whenever K2 is empty
(so as to avoid the generation of empty patterns).
Binders for object names
include object definitions (binding the defined object) and
patterns (binding the received names).
In a reaction rule J |> P, the join pattern
J binds fn(J) with scope P.
In a refinement clause K1 Þ K2 |> P, the selection pattern
K1 binds fn(K1) with scope K2 and P; the modification
pattern K2 binds fn(K2)\ fn(K1) with scope P.
Finally, self(x) C binds the object name x to the receiver (self) with
scope C.
Class definitions class c = C in P are the only binders for class
names c, with scope P.
The scoping rules appear in Figure 4; as usual,
+ means disjoint union.
Processes, classes, and reaction rules are taken up to
a-conversion.
Labels don't have scopes.
Labels declared in patterns and classes, written dl(K) and dl(C),
are specified in Figure 4. We say that a label is
declared but undefined when it is declared only in abstract classes.
3.3 |
Rewriting semantics of the class language |
|
Figure 5: Rewriting semantics of the class language
Rules for processes ( |-® )
Class-Red |
|
|
obj x = C init P in P'
|-® obj x = C' init P in P' |
|
|
Rules for classes ( |-x® )
|
Or-Pat |
J or J' |> P |-x® J |> P or J' |> P |
|
|
Match |
C with S |-® C' dl(S) Í dl(C') |
|
|
match C with S end |-x® C' |
|
|
|
Evaluation contexts for classes
E{·} ::= {·} |
match E{·} with S end | E{·} or C | C or E{·}
Rules for filters ( |-® )
to 0em (Side conditions in the text)
-1em |
Filter-Apply |
K1 & K |> P with K1 Þ K2 |> Q | S
|-®
K2 & K |> P & Q or dl(K1) \ dl(K2) |
|
|
Filter-Next |
M |> P with S |
|
C'
dl(K1) ¬ Ídl(M) |
|
|
|
M |> P with K1 Þ K2 |> Q | S
|
|
C' |
|
|
|
|
Filter-Or |
C1 with S |-® C1' C2 with S |-® C2' |
|
|
(C1 or C2) with S |-® C1' or C2' |
|
|
|
The semantics of classes is defined by reduction to the core calculus.
The rules are given in Figure 5. Rules Class-Subst and Class-Red describe class rewritings for
processes. Rule Class-Red lifts an auxiliary reduction on
classes |-x® to processes. This auxiliary reduction
is parameterized by the name of the object and replaces
the (outermost) self names with the reduction parameter.
Rule Self removes inner bindings for the name of self.
Rule Or-Pat lifts or constructs from patterns to classes.
The next two rules for classes simplify abstract classes,
rule Class-Abstract discards empty abstract classes;
rule Abstract-Cut discards abstract labels that are declared elsewhere.
Rule Match reduces selective refinements
match C with S end by means of an auxiliary relations, described below.
Rule Class-Context applies rewriting under disjunctions and
selective refinements.
The auxiliary reduction |-® computes filters of the form C with S.
Every reaction rule M |> P in C is rewritten according to the leftmost
clause of S that matches M, that is, whose selection pattern K
is a sub-pattern of M (rules Filter-Next and
Filter-Apply). If no clause of S matches M, then the
reaction rule is left unchanged (rule Filter-End).
Abstract classes L in C are also left unchanged
(rule Filter-Abstract).
Note that rule Filter-Apply can be used only if the pattern K2 & K introduced by rule
Filter-Apply is well-formed, i.e.,
(1) K2 and K are not both empty,
(2) fn(K2) Ç fn(K) = Ø, and
(3) dl(K2) Ç dl(K)= Ø.
Condition (1) is enforced by syntactic restriction
2 of Section 3.2.
Condition (2) can be enforced by a-conversion.
Condition (3) will be checked by the type system.
The rewriting C with S |® C' may erase every reaction rule
defining a label of C. Specifically, rule Filter-Apply
removes the labels dl(K1) \ dl(K2). To prevent those
labels from being undeclared in C', rule Filter-Apply
records them as abstract labels.
The type system of Section 6 will compute an approximation
of abstract names to statically ensures that every erased label is
actually redefined before the class is instantiated.
Conversely, the rewriting C with S |® C' may introduce labels in C' that
are undeclared in C. Specifically, rule Filter-Apply
introduces the labels dl(K2) \ dl(K1).
The set dl(S) defined in Figure 4 statically collects all such labels.
However, some clauses of S may not be used, hence some label of dl(S) may not
be declared in C'.
This situation often corresponds to a programming error. To prevent
it, we supplement rule Match with the premise dl(S) Í
dl(C') that blocks the rule, and we interpret this situation as a
dynamic refinement error.
Next, we summarize the outcome of class reduction for processes.
One can easily check that the rewriting semantics is deterministic and
always terminates.
Using rule Class-Subst, any class construct can be eliminated, so
we focus on object creations:
Lemma 1 [Rewriting]
Let P be a process of the form obj x = C init Q in Q' such that
rule Class-Red does not apply to P. One of the following holds:
-
Completion:
- C is a disjunction of reaction rules
(C = ori = 1n Mi |> Pi).
- Failure:
- For some evaluation context E, we have:
-
C = E{c} and c is free (undefined class).
- C = E{L} and L is not under a
match (undefined label).
- Refinement error:
- C contains a blocked refinement in evaluation
context:
C = E { match C' with S end}, C' with S |-® C'',
and dl(S) ¬ Ídl(C'').
The distinction between failures and refinement errors matters only in the
typed semantics, which prevents all failures but not necessarily
refinement errors.
Like in Section 2, we call ``definition'' and write D
instead of C for any class of the form given in the Completion case.
3.4 |
Implementation issues |
|
In order to compile disjunctions and selective refinements, one
must access the patterns of parent classes. This hinders the abstract
compilation of patterns, but does not otherwise preclude separate
compilation.
As in a functional setting, the guarded processes attached to
individual reaction rules can be immediately compiled into closures
abstracted with respect to their free names, including formal message
parameters.
This approach is compatible with the JoCaml implementation, which
keeps a concrete representation of join patterns as vectors of bits;
the control of the synchronization of messages and the activation of
guarded processes is then realized by interpreting these bit vectors at
runtime [16].
In an implementation of the object calculus with classes, such vectors
of bits would serve as a basis of a data structure for representing classes
at runtime.
In the core objective join calculus, patterns do not contain
alternatives `` or''. To eliminate them, rule Or-Pat
duplicates reaction rules whose patterns contain alternatives.
Alternatively, we could have supplemented the object calculus with
or-patterns, but we view this as an optimization issue.
Perhaps more importantly, the unsharing of reaction rules
performed by rule Or-Pat
does not mean that guarded processes are duplicated by the compiler.
Since guarded processes are compiled as closures, duplicating P in
the semantics means duplicating an indirection to the closure that
implements P.