A Calculus for Concurrent Objects

Paolo Di Blasio^{1} and Kathleen Fisher^{2} ^{⋆}

1 Dipartimento di Informatica e Sistemistica Università “La Sapienza”, via Salaria 113, 00198 Roma

                   diblasio@dis.uniroma1.it

2 Computer Science Department Stanford University, Stanford, CA 94305

                   kfisher@cs.stanford.edu

Abstract. This paper presents an imperative and concurrent extension of the functional object-oriented calculus described in [FHM94]. It belongs to the family of so-called prototype-based object-oriented languages, in which objects are created from existing ones via the inheritance primitives of object extension and method override. Concurrency is introduced through the identification of objects and processes. To our knowledge, the resulting calculus is the first concurrent object calculus to be studied. We define an operational semantics for the calculus via a transition relation between configurations, which represent snapshots of the run-time system. Our static analysis includes a type inference system, which statically detects message-not-understood errors, and an effect system, which guarantees that synchronization code, specified via guards, is side-effect free. We present a subject reduction theorem, modified to account for imperative and concurrent features, and type and effect soundness theorems.

1 Introduction

In the past few years, the desire to bring the benefits of object-oriented programming (modularity, re-usability and incremental design) to multiprocessor environments has led to a significant interest in concurrent object-oriented programming. The fact that objects seem to provide a suitable abstraction for concurrent programming has further encouraged research in this area. Various languages have been designed, some from scratch (e.g. POOL [Ame89] and ABCL [Yon90]), and others by adding concurrent features to existing object-oriented languages (e.g. concurrent C++ [CGH89] and Eiffel[Car93]). Despite this broad interest, the most effective combination of the object-oriented and concurrent paradigms has not yet emerged.

Considerable effort has been spent in developing theoretical frameworks for studying this issue. To date, there have been two main approaches to such studies: actor languages and process algebras. The actor model [Agh86] can easily

⋆ Supported in part by a Fannie and John Hertz Foundation Fellowship and NSF Grant CCR-9303099.

represent concurrent objects [Agh90] and has been used as a foundation for designing various concurrent object-oriented languages (e.g. ABCL [Yon90] and [FA93]). Theoretical research using this model has focused on semantics and equational theories (e.g. [AMS92, Tal96]). The process algebra approaches to modeling concurrent object-oriented systems [PT94, Vas94, Nie92, KY94, Jon93] are often extensions of the π-calculus, obtained by adding objects and functional constructs. Researchers adopting this approach have paid particular attention to typing issues (c.f. [Vas94, KY94]).

Both the actor and the process algebra approaches suffer from not directly supporting objects, a lack which makes some object-oriented features quite difficult to represent in these frameworks. In contrast, functional object-oriented calculi [AC94, FHM94] already have primitives for object-oriented features and so are a convenient starting point for studying concurrent object-oriented systems. Despite the naturalness of adding concurrency to such calculi, this approach has not been extensively investigated. To our knowledge, Cardelli’s object-based language for distributed computation Obliq [Car95] is the only existing language that adopts this philosophy. Except for its sequential imperative core [AC95], however, no formal study of Obliq’s semantics or its types has been carried out.

The general goal of this research is to establish theoretical foundations for concurrent object-oriented programming, focusing on the development of intuitive semantics and sound type systems. As a first step towards this goal, we present an imperative and concurrent extension of the calculus in [FHM94]. We believe that one of the contributions of this work is to introduce a new direction for the design of formal systems for studying concurrent object-oriented programming, that of adding concurrency primitives to object calculi.

The rest of the paper is organized as follows. In Section 2, we describe our extended language, focusing on the design choices we made in defining our calculus. In Section 3 we present an example program-fragment to illustrate our language. Section 4 describes an operational semantics for the language, and Section 5 presents its static type system. Section 6 contains the technical results of the paper, including a subject reduction theorem, modified to account for imperative and concurrent features. Type soundness follows as a corollary. Section 7 concludes with some notes on future work.

2 The language: an overview

In this section, we give an overview of our concurrent object-calculus, focusing on the design choices we made in its development. Typing. The usefulness of static type systems in increasing the reliability and readability of programs, in detecting compile-time type errors, and in providing useful compile-time information is widely recognized. Hence, we chose to define a static type system for our calculus. Reassuringly, only straightforward modifications to the type system of the functional object calculi of [FHM94] were required. One such modification was the incorporation of an effect system [LG88] to insure that the guards we use to define synchronization code are side-effect free (See below). The potential to leverage prior work in this fashion is one of the appeals of designing concurrent object-oriented calculi by extending sequential functional ones.

Prototype-based calculus. The object model of our calculus uses a prototypebased approach to represent inheritance. In other words, new objects are created from existing ones via the inheritance primitives of object extension and method override. A consequence of this approach is that the methods of each object are embedded in the object itself, which is important for managing method lookup when objects are physically distributed on a network. In our syntax the expression ⟨⟩ creates an empty object, ⟨ob ←+ m = method ⟩ extends object ob with new method m whose code is specified in method, and ⟨ob ← m = method ⟩ replaces ob’s m-method with new code method. We adopt these inheritance primitives instead of the more complex operators defined in Obliq (e.g. clone) because Obliq’s operators can be encoded.

Processes as objects. Objects represent a suitable and appealing abstraction for the notion of a process, so we introduce concurrency by identifying objects and processes. It is hoped that this unification might simplify the process of writing concurrent code. More definitely, it allows us to use our object primitives to create and activate processes, thus reducing the number of primitives in the calculus.

Communication mechanisms. Concurrent object-oriented languages that unify the notions of object and process use three kind of communication: synchronous, asynchronous and eager invocation [WKH92]. In our calculus, we chose to directly support synchronous and asynchronous method invocation because both are interesting and neither is encodable in the other without adding more syntax. We do not directly provide eager invocation because it can be derived via an encoding of future variables as objects. In our syntax, expression ob ⇐_{a} m(arg) sends message m asynchronously with argument arg to object ob. The corresponding synchronous invocation is ob ⇐_{s} m(arg).

