Previous Up Next
4 Solving challenging examples

As remarked by many authors, the classical point of view on class abstraction---method names and signatures are known, method bodies are abstract---does not mix well with concurrency. More specifically, the signature of a parent class does not usually convey any information on its synchronization behavior. As a result, it is often awkward, or even impossible, to refine a concurrent behavior using inheritance. (More conservatively, object-oriented languages with plain concurrent extensions usually require that the synchronization properties be invariant through inheritance, e.g., that all method calls be synchronized. This strongly constrains the use of concurrency.) This well-known problem is often referred to as the inheritance anomaly. Unfortunately, inheritance anomaly is not defined formally, but by means of problematic examples.

In [18] for instance, Matsuoka and Yonezawa identify three patterns of inheritance anomaly. For each pattern, they propose a refinement of the class language that suffices to express the particular synchronization property at hand: they identify the parts of the code that control synchronization in the parent class (which are otherwise hidden in the body of the inherited methods); they express this ``concurrency control'' in the interface of the class; and they rely on the extended interface to refine synchronization in the definition of subclasses.

In principle, it should be possible to fix any particular anomaly by enriching the class language in an ad hoc manner. However, the overall benefits of this approach are unclear. Our approach is rather different: we start from a core calculus of concurrency, rather than programming examples, and we are primarily concerned with the semantics of our inheritance operators. Tackling the three patterns of inheritance anomaly of [18], as we do in this section, appears to be a valuable test of our design. Indeed, the issue of inheritance anomaly is out of the scope of this paper. We refer to other studies, such as [20], for analyses of this issue, which, however, concern different and untyped frameworks.

We consider the same running example as Matsuoka and Yonezawa: a FIFO buffer with two methods put and get to store and retrieve items. We also adopt their taxonomy of inheritance anomaly: inheritance induces desirable modifications of ``acceptable states'' [of objects], and a solution is a way to express these modifications.

In the following examples, we use a language extended with basic datatypes. Booleans and integers are equipped with their usual operations. Arrays are created by create(n), which gives an uninitialized array of size n. The size of an array A is given by A.size. Finally, the array A[i] <- v is obtained from A by overwriting its i-th entry with value v.

The FIFO buffer of [18] can then be written as follows: 
class buff = self (z)
   put(v,r) & (Empty(A, i, n) or Some(A, i, n)) |>
     r.reply() & z.Check(A[(i+n) mod A.size] <- v, i, n+1)
or get(r) & (Full(A, i, n) or Some(A, i, n)) |>
     r.reply(A[i]) & z.Check(A, (i+1) mod A.size, n-1)
or Check(A,i,n) |>
     if n = A.size then z.Full(A, i, n)
     else if n = 0 then z.Empty(A, i, n)
     else z.Some(A, i, n)
or Init(size) |> z.Empty(create(size), 0, 0)
The state of the buffer is encoding a circular array represented by a message with label Empty, Some, or Full. These labels carry three arguments. The first one, A is the array; the second one, i is the index of the first element of the buffer; the third one, n is the number of elements in the buffer. The buffer may react to messages on put when non-full, and to messages on get when non-empty; this is expressed in a concise manner using the or operator in patterns. Once a request is accepted, the state of the buffer is recomputed by sending an internal message on Check. Since Check appears alone in a join pattern, message sending on Check acts like a function call.

Partitioning of acceptable states.
The class buff2 supplements buff with a new method get2 that atomically retrieves two items from the buffer. For simplicity, we assume size> 2.

Since get2 succeeds when the buffer contains two elements or more, the buffer state needs to be refined. Furthermore, since for instance a successful get2 may disable get or enable put, the addition of get2 has an impact on the ``acceptable states'' of methods get and put, which are inherited from the parent buff. Therefore, label Some is not detailed enough and is replaced with two labels One and Many. One represents a state with exactly one item in the buffer; Many represents a state with two items or more in the buffer. 
class buff2 = self(z)
   get2(r) & (Full(A,i,n) or Many(A, i, n)) |>
        r.reply(A[i], A[(i+1) mod A.size])
     &  z.Check(A, (i+2) mod A.size, n-2)
or match buff with
     Some(A, i, n) => (One(A, i, n) or Many(A, i, n)) |> nil
   end
or Some(A, i, n) |>
     if n > 1 then z.Many(A, i, n) else z.One(A, i, n)
In the program above, a new method get2 is defined, with its own synchronization condition. The new reaction rule is cumulated with those of buff, using a selective refinement that substitutes ``One(...) or Many(...)'' for every occurrence of ``Some(...)'' in a join pattern. The refinement eliminates Some from any inherited pattern, but it does not affect occurrences of Some in inherited guarded processes: the parent code is handled abstractly, so it cannot be modified. Instead, the new class provides an adapter rule that consumes any message on Some and issues a message on either One or Many, depending on the value of n.

History-dependent acceptable states.
The class gget_buff alters buff as follows: the new method gget returns one item from the buffer (like get), except that a request on gget can be served only immediately after serving a request on put. More precisely, a put transition enables gget, while get and gget transitions disable it. This condition is reflected in the code by introducing two labels AfterPut and NotAfterPut. Then, messages on gget are synchronized with messages on AfterPut. 
class gget_buff = self (z)
   gget(r) & AfterPut() & (Full(A, i, n) or Some(A, i, n)) |>
        r.reply(A[i]) & z.NotAfterPut()
     &  z.Check(A, (i+1) mod A.size, n-1)
