Previous Up Next
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.

3.2 Syntax

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:
  1. 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.

  2. 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-Subst
class c = C in P |-® P {C/c}

Class-Red
C |-x® C'
obj x = C init P in P' |-® obj x = C' init P in P'
Rules for classes ( |-x® )
Self
self(z)  C |-x® C {x/z}
Or-Pat
J or J' |> P |-x® J |> P or J' |> P

Class-Abstract
C or Ø |-x® C
Abstract-Cut
L' = L \ dl(C)      L ¹ L'
C or L |-x® C or L'

Match
C with S   |-®   C'      dl(S) Í dl(C')
match C with S end   |-x®   C'
Class-Context
C |-x® C'
E[C] |-x® E[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-End
C with Ø   |-®   C
Filter-Or
C1 with S   |-®   C1'      C2 with S   |-®   C2'
(C1 or C2) with S   |-®   C1' or C2'

Filter-Abstract
L with S   |-®   L

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:
  1. C = E{c} and c is free (undefined class).
  2. 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.

Previous Up Next