Synchronization constraints. In a concurrent object-oriented language, at any given time an object may only be able to respond to a subset of its entire set of messages without losing its internal integrity. For example, a buffer object cannot meaningfully respond to a put message if its internal storage is full. Instead, it must wait until a get message causes some of its space to become free. Such restrictions on the availability of methods are called synchronization constraints because they affect the order in which methods are executed. Code that controls method availability is called synchronization code [MY93]. We use guards for this purpose, because they provide one of the most natural ways to define synchronization code and they require minimal additional syntax. (See [Yon90] for another use of guards.) In our language, each method consists of a guard and a method body, i.e., each method has the form when(g) body. To insure that guards behave properly, our static analysis guarantees that guards return boolean values and cause no side effects.

Protection. A crucial point in the calculus is the distinction between self and non-self-inflicted operations. According to the definitions introduced in [Car95], method overriding ⟨ob ← m = method ⟩ and invocation ob ⇐ m(arg)^{3} are selfinflicted iff ob is the same object as the self -parameter of the current method. Otherwise the operation is non-self-inflicted^{4}. Method overriding has different semantics in these two cases. In the self-inflicted case, ⟨ob ← m = method ⟩ replaces the method m of the object ob. This operation is the only way to update the state of an object in our calculus. The non-self-inflicted overriding has a cloning semantics, meaning that we first create a copy of the object ob and then replace the m method with the new method^{5}. There are two reasons for these choices. First, we want to provide a form of protection against external writing operations. By insuring that only self-inflicted operations can modify their host object, we can safeguard internal invariants of objects. Secondly, the cloning semantics allows us to support depth inheritance (via method overriding)^{6}.

Serialized objects. As we will formalize in Section 4, an object can be in either an idle or a busy state. Non-self-inflicted operations can be executed only if their target object is in the idle state. This restriction gives each object a serialized structure: at any time a given object is involved in at most one thread of computation. This single-threadedness helps maintain object invariants, since we are guaranteed that once an object starts a computation, it will not be interrupted by an outside request until it has finished its computation. Selfinflicted operations do not have to wait for their target object to become idle. The methods of an object need to be able to access other host object methods without immediately causing deadlock. This freedom maintains the single-threadedness of objects, since self-inflicted operations continue in the same thread.

As can be seen from the preceding paragraphs, the notion of self-infliction is an important concept. Unfortunately, whether an operation is self-inflicted or not can generally only be determined at run-time. Currently, our type system does not approximate this distinction. We leave this question to future work.

3 Example: a buffer and a producer

To provide some intuition for this calculus, we give example producer and oneslot buffer objects. A more complete version can be found in [DF96]. As we will see formally in the next section, the language consists of the untyped λcalculus extended with the object primitives described above. As a notational convenience, we adopt the following syntactic conventions. We write ⟨m_{1} = when(e_{1})e′_{1}, …, m_{k} = when(e_{k})e′_{k}⟩ for ⟨… ⟨⟨⟩ ←+ m_{1} = when(e_{1})e′_{1}⟩ … ←+ m_{k} = when(e_{k})e′_{k}⟩. If we have a method invocation with no parameters, we write e_{1} ⇐ m instead of e_{1} ⇐ m(nil), where nil is a constant with type unit. We introduce the semicolon operator e_{1}; e_{2} as syntactic sugar for ((λz. λx. x)e_{1})e_{2}, which has the expected meaning for sequencing as our semantics reflects call-by-value evaluation. Finally, we use integer constants and their related operations.

3 The symbol ⇐ indicates either synchronous and asynchronous method invocation. 4 Note that self-inflicted method extension is prevented by the type system. 5 Non-self-inflicted method extension has the same semantics. 6 Width inheritance is obtained via object extension.

The following code creates an empty one-slot buffer object:

buffer = ⟨ x = λself. λarg. 0,
size = λself. λarg. 0,
put = when(λself.(self ⇐_{s} size) = 0)
λself. λv.⟨⟨self ← x = λs. λa. v⟩ ← size = λs. λa. 1⟩,
get = when(λself.(self ⇐_{s} size) = 1)
λself. λarg.⟨self ← size = λs. λa. 0⟩; self ⇐_{s} x ⟩

Both guards and method bodies occasionally need to access other methods of their host object. To grant this access, we write them as functions from a self parameter to their actual code. The operational semantics binds these parameters to the host object when the corresponding methods are invoked.

The x method represents the storage of the buffer. The size method indicates whether or not the buffer is full by storing either a 0 (for empty) or a 1 (for full). Both of these methods have constantly true guards, which we omit for clarity. The put method is only available if the buffer is currently empty, which its guard checks by comparing its current size to 0. When available, put stores a new value into the buffer’s storage x and sets the size to 1. Finally, the get method, which is only available if the buffer is full, sets the current size to 0 and returns the value contained in the storage x.

When an object is created, it is associated with an address generated by the system. Future interactions with that object occur via the generated address, which may be thought of as the name of the object. For expository purposes, we will assume that the name generated for the above buffer object is buff.

We may write a producer object that interacts with the buff object as follows:

producer = ⟨m = λself. λarg.((λy. buff ⇐_{a} put(y))(value prod())) ; self ⇐_{a} m⟩

Invoking a producer object’s m method causes a non-terminating computation to start. During each iteration of this computation, the producer gets a new value by calling the function value prod and then stores this value in the buffer by asynchronously sending buff the message put. We will assume the name generated for the producer object is prod.

We illustrate the computational behavior of our objects using the following simplified evaluation rule that reflects the operational semantics defined precisely below:

⟨m_{1} = when(e′_{1})e_{1}, …, m_{k} = when(e′_{k})e_{k}⟩ ⇐ m_{i} ⟶ e_{i} ⟨m_{1} = when(e′_{1})e_{1}, …, m_{k} = when(e′_{k})e_{k}⟩

This rule allows us to evaluate a message send by retrieving the appropriate method body from the object and applying it to the entire object itself.

Using the rule above and call-by-value β-reduction, we may evaluate the message send prod ⇐_{a} m, assuming value prod() ⟶ v_{1}:

prod ⇐_{a} m ⟶ (λself. λarg.((λy. buff ⇐_{a} put(y))(value prod())) ; self ⇐_{a} m) prod nil
⟶ ((λy. buff ⇐_{a} put(y))(value prod())) ; prod ⇐_{a} m)
⟶ (buff ⇐_{a} put(v_{1})) ; prod ⇐_{a} m
⟶ prod ⇐_{a} m

The asynchronous method invocation buff ⇐_{a} put(v_{1}) (a non-self-inflicted operation) is put in the queue of pending messages, and the computation continues, sending again message m to the object prod. When the buffer is free to receive the message put(v_{1}), it evaluates the guard for the method put. If this evaluation returns true, then the put(v_{1}) message is removed from the queue and the method body is executed. Otherwise, the message remains in the queue. The put method reduces as follows:

buff ⇐_{a} put(v_{1}) ⟶ (λself. λv.⟨⟨self ← x = λs. λa. v⟩ ← size = λs. λa. 1⟩) buff v_{1}
⟶ ⟨⟨buff ← x = λs. λa. v_{1}⟩ ← size = λs. λa. 1⟩
⟶ ⟨buff ← size = λs. λa. 1⟩
⟶ buff

This evaluation overrides the methods x and size (both self-inflicted operations), so the object buff now has the following structure, modulo α-conversion:

buff : ⟨ x = λself. λarg. v_{1},
size = λself. λarg. 1, put = …, get = … ⟩

4 Operational Semantics

We formalize the operational semantics of the calculus as a transition relation on configurations, which can be thought of as global snapshots of the run-time system. A configuration contains the collection of all created objects and all pending messages. Formally, a configuration ⟨⟨ α | μ ⟩⟩ consists of an object soup α, containing run-time objects, and a collection of pending asynchronous messages μ. More precisely, μ is a finite map from integers to pending messages. As a notational simplification, we use a single collection of pending messages instead of having a smaller queue for each object.

An object is represented at run-time as a triple (a, η_{a}, [S_{a}]), where a is the object’s address, η_{a} is its method table, and S_{a} its state. A method table is a partial function from the set of method names M to guarded expressions of the form when(e_{2})e_{3}. The state S_{a} can be either idle ([I]) or busy ([te_{a}]), in which case the expression te_{a} represents the remaining computation. An object passes from the idle to a busy state in response to either a synchronous or an asynchronous method invocation. At the end of the resulting computation, it returns to the idle state.

4.1 Formal Language Specification

In this section, we introduce the notation needed to formally describe the operational semantics of the calculus.

Language expressions:

\begin{aligned}e : : = & x | c | a | λx. e | e_{1}e_{2} | ⟨⟩ | e_{1} ⇐_{a} m(e_{2}) | e_{1} ⇐_{s} m(e_{2}) \\ & | ⟨e_{1} ←+ m = when(e_{2})e_{3}⟩ | ⟨e_{1} ← m = when(e_{2})e_{3}⟩ \end{aligned}

te : : = gs(e, a) | ret(e, a) | ga(e, c) | nonret(e)

In the set of expressions e, x is a variable, c is a constant symbol, a is an object address, λx. e is a lambda abstraction, and e_{1}e_{2} is function application. The remaining syntactic forms are the object primitives described in Section 2. All expressions e except a may occur in source programs. The top-level expressions te appear as the states of busy objects in object triples. They allow us to determine if the expression we are reducing corresponds to a guard evaluation or to a method body application and further, if the reduction is in response to a synchronous or an asynchronous invocation. (We will see an example of this in the next section, where these top-level expressions are explained in more detail.)

To describe transitions internal to an object, we need to uniquely decompose each non-value expression into a reduction context filled with a redex. With this intent, we define values, redexes and reduction contexts.

Values:  v : : = x | c | a | λx. e
Top Values: tv : : = gs(v, a) | ret(v, a) | ga(v, c) | nonret(v)
Redexes:  e_{rdx} : : = v_{1}v_{2} | ⟨⟩ | v_{1} ⇐_{a} m(v_{2}) | v_{1} ⇐_{s} m(v_{2})

| ⟨v_{1} ←+ m = when(e)v_{2}⟩ | ⟨v_{1} ← m = when(e)v_{2}⟩

Inner Reduction Contexts:

r_{in} : : = □ | r_{in}e | v r_{in}
| r_{in} ⇐_{a} m(e) | v ⇐_{a} m(r_{in}) | r_{in} ⇐_{s} m(e) | v ⇐_{s} m(r_{in})
| ⟨r_{in} ←+ m = when(e)e_{1}⟩ | ⟨v ←+ m = when(e)r_{in}⟩
| ⟨r_{in} ← m = when(e)e_{1}⟩ | ⟨v ← m = when(e)r_{in}⟩

Top Reduction Contexts:

r_{top} : : = gs(r_{in}, a) | ret(r_{in}, a) | ga(r_{in}, c) | nonret(r_{in})

The reduction contexts identify which subexpression of a given expression is to be evaluated next. These contexts correspond to the standard call-by-value reduction strategy. Because we have two forms of expressions, we need two forms of reduction contexts: inner and top. The following lemma tells us that local computation inside objects is deterministic.

Lemma 1 Unique Decomposition. Given an expression te, then either te is a top value or there exists a unique (r_{top}, e_{rdx}) such that te = r_{top}[e_{rdx}].

4.2 Reduction Rules