or match buff with
   Init(size) => Init(size) |> z.NotAfterPut()
 | put(v, r) =>
     put(v, r) & (AfterPut() or NotAfterPut()) |> z.AfterPut()
 | get(r) =>
     get(r) & (AfterPut() or NotAfterPut()) |> z.NotAfterPut()
end
The first clause in the match construct refines initialization, which now also issues a message on NotAfterPut. The two other clauses refine the existing methods put and get, which now consume any message on AfterPut or NotAfterPut and produce a message on AfterPut or NotAfterPut, respectively.

Modification of acceptable states.
We first define a general-purpose lock with the following locker class: 
class locker = self (z)
   suspend(r) & Free() |> r.reply() & z.Locked()
or resume(r) & Locked() |> r.reply() & z.Free()
This class can be used to create locks, but it can also be combined with some other class such as buff to temporarily prevent message processing in buff. To this end, a simple disjunction of buff and locker is not enough and some refinement of the parent class buff is required: 
class locked_buff = self (z)
   locker
or match buff with
     Init(size) => Init(size) |> z.Free()
   | nil => Free() |> z.Free()
   end
The first clause in the match construct supplements the initialization of buff with an initial Free message for the lock. The second clause matches every other rule of buff, and requires that the refined clause consume and produce a message on Free. (The semantics of clause selection follows the textual priority scheme of ML pattern-matching, where a clause applies to all reaction rules that are not selected by previous clauses, and where the empty selection pattern acts as a default case.)

As a consequence of these changes, parent rules are blocked between a call to suspend and the next call to resume, and parent rules leave the state of the lock unchanged. In contrast with previous examples, the code above is quite general; it applies to any class following the same convention as buff for initialization.

Further anomalies
Dealing with the examples above does not mean that we solved the inheritance anomaly problem. Indeed, most limitations of expressiveness can be interpreted as inheritance anomalies. We conclude this section with a more difficult example, for which we only have a partial solution. The difficulty arises when we try to delegate privileged access to an object.

Consider a class with some mutable state, such as the one-place buffer of Section 3.1: 
class buffer = self(z)
   get(r)  & Some(n) |> r.reply(n) & z.Empty()
or put(n,r) & Empty() |> r.reply() & z.Some(n)


We want to supplement buffer with an incr method that increments the buffer content. One might also require incr to be performed by using get and put from another object server: 
obj server =
   do_incr(x,r) |> obj s = reply(n) |> x.put(n+1,r) in x.get(s)
Furthermore, we require that the call to put from inside do_incr never block. Thus, any other call to put should be blocked during the execution of do_incr. To enforce this partial exclusion, we introduce an Exclusive flag, we take two copies of the parent class, and we specialize their definitions of put for external calls (disallowed during an increment) and privileged calls (performed only from the server). In the latter refinement clause, the conflicting method put is renamed to Put_priv, and a ``proxy object'' that forwards put calls to Put_priv is passed to the server. 
class counter = self(z)
      match buffer with
        put(n,r) => put(n,r) & Exclusive() |> z.Exclusive() 
      end
   or match buffer with 
        put(n,r) => Put_priv(n,r) |> nil
      end
   or incr(r) & Exclusive() |> 
        obj s = reply() |> r.reply() & z.Exclusive() in 
        obj proxy = get(r) |> z.get(r) 
                 or put(n,r) |> z.Put_priv(n,r) in 
        server.do_incr(proxy,s) 
   or Init() |> z.Empty() & z.Exclusive()
Our solution is not entirely satisfactory. In particular, the duplication of method put forces further refinements of counter to treat the two methods put and Put_priv in a consistent manner. For instance, if we refine counter in order to log successful puts, as we do in example logged_buffer_bis of Section 3.1, then the puts from server are not logged.

We can improve this by keeping a single copy of put ---the private one--- and make the public method pub synchronously forwarding its call to the private version (synchrony is required to ensure that the Exclusive lock is only released when the forwarded call to the private version of put has returned.) 
class counter = self(z)
      match buffer with
        put(n,r) => Put_priv(n,r) |> nil
      end
   or put(n,r) & Exclusive() |> 
        obj s = reply(x) |> r.reply(x) & z.Exclusive() in
        z.Put_priv(n,s)
   or incr(r) & Exclusive() |> 
        obj s = reply() |> r.reply() & z.Exclusive() in 
        obj proxy = get(r) |> z.get(r) 
                 or put(n,r) |> z.Put_priv(n,r) in 
        server.do_incr(proxy,s) 
   or Init() |> z.Empty() & z.Exclusive()
The class can not be inherited as long as the clients operates on the private version Put_private instead of the public name put that is just used as an entry point.

A more elegant approach is to stick to views in the style of [27, 30]. A view is a map from method names to method slots. Method slots are positions for method implementations in a class, which are used for self-referencing other methods of the same object. Overriding of a method amounts to change the method implementation, thus affecting the other methods that reference the overridden method slot. Overriding must preserve method slot types. Therefore method slots cannot be hidden in classes, since otherwise, they could be redefined with another incompatible type. On the contrary, a method name can be safely erased from a view, leaving its slot unreachable (in that view). A later redefinition of the same name will simply allocate a new unrelated slot. In the traditional approach---the one that we followed---names and slots are in a one-to-one correspondence. Hence, methods cannot be forgotten in classes (they can only become abstract and will have to be redefined later before taking an instance of the class). Views are a much more powerful mechanism, but they require a significant complication of the type system.

Previous Up Next