In this section we define the transition relation ⟼ between configurations. We describe in detail the rules for evaluating asynchronous, non-self-inflicted invocations and method override because these rules illustrate the key concepts of the transition system. The other rules are similar to these or are straightforward and can be found in Appendix A. Although this transition relation describes an interleaving semantics for the calculus, a straightforward modification produces a truly concurrent semantics. Asynchronous, Non-Self-Inflicted Reductions. These rules describe the computation that results when an object a sends object b the message m asynchronously. The first rule says that the execution of an asynchronous method invocation proceeds by putting the message in the pending queue. The constant nil is returned to a to reflect the fact that the message has been placed in the queue. Integer i serves as the name or index of the pending message.

(⇐_{a}) non-self-inflicted i is fresh. ⟨⟨ α, (a, η, [r_{top}[b ⇐_{a} m(v)]]) | μ ⟩⟩ ⟼ ⟨⟨ α, (a, η, [r_{top}[nil]]) | μ, i: b ⇐_{a} m(v) ⟩⟩

When object b is in the idle state and there is a pending message m in μ for b, then b evaluates its guard for m within top-level expression ga according to the rule (μ):

(μ) η(m) = when(e)v ⟨⟨ α, (b, η, [I]) | i: b ⇐_{a} m(v′), μ ⟩⟩ ⟼ ⟨⟨ α, (b, η, [ga(e b, i)]) | i: b ⇐_{a} m(v′), μ ⟩⟩

The top-level expression ga stores the index of the message send from the queue. This information is needed so that the proper message send will be removed from the queue when the method body starts its evaluation.

If the guard evaluates to true, rule (μ-true) directs object b to start evaluating the method body for m within the top-level expression nonret. This rule also removes the message send at index i from the queue, since that message send is now being executed. This rule illustrates the role of the top-level expressions. If we simply had value true not wrapped by ga as the state of object b, we would not have enough information to figure out the new state for b.

(μ-true) η(m) = when(e)v ⟨⟨ α, (b, η, [ga(true, i)]) | i: b ⇐_{a} m(v′), μ ⟩⟩ ⟼ ⟨⟨ α, (b, η, [nonret(v b v′)]) | μ ⟩⟩

Finally, when the body of the method has been evaluated to a value, rule (nonret) returns object b to the idle state and throws away the resulting value. Note that if we simply had value v′′ as the state of object b, we would not have enough information to determine that v′′ is the result of an asynchronous method invocation and hence should be thrown away.

(nonret) ⟨⟨ α, (b, η, [nonret(v′′)]) | μ ⟩⟩ ⟼ ⟨⟨ α, (b, η, [I]) | μ ⟩⟩

Method Override Reductions. There are two different rules for evaluating the method override operation, one for self-inflicted and one for non-self-inflicted operations. In the self-inflicted case, we simply replace the guard and body of the method m in the method table of a:

(←) self-inflicted

⟨⟨ α, (a, η, [r_{top}[⟨a ← m = when(e)v⟩]]) | μ ⟩⟩ ⟼

⟨⟨ α, (a, η[m]: = when(e)v, [r_{top}[a]]) | μ ⟩⟩

Note that because this operation is self-inflicted, we do not wait for a to become idle before performing the update. The notation η[m]: = when(e)v stands for the function η′ that is just like η except that it maps m to when(e)v. This operation returns the address of the modified object as its result. In the non-self-inflicted case, we must wait for b to enter the idle state before performing a method override requested by object a:

(←) non-self-inflicted b′ is a fresh address

⟨⟨ α, (a, η, [r_{top}[⟨b ← m = when(e)v⟩]]), (b, η′, [I]) | μ ⟩⟩ ⟼ ⟨⟨ α, (a, η, [r_{top}[b′]]), (b, η′, [I]), (b′, η′[m]: = when(e)v, [I]) | μ ⟩⟩

This rule first clones object b to create a new object b′ and then replaces b′’s m method with the new guard and body. The address of the new object is returned. Note that we cannot clone object b if it is busy. To see this point, suppose we create b′ while b is executing e. If we put b′ in the idle state, we can violate the integrity of b′, because we do not complete the pending computation e, which could be responsible for restoring some invariant for b′. On the other hand, if we clone the state of b as well, we execute the pending computation e twice, potentially causing unwanted side-effects.

5 Type and Effect System

For the most part, the type system presented here is similar to the one defined in [FHM94]. The most novel parts are the effect system and the rules for typing asynchronous method invocation and guards. Because of space considerations, we present only the main ideas here. A complete presentation is in [DF96]

Pro Types. The type of an object is called a pro type, short for prototype. The following type expression:

pro t ⟨⟨m_{1} : τ_{1} → τ′_{1}, …, m_{k} : τ_{k} → τ′_{k}⟩⟩

defines a type t with the property that any expression e of this type is an object such that for 1 ≤ i ≤ k, the result of e ⇐_{s} m_{i}(e_{i}) is a value of type τ′_{i}, if e_{i} is of type τ_{i}. Keyword pro is a type binding operator. When bound type variable t appears in the types τ_{1} … τ_{k}, τ′_{1} … τ′_{k}, it refers to the entire type. Thus, when we say e ⇐_{s} m_{i}(e_{1}) has type τ′_{i}, we mean type τ′_{i} with any free occurrences of t in τ′_{i} replaced by the type pro t ⟨⟨m_{1} : τ_{1} → τ′_{1}, …, m_{k} : τ_{k} → τ′_{k}⟩⟩. Thus, pro types are a special form of recursive type.

As an example of this kind of type, we may give the one-slot buffer object considered above the type:

\begin{aligned}buff : pro t ⟨⟨ & x : unit → int, & size : unit → int, \\ & put : int → t, & get : unit → int⟩⟩ \end{aligned}

Effects. Our static analysis includes an effect system [LG88] that ensures that the evaluation of guards is side-effect free. This guarantee is important because the guard for a method may be invoked an arbitrary number of times before its corresponding body is allowed to proceed. Since this number is a property of how the system orders pending messages, it is undesirable for guards to produce any observable effects.

We formalize this requirement by adding pure and impure effects to our static analysis. Only those expressions with pure effect will be permitted in guards because such expressions are guaranteed to produce no observable effects. Although a finer analysis of effects is possible, for our current purposes this coarse division suffices. The effect expressions include the constants pure and impure, and ϵ_{1} ∨ ϵ_{2}, which is impure if either ϵ_{1} or ϵ_{2} is impure.

Typing and Effecting Rules. We describe in detail only the rule for typing asynchronous method invocation. More rules can be found in Appendix B.

(pro ⇐_{a})  \frac{\begin{matrix}Γ ⊢ e_{1} : τ & ϵ_{1} \\ Γ ⊢ e_{2} : [τ/t]τ_{1} & ϵ_{2} \end{matrix}}{Γ ⊢ e_{1} ⇐_{a} m(e_{2}) : unit & impure}

where τ = pro t ⟨⟨R | m : (τ_{1} →^{ϵ} τ_{2}) & ϵ′⟩⟩

The first hypothesis of this rule requires e_{1} to be an object that has at least a method m with type τ_{1} → τ_{2} plus other possible methods represented by R. The second hypothesis forces the type of the parameter e_{2} to be the same as the argument type of the method m, once we have substituted τ for any free variables t in τ_{1}. This substitution reflects the recursive structure of pro types. The type of the expression e_{1} ⇐_{a} m(e_{2}) is unit, because the asynchronous method invocation does not return any result. The effect is impure because we modify the queue of pending messages.

The latent effect of a method occurs whenever that method is executed. We discuss the effect portions of this rule in detail to illustrate how we track such effects. Because of call-by-value semantics, the body of the method m has the syntactic form λself. e. Effect ϵ′ records the latent effect of e, visible when we first reduce the method body by applying it to its host object and a parameter p: (λself . e) a p. In other words, the expression ([a/self]e)p reduces to (λarg. e′) p producing an effect ϵ′. Then [p/arg]e′ reduces to a value producing the effect ϵ.

6 Main Results

In this section we present subject reduction, side-effect freeness for guards, and type soundness theorems. We prove these results for programs, which are closed, address-free terms typeable in the empty context. Given a program e, its possible computations originate from the following initial configuration:

⟨⟨ (main, η, [I]) | μ ⟩⟩ where η(begin) = λself. λarg. e and μ(1) = main ⇐_{a} begin

which contains one object, whose address is main, with a method begin storing the program and one message pending that invokes method begin of main.

We let g and its decorated variants range over configurations. A computation sequence is a finite sequence of transitions of the form [g_{i} ⟼ g_{i+1} | i < n], for some natural number n, where g_{0} is an initial configuration.

Using techniques similar to those of [Har94], we prove a subject reduction theorem by extending typing judgments to type object addresses and method tables. With this intent, we extend our contexts to contain typing assumptions for object addresses:

Γ : : = … | Γ, a: τ where τ is a closed pro type. (See Appendix B for formal definitions of context and judgment.) We use Λ to indicate the projection of the context Γ onto the set of object addresses A. More formally, a: τ ∈ Λ iff a: τ ∈ Γ and a ∈ A. To state our subject reduction theorem, we need the following definitions.

Definition 2. A method table η_{a} of an object a is typeable in Γ if when Λ(a) = pro t ⟨⟨R | m : τ & ϵ⟩⟩ and ∀m_{i} ∈ dom(η_{a}), 1 ≤ i ≤ k, η_{a}(m_{i}) = when(e_{i})v_{i}, then the judgments

Γ, r: T → {m} ⊢ v_{i} : [pro t ⟨⟨r t | m : τ & ϵ⟩⟩/t](t →^{ϵ_{i}} τ_{i}) & pure

and

Γ, r: T → {m} ⊢ e_{i} : pro t ⟨⟨r t | m : τ & ϵ⟩⟩ →^{pure} bool & pure,

are both derivable.

In this definition m : τ & ϵ is an abbreviation for m_{1} : τ_{1} & ϵ_{1}, …, m_{k} : τ_{k} & ϵ_{k}. ObjAddr(α) stands for the set of addresses of objects contained in α.

Definition 3. An object soup α is typeable in Γ if dom(Λ)=ObjAddr(α) and ∀a ∈ ObjAddr(α), the method table η_{a} is typeable in Γ and if a is busy with state e_{a}, there exist type τ_{a} and effect ϵ_{a} such that the judgment Γ ⊢ e_{a}: τ_{a} & ϵ_{a} is derivable.

Definition 4. A pending queue μ is typeable in Γ if ∀i ∈ dom(μ), there exist type τ_{i} and effect ϵ_{i} such that the judgment Γ ⊢ μ(i) : τ_{i} & ϵ_{i} is derivable.

Definition 5. A configuration ⟨⟨ α | μ ⟩⟩ is typeable in Γ if α and μ are typeable in Γ.

In proving subject reduction, we are not interested in showing that the types of top-level expressions are preserved by reduction. Indeed, the types of these expressions are trivially preserved as they are always unit (see the typing rules in the Appendix B). Instead, we are interested in preserving the types of the expressions that occur one level below the top expressions. For example, if the state of object a is e_{a} ≡ ret(r_{in}[e_{rdx}], b) then r_{in}[e_{rdx}] is a’s one-level-down expression. If after one reduction step we have e′_{a} ≡ ret(r_{in}[e′], b), then we want to prove that r_{in}[e′] has whatever type we gave to r_{in}[e_{rdx}]. Moreover, note that subject reduction holds only for objects whose states before and after a transition are related. In particular, if an object passes through an idle state or transitions from evaluating a guard to evaluating a method body, then the types of its state before and after the transition will be unrelated. This makes sense, since the computations before and after such a transition are not connected.

Definition 6. If ⟨⟨ α | μ ⟩⟩ ⟼ ⟨⟨ α′ | μ′ ⟩⟩ via some transition rule T with a ∈ ObjAddr(α), we say that the states of a in α and α′ are related if a is busy in α and α′, and T is neither (μ-true) nor (⇐_{s}-true) on object a.

We order effects as follows: pure ≤ impure. The notation ϵ′ ≤ ϵ means that if ϵ is pure then ϵ′ is pure as well.

Definition 7. Given a transition g ⟼ g′ with g = ⟨⟨ α | μ ⟩⟩ and g′ = ⟨⟨ α′ | μ′ ⟩⟩ typeable in Γ and Γ′ respectively, we say that g and g′ are compatible if:

– α and α′ are compatible, that is, for all objects a whose states e_{a} and e′_{a} in α and α′ are related, there exist type τ_{a} and effects ϵ_{a} and ϵ′_{a} such that the judgments Γ ⊢ r_{in}[e_{rdx}]_{a}:τ_{a} & ϵ_{a}^{7} and Γ′ ⊢ r_{in}[e_{rdx}]′_{a}:τ_{a} & ϵ′_{a}, with ϵ′_{a} ≤ ϵ_{a} are both derivable;

– μ and μ′ are compatible, that is, ∀ i ∈ dom(μ) ∩ dom(μ′), there exists type τ and effect ϵ such that the judgments Γ ⊢ μ(i) : τ & ϵ and Γ′ ⊢ μ′(i) : τ & ϵ are derivable.

Theorem 8 Subject Reduction. Given a computation sequence [g_{i} ⟼ g_{i+1} | i < n], if g_{0} is typeable in some context Γ_{0}, then ∀i < n, there exist contexts Γ, Γ_{i}, Γ_{i+1}, with Γ_{i+1} ≡ Γ_{i}, Γ, such that g_{i} and g_{i+1} are typeable in Γ_{i} and Γ_{i+1}, respectively, and are compatible.

Side-effect freeness for guards and type soundness follow as corollaries of the previous theorem under the same hypothesis.

Corollary 9 Effect Freeness. Guard evaluation is side-effect free.

Definition 10. We define the error expressions of an object soup α to be those expressions of the forms (where r_{c} can be either r_{in} or r_{top}):

– r_{c}[v_{1} v_{2}] where v_{1} ≠ λx.e for some e;

– r_{c}[v_{1} ⇐ m(v_{2})] where v_{1} is not an object address a such that a ∈ ObjAddr(α) and η_{a}(m) exists.

– r_{c}[v_{1} ← m = when(e)v_{2}] where v_{1} is not an object address a such that a ∈ ObjAddr(α) and m ∈ dom(η_{a}).

– r_{c}[v_{1} ←+ m = when(e)v_{2}] where v_{1} is not an object address a such that a ∈ ObjAddr(α) and m ∉ dom(η_{a}).

Corollary 11 Type Soundness. Given a computation sequence [g_{i} ⟼ g_{i+1} | i < n], if g_{0} is typeable in some context Γ_{0}, then for every configuration g_{i} = ⟨⟨ α_{i} | μ_{i} ⟩⟩ and for every busy object a ∈ ObjAddr(α_{i}), e_{a} is not an error expression of the object soup α_{i}.

Type soundness, which follows from Theorem 8, guarantees that the type system statically detects all expressions that can reduce to the following error expressions: applying a non-functional value to an argument, sending an object a message for which it has no defined method (message not understood error), overriding a method which has not been defined, and extending an object with a method it already has.

7 Conclusions

We have presented what we believe is the first typed, prototype-based calculus for concurrent objects. We have described an operational semantics using a

7 Note that if e_{a} is typeable in Γ, then its one-level down expression r_{in}[e_{rdx}]_{a} is typeable in Γ as well.

transition system between configurations and have given a type and effect system. We have proven the soundness of our static analysis with respect to the operational semantics via a subject reduction theorem.

This work is intended as a starting point for studying the theoretical foundations of concurrent object-oriented programming. In the following, we briefly describe some issues we intend to investigate further. Our current type system does not support subtyping because subtyping is unsound in pure prototypebased calculi [FM94]. This problem has been solved for the sequential version of our calculus [FM95], and we believe this solution will carry over to our concurrent setting. A second research direction focuses on method availability. Our type soundness theorem demonstrates that the type system we have given detects “message not understood” errors at compile time, in the sense that no object will ever receive a message for which it has no method defined. However, the theorem does not ensure that the method in question is available (by virtue of having a true guard) when its execution is required. Although method unavailability is not a problem for asynchronous method invocation, it can cause deadlock in the synchronous case. Addressing this problem requires additional analysis to account for the communication behavior of objects. Such analyses may be done by modeling communication behaviors as process algebra expressions in the style of [NN93, Nie93]. Finally, we would like to investigate the equational theory of our calculus by defining an observational semantics in the style of [AMS92].

Acknowledgment. We are grateful to Carolyn Talcott and Anna Patterson for insightful discussions and carefully reading a draft of this paper.

References

[AC94] M. Abadi and L. Cardelli. A theory of primitive objects: untyped and first order systems. In Proc. of TACS’94, 1994.

[AC95] M. Abadi and L. Cardelli. An imperative object calculus: basic typing and soundness. In Proc. of second ACM-SIGPLAN workshop on state in programming Languages, 1995.

[Agh86] G. Agha. Actors: a model of concurrent computation in distributed systems. MIT Press, Cambridge, Mass., 1986.

[Agh90] G. Agha. Concurrent object-oriented programming. In Communication ACM 33(9), 1990.

[Ame89] P. America. Issue in the design of a parallel object-oriented language. In Formal Aspects of Computing, 1, 366-411, 1989.

[AMS92] G. Agha, I. Mason, S. Smith, and C. Talcott. Towards a theory of actor computation. In Proc. of CONCUR’92, 1992.

[Car93] D. Caromel. Towards a method of concurrent object-oriented programming. In Communication of ACM, 36(9), 1993.

[Car95] L. Cardelli. A language with distributed scope. In Computing Systems, 8(1):27–59, 1995.

[CGH89] R. Chandra, A. Gupta, and J. Hennessy. COOL: A language for parallel programming. In Proc. 2nd workshop on programming languages and compilers for parallel computing, IEEE CS, 1989.

[DF96] P. Di Blasio and K. Fisher. A calculus for concurrent objects. Stanford University, Technical Note STAN-CS-TN-96-35, 1996.

[FA93] S. Frolund and G. Agha. A language framework for multi-object coordination. In Proc. of ECOOP’93, 1993.

[FHM94] K. Fisher, F. Honsell, and J.C. Mitchell. A lambda calculus of objects and method specialization. In Nordic J. Computing (formerly BIT), 1:3–37, 1994. Preliminary version appeared in Proc. IEEE Symp. on Logic in Computer Science,, 26–38, 1993.

[FM94] K. Fisher and J.C. Mitchell. Notes on typed object-oriented programming. In Proc. Theoretical Aspects of Computer Software, pages 844–885. Springer LNCS 789, 1994.

[FM95] K. Fisher and J.C. Mitchell. A delegation-based object calculus with subtyping. In Proc. 10th Int’l Conf. Fundamentals of Computation Theory (FCT’95), pages 42–61. Springer LNCS 965, 1995.

[Har94] R. Harper. A simplified account of polymorphic references. In Information Processing Letters 51(4), 1994.

[Jon93] C. Jones. A pi-calculus semantics for an object-based design notation. In Proc. of CONCUR’93, 1993.

[KY94] N. Kobayashi and A. Yonezawa. Type theoretic foundations for objectoriented concurrent programming. In Proc. of OOPSLA’94, 1994.

[LG88] J. Lucassen and D. Gifford. Polymorphic effect systems. In Proc. of POPL’88, 1988.

[MY93] S. Matsuoka and A. Yonezawa. Analysis of inheritance anomaly in objectoriented concurrent programming languages. In Research Directions in Concurrent Object-Oriented Programming, MIT Press, 1993.

[Nie92] O. Nierstrasz. Towards an object calculus. In Proc. of the ECOOP’91 Workshop on Object-Based Concurrent Computing, 1992.

[Nie93] O. Nierstrasz. Regular types for active objects. In Proc. of OOPSLA’93, 1993.

[NN93] F. Nielson and H. Nielson. From CML to process algebra. In Proc. of CON-CUR’93, 1993.

[PT94] B. Pierce and D. Turner. Concurrent objects in a process calculus. In Proc. of Theory and Practice of Parallel Programming, 1994.

[Tal96] C. Talcott. Interaction semantics for components of distributed systems. In Proc. of FMOODS96, 1996.

[Vas94] V. T. Vasconcelos. Typed concurrent objects. In Proc. ECOOP’94, 1994.

[WKH92] B. Wyatt, K. Kavi, and S. Hufnagel. Parallelism in object-oriented languages: A survey. In IEEE Software, 1992.

[Yon90] A. Yonezawa. ABCL: An object-oriented concurrent system. MIT Press, Cambridge, Mass., 1990.

A Operational Semantics

The following rules complete the ones in section 4.2.

(λ) ⟨⟨ α, (a, η, [r_{top}[(λx. e)v]]) | μ ⟩⟩ ⟼ ⟨⟨ α, (a, η, [r_{top}[[v/x]e]]) | μ ⟩⟩
(⟨⟩) ⟨⟨ α, (a, η, [r_{top}[⟨⟩]]) | μ ⟩⟩ ⟼ ⟨⟨ α, (a, η, [r_{top}[a′]]), (a′, η′, [I]) | μ ⟩⟩

where dom(η′) = ∅ and a′ ∉ ObjAddr(α).

(←+) non-self-inflicted

⟨⟨ α, (a, η, [r_{top}[⟨b ←+ m = when(e)v⟩]]), (b, η′, [I]) | μ ⟩⟩ ⟼

⟨⟨ α, (a, η, [r_{top}[b′]]), (b, η′, [I]), (b′, η′[m]: = when(e)v, [I]) | μ ⟩⟩
where b′ ∉ ObjAddr(α).

(⇐_{a}) self-inflicted ⟨⟨ α, (a, η, [r_{top}[a ⇐_{a} m(v′)]]) | μ ⟩⟩ ⟼ ⟨⟨ α, (a, η, [r_{top}[(λx. nil)(v a v′)]]) | μ ⟩⟩

where η(m) = when(e)v.

(μ-false)

⟨⟨ α, (a, η, [ga(false, i)]) | i: a ⇐_{a} m(v′), μ ⟩⟩ ⟼
⟨⟨ α, (a, η, [I]) | i: a ⇐_{a} m(v′), μ ⟩⟩

(⇐_{s}) self-inflicted ⟨⟨ α, (a, η, [r_{top}[a ⇐_{s} m(v′)]]) | μ ⟩⟩ ⟼ ⟨⟨ α, (a, η, [r_{top}[v a v′]]) | μ ⟩⟩

where η(m) = when(e)v.

The next four rules share the condition that η_{b}(m) = when(e)v. (⇐_{s}) non-self-inflicted

⟨⟨ α, (a, η_{a}, [r_{top}[b ⇐_{s} m(v′)]]), (b, η_{b}, [I]) | μ ⟩⟩ ⟼

⟨⟨ α, (a, η_{a}, [r_{top}[b ⇐_{s} m(v′)]]), (b, η_{b}, [gs(e b, a)]) | μ ⟩⟩

(⇐_{s}-true)

⟨⟨ α, (a, η_{a}, [r_{top}[b ⇐_{s} m(v′)]]), (b, η_{b}, [gs(true, a)]) | μ ⟩⟩ ⟼

⟨⟨ α, (a, η_{a}, [r_{top}[b ⇐_{s} m(v′)]]), (b, η_{b}, [ret(v b v′, a)]) | μ ⟩⟩

(⇐_{s}-false) ⟨⟨ α, (b, η_{b}, [gs(false, a)]) | μ ⟩⟩ ⟼ ⟨⟨ α, (b, η_{b}, [I]) | μ ⟩⟩ (⇐_{s}-ret)

⟨⟨ α, (a, η_{a}, [r_{top}[b ⇐_{s} m(v′)]]), (b, η_{b}, [ret(v′′, a)]) | μ ⟩⟩ ⟼
⟨⟨ α, (a, η_{a}, [r_{top}[v′′]]), (b, η_{b}, [I]) | μ ⟩⟩

B Type and Effect System

Effects  ϵ : : = pure | impure | ϵ_{1} ∨ ϵ_{2}
Types  τ : : = t | τ_{1} →^{ϵ} τ_{2} | pro t R | bool | unit | int
Rows  R : : = r | ⟨⟨⟩⟩ | ⟨⟨R | m: τ & ϵ⟩⟩ | λt. R | Rτ
Kinds kind : : = T | κ κ : : = {m} | T →{m}
Contexts  Γ : : = ϵ | Γ , x: τ | Γ , t: T | Γ , r : κ | Γ , a: τ
Judgments Γ ⊢ ∗ well-formed context Γ ⊢ e: τ & ϵ term has type and effect

Γ ⊢ τ : T well-formed type Γ ⊢ R: κ row has kind

Rules for assigning types to terms We present only the rules concerning objects. The complete set is in [DF96].

(addr projection)  \frac{\begin{matrix}Γ ⊢ ∗ \\ a: τ ∈ Γ \end{matrix}}{Γ ⊢ a : τ & pure}
(empty object)  \frac{Γ ⊢ ∗}{Γ ⊢ ⟨⟩ : pro t ⟨⟨⟩⟩ & impure}
(pro ⇐_{s})  \frac{\begin{matrix}Γ ⊢ e_{1} : τ & ϵ_{1} \\ Γ ⊢ e_{2} : [τ/t]τ_{1} & ϵ_{2} \end{matrix}}{Γ ⊢ e_{1} ⇐_{s} m(e_{2}) : [τ/t]τ_{2} & ϵ_{1} ∨ ϵ_{2} ∨ ϵ′ ∨ ϵ}

where τ = pro t ⟨⟨R | m : (τ_{1} →^{ϵ} τ_{2}) & ϵ′⟩⟩

(pro ext)

\frac{\begin{matrix}Γ ⊢ e_{1} : pro t ⟨⟨R | ℓ : σ⟩⟩ & ϵ_{1} \\ Γ, t: T & ⊢ & R : \{ℓ, m\} \\ Γ, r : T →\{ℓ, m\} ⊢ e_{2} : pro t ⟨⟨r t | ℓ : σ, m : (τ_{1} →^{ϵ} τ_{2}) & ϵ′⟩⟩ →^{pure} bool & pure \\ Γ, r : T →\{ℓ, m\} ⊢ e_{3} : [pro t ⟨⟨r t | ℓ : σ, m : (τ_{1} →^{ϵ} τ_{2}) & ϵ′⟩⟩/t](t →^{ϵ′} τ_{1} →^{ϵ} τ_{2}) & ϵ_{3} \end{matrix}}{Γ ⊢ ⟨e_{1} ←+ m=when(e_{2})e_{3}⟩ : pro t ⟨⟨R | ℓ : σ, m : (τ_{1} →^{ϵ} τ_{2}) & ϵ′⟩⟩ & impure}

(pro ov)

\frac{\begin{matrix}Γ ⊢ e_{1} : pro t ⟨⟨R | ℓ : σ, m : (τ_{1} →^{ϵ} τ_{2}) & ϵ′⟩⟩ & ϵ_{1} \\ Γ, r : T →\{ℓ, m\} ⊢ e_{2} : pro t ⟨⟨r t | ℓ : σ, m : (τ_{1} →^{ϵ} τ_{2}) & ϵ′⟩⟩ →^{pure} bool & pure \\ Γ, r : T →\{ℓ, m\} ⊢ e_{3} : [pro t ⟨⟨r t | ℓ : σ, m : (τ_{1} →^{ϵ} τ_{2}) & ϵ′⟩⟩/t](t →^{ϵ′} τ_{1} →^{ϵ} τ_{2}) & ϵ_{3} \end{matrix}}{Γ ⊢ ⟨e_{1} ← m=when(e_{2})e_{3}⟩ : pro t ⟨⟨R | ℓ : σ, m : (τ_{1} →^{ϵ} τ_{2}) & ϵ′⟩⟩ & impure}

Rules to assigning types to top level expressions.

\begin{matrix}(exp gs) ; \frac{\begin{matrix}Γ ⊢ e : bool & pure \\ Γ ⊢ a : τ & pure \end{matrix}}{Γ ⊢ gs(e, a) : unit & pure} & (exp ret) ; \frac{\begin{matrix}Γ ⊢ e : τ_{1} & ϵ \\ Γ ⊢ a : τ_{2} & pure \end{matrix}}{Γ ⊢ ret(e, a) : unit & ϵ ∨ pure} \\ (exp ga) ; \frac{\begin{matrix}Γ ⊢ e : bool & pure \\ Γ ⊢ c : int & pure \end{matrix}}{Γ ⊢ ga(e, c) : unit & pure} & (exp nonret) ; \frac{Γ ⊢ e: τ & ϵ}{Γ ⊢ nonret(e) : unit & ϵ} \end{matrix}