BRICS RS-99-44 Nestmann et al.: Aliasing Models for Mobile Objects BRICS

Basic Research in Computer Science

Aliasing Models for Mobile Objects

Uwe Nestmann Hans Hüttel Josva Kleist Massimo Merro

BRICS Report Series RS-99-44

ISSN 0909-0878 December 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Uwe Nestmann & Hans Hüttel & Josva Kleist &

Massimo Merro. BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/99/44/

Aliasing Models for Mobile Objects^{∗}

Uwe Nestmann, Hans Hüttel, Josva Kleist BRICS^{†}, Aalborg University, Denmark

Massimo Merro^{‡} INRIA, Sophia-Antipolis, France

Abstract

In Obliq, a lexically scoped, distributed, object-oriented programming language, object migration was suggested as the creation of a copy of an object’s state at the target site, followed by turning the object itself into an alias, also called surrogate, for the remote copy. We consider the creation of object surrogates as an abstraction of the above-mentioned style of migration. We introduce Øjeblik, a typed distributionfree subset of Obliq, and provide four different configuration-style semantics, which only differ in the respective aliasing model. We show that two of the semantics, one of which matches Obliq’s implementation, render migration unsafe, while our new proposal allows for safe migration at least for a large class of program contexts. In addition, we propose a type system that allows a programmer to statically guarantee that programs belong to that class. Our work suggests a straightforward repair of Obliq’s aliasing model.

∗This paper is a revised and extended subset of Migration = Cloning ; Aliasing [HKMN99], which appeared in the Informal Proceedings of FOOL 6. An extended abstract of this revision, entitled Aliasing Models for Object Migration, appeared in the Proceedings of EUROPAR ’99, LNCS 1685, September 1999.

†Basic Research in Computer Science, Centre of the Danish National Research Foundation.

‡Supported by a Marie Curie fellowhip, No. ERBFMBICT983504, in the EU TMR-programme.

Contents

1 Introduction 1

2 Typed Protected Serialized Concurrent Objects 3 2.1 Syntax and Informal Semantics . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Types and Typing, but no Subtyping . . . . . . . . . . . . . . . . . . . . . 7

3 Intermezzo: Towards Formal Semantics 7 3.1 Facts: On the Stability of Alias Chains . . . . . . . . . . . . . . . . . . . . 9 3.2 Design Choices: Four Aliasing Models . . . . . . . . . . . . . . . . . . . . . 10

4 Four Operational Semantics for Øjeblik 13 4.1 Common Basic Concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.2 Aliasing Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 4.3 Behavioral Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 4.4 Peculiarities of Infliction, Aliasing, and Fork . . . . . . . . . . . . . . . . . 24 4.5 Invariant Run-Time Properties . . . . . . . . . . . . . . . . . . . . . . . . 25 4.6 Reduction vs Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

5 On the Safety of Surrogation 31 5.1 Safety as an Equation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 5.2 Aliasing Models for External Surrogation . . . . . . . . . . . . . . . . . . . 33 5.3 Self-Inflicted Surrogation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 5.4 On the Absence of Self-Surrogation . . . . . . . . . . . . . . . . . . . . . . 37 5.5 Towards a Safety Theorem for Provers . . . . . . . . . . . . . . . . . . . . 38 5.6 Towards a Safety Theorem for Programmers . . . . . . . . . . . . . . . . . 39

6 Conclusion 41

1 Introduction

Mobile object systems have been investigated for more than one decade, starting out with early representants, like Emerald [JLHB88], and recently a whole series of scientific workshops has been dedicated to mobile object systems [Vit99]. While mobility in object systems has well-known advantages, for example as support for load balancing or mobile agents, there is no common agreement on how mobile objects should actually be realized.

In this paper, our main goal is not to argue for one and against another particular way to implement mobile objects, but rather to study in considerable formal detail one proposal that was already suggested for the above-mentioned Emerald: the proposal that object migration can be derived from two other primitives—cloning and aliasing—by just performing them one after the other.

Migration = Cloning ; Aliasing This particular style of programming mobile objects was also advocated by Cardelli within the context of the lexically-scoped distributed programming language Obliq [Car95]. Since we are aiming at a formal investigation into mobile objects, we prefer to study migration in Obliq rather than in Emerald since the former can easily be seen as a proper extension of Abadi and Cardelli’s theoretically well-founded object calculi [AC96].

Obliq is well-suited for the above style of migration. Lexical scoping in distributed settings makes program analysis easier since the binding of variables is only determined by their location in the program text, and not by the execution site. While immutable values can be copied from site to site, mutable values are stationary; when they are exchanged between programs on different sites only network references are transmitted. Accordingly, since objects are mutable, the migration of an object does not physically move the object, but instead creates a clone of the object at the target site and then turns the original (local) object into an alias—sometimes called proxy—for the new (remote) object.

In concurrent and distributed programs, it is important that certain state changes in parts of the running system may happen transparently from the point of view of the rest of the system. Ensuring that the implementation of such state changes is in fact transparent can be a difficult task since the programmer must in principle anticipate all possible execution scenarios. So the question arises naturally, whether object migration in Obliq is transparent to the object’s clients, and how that can be stated formally.

Intuitively, migration of an object a to some other site works transparently, or safely, if (1) after the migration a client of a cannot tell that a is now an alias, and if (2) during migration it is not possible to interact with a in a way that prevents the migration operation from proper completion. In Obliq, mobile objects are therefore required to be protected and serialized: protection guarantees that aliases are persistent; serialization guarantees atomicity of the two-phase migration operation. Unfortunately, Obliq is not equipped with a formal semantics, except for an unpublished note by Talcott [Tal96], which provides a configuration-style semantics for a subset of Obliq excluding migration, so no formal treatment of the safety of migration has been possible up to now. The aim of our project [Nes99] is to remedy the lack of formality and to reason formally about migration.

From Migration to Surrogation We formalize the safety of migration based on an abstraction of it in a distribution-free setting. Indeed, since Obliq is lexically scoped, with respect to the results of Obliq computations we may safely ignore all aspects of distribution unless distribution sites fail. Following this idea, we define Øjeblik as Obliq’s concurrent core. On the other hand, Øjeblik can also be seen as a particular concurrent extension of the Imperative Object Calculus [AC96]. In this core language, the surrogation of an object a is described as the creation of a clone b of a and then turning a itself into a proxy for b, which forwards future request for methods of a to b. This precisely models migration, except that neither a nor b are attached to any distribution site at all.

Aliasing Models for Mobile Objects For a formal study of surrogation, we have to come up with a formal semantics. However, there are many possible design choices. As in Obliq, the creation of stationary aliases due to surrogation usually results in general alias chains in a running system and, as it turns out, it is essential for the safety of migration to get just the modeling of nodes in alias chains right. A detailed discussion and formal presentation of four different aliasing models for Øjeblik represents the core of this paper. Interestingly, one of these models corresponds to the implementation of Obliq [Car94], while another one corresponds to Talcott’s formal semantics for a subset of Obliq [Tal96], the only formal semantics for Obliq that we are aware of. Both of these models have severe problems with respect to the transparency of migration, as we shall exhibit formally by means of simple counterexamples.

Outline In Section 2, we present in detail our language Øjeblik for typed protected serialized concurrent objects. In Section 3, we informally develop four different aliasing models trying to emphasize the different design decisions behind them. In Section 4, we then formalize the models in terms of a configuration-style global-view semantics. To strengthen the meaningfulness of the semantics, we also collect a series of run-time properties of configurations and formulate them as invariants. In particular, we have a subject reduction theorem, so the typing of Øjeblik terms is compatible with the operational semantics. In Section 5, we investigate the safety of surrogation in the various aliasing models, where it turns out to be crucial whether an operation on an object occurs internally (requested by some method from within the object itself) or externally (requested from the outside of the object). This distinction enables us to draw several fundamental conclusions: (1) surrogation cannot be generally safe if its internal use is permitted, which is independent of the aliasing model; however, (2) only our so-called forwarder aliasing models have a chance to be safe for external surrogation; finally, (3) we provide a type system that statically guarantees that surrogations will always be external. In Section 6, we sum up our observations, we offer some interpretations, and we sketch some future work.

Related work Apart from Talcott [Tal96], closest to our work and like ours based on Abadi and Cardelli’s object calculus [AC96] are two concurrent object calculi, one by Gordon and Hankin [GH98], and one by Di Blasio and Fisher [DF96]. However, no account on object migration has been addressed in these works. Sekiguchi and Yonezawa present an encoding of coreObliq into their calculus λdist, but they do not consider aliasing [SY97]. Emerald [JLHB88] has many things in common with Obliq, including a similar style of migration by means of cloning and aliasing, as proposed at an early stage. In Distributed Oz [VHB^{+}97] object migration is a primitive notion, so objects are physically mobile and travel according to a provably safe mobile state protocol from site to site, wherever they are needed or intend to go.

2 Typed Protected Serialized Concurrent Objects

In the predecessors of this paper, we presented Øjeblik as an untyped language [HKMN99, NHKM99]. However, types can be added in a straightforward manner, which we do here in order to provide a more complete semantic model of Øjeblik, e.g., by investigating its compatibility with reduction. Another interesting point is that subtyping cannot be straightforwardly introduced due to peculiarities of aliasing (cf. § 2.2).

For the sake of simplicity, in comparison with Obliq [Car95], we omit ground values (like numbers, booleans, strings, etc.), data operations, and procedures, we restrict field selection to method invocation, we restrict multiple cloning to single cloning, we omit flexibility of object attributes, we replace field aliasing with object aliasing, we omit explicit distribution, and we omit exceptions and advanced synchronization, so we get a feasible, but still non-trivial language.

a, b, c ::= [l_{j} =m_{j}]_{j∈J}  object record
| a.l⟨ c̃⟩  method invocation
| a.l⇐m  method update
| a.clone  shallow copy
| a.alias⟨b⟩  object aliasing
| a.surrogate  object surrogation
| a.ping  object identity
| s, x, y, z  variables
| let x:A = a in b  local definition
| fork⟨a⟩  thread creation
| join⟨a⟩  thread destruction
m_{j} ::= ς(s_{j}:A, x̃_{j}:B̃_{j})b_{j} method
A, B, C ::= [l_{j} :B̃_{j}→C_{j}]_{j∈J}  object record type
| Thr(A)  thread type

Table 1: Syntax of Øjeblik expressions

2.1 Syntax and Informal Semantics

The set L of typed Øjeblik-expressions is generated as shown in Table 1, where method labels l and variables s, x, y, z are taken from countable sets L and X, respectively. Our type system extends the typing rules for the Imperative Object Calculus of [AC96] with a family of thread types Thr(A). Pairs x̃_{j}:B̃_{j} denote sequences x_{1_{j}}:B_{1_{j}}, …, x_{n_{j}}:B_{n_{j}}.

Function types A→B do only occur in object types [l_{j} :B̃_{j}→C_{j}]_{j∈J}, so they are not first-class types. Nevertheless, we sometimes abbreviate such object types by [l_{j} :A_{j}]_{j∈J}, when we intend to clarify that a type is not a thread type. Whenever appropriate or unambiguous, we deliberately omit the type information in bindings.

The remainder of this subsection presents an informal explanation of the semantics of Øjeblik terms, as suggested for Obliq [Car95], first ignoring aspects of protection and serialization, which are then explained as a second step. In the presentation, we assume that all terms are well-typed according to § 2.2, which formalizes that operations will always be “understandable”. Here, we mean that operations are always only requested on objects with a matching interface, but we avoid the term “understood” here, since operations may be invalid due to protection, or delayed due to serialization (see below).

Computation follows the call-by-value (leftmost-innermost) evaluation order of Obliq. In particular, in the following, whenever we use a term a, we implicitly assume that we have first evaluated a to some actual value, i.e., in most cases to an object reference.

Objects An object record [l_{j} =m_{j}]_{j∈J} is a finite collection of updatable named methods l_{j} =m_{j}, more generally called fields, for pairwise distinct labels l_{j} . In a method ς(s, x̃)b, the letter ς denotes a binder for the self variable s and argument variables x̃ within the body b. Moreover, every object in Øjeblik comes equipped with special methods for cloning, aliasing, surrogation, and ping, which cannot be overwritten by the update operation.

Method invocation a.l⟨ c̃⟩ with field l of the object a containing the method ς(s, x̃)b results in the body b with the self variable s replaced by (a reference to) the enclosing object a, and the formal parameters x̃ replaced by (references to) the actual parameters c̃ of the invocation.

Method update a.l⇐m overwrites the current content of the named field l in object a with method m and evaluates to the modified object.

The operation a.clone creates an object with the same fields as the original object and initializes the fields to the same entries as in the original object.

The operation a.alias⟨b⟩ replaces object a with an alias to b, written a≫b, regardless of whether a is already an alias or still an object record; if b itself is an alias, e.g. b≫c, then we consequently and naturally create an alias chain a≫b≫c. From the computational point of view, requests arriving at a after the operation a.alias⟨b⟩ should be forwarded to b.

The operation a.surrogate represents our abstraction of migration: by calling it, object a is turned into an alias to a clone of itself, which is implemented by providing a uniform method surrogate=ς(s)s.alias⟨s.clone⟩. Behaving like standard methods, surrogation is forwarded by aliased objects. This is indeed a behavior that is required if surrogation shall correctly mimic migration, because an object should be surrogatable more than once, so double-surrogation a.surrogate; a.surrogate (where ; denotes sequential composition, as defined below) should obviously be equivalent to a.surrogate.surrogate. Without forwarding, the surrogation of an already surrogated object would mistakenly surrogate the proxy.

The operation a.ping is also implemented by providing a uniform method: ping=ς(s)s. Thus, a.ping returns the “identity” of an object o resulting from the evaluation of a; note that, due to aliasing and forwarding, this could be the “identity” of the current endpoint of an alias chain potentially starting at object o. We add the a.ping method uniformly to Øjeblik objects, because it allows us to conveniently express an algebraic equation for the correctness of surrogation in Section 5. Furthermore, such a method could be used by clients for garbage collection of references to surrogated servers by interrogating the current identity and using it directly instead of the former indirect reference.

Scoping Apart from the binding of variables in method bodies, Øjeblik also offers explicit scope declarations. An expression let x = a in b first evaluates a, binding the result to x, and then evaluates b within the scope of the new binding.

We use the standard inductive definition fv(a) to denote the free variables of term a with respect to our two forms of binding. Øjeblik only admits non-recursive expressions let x = a in b, i.e., with x ∉ fv(a). Then, a; b denotes let x = a in b, where x ∉ fv(b). Finally, L_{0} denotes the set of closed Øjeblik terms a ∈ L, i.e., where fv(a) = ∅.

Concurrency While objects represent persistent stateful structural entities, computational activity takes place within threads. Apart from the main thread that is initially started up with the execution of a term, new separate threads can be created by the fork command. The term fork⟨a⟩ returns a new thread identifier to denote the thread evaluating a. The result of a fork’ed computation is grabbed by the join command. If a evaluates to a thread identifier, then join⟨a⟩ potentially blocks until that thread finishes and returns the thread’s result, or blocks forever, if a join on thread a was already performed earlier.

Self-Infliction, Serialization, Protection The current method of a thread is the last method invoked in it that has not yet completed. The current self of a thread is the self of its current method. An Øjeblik operation is self-inflicted, also called internal, if it addresses the current self; an operation is external if it is not self-inflicted.

In concurrent object-based settings, the invariant that at most one thread at a time may be active within an object is often called serialization. The simplest way to ensure serialization is to associate with an object a mutex that is locked when a thread enters the object and released when the thread exits the object. However, this approach is too restrictive—for instance, it prevents recursion. Based on the notion of thread, so-called reentrant mutexes, as in Java, can be used to allow an operation to re-enter an object under the assumption that this operation belongs to the same thread as the operation that is currently active in the object. In Obliq, however, the more cautious idea of selfserialization requires, based on the above notion of self-infliction, that the mutex is always acquired for external operations, but never for self-inflicted ones. Note that this concept allows a method to recursively call its siblings through self, but it excludes the kind of inter-object mutual recursion, where a method in an object a calls a method in another object b, which then tries to ‘call back’ another method in a.

Based on self-infliction, objects are protected against external modifications in a natural way: updates, cloning, and aliasing, are only allowed if these operations are selfinflicted. In Øjeblik, for simplicity, all objects are both protected and serialized.

Executive Summary It is instructive to classify the operations on Øjeblik objects, as we do in the following table, not only according to the protection conditions (subject to self-infliction, or not), but also with respect to the node of action denoting the node where the operation is finally carried out (locally at the initially called node, or only at the endpoint of a chain starting at the called node). All of these properties are unambiguously stated in Obliq’s informal semantics:

operation  protection condition? node of action
cloning, aliasing  Y: self-inflicted  local
update  Y: self-inflicted  endpoint
invocation, surrogation, ping  N: unconstrained  endpoint

According to this table, we sometimes use the term “local request” to denote a request for cloning or aliasing and “endpoint request” for the others. Similarly, we sometimes use the term “unconstrained request” for those operations that are not subject to protection. Note the hybrid role of update requests, which are endpoint requests as well as subject to apparently local protection.

2.2 Types and Typing, but no Subtyping

In Table 2, we present the rules for static typing. Type environments Γ are finite lists of pairs of variables and types; they can also be seen as functions, where Γ(x) searches in Γ from right to left for the first occurrence of x and returns the associated type. Type judgments are of the form Γ ⊢ a:A and express that term a has type A under the assumptions Γ on the free variables of a. The typing rules themselves are not surprising. The operations clone, alias, surrogate, ping, and update, all yield a result of the same type as the object that they address. While fork packs a type into a thread type, join unpacks it accordingly. The rules for variables, let, objects, and invocations are standard.

The only potential surprise is that we cannot assume the usual subtyping rules of the Imperative Object Calculus [AC96]. These rules state that ⊢ [l_{j} :B]_{j∈J} <: [l_{j} :B]_{j∈I} if I⊆J (T-SubObj) and that Γ ⊢ a:B if Γ ⊢ a:A and Γ ⊢ A<:B (T-Subsum). In

let x:[l_{1}:B_{1}, l_{2}:B_{2}] = a in let y:[l_{1}:B_{1}] = b in x.alias⟨y⟩; x. l_{2}

with arbitrary types B_{1} and B_{2} and terms a and b of the required types, the alias operation in the term is well-typed, as we can give a the type [l_{1}:B_{1}] by (T-Subsum). However, the program will fail at run-time when, after the aliasing, we activate the method l_{2} on x, as l_{2} is not available in y. So, we refrain from giving an account of subtyping (cf. § 6).

\frac{Γ(x) = A}{Γ ⊢ x:A} (T-Var)  \frac{Γ ⊢ a:A Γ, x:A ⊢ b:B}{Γ ⊢ let x:A = a in b : B} (T-Let)
\frac{Γ ⊢ a:A}{Γ ⊢ fork⟨a⟩ : Thr(A)} (T-Fork)  \frac{Γ ⊢ a : Thr(A)}{Γ ⊢ join⟨a⟩ : A} (T-Join)

\frac{∀j∈J Γ, s_{j}:A, x̃_{j}:B̃_{j} ⊢ b_{j}:C_{j} A = [l_{j} :B̃_{j}→C_{j}]_{j∈J}}{Γ ⊢ [l_{j} =ς(s_{j}:A, x̃_{j}:B̃_{j})b_{j}]_{j∈J} : A} (T-Obj)

\frac{Γ ⊢ a : [l_{j} :B̃_{j}→C_{j}]_{j∈J}  Γ ⊢ b̃_{k}:B̃_{k}  k∈J}{Γ ⊢ a.l_{k}⟨ b̃_{k} ⟩ : C_{k}} (T-Inv)
\frac{Γ ⊢ a:A A = [l_{j} :B̃_{j}→C_{j}]_{j∈J}  Γ, s:A, x̃:B̃_{k} ⊢ b:C_{k}  k∈J}{Γ ⊢ a.l_{k}⇐ς(s:A, x̃:B̃_{k})b : A} (T-Upd)

\frac{Γ ⊢ a:A A = [l_{j} :A_{j}]_{j∈J}}{Γ ⊢ a.ping : A} (T-Ping)

\frac{Γ ⊢ a:A A = [l_{j} :A_{j}]_{j∈J}}{Γ ⊢ a.clone : A} (T-Clo)

\frac{Γ ⊢ a, b:A A = [l_{j} :A_{j}]_{j∈J}}{Γ ⊢ a.alias⟨b⟩ : A} (T-Ali)

\frac{Γ ⊢ a:A A = [l_{j} :A_{j}]_{j∈J}}{Γ ⊢ a.surrogate : A} (T-Sur) Table 2: Typing Rules

3 Intermezzo: Towards Formal Semantics

Although the informal semantics of Obliq is reasonably clear at first sight, its formalization enforces one to reason about even the slightest detail. In doing so, we discovered several fundamental facts on alias chains, implied by a few basic assumptions on Øjeblik’s operations, that are worth being spelled out explicitly (§ 3.1). Based on them and the classification of operations in Section 2.1, a whole range of design choices for the forwarding of requests come into play preparing the ground to properly introduce the various aliasing models discussed in this paper (§ 3.2).

3.1 Facts: On the Stability of Alias Chains

As a matter of fact, according to the operations’ character with respect to self-infliction and the intended node of action, a node x in an alias chain can be unstable, which means that if it currently points to node y, it may later on point to different node z. In order to clarify this phenomenon, we distinguish two cases based on the notion of a task, which is the run-time entity that is created by method invocation within a single object. A thread may then actually be seen as a stack of tasks connected via invocations. Now, a node can be active, in which case it contains running tasks, or not. The punchline of this subsection is then that an alias node can not become stable before it has terminated its current tasks.

Below, we introduce pictures where we use single/double boxes to denote inactive/active nodes, and single/double arrows to denote unstable/stable aliases. Furthermore, dashed boxes and dotted arrows denote unspecified respective entities.

Inactive Nodes: No Tasks By definition, the only way to receive a self-inflicted request is to have already at least one local task running. In other words, if there is no local task, then each incoming request is doomed to be external. Now, consider the example term let z = [ l=“bar” ] in let y = [ l=“foo” ] in let x = [ l=ς(s, w)s.alias⟨w⟩] in x.l⟨ y ⟩; x.l⟨ z ⟩ after it carried out the call x.l⟨ y ⟩, which means that the object referred to by x has turned itself into an alias for y and then terminated its activity. We depict the situation as follows

[figure: ≫; ?; ?; x; y; z]

where, in general, the node x may itself be referred to by other aliases, while y and z may be either an alias or an object record. In fact, the alias x≫y is stable in the very sense: no re-aliasing operation on x to another node will ever possibly take place since it could only be carried out in a self-inflicted way by one of its own methods, but any request to such a method potentially starting such a self-inflicted operation, e.g., by calling x.l⟨ z ⟩, is itself forwarded to y such that it can never take place in x.

Active Nodes: At Least One Task As an example, let us first consider the term let z = [ l=“bar” ] in let y = [ l=“foo” ] in let x = [ l=ς(s, w)s.alias⟨w⟩; \underline{“bla”} ] in x.l⟨ y ⟩ just after object x has accepted the request for method l and turned itself into an alias for y. Since x continues to operate on itself, according to “bla” in method l, x is an active alias node.

[figure: ≫; ?; ?; x; y; z]

The alias x≫y is marked as unstable since “bla” may contain further self-inflicted requests, e.g., to perform a re-aliasing or a cloning. Thus, if “bla” calls s.alias⟨z⟩ or s.clone, we get

[figure: ≫; ?; ?; x; y; z; or; ≫; ≫; ?; ?; x; y; z]

and such changes may continue as long some current task in x is active. Here, the re-aliased x remains active, thus unstable, until all current tasks in x, in our example according to “bla”, have terminated. Note that the cloning of an active unstable alias x≫y provides a new inactive stable alias x′≫y, because only the state of x is copied, not its tasks.

Generalizing the above example, we may consider the case where several tasks of the current thread are running in an alias or an object. However, by the definition of synchronous method invocation, only one of them may be active—namely the one on top of the thread’s call-stack—while the others must be blocked. Now, note that it is the active task or any of its ancestors in the call-stack who turned the current node into an alias (in the example it is method l); otherwise, the node would be stable and the current tasks would not exist, but have been created in one of the successors of the stable alias node.

3.2 Design Choices: Four Aliasing Models

Apart from the above-mentioned facts about the stability of alias nodes, Obliq’s informal semantics is rather imprecise on the behavior of alias nodes. In particular, there is quite some freedom on how to precisely model serialization and protection in aliased objects.

There are many possible variants, some of which we list below. First, we provide an abstract characterization. Then, we refine the description of the individual models by means of a comparison on how requests are forwarded, respectively.

How much Protection and Serialization? In this paper, we introduce and study

• a conservative model (C) that keeps protection and serialization unchanged,

• a relaxed model (R) that relaxes protection to some extent, but ignores serialization,

• a forwarder model (F) that relaxes protection even more, and

• a serialized model (S) that reintroduces some serialization to the forwarder model.

Our motivation for investigating and presenting all of the above four models is that C corresponds to Cardelli’s implementation [Car94], while R corresponds to Talcott’s operational semantics [Tal96]. As we will see in Section 5, neither of these two models provides sufficiently nice properties regarding the safety of surrogation. Therefore, we developed ourselves the model F as a consequent generalization of R that does well for surrogation, and S as a version of F with better programming and implementation properties.

Request Forwarding: Which? What? When? Each request arriving at an alias node must carry with it the knowledge about its “current self”, i.e., an identification of the caller; this is required since otherwise self-infliction could not be checked locally by the requested node. The essential design choices to be made are the following:

1. Which requests (cf. table on page 7) are forwarded? (protection)

2. What is the current self of forwarded requests? (protection/serialization)

3. When does the forwarding take place? (serialization)

We use these questions to compare the individual above-mentioned aliasing models.

Which? The most intuitive model with respect to the first question, at least at first sight, is probably model R: only endpoint requests are forwarded, local requests are handled locally. In contrast, model C is more restrictive for the case of updates. Recall that updates have a hybrid status in that they are protected endpoint requests: they can only perform meaningfully on object records, i.e., on endpoints of alias chains, and they can only be carried out when self-inflicted. Since in model C, as in Cardelli’s implementation, object aliasing is just as a macro for universal field aliasing, alias nodes are just the original objects with field redirection, so protection and serialization are still fully intact. Therefore, only unconstrained requests are forwarded, while the others—including updates—are either performed or blocked. If updates are self-inflicted in an intermediate node, then in model R they will be rejected only at the endpoint, while in model C already in the successor. The models F/S are more liberal than model R and forward all requests except for self-inflicted local ones, because they are the only ones that can be carried out successfully in the requested node. This behavior will be of vital importance in Section 5.

What? This question has just two possible answers: either forwarding changes the current self of the request, or it does not. If it changes it, which is the case only in model C, then the new current self is the one of requested node. In the models R/F/S, however, forwarding does not change the current self. Although the difference is apparently minor, its impact is crucial for both protection and serialization: for example, consider a forwarded update request that keeps the same current self as it started out with—it may finally reach the endpoint of the alias chain and be self-inflicted there! The impact in the models F/S is even bigger, because, as mentioned above, even cloning and aliasing requests may be forwarded.

When? The third question just concerns how much serialization is present in alias nodes. Here it is crucial to recall the fact that alias nodes are unstable as long as they are active (cf.§ 3.1). Should those external requests that are to be forwarded wait until the alias becomes stable, or should they be forwarded immediately, i.e., independent of stability? Here, the four models that we discuss behave again differently: model C, as explained before, keeps serialization in aliases, so all external requests have to wait. Furthermore, the alias is afterwards locked until the forwarded request has successfully signaled termination from its point of action, so we may call this forwarding game lockand-go. The models R and F completely ignore serialization in alias nodes, so forwarding of all intended requests is immediate. It is only now that we introduce our model S as a variant of model F: here, all external requests to an alias node are blocked until the current tasks have finished. Then, the pending requests are forwarded without waiting for the previously forwarded request to signal termination; we call this forwarding game touch-and-go since external requests in alias nodes have to wait for the appearance of the node’s mutex, but once it becomes available—in fact, just touchable—they will not grab it, but will simply go ahead. As we will argue later on (§ 4.4), in comparison with model F, model S is better suited for programming since it enhances the predictability of program behaviors. It can also be used for path-compression, i.e., the optimization of alias chains to turns aliases into aliases for the farthest stable successor.

We summarize this rather complex discussion on design choices for aliasing models in Øjeblik by the following table. The important aspects are that the lower a model is listed in the table the more requests are forwarded, which prevents a client of an alias node to observe that the node really is an alias. This, however, only holds if the current self of forwarded requests is not changed by the alias node they pass.

Which requests?  What current self?  When?
C all unconstrained  intermediate  lock-and-go
R all endpoint  unchanged  immediate
F all endpoint + external local  unchanged  immediate
S all endpoint + external local  unchanged  touch-and-go

There would, of course be more variants and combinations of different design decisions, but we chose the above due to their existing counterparts in Obliq (C/R) on the one hand, and due to their better surrogation properties (F/S) on the other hand.

Design Consequences The notion of current self is essential for the meaning of selfinfliction. In fact, in the models R, F, and S, which have in common that they do not change the current self of forwarded requests, self-infliction mutates naturally into pre-infliction: a thread may reenter an object or alias node from another node if it has only visited predecessors of the current node since its last visit of the current node. In terms of an implementation using object mutexes, this amounts to a generalization of self-inflicted mutexes towards reentrant mutexes, but in a controlled way, so we may coin the term preentrant mutexes for this purpose. At Aalborg University, we have developed a prototype implementation, which allows us to experiment with the feasibility of such mutexes in practise [NOI^{+}99].

4 Four Operational Semantics for Øjeblik

Our various transition semantics for Øjeblik terms follow loosely the one sketched by Talcott [Tal96]. Her semantics addresses a larger subset of Obliq than we do with Øjeblik, in particular including distribution concepts, but nevertheless excludes, for example, migration and join. The section is organized by first presenting the common basic concepts (§ 4.1) of the formal semantics for the various aliasing models (§ 4.2). We then offer behavioral semantics (§ 4.3), examples (§ 4.4), and an investigation of various properties of our semantics that prove the meaningfulness of our semantics (§ 4.5–4.6).

4.1 Common Basic Concepts

The semantics performs local changes on global run-time configurations, which are mappings from references v ∈ R to run-time entities. More precisely, a configuration ℭ maps task references t ∈ R_{T} to tasks T, and object references o ∈ R_{O} to objects O (see below). We use dom_{X}(ℭ) to denote dom(ℭ)∩R_{X} for X ∈ {T , O}, and ↑ for undefined references.

a, b ::= … | v | wait

Table 3: Syntax of Øjeblik run-time expressions

Run-Time Entities A run-time expression a is generated from the extended Øjeblik grammar in Table 3, where we introduce references v as values, as well as an additional construct wait whose meaning will become clear from its use later on. Let us refer to this extended set of terms as L_{R}. A run-time object O ∈ O is either an object record 𝕆 (ranging over [l_{j} =m_{j}]_{j∈J}) or a pointer ≫o to an object reference o ∈ R_{O}. A run-time task T is a triple ⟨ p, s, a ⟩ ∈ R_{T} × R_{O} × L_{R} that refers to a parent p, a current self s, and a run-time expression a that remains to be evaluated. By the partial functions s_{ℭ}(t) and p_{ℭ}(t), we refer to the—possibly undefined—current self and parent of the task associated with reference t in ℭ. We reserve the task references t_{m}, t_{g} ∈ R_{T} for special purposes.

Alias chains The partial function ali_{ℭ} : R_{O} ⇀ R_{O}^{∗} ∪ (R_{O}^{∗} · {↑}) with

ali_{ℭ}(o) =^{def} \begin{cases}↑ & if ℭ(o) = ↑ \\ o & if ℭ(o) = 𝕆 \\ o · ali_{ℭ}(o′) & if ℭ(o) = ≫o′ \end{cases}

computes the alias chain, starting at reference o, where · denotes concatenation of (sets of) strings of references, in general possibly ending with ↑. This computation obviously only terminates, if there are no cycles in the chain. The endpoint of an alias chain is denoted by end(ali_{ℭ}(o)); if it exists, then the semantics will guarantee that it is associated with an object record 𝕆 (cf. Lemma 4.5.1). We write o′ ∈ ali_{ℭ}(o) if o′ occurs in the string representing the alias chain starting at o and we sometimes abbreviate finite alias chains {o := ≫o_{1}, …, o_{i} := ≫o_{i+1}, …, o_{n} := 𝕆} with {o≫o_{1}⋯o_{i}≫o_{i+1}⋯o_{n} := 𝕆}).

As a specialization of the above function, we define

pre_{ℭ}(o, s) =^{def} \begin{cases}↑ & if ℭ(o) = ↑ \\ o & if ℭ(o) = 𝕆 or o = s \\ o · pre_{ℭ}(o′, s) & if ℭ(o) = ≫o′ and o ≠ s \end{cases}

which yields the prefix of the alias chain starting in o that ends with the first occurrence of s, if it exists. If s ∉ ali_{ℭ}(o), then pre_{ℭ}(o, s) = ali_{ℭ}(o).

We sometimes refer to object references as nodes, reflecting the fact that may be nodes in an alias chain. A node o ∈ dom_{O}(ℭ) is active if there is t ∈ dom_{T} (ℭ) with s_{ℭ}(t) = o, otherwise it is called idle. An alias node is a node o ∈ dom_{O}(ℭ) with ℭ(o) = ≫o′ for o′ ∈ dom_{O}(ℭ). An alias node is stable (c.f. § 3.1), if it is idle.

Threads Since tasks, in general, refer explicitly to their parent, we can build up task chains, which start in tasks that have no parent assigned. Such chains precisely correspond to Øjeblik threads, as derived from a task as the task’s ancestors, similar to call-stacks in an implementation. Let his_{ℭ} : R_{T} → R_{T}^{∗} with

his_{ℭ}(t) =^{def} \begin{cases}ϵ & if ℭ(t) = ↑ \\ t & if t ∈ dom_{T} (ℭ) and p_{ℭ}(t) = ↑ \\ t · his_{ℭ}(p_{ℭ}(t)) & otherwise \end{cases}

be the history of a task t, where ϵ denotes the empty string.

Furthermore, let trc_{ℭ} : R_{T} → R_{O}^{∗} with

trc_{ℭ}(t) =^{def} \begin{cases}ϵ & if ℭ(t) = ↑ \\ ϵ & if t ∈ dom_{T} (ℭ) and p_{ℭ}(t) = ↑ \\ s_{ℭ}(t) · trc_{ℭ}(p_{ℭ}(t)) & otherwise \end{cases}

be the trace of a task, representing the string of object references that occur as the current self of itself and its ancestors. For example, if ℭ = {t_{0} := ⟨↑, ↑, a_{0}⟩, t_{1} := ⟨t_{0}, s_{1}, a_{1}⟩, t_{2} := ⟨↑, ↑, a_{2}⟩}, then his_{ℭ}(t_{1}) = t_{1}t_{0} and trc_{ℭ}(t_{1}) = s_{1}. A task with reference t≠t_{g} is current in ℭ, if (1) it is defined in ℭ, (2) it is not the parent of any other task in ℭ, and (3) it does not have parent t_{g}. The threads of ℭ are the histories of the current tasks in ℭ:

cur(ℭ) =^{def} { t ∈ R_{T} | t is current in ℭ }
thr(ℭ) =^{def} { his_{ℭ}(t) | t ∈ cur(ℭ) }

In the above example, there are just the two threads t_{1}t_{0} and t_{2}.

Evaluation Table 4 also contains grammars for generating redexes r and evaluation contexts e[·], which we use to control the evaluation [FF86] of (the expression part of) run-time tasks. The contexts are designed such that evaluation proceeds leftmost-innermost. Note that fork⟨a⟩ is a redex independent of a being a value; similarly, an expression let x = a in b becomes a redex as soon as the bound expression a has reduced to a value. According to this definition, a simple algorithm computes for every closed run-time expression a ∉ R a unique pair of a redex r and a context e[·] such that a = e[r].

Behaviors The semantics of a closed term a ∈ L_{0} is given by assigning to it the initial configuration [[[ a]]] := {t_{m}:=⟨ ↑, ↑, a ⟩, t_{g}:=⟨ ↑, ↑, t_{m} ⟩}. The task referred to by t_{m} represents the start of the so-called main thread; the task reference t_{g} is used as the parent of all garbage task references, i.e., references to threads that are accomplished during reduction, and that have already been join’ed. Both, t_{m} and t_{g} are always defined in configurations.

The behavior of configurations is generated from (subsets of) the rules in Tables 5–12. In each case we pick some task and object references in a particular configuration ℭ, which under the respective conditions may enable a transition to take place in ℭ. In the premises, note that the expressions of tasks are always in unique context-redex decomposed form. In the conclusions of the rules, ℭ{t:=T, o:=O} means that the mapping ℭ is either extended or overwritten with the association of task reference t with task T, and object reference o with run-time object O.

The rules in Table 5 describe the local activity in a single task t in a straightforward manner; recall that let is not recursive. Furthermore, we assume that the value v is either a task or an object reference whose actual run-time entity is accessible through ℭ.

The rules in Table 6 exhibit the interplay of fork and join: in rule (Fork), a new task t′ is spawned off, which runs the expression a without current self. In rule (Join), the parent referring to its child t′ is returned a value v. Note that fork’ed tasks do not know their parent, so they indeed represent initial tasks of new threads. As soon as a thread t is join’ed, it is marked as garbage by means of the special reference t_{g} as its parent; no further attempt to join t will succeed, and t can not be reused after the first join.

The rules in Table 7 exemplify the synchronous method invocation protocol. In the rule schema (X -Inv), a call to an object results in the creation of a new (callee-) task within the target object, while the caller-task is delayed, which is syntactically represented by the term wait inserted into its evaluation context. In rule (Ret), this caller-callee pair can communicate the result as soon as the callee-expression has reduced to a value; the task then disappears. A reference to a callee-task may even be reused after a successful (Ret), because the semantics guarantees that there is exactly one task, namely the caller-task, that is wait’ing for the callee-task to finish (cf. Lemma 4.5.2); in particular, references to callee-tasks never occur in run-time expressions—only references to fork’ed tasks can. Like the other rules of the operational semantics in Tables 8–12, especially the rules (Ali)/(Cln)/(Upd) for protected operations on objects, the rule (X -Inv) for invocation crucially depends on how aliased objects should behave. Therefore, we parameterized the above rule schema, and start splitting up our presentation into different variants corresponding to different aliasing models X, as introduced in the next subsection.

Self-Infliction In order to formalize the test for the either self-inflicted or pre-inflicted character of operations on objects, we introduce some suitable notation based on the information of alias chains in configurations. Let s be the current self of the caller-task, and o be the requested object reference. Then the following definitions are obvious.

r ::= 𝕆 | wait | o.l⇐m
| o.l⟨ ṽ ⟩
| o.clone
| o.alias⟨o′⟩
| o.surrogate | o.ping
| let x = v in b
| fork⟨a⟩  | join⟨t⟩

e[·] ::= [·] | e[·].l⇐m
| e[·].l⟨ ã ⟩  | o.l⟨ ṽ, e[·], ã ⟩
| e[·].clone
| e[·].alias⟨b⟩ | o.alias⟨e[·]⟩
| e[·].surrogate | e[·].ping
| let x = e[·] in b
| join⟨e[·]⟩

Table 4: Evaluation of Øjeblik run-time expressions

\frac{ℭ(t) = ⟨ p, s, e[let x = v in b] ⟩}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[b\{^{v}/_{x}\}] ⟩\}} (Let)
\frac{ℭ(t) = ⟨ p, s, e[𝕆] ⟩  ℭ(o) = ↑}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[o] ⟩, o := 𝕆\}} (New)

Table 5: Local transitions

\frac{ℭ(t) = ⟨ p, s, e[fork⟨a⟩] ⟩ ℭ(t′) = ↑}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[t′] ⟩, t′ := ⟨ ↑, ↑, a ⟩\}}  (Fork)
\frac{ℭ(t) = ⟨ p, s, e[join⟨t′⟩] ⟩  ℭ(t′) = ⟨ ↑, ↑, v ⟩}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[v] ⟩, t′ := ⟨ t_{g}, ↑, v ⟩\}} (Join)

Table 6: Concurrency transitions

\frac{\begin{matrix}ℭ(t) = ⟨ p, s, e[o.l_{k}⟨ ṽ ⟩] ⟩ & k∈J \\ ℭ(o) = [l_{j} =ς(s_{j}, x̃_{j})b_{j}]_{j∈J} & …  ℭ(t′) = ↑ \end{matrix}}{ℭ ⟶ ℭ\{ t := ⟨ p, s, e[wait] ⟩, t′ := ⟨ t, o, b_{k}\{^{oṽ}/_{s_{k}x̃_{k}}\} ⟩\}} (X -Inv)
\frac{ℭ(t) = ⟨ p, s, e[wait] ⟩ ℭ(t′) = ⟨ t, s′, v ⟩}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[v] ⟩, t′ := ↑\}}  (Ret)

Table 7: Synchronous Method Invocation

self-infliction (C)  : s = o
pre-infliction for endpoint ops (R/F/S) : s = end(ali_{ℭ}(o))
pre-infliction for local ops (F/S)  : s ∈ ali_{ℭ}(o)

In addition, we have to be able to check formally that an intended node o is currently available to deal with requests from task t:

Avail_{ℭ}(o, t) =^{def} \underbrace{⋀_{t′∈ dom_{T} (ℭ)}(o ≠ s_{ℭ}(t′))}_{o is idle} ∨ \underbrace{(o = s_{ℭ}(t))}_{self-inflicted}

An object o is available for task t in ℭ, if o is idle, or it it is the same as the current self of t, such that operations from t on o would be self-inflicted.

4.2 Aliasing Models

According to the four models informally proposed in Section 3.2, we now provide coherent formal semantics for each of them, where the inclusion of a rule to the semantics of a particular aliasing model is indicated by prefixing its name with C, R, F, or S.

4.2.1 The Conservative Model

Each alias node is protected. Thus, the rules in Table 8, all of which address protected operations on object o—which can only happen if they are self-inflicted—require the premise o = s. Note that for simplicity we do not generate run-time errors (as in Obliq) for invalid access to protected operations; the calls to such operations just block forever.

As exemplified in rule (X -Inv), the rules (C-Inv_{1})/(C-Inv_{2}) in Table 9 formalize synchronous method invocation by means of new task t′ in the target object o, while forcing the caller t to wait. The difference between these two rules is, whether the target o is an object record or an alias. In the former case, the available method body is instantiated immediately; in the latter case, instead, a new call is placed in the target object o, but now directed to the new target o′, according to the aliasing information in ℭ.

Each alias node is serialized. To this aim, the use of Avail_{ℭ}(o, t) checks for availability of the current call from task t with respect to the target o. Note that a method call on an aliased object o in rule (C-Inv_{2}) creates a forwarding sub-task t′ with current self o. Essentially, this means that o’s mutex is now locked by this task and that the current self of the forwarded call has been changed, according to the discussion in § 3.2.

4.2.2 The Relaxed Model

While protection is kept in alias nodes, serialization is ignored. Talcott [Tal96] proposes a scheme for method calls in Obliq, which is optimized in the sense that it directly addresses the endpoint of a chain, if it exists, and instantly creates a sub-task there. In rule (R/F-Inv) of Table 10, this scheme is formalized in terms of the functions end and ali_{ℭ}. In particular, no tasks are created in intermediate nodes between o and ô, which also means that none of the intermediate nodes is locked, and the availability of the endpoint is checked with respect to the current self s of the calling task t.

Although aliased objects are protected, updates on aliased objects are modeled as in rule (R/F-Upd): if an update on o is originating from the current endpoint of its alias chain (as checked by the condition end(ali_{ℭ}(o)) = s), then it is forwarded there to take effect, there. Otherwise, the caller is blocked. It is this peculiar behavior that inspired us to formally introduce the notion of pre-infliction (cf. § 4.1).

While it is a convenient abstract optimization to immediately forward requests to the endpoint of a chain, as it is it does not give rise to a proper implementation technique, because unstable nodes are transparently traversed although they may give rise to different alias chain later on (c.f. § 3.1).

4.2.3 The Forwarder Model

We ‘learn’ from the peculiar modeling of update transitions in the relaxed model, and generalize it to also apply to cloning and aliasing: the rules in Table 11 replace the former tests o = s for immediate self-infliction with a test for self-infliction on successors in the alias chain starting from the entry in the chain. In effect, this behavior prescribes an implementation of an aliased object as a pure forwarder for external and a partial forwarder for internal requests: partial since requests for invocation and update are forwarded, while requests for cloning and aliasing are accepted, if self-inflicted.

4.2.4 The Serialized Model

The step from the forwarder model to the serialized model is simple. To every rule for calling an operation at an object, we add the requirement that all alias nodes that have to be traversed in the alias chain starting from the entry node up to the point of action have to be available for the calling task. In the rules for endpoint operations (S-Inv) and (S-Upd), we add ∀ȯ ∈ ali_{ℭ}(o) : Avail_{ℭ}(ȯ, t) to check the chain until the endpoint. In the rules for local operations (S-Cln) and (S-Ali), we instead add ∀ȯ ∈ pre_{ℭ}(o, s) : Avail_{ℭ}(ȯ, t) to check the chain until we reach self-infliction.

4.2.5 Roundup

Whenever we refer to a particular aliasing model, we use the notation X [[[ a]]] to denote the semantics of a according to model X ∈ {C, R, F, S}; otherwise, we simply write [[[ a]]]. In general, let ⟶^{∗} denote the reflexive-transitive closure of the transition relation on Øjeblik-configurations.

\frac{ℭ(t) = ⟨ p, s, e[o.alias⟨o′⟩] ⟩ o = s}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[o′] ⟩, s := ≫o′\}}  (C/R-Ali)
\frac{ℭ(t) = ⟨ p, s, e[o.clone] ⟩ o = s ℭ(o′) = ↑}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[o′] ⟩, o′ := ℭ(s)\}} (C/R-Cln)
\frac{\begin{matrix}ℭ(t) = ⟨ p, s, e[o.l_{k}⇐m] ⟩ & o = s \\ ℭ(s) = [l_{j} =m_{j}]_{j∈J} & k∈J \end{matrix}}{ℭ ⟶ ℭ\{ t := ⟨ p, s, e[s] ⟩, s := [l_{k}=m, l_{j ≠k}=m_{j}]_{j∈J}\}} (C-Upd)

Table 8: Protected transitions in the conservative (and relaxed) models

\frac{ℭ(t) = ⟨ p, s, e[o.l_{k}⟨ ṽ ⟩] ⟩ Avail_{ℭ}(o, t) ℭ(t′) = ↑ ℭ(o) = [l_{j} =ς(s_{j}, x̃_{j})b_{j}]_{j∈J} k∈J}{ℭ ⟶ ℭ\{ t := ⟨ p, s, e[wait] ⟩, t′ := ⟨ t, o, b_{k}\{^{oṽ}/_{s_{k}x̃_{k}}\} ⟩\}} (C-Inv_{1})
\frac{\begin{matrix}ℭ(t) = ⟨ p, s, e[o.l⟨ ṽ ⟩] ⟩ & Avail_{ℭ}(o, t) ℭ(t′) = ↑ \\ ℭ(o) = ≫o′ \end{matrix}}{ℭ ⟶ ℭ\{ t := ⟨ p, s, e[wait] ⟩, t′ := ⟨ t, o, o′.l⟨ ṽ ⟩ ⟩\}} (C-Inv_{2})

Table 9: Method transitions in the conservative model

\frac{ℭ(t) = ⟨ p, s, e[o.l_{k}⟨ ṽ ⟩] ⟩ end(ali_{ℭ}(o)) = ô Avail_{ℭ}(ô, t) ℭ(ô) = [l_{j} =ς(s_{j}, x̃_{j})b_{j}]_{j∈J}  k∈J  ℭ(t′) = ↑}{ℭ ⟶ ℭ\{ t := ⟨ p, s, e[wait] ⟩, t′ := ⟨ t, ô, b_{k}\{^{ôṽ}/_{s_{k}x̃_{k}}\} ⟩\}} (R/F-Inv)
\frac{ℭ(t) = ⟨ p, s, e[o.l_{k}⇐m] ⟩ end(ali_{ℭ}(o)) = s ℭ(s) = [l_{j} =m_{j}]_{j∈J}  k∈J}{ℭ ⟶ ℭ\{ t := ⟨ p, s, e[s] ⟩, s := [l_{k}=m, l_{j ≠k}=m_{j}]_{j∈J}\}}  (R/F-Upd)

Table 10: Method invocation and update in the relaxed and forwarder models

\frac{ℭ(t) = ⟨ p, s, e[o.clone] ⟩ s ∈ ali_{ℭ}(o) ℭ(o′) = ↑}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[o′] ⟩, o′ := ℭ(s)\}} (F-Cln)
\frac{ℭ(t) = ⟨ p, s, e[o.alias⟨o′⟩] ⟩ s ∈ ali_{ℭ}(o)}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[o′] ⟩, s := ≫o′\}}  (F-Ali)

Table 11: Protected transitions in the forwarder model

\frac{ℭ(t) = ⟨ p, s, e[o.l_{k}⟨ ṽ ⟩] ⟩ end(ali_{ℭ}(o)) = ô ∀ȯ ∈ ali_{ℭ}(o) : Avail_{ℭ}(ȯ, t) ℭ(ô) = [l_{j} =ς(s_{j}, x̃_{j})b_{j}]_{j∈J}  k∈J  ℭ(t′) = ↑}{ℭ ⟶ ℭ\{ t := ⟨ p, s, e[wait] ⟩, t′ := ⟨ t, ô, b_{k}\{^{ôṽ}/_{s_{k}x̃_{k}}\} ⟩\}} (S-Inv)
\frac{ℭ(t) = ⟨ p, s, e[o.l_{k}⇐m] ⟩ end(ali_{ℭ}(o)) = s ∀ȯ ∈ ali_{ℭ}(o) : Avail_{ℭ}(ȯ, t) ℭ(s) = [l_{j} =m_{j}]_{j∈J}  k∈J}{ℭ ⟶ ℭ\{ t := ⟨ p, s, e[s] ⟩, s := [l_{k}=m, l_{j ≠k}=m_{j}]_{j∈J}\}} (S-Upd)
\frac{ℭ(t) = ⟨ p, s, e[o.clone] ⟩ s ∈ ali_{ℭ}(o) ∀ȯ ∈ pre_{ℭ}(o, s) : Avail_{ℭ}(ȯ, t) ℭ(o′) = ↑}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[o′] ⟩, o′ := ℭ(s)\}} (S-Cln)
\frac{ℭ(t) = ⟨ p, s, e[o.alias⟨o′⟩] ⟩ s ∈ ali_{ℭ}(o) ∀ȯ ∈ pre_{ℭ}(o, s) : Avail_{ℭ}(ȯ, t)}{ℭ ⟶ ℭ\{t := ⟨ p, s, e[o′] ⟩, s := ≫o′\}} (S-Ali)

Table 12: Operations in the serialized model Uniform Methods Both surrogate and ping are represented in Øjeblik as uniform methods that are treated like standard methods, except that they shall not be updatable. Thus, the treatment of requests for surrogate and ping in the various aliasing models is analogue the (Inv)-rules for standard methods, except that there is no requirement k∈J to match one of the defined labels since surrogate and ping are uniformly and implicitly present.

Program Contexts In order to define a contextual notion of program equivalence in the next subsection, we need a general notion of program context that differs from the notion of evaluation context given in Table 4. More specifically, according to Table 13, a context C[·] has a single hole [·] that may be filled with an Øjeblik term.

C[·] ::= [·]  | [ l_{k}=ς(s, x̃)C[·] , l_{j ≠k}=m_{j≠k} ]_{j∈J}
| C[·].l⟨ ã ⟩  | a.l⟨ ã, C[·], ã ⟩
| C[·].l⇐m  | a.l⇐ς(s, x̃)C[·]
| C[·].clone
| C[·].alias⟨b⟩ | a.alias⟨C[·]⟩
| C[·].surrogate | C[·].ping
| let x = C[·] in b | let x = a in C[·]
| fork⟨C[·]⟩  | join⟨C[·]⟩

Table 13: Øjeblik contexts

4.3 Behavioral Semantics

Based on a may-variant of convergence [Mor68] of terms, we define a contextual notion of equivalence [GHL97] uniformly for the four semantics of Øjeblik. In the context of a concurrent language with fork, threads may nondeterministically affect the outcome and convergence of evaluation. So, with respect to our goal of reasoning about surrogation, we regard must-variants of convergence as too strong (see also the testing semantics of the Join Calculus [Lan96]; stronger versions of equivalence based on barbed bisimulation can be found in [BFL98]).

Definition 4.3.1 (Convergence). A closed term a ∈ L_{0} converges, written a⇓, if there is a configuration ℭ with [[[ a]]] ⟶^{∗} ℭ and ℭ(t_{m}) = ⟨ ↑, ↑, v ⟩ for some v.

This notion of convergence does not mean that the whole computation of term a terminates, but rather that the main task t_{m} does so: the evaluation of [[[ a]]] may converge to a value v and can be reached in finite time within t_{m}. Note that there might be fork’ed computations around that have not yet been join’ed, and which may possibly run forever.

Definition 4.3.2 (Equivalence). Two terms a, b ∈ L are equivalent, written a ≅ b, if for all closing contexts C[·] (s.t. C[a] and C[b] are closed): C[a]⇓ iff C[b]⇓.

In a typed language, it is natural to sometimes only consider well-typed terms. Although the notion of convergence itself is defined on all terms, it is natural to consider only well-typed contexts for equivalence.

Definition 4.3.3 (Typed Equivalence). Two terms a, b ∈ L with Γ ⊢ a, b : A for some type A are typed equivalent, written a =^{⊢} b, if for all well-typed closing contexts C[·], i.e., with ∅ ⊢ C[a], C[b] : B for some type B, we have C[a]⇓ iff C[b]⇓.

Note that the definition of typed equivalence does not use the type information to equate more terms—it just reduces the number of contexts that are taken into account for equivalence. We have the following close relation between the typed and untyped equivalence.

Lemma 4.3.4. Let a, b ∈ L. If a ≅ b and Γ ⊢ a, b : A, then a =^{⊢} b.

A proof of this lemma is trivial since we check strictly fewer context for establishing a =^{⊢} b.

Conjecture 4.3.5. Let a, b ∈ L. If a =^{⊢} b, then a ≅ b.

We have not proved this conjecture, but we strongly believe that it holds since the only way an ill-typed context can invalidate a ≅ b is basically by using method labels inappropriately. Then, we conjecture that any such misbehaving context could be simulated by a well-typed one that simply diverges in the case that the ill-typed context produces a message-not-understood. We also expect the conjecture to hold when we take ground values into account. However, note that it would not hold in the context of subtyping: where the typing system would allow us to compare two objects a := [ l_{1}=c_{1}, l_{2}=c_{2} ] and b := [ l_{1}=c_{1} ] at the common type [ l_{1} : C_{1} ], thus rendering them equal, although the ill-typed context (c.f. Table 13) C[·] := [·].l_{2} would obviously be able to distinguish them.

We postpone the study of properties of our four semantics until after the next subsection, where we expose several sometimes surprising example behaviors that can be formulated in terms of Øjeblik.

4.4 Peculiarities of Infliction, Aliasing, and Fork

As an abbreviation, we use the method definitions l=id and k=Ω to denote l=ς(s)s and k=ς(s)s.k, respectively, where obviously [ …, l=id, …].l⇓ and [ …, k=Ω, …].k⇓̸.

Example 4.4.1 (Self-infliction via Substitution). Protected operations can be called from within methods not only literally on the self variable s, but also indirectly by an expression—for example an object variable—that evaluates to the object itself:

let x = [ l=ς(s, z)z.clone ] in x.l⟨x⟩  (1)

The behavior of this term is unproblematic and independent of X: the cloning operation may take place since z is replaced with x such that the call z.clone is indeed self-inflicted.

Example 4.4.2 (Self-Aliasing and Cycles). Øjeblik does not prevent the programmer from (either consciously or accidentally) introducing self-aliases or alias chains with cycles, e.g. as in Equation (1) via substitution:

let x = [ k=id , l=ς(s, z)s.alias⟨z⟩] in x.l⟨x⟩; x.k  (2)

In the semantics, after carrying out the aliasing operation, by means of the call to x.l⟨x⟩, yielding configuration ℭ, the call to x.k results in the function ali_{ℭ} not terminating. Thus, every operation on an object in an alias chain with cycles via the object’s successors will block (unless one of the objects breaks the cycle by means of internal re-aliasing; cf. § 3.1).

Example 4.4.3 (Re-aliasing vs Serialization). Øjeblik allows the programmer to perform aliasing twice, one after the other, e.g. as in the following term:

let x = [ k=id , l=id ] in
let y = [ k=Ω , l=id ] in
let z = [ k=Ω , l=ς(s)s.alias⟨x⟩; s.alias⟨y⟩] in
fork⟨z.l⟩; z.k

(3)

Interestingly, the outcome of the whole term depends on the chosen aliasing model. First, computation starts by setting up the three objects. Then, two competing method calls are launched on z. If the double-aliasing method on label l gets into z first, then we may reach the state, where this method has just performed the first aliasing request, ready to perform the second aliasing request, but having just opened a “convergence window” for z.k.

Now, it matters whether or not the competing method call on label k is granted to pass through the locked object. If yes, as in the forwarder model F (and also model R), then the main thread may reach a terminating state; otherwise, as in the serialized forwarder model S (and also model C), the competing request may not pass through until the current method has terminated itself. However, then the second alias request must have been performed, and the pending request on label k will again be doomed to fail, i.e., it diverges.

Example 4.4.4 (Reflexive Threads). Øjeblik allows the programmer, independent of the underlying aliasing model X, to fork off a concurrent thread that gets to know its own thread identifier by means of an intermediate storage cell and uses it afterwards:

let x = [ use=ς(s, t)join⟨t⟩ , get=ς(s)fork⟨[ ]⟩ , put=ς(s, t)s.get⇐ς(s)t; t] in

x.put⟨ fork⟨x.use⟨ x.get ⟩⟩ ⟩

(4)

We are not aware of a good application of this behavior, but at least we found it interesting to observe that it can be formulated within Øjeblik.

4.5 Invariant Run-Time Properties

In this subsection, we collect facts and lemmas about the well-definedness of our operational semantics. Although we concentrate our explanations and proofs here on the serialized model S, which is our reference semantics, the results also hold for the other models.

Essentially, we collect properties of configurations that are invariant under reduction, under the assumption that we start out with an initial configuration that arises from a static term, as we may call terms in the original Øjeblik syntax, following the terminology of [GHL97]. Subject reduction, i.e., the invariance of typing under reduction, is then developed and proved in the next subsection. We start with a simple fact.

Fact 4.5.1 (Alias chains). Let a ∈ L_{0} and S[[[ a]]] ⟶^{∗} ℭ. For all o ∈ dom_{O}(ℭ) : either ali_{ℭ}(o) does not terminate, or ℭ(end(ali_{ℭ}(o))) is an object record [l_{j} =m_{j}]_{j∈J}.

A configuration ℭ is well-behaved if all of its objects are inhabited by at most one current task, if all run-time terms do not contain free variables, if all wait’ing tasks have exactly one deliverer for results, and if all non-current tasks are actually wait’ing. All configurations reachable in our semantics are well-behaved.

Lemma 4.5.2 (Well-behavior). Let a ∈ L_{0} and S[[[ a]]] ⟶^{∗} ℭ.

1. For all o ∈ dom_{O}(ℭ) : there is at most one task t ∈ dom_{T} (ℭ) with o = s_{ℭ}(t) and t current in ℭ.

2. For all t ∈ R_{T}, o ∈ R_{O} : if ℭ(t) = ⟨ p, s, b ⟩, then b is a closed run-time term. if ℭ(o) = 𝕆, then 𝕆 is a closed run-time term.

3. For all t ∈ R_{T} :

(a) if ℭ(t) = ⟨ p, s, e[wait] ⟩,

then there is exactly one t′ ∈ R_{T} with ℭ(t′) = ⟨ t, s′, c ⟩ for some s′ and c.

(b) if ℭ(t) = ⟨ p, s, e[b] ⟩ and there is t′ ∈ R_{T} with ℭ(t′) = ⟨ t, s′, c ⟩ for some s′ and c, then b = wait.

Proof. By induction on the length of S[[[ a]]] ⟶^{∗} ℭ.

A configuration ℭ is closed if all object and task references occurring in run-time terms of task or in run-time object records are also captured within ℭ, and if all task references occurring in run-time terms are mapped to thread-initial tasks, which also may have become garbage. All configurations reachable in our semantics are closed in that sense.

Lemma 4.5.3 (Closedness). Let a ∈ L_{0} and S[[[ a]]] ⟶^{∗} ℭ.

1. Let t ∈ R_{T} and o, o′ ∈ R_{O} : if ℭ(t)=⟨ p, s, C[o′] ⟩ or ℭ(o)=C[o′] for some p, s, and C[·], then o′ ∈ dom_{O}(ℭ).

2. Let t, t′ ∈ R_{T} and o ∈ R_{O} : if ℭ(t)=⟨ p, s, C[t′] ⟩ or ℭ(o)=C[t′] for some p, s, and C[·], then t′ ∈ dom_{T} (ℭ). Moreover ℭ(t′) = ⟨ p′, s′, b ⟩ for some s′, b, and p′ = ↑ or p′ = t_{g}.

Proof. By induction on the length of S[[[ a]]] ⟶^{∗} ℭ.

Serialization in Øjeblik, and also in general, means that each object is inhabited by at most one thread. Self-serialization adds the requirement that whenever a thread successfully re-calls an object it has actually never left the object since its first visit.

Definition 4.5.4 (Self-Serialization). A configuration ℭ is

• serialized, if for all t̂_{1}, t̂_{2} ∈ cur(ℭ):

if trc_{ℭ}(t̂_{1}) ∩ trc_{ℭ}(t̂_{2}) ≠ ∅, then t̂_{1} = t̂_{2}.

• self-serialized, if, in addition, for all sequences t_{n} … t_{0} ∈ thr(ℭ): if s_{ℭ}(t_{i}) = s_{ℭ}(t_{j}) for 0 ≤ i < j ≤ n, then s_{ℭ}(t_{i}) = s_{ℭ}(t_{i+1}) = … = s_{ℭ}(t_{j−1}).

Note that this definition is compatible with pre-infliction. In the models R, F, and S, there is no book-keeping on traversed predecessor nodes, when requests are forwarded. Thus, when checking for the intersection of traces, we only see the “nodes of action”.

Proposition 4.5.5. Let a ∈ L_{0}. If [[[ a]]] ⟶^{∗} ℭ, then ℭ is self-serialized.

Proof (Sketch). Again, by induction on the length of S[[[ a]]] ⟶^{∗} ℭ, exploiting in each case the premises of the transition rules that address self-infliction and availability of objects. The only rule cases of interest are, when tasks are added, which is for (Inv) and (Fork), because only then the invariant may be broken. The actual proof in these cases is mere algebra. If tasks are removed from the current configuration, as with (Ret), then tasks are always only removed from the top of threads. Moreover, threads are never split up into two, so there is no danger of possibly invalidating the invariant that way. If we neither add nor remove tasks, then the invariant holds trivially, except for the case of (Join), which is the only rule that changes the parent of a task. Yet, also this case is harmless since it does not interfere with the condition of serialization due to initial and garbage tasks not having a current self and, thus, no trace.

4.6 Reduction vs Typing

We show that reduction preserves typing and, consequently, that every configuration reachable from a well-typed term is also well-typed. Therefore, we have to extend our type system to the domain of run-time configurations ℭ, which involves all run-time extensions: references v, tasks T, proxies ≫o, and run-time terms a ∈ L_{R}. For convenience in the typing of run-time terms, especially to keep track of the types and occurrences of wait, we introduce the task-annotated construct wait_{t}, which is uniquely determined on its creation within the (Inv)-rules. Accordingly, we may strengthen Lemma 4.5.2-3.

Lemma 4.6.1. Let a ∈ L_{0} and [[[ a]]] ⟶^{∗} ℭ. Let t, p ∈ R_{T} and s ∈ R_{O}.

1. If ℭ(t) = ⟨ p, s, e[wait_{t′}] ⟩ for some t′, then ℭ(t′) = ⟨ t, s′, c ⟩ for some s′ and c.

2. If ℭ(t) = ⟨ p, s, e[b] ⟩ and ℭ(t′) = ⟨ t, s′, c ⟩ for some b, t′, s′, and c, then b = wait_{t′}. Furthermore, if ℭ(t′′) = ⟨ p′′, s′′, e′′[wait_{t′}] ⟩, then t′′ = t, s′′ = s, and e′′[·] = e[·].

Note that the second property of this lemma now tells us that there are never two different parents waiting for the same task to finish. In Lemma 4.5.2-3, no such confusion could arise since parents did not know their children—with annotated wait, parents learn about their children, so we must explicitly prove that parents do not share their children.

Proof. By induction on the length of [[[ a]]] ⟶^{∗} ℭ.

Since we annotate all binding occurrences of variables with types, together with the dynamic annotation of all occurrences of wait, and also the fact that we record types for all references ever created, the proof of subject reduction is smooth, even in the critical cases of method invocation and return, as well as the interplay between fork and join. Note that it is also because of subject reduction that we model garbage threads explicitly; as long as a thread may be referred to, we need some typing assumption to preserve typability.

\frac{Γ ⊢ a:A  p ∉ \{↑, t_{g}\}}{Γ ⊢ ⟨ p, s, a ⟩ : A} (T-Task)  \frac{Γ(v) = A}{Γ ⊢ v:A} (T-Ref)

\frac{Γ ⊢ a:A  p ∈ \{↑, t_{g}\}}{Γ ⊢ ⟨ p, ↑, a ⟩ : Thr(A)} (T-Thrd)  \frac{Γ(t) = A}{Γ ⊢ wait_{t} : A} (T-Wait)

\frac{Γ ⊢ o:A}{Γ ⊢ ≫o : A} (T-Proxy)

Table 14: Typing rules for run-time entities and run-time terms

As new forms of typing judgments we need Γ ⊢ v:A, Γ ⊢ T:A, Γ ⊢ ≫o:A, and Γ ⊢ a:A, where the type environments Γ now may also include pairs v:A as assumptions on the types of references. The extended type system consists of the former rules in Table 2, now extended to admit run-time terms, and the additional rules in Table 14. The rules (T-Task) and (T-Thrd) derive the type of a task directly from the type of its enclosed runtime expression, where thread types only appear for orphan or garbage tasks. Similarly, the rule (T-Proxy) derives the type of proxies from the type of the target object. Recall from Lemma 4.5.2 that run-time expressions within tasks are always closed terms, so the type environment Γ in these cases will just have to contain typings for references, not for variables. Moreover, there are trivial rules to extract the types of references from the assumptions (T-Ref) and to extract the type of wait from its annotated task (T-Wait).

The typability of a configuration ℭ follows the standard idea of a sanity check that all of the run-time entities mentioned in the configuration, via references v, have to be typable under the assumptions that Γ makes of the types of those references (c.f. [Rep92]).

Definition 4.6.2. A closed, well-behaved configuration ℭ is called well-typed with respect to an environment Γ, written Γ ⊢ ℭ, if for all v ∈ dom(ℭ), indeed Γ ⊢ ℭ(v) : Γ(v).

For subject reduction, we further need a series of standard lemmas, which we present without proofs, that allow us to manipulate type environments. In the following, q ranges over variables and references, and refs(a) extracts the references that occur within term a. The following typing results hold for all aliasing variants of our operational semantics.

The first two lemmas allow us to add and remove type assumptions about variables or references not used in the term being typed.

Lemma 4.6.3 (Weakening). If Γ ⊢ a:A and q ∉ dom(Γ), then Γ, q:B ⊢ a:A.

Lemma 4.6.4 (Contraction). If Γ, q:B ⊢ a:A and q ∉ fv(a) ∪ refs(a), then Γ ⊢ a:A.

The next standard lemma allows us to substitute a term for a variable if the variable is assumed to have the same type as the term.

Lemma 4.6.5 (Substitution). If Γ, x:B ⊢ a:A and Γ ⊢ b:B, then Γ ⊢ a{^{b}/_{x}} : A.

We often need to move terms in and out of evaluation contexts. Lemma 4.6.7 states when we may do so in a “type-safe” manner. The first part states the obvious fact that if we can type the composition of an evaluation context e[·] and a term a, then the bare term a is also typable. The second part states that we can exchange terms of the same type within typable evaluation contexts. First, however, we need a way to relate the type environments involved in the lemma.

Definition 4.6.6. Two type environments Γ and Γ′ are compatible, written Γ ≍ Γ′, if Γ(q) = Γ′(q) for all q ∈ dom(Γ) ∩ dom(Γ′). A type environment Γ′ is a compatible extension of Γ, written Γ′ ⪰ Γ, if dom(Γ) ⊆ dom(Γ′) and Γ ≍ Γ′.

Lemma 4.6.7. Let Γ ⊢ e[a] : B and fv(e[a]) = ∅. Then:

1. There is a Δ ⪰ Γ and A such that Δ ⊢ a:A.

2. If Δ ⊢ a, b : A and (fv(b) ∪ refs(b)) ⊆ (fv(a) ∪ refs(a)), then Γ ⊢ e[b] : B.

We now proceed to the essential part of this subsection. The main result, subject reduction, states that typability of reachable configurations is preserved under reduction. Type safety, i.e., the property that every reachable configuration is in fact typable, is then proved by a simple induction using the main result.

Theorem 4.6.8 (Subject Reduction). Let a ∈ L_{0} with ∅ ⊢ a:A. Let [[[ a]]] ⟶^{∗} ℭ. If Γ ⊢ ℭ and ℭ → ℭ′, then there is Γ′ with Γ ≍ Γ′ such that Γ′ ⊢ ℭ′.

Proof. By transition induction. All cases in the proof follow the same scheme. Transitions ℭ → ℭ′ involve one or two tasks. We need to construct a new type environment Γ′ ≍ Γ such that Γ′ ⊢ ℭ′. Therefore, we extend Γ to Γ′ by application of the rules (New), (Cln), (Inv), and (Fork), while (Ret) shrinks Γ to Γ′ and in the other cases we have Γ′ = Γ.

If Γ ⊢ ℭ, then for a task T := ℭ(t) = ⟨ p, s, a ⟩, we must have Γ ⊢ T:C and Γ ⊢ a:B; if p ∈ {↑, t_{g}}, then C = Thr(B), otherwise C = B (c.f. Table 16). Now consider that task T = ⟨ p, s, a ⟩ takes part in a transition. Then, term a is decomposed into a context e[·] and a redex r, and a transition causes the redex to change into a run-time term b. What we need to show is that e[b] has the same type as a = e[r]. This we do by first using Lemma 4.6.7-1 to derive a type for the redex r, then we argue that b has the same type as r, then we use Lemma 4.6.7-2 to derive that e[b] has the same type as a. Finally, we can derive that the task ⟨ p, s, e[b] ⟩ has the same type as T by observing that p does not change (except for the rule (Join), but there it changes from ↑ to t_{g}, so the type is preserved also in that case). Having done so for the tasks involved in a transition we get that Γ′ ⊢ ℭ′ (tasks not involved in a transition need not be considered, since we do not change assumptions about references when constructing Γ′, we only add and remove assumptions).

(Let) By assumption Γ ⊢ e[let x:A = v in b] : B for some type B. By Lemma 4.6.7-1, there exists a Δ ⪰ Γ such that for some type B′, Δ ⊢ let x:A = v in b : B′. The only typing rule that applies here is (T-Let), implying that Δ ⊢ v:A and Δ, x:A ⊢ b:B′. By Lemma 4.6.5, Δ ⊢ b{^{v}/_{x}} : B′, and by Lemma 4.6.7-2, Γ ⊢ e[b{^{v}/_{x}}] : B.

(X -Inv) By assumption, Γ ⊢ e[o.l_{k}⟨ ṽ ⟩]:B, ℭ(o):Γ(o) and ℭ(o) = [l_{j} =ς(s_{j}:A, x̃_{j}:B̃_{j})b_{j}]_{j∈J}. The only rule allowing us to type [l_{j} =ς(s_{j}:A, x̃_{j}:B̃_{j})b_{j}]_{j∈J} is (T-Obj) and therefore Γ(o) must be a type [l_{j} :B̃_{j}→C_{j}]_{j∈J}. By Lemma 4.6.7-1, there is Δ ⪰ Γ such that Δ ⊢ o.l_{k}⟨ ṽ ⟩ : C, which could only occur with an application of (T-Inv). Therefore C = C_{k} and Δ ⊢ ṽ : B̃_{k}. By Lemma 4.6.4, we derive that Γ ⊢ ṽ : B̃_{k}. By Lemma 4.6.5, we derive that Γ ⊢ b_{k}{^{oṽ}/_{s_{k}x̃_{k}}} : C_{k}, because Γ, s_{k}:[l_{j} :B̃_{j}→C_{j}]_{j∈J}, x̃_{k}:B̃_{k} ⊢ b_{k}:C_{k}. Let ⟨ p′, o, b_{k}{^{oṽ}/_{s_{k}x̃_{k}}} ⟩ be the new task asscociated with t′ ∉ dom(Γ), created by (Inv). Let Γ′ = Γ, t′:C_{k}. Then, we get Γ′ ⊢ b_{k}{^{o,ṽ}/_{s_{k},x̃_{k}}} : Γ′(t′). Finally, we get Γ′ ⊢ e[wait_{t′}] : B by rule (T-Wait) and Lemma 4.6.7-2.

(Ret) We have two tasks ℭ(t) = ⟨ p, s, e[wait_{t′}] ⟩ and ℭ(t′) = ⟨ t, s′, v ⟩, where Γ ⊢ e[wait_{t′}] : B and Γ ⊢ v:C. By Lemma 4.6.7-1, we have a Δ ⪰ Γ such that Δ ⊢ wait_{t′} : C, which can only be using (T-Wait) with Δ(t′) = Δ(v) = A = C. By Lemma 4.6.7-2, we immediately get Γ ⊢ e[v]:B. Let Γ′ = Γ\{t′}. Finally, by Lemma 4.6.4, also Γ′ ⊢ e[v]:B, which reflects the fact that the task reference t′ is no longer used.

(Fork) Assume Γ ⊢ e[fork⟨a⟩] : B. By Lemma 4.6.7-1, we have Δ ⊢ fork⟨a⟩ : C for some Δ ⪰ Γ and C. The only way to type fork⟨a⟩ is using (T-Fork) implying that C = Thr(A) and Δ ⊢ a:A. By Lemma 4.5.2, fv(a) = ∅, and by Lemma 4.6.4, Γ ⊢ a:A. Let Γ′ = Γ, t′: Thr(A). Then, by Lemmas 4.6.3 and 4.6.7-2, Γ′ ⊢ e[t′]:B, a:A.

(Join) Assume ℭ(t′) = ⟨ ↑, ↑, v ⟩ and Γ ⊢ e[join⟨t′⟩]:B, ⟨ ↑, ↑, v ⟩:C. The only way to type ⟨ ↑, ↑, v ⟩:C is using (T-Thrd) implying that C = Thr(C′) and Γ ⊢ v:C′. Since Γ ⊢ ℭ, Γ(t′) = Thr(C′). By Lemma 4.6.7-1 for some Δ ⪰ Γ and A, Δ ⊢ join⟨t′⟩ : A. This typing must use (T-Join) as the last rule, this (together with (T-Ref)) implies that A = C′. By Lemma 4.6.3, Δ ⊢ v:C′, and by Lemma 4.6.7-2, Γ ⊢ e[v] : A. The join’ed task becomes a garbage task ⟨ t_{g}, ↑, v ⟩, but this does not change its type since tasks with an undefined parent or the garbage parent both are typed with (T-Thrd).

(X -Ali) As usual we have a Δ ⪰ Γ and A such that Δ ⊢ o.alias⟨o′⟩ : A. By (T-Ali) and (T-Ref), this implies that Δ(o) = Δ(o′) = A. By the observation that evaluation contexts do not bind references, Γ(o) = Γ(o′) = A. By Lemma 4.6.7-2, Γ ⊢ e[o′] : A. Consider an alias run-time entity ℭ(s^{∗}) = ≫o^{∗} with Γ ⊢ ℭ. We claim that s^{∗} and o^{∗} must have the same type. This is because, if Γ ⊢ ℭ, then for all references v in ℭ, Γ ⊢ ℭ(v) : Γ(v), then for a part of an alias chain ℭ(s^{∗}) = ≫o^{∗}, Γ ⊢ o^{∗} : Γ(s). Therefore, if s ∈ ali_{ℭ}(o), then Γ ⊢ s:A and Γ ⊢ ≫o^{∗} : Γ(s) as required.

(X -Cln) Assume Γ ⊢ e[o.clone]. By Lemma 4.6.7-1, we have a Δ ⪰ Γ and A such that Δ ⊢ o.clone : A. By Lemma 4.6.4, we get Γ ⊢ o.clone : A, and by (T-Clo) and (T-Ref), we get A = Γ(o). If s ∈ ali_{ℭ}(o), like in case (X -Ali), we have Γ(s) = Γ(o). Now let Γ′ = Γ, o′:Γ(s). By Lemma 4.6.7-2, Γ′ ⊢ e[o′] : B and Γ′ ⊢ ℭ′(o′) : Γ′(o′).

Theorem 4.6.9 (Type Safety). Let a ∈ L_{0} with ∅ ⊢ a:A. If [[[ a]]] ⟶^{∗} ℭ, then there is Γ such that Γ ⊢ ℭ.

Proof. By induction on the length of the reduction sequence.

(base case) Initial configurations of well-typed terms are well-typed:

{t_{m}: Thr(A), t_{g}: Thr(Thr(A))} ⊢ [[[ a]]]. (induction step) Let [[[ a]]] ⟶^{n−1} ℭ_{n−1} ⟶ ℭ_{n} = ℭ. Assume, by induction, that there is

Γ_{n−1} such that Γ_{n−1} ⊢ ℭ_{n−1}. Then, Theorem 4.6.8 concludes the proof.

A final remark is due on the notion of type preservation. Indeed, we allow in our semantics that task references that are allocated for invocations are released after a successful termination in rule (Ret). This is witnessed by the fact that, only in this case, the type environment may shrink. If, at some later moment in evaluation, the reference would be reused, this may in general be with a different type. Yet, this does not harm for subject reduction since one needs at least two steps to “change” the type of a task reference, while Theorem 4.6.8 is addresses single steps only. On the other hand, we may easily provide a semantics where task references are not reusable such that type environments never shrink.

5 On the Safety of Surrogation

The goal of this section is manifold. We motivate how to formulate the safety of surrogation in Øjeblik as an equation (§ 5.1). We study the two different kinds of external (§ 5.2) and self-inflicted (§ 5.3) surrogation and discuss how the various aliasing models behave in each of the cases. Then, we show how to formalize the fact that a certain surrogation is uniformly external (§ 5.4) and hint at a formal proof for the case of external surrogation (§ 5.5) that we report on in a companion paper. Finally, we provide a simple extension of Øjeblik’s type system that guarantees uniformly external surrogation (§ 5.6).

5.1 Safety as an Equation

We formalize the idea that an object before and after surrogation should behave the same in all possible contexts as an equation using the notion of typed equivalence of Definition 4.3.3. Let a ∈ L be an Øjeblik term. Our first attempt was to require:

a =^{⊢} a.surrogate  (5)

It turns out that this conjecture is rather naive, and indeed wrong with all four aliasing models. In the remainder of this section we adapt and narrow down the above equation such that it becomes true, and provably so. The following discussion also generalizes to migration in a distributed lexically-scoped setting, like Obliq.

The simplest case of Equation 5 is where a is an Øjeblik object 𝕆. In this case the surrogation is surely safe in all four semantics, because (1) the process of surrogation is carried out correctly since, due to serialization, only the surrogation thread can interact with the object 𝕆, i.e., there cannot be any interference with another thread or activity, and (2) every interaction with 𝕆 is mimicked identically by 𝕆.surrogate, which suffices since after surrogation nobody has access to the previous 𝕆.

In the general case, however, neither of the two above arguments holds. The reason is mainly because of possible copying of a reference to the former object such that, after surrogation, requests can still be directed to that reference. If these requests are subject to protection and serialization, then the semantics of aliasing models comes into the play. Observing that a =^{⊢} let x = a in x (in all contexts, the let just adds one unconditional step after reducing a) and that the notion of equivalence takes all well-typed Øjeblik contexts into account, Equation 5 can be reduced to the problem of surrogation on variables:

x =^{⊢} x.surrogate  (6)

However, there is an inherent problem with that equation, which is exhibited by the following context that, as the example in Equation (2), creates a self-alias via method call:

C[·] := let x = [ l=ς(s)s.alias⟨s⟩ ] in x.l; [·]  (7)

Independent of the underlying aliasing model, C[x]⇓ since x returns immediately, while C[x.surrogate]⇓̸, because x.surrogate sends the request into a loop along the trivially cyclic alias chain. Due to the above problem, we refine the safety equation to include some trivial request to check whether the object before surrogation is actually reachable:

x.ping =^{⊢} x.surrogate  (8)

This equation detects cyclic chains by means of the simple ping-request which travels to the endpoint of the alias chain possibly starting at x. For the above context, C[x.ping]⇓̸.

A closer look at Øjeblik examples, as we will have in the following two subsections, shows that for the safety of surrogation it is crucial to distinguish, whether or not the call x.surrogate within a given context C[·] is “external for” x, or whether it is selfinflicted. Note that, unfortunately, this problem is undecidable, as already observed for Obliq [Car95]—only at run-time may we observe which case applies. Intuitively, this means that we must therefore execute a term C[x.ping] until that particular access to x.ping appears at the top-level for evaluation.

5.2 Aliasing Models for External Surrogation

We provide two single-threaded, distinguishing examples that exhibit unsafe surrogations in the conservative and relaxed models, while the forwarder models behave safely. The two examples have a very similar structure, only differing in the object 𝕆 that, for the sake of well-typedness, has to serve single-parameter methods on label l.

C[·] := let x = 𝕆 in [·].l⟨x⟩

This context resembles the term of Equation (1) in that we intend to apply the context C[·] to two different requests: on the one hand x.ping, and on the other hand its surrogating counterpart x.surrogate. Applying our semantics we get that C[x.ping] and C[x.surrogate] roughly leads to x.l⟨x⟩ and x′.l⟨x⟩, respectively, where x′ is bound to the surrogation result, which is definitely different from x itself.

In Table 15, we show the initial steps according to our operational semantics: we indicate the applied transition rules, as well as the respective uniquely defined redex for each following step. (We deliberately omit the garbage reference task associated with t_{g} since it is not used in the examples.) Here, we are not specific about the aliasing model on which the semantics we follow is based, because all models, so far, coincide. Note the two additional steps (Cln) and (Ali) needed to perform the surrogation in between the applications of (Inv) and (Ret). Note further the different resulting states X and S, where either o or o′ is called, respectively, from within the main task t_{m} with o as parameter.

[[[ C[x.ping] ]]]

=\{t_{m} := ⟨ ↑, ↑, let x = \underline{𝕆} in x.ping.l⟨x⟩ ⟩\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(New)} →\{t_{m} := ⟨ ↑, ↑, \underline{let x = o in x.ping.l⟨x⟩} ⟩, o := 𝕆\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Let)} →\{t_{m} := ⟨ ↑, ↑, \underline{o.ping}.l⟨o⟩ ⟩, o := 𝕆\}
\begin{matrix}− \\ − \\ − \\ − \end{matrix}^{(Inv)} →\{t_{m} := ⟨ ↑, ↑, \underline{wait}.l⟨o⟩ ⟩, o := 𝕆, t_{1} := ⟨ t_{m}, o, \underline{o} ⟩\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Ret)} →\{t_{m} := ⟨ ↑, ↑, \underline{o.l⟨o⟩} ⟩, o := 𝕆\} =^{def} X

[[[ C[x.surrogate] ]]]

=\{t_{m} := ⟨ ↑, ↑, let x = \underline{𝕆} in x.surrogate.l⟨x⟩ ⟩\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(New)} →\{t_{m} := ⟨ ↑, ↑, \underline{let x = o in x.surrogate.l⟨x⟩} ⟩, o := 𝕆\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Let)} →\{t_{m} := ⟨ ↑, ↑, \underline{o.surrogate}.l⟨o⟩ ⟩, o := 𝕆\}
\begin{matrix}− \\ − \\ − \\ − \end{matrix}^{(Inv)} →\{t_{m} := ⟨ ↑, ↑, wait.l⟨o⟩ ⟩, t_{1} := ⟨ t_{m}, o, o.alias⟨\underline{o.clone}⟩ ⟩, o := 𝕆\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Cln)} →\{t_{m} := ⟨ ↑, ↑, wait.l⟨o⟩ ⟩, t_{1} := ⟨ t_{m}, o, \underline{o.alias⟨o′⟩} ⟩, o := 𝕆, o′ := 𝕆\}
\begin{matrix}− \\ − \\ − \\ − \end{matrix}^{(Ali)} →\{t_{m} := ⟨ ↑, ↑, \underline{wait}.l⟨o⟩ ⟩, t_{1} := ⟨ t_{m}, o, \underline{o′} ⟩, o≫o′ := 𝕆\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Ret)} →\{t_{m} := ⟨ ↑, ↑, \underline{o′.l⟨o⟩} ⟩, o≫o′ := 𝕆\} =^{def} S

Table 15: Initial Executions of the Counterexample

Countering to the Conservative Model The following context distinguishes a request x.ping and its surrogating counterpart x.surrogate in the model C:

C_{1}[·] := C[·] with 𝕆 instantiated as 𝕆_{1} := [ k=id , l=ς(s, z)z.k ]  (9)

Let X_{1} and S_{1} denote the respective derivatives of C_{1}[x.ping] and C_{1}[x.surrogate] in Table 15. Then, we can trace some more reductions now specific to 𝕆_{1}:

X_{1} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{(Inv)} → \{t_{m} := ⟨ ↑, ↑, wait ⟩, t′ := ⟨ t_{m}, o, \underline{o.k} ⟩, o := 𝕆_{1}\}
\begin{matrix}− \\ − \\ − \\ − \end{matrix}^{(Inv)} → \{t_{m} := ⟨ ↑, ↑, wait ⟩, t′ := ⟨ t_{m}, o, \underline{wait} ⟩, t′′ := ⟨ t′, o, \underline{o} ⟩, o := 𝕆_{1}\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Ret)} → \{t_{m} := ⟨ ↑, ↑, \underline{wait} ⟩, t′ := ⟨ t_{m}, o, \underline{o} ⟩, o := 𝕆_{1}\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Ret)} → \{t_{m} := ⟨ ↑, ↑, o ⟩, o := 𝕆_{1}\} =^{def} X′_{1} ↛

Here we were not specific about the semantics we follow when applying rule (Inv) since the behavior is the same in either case (C-Inv_{1}) or (R/F/S-Inv) and leads to convergence (X_{1}⇓ and thus C_{1}[x]⇓).

In contrast, for the execution of S_{1}, the various semantics exhibit different behaviors (which we indicate by subscripts) after the first common invocation step:

S_{1} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{(Inv)} → \{t_{m} := ⟨ ↑, ↑, wait ⟩, t′ := ⟨ t_{m}, o′, \underline{o.k} ⟩, o≫o′ := 𝕆_{1}\} =^{def} S′_{1}

While the model C blocks after

S′_{1} \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Inv_{2})} →_{C} \{t_{m} := …, t′ := ⟨ t_{m}, o′, wait ⟩, t_{i} := ⟨ t′, o, \underline{o′.k} ⟩, o≫o′ := 𝕆_{1}\}

because the addressed object o′ is already inhabited by task t′, the models R/F/S exhibit further reductions, like X_{1}, although yielding value o′:

S′_{1} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{(Inv)} →_{R/F/S} \{t_{m} := …, t′ := ⟨ t_{m}, o′, \underline{wait} ⟩, t′′ := ⟨ t′, o′, \underline{o′} ⟩, o≫o′ := 𝕆_{1}\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Ret)} →_{R/F/S} \{t_{m} := ⟨ ↑, ↑, \underline{wait} ⟩, t′ := ⟨ t_{m}, o′, \underline{o′} ⟩, o≫o′ := 𝕆_{1}\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Ret)} →_{R/F/S} \{t_{m} := ⟨ ↑, ↑, o′ ⟩, o≫o′ := 𝕆_{1}\} =^{def} S′′_{1} ↛

The reason is simply that in the latter modeling, the intermediate task t_{i} with parent o is not created at all, but instead the forwarding to o′, which represents the endpoint of the alias chain when starting at o, is done immediately, while still coming from parent o′, such that it is accepted as self-inflicted.

To summarize, we observe that in all four aliasing models, C_{1}[x.ping] converges since the critical call z.k of Equation (9) is transformed, at run-time, into o.k with parent o, i.e. into a self-inflicted call. In contrast, for C_{1}[x.surrogate], this call arises at run-time with parent o′, by then the surrogation target of object o, and comes back to o′ as a forwarded request. In the models R/F/S, the whole term converges in accordance with C_{1}[x.ping], but the model C blocks this call, as it is not self-inflicted due to the intermediate parent o created for task t_{i}.

Countering to the Relaxed Model The following context distinguishes between a request x.ping and its surrogating counterpart x.surrogate in the model R:

C_{2}[·] := C[·] with 𝕆 instantiated as 𝕆_{2} := [ l=ς(s, z)z.clone ]  (10)

Let X_{2} and S_{2} denote the respective derivatives of C_{2}[x.ping] and C_{2}[x.surrogate] in Table 15. As before, we now trace some more reductions of X_{2} and S_{2}:

X_{2} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{(Inv)} → \{t_{m} := ⟨ ↑, ↑, wait ⟩, t′ := ⟨ t_{m}, o, \underline{o.clone} ⟩, o := 𝕆_{2}\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Cln)} → \{t_{m} := ⟨ ↑, ↑, \underline{wait} ⟩, t′ := ⟨ t_{m}, o, \underline{o′} ⟩, o := 𝕆_{2}, o′ := 𝕆_{2}\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Ret)} → \{t_{m} := ⟨ ↑, ↑, o′ ⟩, o := 𝕆_{2}, o′ := 𝕆_{2}\} =^{def} X′_{2} ↛

Immediately, we observe the well-behavior of X_{2} in all aliasing models since the cloning requested within task t′ is obviously self-inflicted and leads to convergence (X_{2}⇓, and thus C_{2}[x.ping]⇓).

In contrast, the behavior of the corresponding S_{2} after the first step

S_{2} \begin{matrix}− \\ − \\ − \\ − \end{matrix}^{(Inv)} → \{t_{m} := ⟨ ↑, ↑, wait ⟩, t′ := ⟨ t_{m}, o′, \underline{o.clone} ⟩, o≫o′ := 𝕆_{2}\} =^{def} S′_{2}

is quite different for the respective models, due to the external cloning request. In the model C, we immediately get S′_{2} ↛_{C}. However, also in the model R, we get S′_{2} ↛_{R}; the reason is that forwarding, which helped us in dealing with Example (9), was only proposed for invocations and updates.

This is exactly the motivation for our forwarder models F and S, which remedy the above situation, because they recognize and accept pre-infliction also for cloning and aliasing. Consequently, they lead to convergence (S′_{2}⇓ and thus C_{2}[x.surrogate]⇓):

S′_{2} \begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Cln)} →_{F/S} \{t_{m} := ⟨ ↑, ↑, \underline{wait} ⟩, t′ := ⟨ t_{m}, o′, \underline{o′′} ⟩, o≫o′ := 𝕆_{2}, o′′ := 𝕆_{2}\}
\begin{matrix}− \\ − \\ − \\ − \\ − \end{matrix}^{(Ret)} →_{F/S} \{t_{m} := ⟨ ↑, ↑, o′′ ⟩, o≫o′ := 𝕆_{2}, o′′ := 𝕆_{2}\} =^{def} S′′_{2} ↛

To summarize, again in all four aliasing models, C_{2}[x.ping] converges since the cloning on z of Equation (10) is self-inflicted at run-time. However, among our four candidate semantics only the two forwarder models handle these requests properly for C_{2}[x.surrogate].

5.3 Self-Inflicted Surrogation

A particular class of examples is represented by objects that perform surrogation in a selfinflicted way such that they afterwards—as long as the current method is active—still can perform self-inflicted operations on the surrogated object. Due to these examples, surrogation cannot be safe in general, not even in the forwarder models. We classify two different sets of examples depending on whether they exhibit problems with access to a self-surrogated source or the target thereof. As for the detailed explanation of the examples in terms of their explicit reductions and reachable configurations, we omit them here and leave them as an exercise; they are similar to the developments in the previous subsection.

Target Problems An immediate source of problems is due to the incorrect external use of the surrogation target by means of protected operations, e.g., cloning:

C_{3}[·] := [ k=ς(s)let y = [·] in y.clone ].k  (11)

yields C_{3}[s.ping]⇓ and C_{3}[s.surrogate]⇓̸, because in C_{3}[s.ping] the cloning of y is allowed, while in C_{3}[s.surrogate] the corresponding call is blocked due to protection.

Source Problems Another problem arises by externally sending a request to the surrogation target, but now via the surrogation source, e.g., for updates:

C_{4}[·] := [ k=ς(s)let y = [·] in s.k⇐ id ].k  (12)

yields C_{4}[s.ping]⇓ and C_{4}[s.surrogate]⇓̸. By sending an update to itself after having surrogated, as in C_{4}[s.surrogate], the update of y is blocked, while without previous surrogation the call succeeds and the whole term converges.

The next (and final) example is intended to exhibit the effect of re-aliasing:

C_{5}[·] := let x = [ l=Ω , k=Ω ] in
[ l=id , k=ς(s)let y = [·] in s.alias⟨x⟩; y.l ].k

(13)

yields C_{5}[s.ping]⇓̸ and C_{5}[s.surrogate]⇓. Whereas C_{5}[s.ping] diverges since the alias call to s also affects y in that case, the counterpart C_{5}[s.surrogate] converges since the re-aliasing of s does not affect the target y.

All of these examples of observable self-surrogation can be interpreted as programming errors. In each case, the current method has the complete and local knowledge about the object and its surrogated counterpart at hand—because it itself performed the surrogation—but nevertheless operates on either of the two in an obviously “stupid” and avoidable manner. In these cases, it is not the fault of the semantics, but the fault of the programmer.

5.4 On the Absence of Self-Surrogation

The previous subsection exhibited that self-inflicted surrogation is inherently problematic. Thus, we should try to achieve a safety theorem at least for those cases where surrogation is guaranteed to be always external. Although this is an undecidable criterion, it can be formally defined and then used in formal proofs.

It suffices to concentrate the exposition on endpoint operations op ∈ {ping, surrogate}. Recall from Subsection 4.1 the characterization of self-infliction for the various aliasing models. We use the respective case for endpoint operations op in the context of the serialized forwarder model, which says that a particular request o.op with current self s is pre-inflicted in a particular run-time configuration ℭ if s = end(ali_{ℭ}(o)).

The above definition only helps us to address the question whether a request is external in a particular configuration. However, since concurrent threads may dynamically change the state of the object or alias that a request is directed to, we need a more general definition to express that a request will be external in all reachable configurations.

There are two ways to check for self-surrogation: either (1) consider all surrogation requests in a given term, or (2) consider only one particular request under study and trace it during the computation that brings it to top-level, i.e., in redex position. While the former is quite restrictive, the latter faces the problem to ensure during the reduction sequence that we can keep track on what happens to a particular request under study; in fact, the object or variable that it is syntactically addressed to is going to be replaced during evaluation by some object reference, and the request itself might be installed as subterm of some other piece of code on a task different from the initial one, which can even happen several times.

An obvious technique to trace a request is to tag the subterm of interest with some meta-information that does not affect the semantics, e.g. by means of overlining. To this aim, we may extend the syntax with overlined operations for ping, and surrogate (there would not be a problem doing the same for invocation, update, cloning, and aliasing). For this extended syntax we disallow rules with overlined redexes, but we allow to perform substitutions on them possibly replacing a variable with a reference. If we then start the evaluation of a term with at most one overlined subterm, then the evaluation of the expression inside a task is automatically stopped whenever an overlined subterm appears as a redex at top-level. Note that there can appear several instances of the one overlined redex that we started out with in the case that it was a subterm of a method body, which creates a new copy each time it is called.

Definition 5.4.1 (Uniformly External Contexts). Let C[·] be a context and x.op a request with ∅ ⊢ C[x.op] : B. Then, C[·] is called uniformly external for x.op, if for all ℭ with [[[ C[\overline{x.op}] ]]] ⟶^{∗} ℭ, if ℭ(t) = ⟨ p, s, e[\overline{o.op}] ⟩ for t, o ∈ dom(ℭ), then s ≠ end(ali_{ℭ}(o)).

Fact 5.4.2. Let x be an object variable and C[·] a context with ∅ ⊢ C[x] : B. Then C[·] is uniformly external for x.ping iff C[·] is uniformly external for x.surrogate.

5.5 Towards a Safety Theorem for Provers

According to the above remarks, we concentrate our efforts on reasoning about the equation x.ping =^{⊢} x.surrogate with respect to only those contexts that are uniformly external, because we conjecture that the forwarder models, especially the serialized version S will allow us to prove a theorem for these cases. According to Definition 4.3.1, this means:

Conjecture 5.5.1 (S-Safety). Let x be an object variable and C[·] a context with ∅ ⊢ C[x] : B. If C[·] is uniformly external for x.op, then C[x.ping]⇓ iff C[x.surrogate]⇓.

We restrain ourselves to call this conjecture a theorem, because we did not carry it out for the very notion of convergence as introduced in this paper, as we will explain in the following paragraph. Further comments on this matter can be found in the Conclusions.

In previous work on the Imperative Object Calculus (IOC) [AC96], equivalence between IOC terms was defined in a contextual way [GHL97], similar to Definition 4.3.1. In many cases, it seems simpler to use a semantics by translation into π-calculus [MPW92] to establish the equivalence between terms [KS98]. The main advantage is the large number of equivalences and algebraic laws that can be used to reason about expressions. Since IOC is (almost) a concurrency-free subset of Øjeblik, we chose a similar path for establishing the safety of external surrogation. An early sketch of a proof for a restricted version of Theorem 5.5.1, where only an inductively defined subset of ‘external’ contexts is taken into account, is found in [HKMN99], but the underlying π-calculus translation had several flaws. In our recent paper [MHKN99], we show the non-trivial proof based on a translation of Øjeblik that carefully follows the serialized model, and with respect to the corresponding notions of convergence and uniformly external contexts based on that π-calculus semantics.

5.6 Towards a Safety Theorem for Programmers

We argued earlier that it is the programmer of an object who is often responsible for potential problems caused by self-inflicted surrogation. In order to help a programmer to avoid these problematic cases, it would be useful to provide some syntactic criteria or programming guidelines, although they necessarily would tend to be rather restrictive. Note that the standard technique of restricting protected operations on the literal self, i.e., the innermost surrounding binding for s, does not work in the context of aliasing—see the above counterexamples. Yet, those examples of self-surrogation could be avoided if one was guaranteed that surrogation was the last operation performed on an object by the currently inhabiting tasks. If no operation is afterwards directed to s, then none of the above observable “mistakes” could be done. However, the fact that not only the current task may continue after the surrogation to operate on s, but also potentially other tasks in the call-stack that wait for the current task to return, complicates the quest for a syntactic criterion for a programmer.

There are two ways out of the dilemma of self-surrogation that we can imagine:

1. An application of data-flow analysis could verify that the self-inflicted surrogation is definitely the last operation called in the current self-inflicted method call-stack.

2. A type system could ensure that we never encounter self-surrogation at all, or at least provide us with warnings that self-surrogations might occur.

Here, we propose a solution based on the latter idea. The observation is that, if a evaluates to the current self, or to a node in an alias chain leading to the current self, then a must have the same type as the type of the current self (c.f. rule (T-Proxy) in Table 16).

\frac{∀j∈J Γ, s_{j}:A, x̃_{j}:B̃_{j} ⊢_{A} b_{j}:C_{j} A = [l_{j} :B̃_{j}→C_{j}]_{j∈J}}{Γ ⊢_{D} [l_{j} : ς(s_{j}:A, x̃_{j}:B̃_{j})b_{j}]_{j∈J} : A} (T-Obj)

\frac{Γ ⊢_{D} a:A A = [l_{j} :B̃_{j}→C_{j}]_{j∈J}  Γ, s:A, x̃:B̃_{k} ⊢_{A} b:C_{k}  k∈J}{Γ ⊢_{D} a.l_{k}⇐ς(s:A, x̃:B̃_{k})b : A} (T-Upd)

\frac{Γ ⊢_{D} a:A A = [l_{j} :A_{j}]_{j∈J} D ≠ A}{Γ ⊢_{D} a.surrogate : A} (T-Sur)

\frac{Γ ⊢_{Thr(A)} a:A}{Γ ⊢_{D} fork⟨a⟩ : Thr(A)} (T-Fork)

Table 16: Typing rules ensuring external surrogate operations

This implies, that if we ensure that the type of a is not the same as for the current self, then a.op cannot result in op being an internal operation. Such a check can be easily incorporated into the type system of Table 2. In the resulting system, judgments are of the form Γ ⊢_{D} a:A, where D denotes the type of the self variable for the method enclosing a. In Table 16 we present the modifications of the type system; the rules missing are as the ones in Table 2 with ⊢ replaced by ⊢_{D}.

The following theorem witnesses a static guarantee for uniformly external contexts provided by the type system. Here, as well as in the rule (T-Fork), we have to assign some current-self type to the top-level judgment. Since, by definition, threads do not have a current self, the natural choice is to use a thread type Thr(A) as the current-self type. The reason is that thread types never face the danger of being confused. Note that we could also simply use the type Thr([ ]) in these cases.

Theorem 5.6.1. Let x be a variable and C[·] be a program context with ∅ ⊢ C[x] : A. If ∅ ⊢_{Thr(A)} C[x.surrogate] : A, then C[·] is uniformly external for x.surrogate.

Proof. The proof is by contradiction: Assume ∅ ⊢_{Thr(A)} C[x.surrogate] : A where C[·] is not uniformly external for x.surrogate. Then, by Definition 5.4.1, there exists a configuration ℭ with C[ \overline{x.surrogate} ] ⟶^{∗} ℭ, where ℭ(t) = ⟨ f, s, e[ \overline{o.surrogate} ] ⟩ for t, o ∈ dom(ℭ), but s = end(ali_{ℭ}(o)). Here, the typing assumption for C[x.surrogate], which tells that o and s have different type, contradicts the fact that alias chains in configurations reachable from well-typed terms are homogeneously typed, which proves the theorem.

Let =_{ext}^{⊢} denote the equivalence of Definition 4.3.3 adapted to the new type system.

Conjecture 5.6.2. Let x be an object variable. Then x.ping =_{ext}^{⊢} x.surrogate.

Proof. Immediate from Theorem 5.6.1, Lemma 5.4.2, and Conjecture 5.5.1.

Note that Conjecture 4.3.5 does obviously not hold for the extended type system, because now the type system can no longer mimic any kind of misbehavior of ill-typed contexts; this fact is of course the whole purpose of the definition of the extended type system.

6 Conclusion

Résumé We have shown, by means of examples and the precise examination of their behavior according to formal semantics, that object surrogation in Øjeblik, and consequently object migration in Obliq, is not transparent. We have verified, using the Obliq interpreter [Car94], that these examples indeed expose problems with surrogation/migration in Obliq. Most of the migration problems were actually discovered, when trying to prove the safety of surrogation using π-calculus translations that implemented, first Obliq’s semantics, then Talcott’s semantics. Experimenting with these failed attempts led us to our final semantics for Øjeblik. The major improvement suggested by our studies is the use of forwarder models for the treatment of aliasing, which seems to be necessary in order to ensure transparency of, at least, external surrogation.

As pointed out in Subsection 4.1, the forwarder models can be understood as a good compromise between the concepts of self-infliction mutexes and of re-entrant mutexes to so-called pre-entrant mutexes: any request is allowed to re-enter an object, if it has only traveled through predecessors of the object since its last visit. A repaired version of Obliq should, by adopting the forwarder model, employ object aliasing rather as a primitive operation than merely derived from field aliasing. By that, the appropriate amount of serialization and protection for nodes in an alias chain can be implemented.

The major lesson learned from the work presented in this paper, is that concurrent objects need formal analysis—not only because one should prove properties for their own sake, but because formal analysis is a good debugging tool.

Language Design Issues Our formal discussion on the various aliasing models allows us to propose even more possibilities on how to model nodes in alias chains.

Since object aliasing had better be a primitive operation rather than derived from field aliasing, one may turn alias nodes into pure forwarders, even for local operations. The idea is that re-aliasing is useful for individual fields, but can be harmful for whole objects, where re-aliasing can anyway only occur as long as the node is active (cf. § 3.1). With field aliasing, re-aliasing could be initiated by activities of local siblings, which makes sense even after the current aliasing method has terminated. Note that in this proposal there is no need for protection as a requirement for surrogation since object aliases would be immediately stable if re-aliasing was prevented. (We do not question the general usefulness of protection, although this may be subject to further discussion.)

If the design of Obliq was not based on mutexes for self-infliction, but rather on reentrant mutexes, then the counterexample of Equation (9) would be resolved properly, but there would still be the other counterexample of Equation (10), where pre-entrant cloning would be needed, and also the counterexamples with respect to self-surrogation would still apply. Thus, if the concept of being reentrant would include protection in addition to serialization, then this design proposal would become as good as forwarder models, and even more liberal. However, the increased liberty of reentrant mutexes for serialization was already an argument for Cardelli to reject them for Obliq, and to prefer self-infliction. In this paper, we give formal and practical arguments for why pre-entrant mutexes and protection are the best choice from the point of view of transparent (external) migration.

Is Migration = Cloning ; Aliasing a good idea, after all? Since we completely ignored in our study the question of performance, or the feasibility of a run-time system to deal with ever-growing alias chains, it is hard to compare this style of migration to others that have been proposed, for example for Distributed Oz [VHB^{+}97]. (These matters go well beyond the scope of this paper, but we may note here that the compression of alias chains should be straightforward based on our formal notion of stable alias nodes.) However, we would like to emphasize that the intuitive simplicity of the concept does not quite compensate for the complexity that it imposes on formal reasoning, and also not for the sometimes unpredicted and surprising outcome of computations. It should be very interesting to study the safety of migration of other styles.

Current and Future Work We are about to use our semantics to show further properties about Øjeblik. For instance, we are about to show that join(fork(a))≅a holds, although this may only be true under certain self-infliction conditions, and we also expect some laws of Moggi’s computational λ-calculus [Mog89] to hold naturally. Similar properties have already been proved by Kleist and Sangiorgi [KS98] using a π-calculus semantics for the IOC, of which our translation in [MHKN99] is a rather direct generalization.

As noted in the Introduction, our conjectures on safe surrogation will only hold unless sites may fail, which is obvious by considering that the proxy site (where the object returned from s.ping resides) may fail, while the target site (where the object returned from s.surrogate resides) is still alive. Naturally, it would be interesting to study what safety of migration in a faulty setting could mean and in what precise sense it would be satisfied.

It would be challenging to exploit the operational semantics of the forwarder models, or suitable variants of it, directly for carrying out safety proofs. This is work in progress.

We sketch two more strands of ongoing work in the next paragraphs.

Operational Correspondence For the serialized aliasing model, we have given two different kinds of semantics, an operational semantics (OS) presented in this paper, and a semantics by translation into π-calculus (PI). An immediate question arises about the formal correspondence between these two semantics, which is even more critical in our case since, up to now, we have used PI for the main safety proof of the serialized model.

The basic complication to resolve is not a surprising one: the OS is very much based on a centralized global view of configurations, while the PI adopts a local view, where each node can only talk to its neighboring nodes, i.e., those to which it has references. For computations, this leads to situations where the PI engages in fully distributed interleaved step-by-step forwarding of requests along alias chains and possibly runs into local deadlocks, while the OS would recognize potential deadlock situations earlier and block the one-step forwarding of a request along the chain immediately. In a formalization of an operational correspondence between OS and PI, this discrepancy has to be taken into account properly.

The main property that the operational correspondence should yield is that convergence defined in the OS coincides with convergence in the PI, because convergence is what the chosen notion of typed equivalence is built upon. Based on the current state of affairs, we strongly believe to be able to achieve that goal.

Regaining Subtyping As we showed in Subsection 2.2, aliasing is not directly compatible with the subtyping rules of the IOC. The problem is that, in order to ensure that b is able to properly deal with all requests sent to a, when typing an alias operation a.alias⟨b⟩ we must know explicitly all the methods available in a. In this section, we briefly discuss a proposal to modify the type system, such that subtyping becomes possible again.

Our solution is to add some syntactic restrictions on the source a of an alias operation a.alias⟨b⟩. Since aliasing is a protected operation, a must be an expression that evaluates to (a node in a chain leading to) the current self. But since we know what a must evaluate to, in order for the aliasing operation to succeed, we may as well add the syntactic restriction that a must be the self variable of the enclosing method. By doing this we can use the fact that when typing an object we give the self variable a type containing all methods in the type environment. The only potential drawback we see in this proposal is that it prevents from pre-entrant aliasing, but this does not harm very much.

In Table 17, we show the rules for the modified type system. Here, a type judgment Γ ⊢_{s} a : A now contains an annotation on the ⊢, which provides the syntactic information

\frac{−}{Γ, x:A ⊢_{s} x:A} (S-Var) \frac{Γ ⊢_{s} a:A Γ, x:A ⊢_{s} b:B  s ≠ x}{Γ ⊢_{s} let x:A = a in b : B} (S-Let)

\frac{∀j∈J Γ, s_{j}:A, x̃_{j}:B̃_{j} ⊢_{s} b_{j}:C_{j} A = [l_{j} :B̃_{j}→C_{j}]_{j∈J}}{Γ ⊢_{s′} [l_{j} : ς(s_{j}:A, x̃_{j}:B̃_{j})b_{j}]_{j∈J} : A} (S-Obj)

\frac{Γ ⊢_{s′} s′:A A = [l_{j} :B̃_{j}→C_{j}]_{j∈J}  Γ, s:A, x̃:B̃_{k} ⊢_{s} b:C_{k}  k∈J}{Γ ⊢_{s′} s′.l_{k}⇐ς(s:A, x̃:B̃_{k})b : A} (S-Upd)

\frac{Γ ⊢_{s} b:A A = [l_{j} :A_{j}]_{j∈J} A <: Γ(s)}{Γ ⊢_{s} s.alias⟨b⟩ : A} (S-Ali)

\frac{Γ ⊢_{s} a:A A = [l_{j} :A_{j}]_{j∈J} Γ(s) ≮: A}{Γ ⊢_{s} a.surrogate : A} (S-Sur)

\frac{I ⊆ J}{[l_{j} :A_{j}]_{j∈J} <: [l_{i}:A_{i}]_{i∈I}} (S-Sub-Obj)

\frac{A <: B}{Thr(A) <: Thr(B)} (S-Sub-Thread)

Table 17: Typing and Subtyping for Aliasing

about the variable that is the current self. Note also our proposal for the rule (S-Sur) to prevent from self-inflicted surrogation: whenever we call a.surrogate, then it cannot be that the request arrives via forwarding at the current self s since the requirement Γ(s) ≮: A forbids that s could a successor of the chain starting at a with type A.

Acknowledgments We are grateful for discussions with and remarks from Luca Cardelli, Davide Sangiorgi, Carolyn Talcott, and ν-klubben at BRICS Aalborg. Moreover, we thank the anonymous referees for the detailed reading and their constructive remarks, which have helped improving the paper.

References

[AC96] M. Abadi and L. Cardelli. A Theory of Objects. Monographs in Computer Science. Springer, 1996.

[BFL98] M. Boreale, C. Fournet and C. Laneve. Bisimulations for the Join-Calculus. In D. Gries and W.-P. de Roever, eds, Proceedings of PROCOMET ’98. International Federation for Information Processing (IFIP), Chapman & Hall, 1998.

[Car94]  L. Cardelli. obliq-std.exe — Binaries for Windows NT. http://www.luca.demon.co.uk/
Obliq/Obliq.html, 1994.

[Car95] L. Cardelli. A Language with Distributed Scope. Computing Systems, 8(1):27–59, 1995. Short version in Proceedings of POPL ’95. A preliminary version appeared as Report 122, Digital Systems Research, June 1994.

[DF96] P. Di Blasio and K. Fisher. A Concurrent Object Calculus. In U. Montanari and V. Sassone, eds, Proceedings of CONCUR ’96, volume 1119 of LNCS, pages 655–670. Springer, 1996. An extended version appeared as Stanford University Technical Note STAN-CS-TN-96-36, 1996.

[FF86] M. Felleisen and D. P. Friedman. Control Operators, the SECD-machine, and the λ-calculus. In M. Wirsing, ed, Formal Description of Programming Concepts III, pages 193–217. North-Holland, 1986.

[GH98] A. D. Gordon and P. D. Hankin. A Concurrent Object Calculus: Reduction and Typing. In U. Nestmann and B. C. Pierce, eds, Proceedings of HLCL ’98, volume 16.3 of ENTCS. Elsevier Science Publishers, 1998.

[GHL97] A. D. Gordon, P. D. Hankin and S. B. Lassen. Compilation and Equivalence of Imperative Objects. In S. Ramesh and G. Sivakumar, eds, Proceedings of FSTTCS ’97, volume 1346 of LNCS, pages 74–87. Springer, Dec. 1997. Full version available as Technical Report 429, University of Cambridge Computer Laboratory, June 1997.

[HKMN99] H. Hüttel, J. Kleist, M. Merro and U. Nestmann. Migration = Cloning ; Aliasing (Preliminary Version). In Informal Proceedings of the Sixth International Workshop on Foundations of Object-Oriented Languages (FOOL 6, San Antonio, Texas, USA). Sponsored by ACM/SIGPLAN, 1999.

[JLHB88] E. Jul, H. Levy, N. Hutchinson and A. Black. Fine-Grained Mobility in the Emerald System. ACM Transactions of Computer Systems, 6(1), Feb. 1988.

[KS98] J. Kleist and D. Sangiorgi. Imperative Objects and Mobile Processes. In D. Gries and W.-P. de Roever, eds, Proceedings of PROCOMET ’98, pages 285–303. International Federation for Information Processing (IFIP), Chapman & Hall, 1998.

[Lan96] C. Laneve. May and Must Testing in the Join-Calculus. Technical Report UBLCS-96-4, DoCS, University of Bologna, March 1996. Revised: May 1996.

[MHKN99] M. Merro, H. Hüttel, J. Kleist and U. Nestmann. Mobile Objects As Mobile Processes.

Submitted. Available from http://www.cs.auc.dk/research/FS/ojeblik/, 1999.

[Mog89] E. Moggi. Computational Lambda Calculus and Monads. In Fourth Annual Symposium on Logic in Computer Science (LICS) (Asilomar, California), pages 14–23. IEEE, Computer Society Press, June 1989.

[Mor68] J.-H. Morris. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, 1968.

[MPW92] R. Milner, J. Parrow and D. Walker. A Calculus of Mobile Processes, Part I/II. Information and Computation, 100:1–77, Sept. 1992.

[Nes99] U. Nestmann. Mobile Objects (A Project Overview). In K. Spies and B. Schätz, eds, Proceedings of FBT ’99: Formale Beschreibungstechniken für verteilte Systeme (München, Juni 1999), Wissenschaft, pages 155–164. Herbert Utz Verlag, 1999.

[NHKM99] U. Nestmann, H. Hüttel, J. Kleist and M. Merro. Aliasing Models for Object Migration. In Proceedings of EUROPAR ’99, volume 1685 of LNCS. Springer, Sept. 1999.

[NOI^{+}99] C. L. Nielsen, L. Outzen, P. M. Ilsøe, S. H. Pedersen, T. Thomadsen and T. Lange. Øjeblink. Term project report, Aalborg University, June 1999. Available from http://www.cs.auc.

dk/research/FS/ojeblik/.

[Rep92] J. Reppy. Higher-Order Concurrency. PhD thesis, Cornell University, June 1992. Technical Report TR 92-1285.

[SY97] T. Sekiguchi and A. Yonezawa. A Calculus with Code Mobility. In Prodeedings of FMOODS’97, Canterbury, July. IFIP, Chapman and Hall, 1997.

[Tal96] C. L. Talcott. Obliq semantics notes. Unpublished note. Available from clt@cs.stanford. edu, Jan. 1996.

[VHB^{+}97] P. Van Roy, S. Haridi, P. Brand, G. Smolka, M. Mehl and R. Scheidhauer. Mobile Objects in Distributed Oz. ACM Transactions on Programming Languages and Systems, 19(5):804–851, Sept. 1997.

[Vit99] J. Vitek. Mobile Object Systems: Homepage. http://cuiwww.unige.ch/~ecoopws/, 1999.

Recent BRICS Report Series Publications

RS-99-44 Uwe Nestmann, Hans Hüttel, Josva Kleist, and Massimo Merro. Aliasing Models for Mobile Objects. December 1999. ii+46 pp. To appear in a special FOOL6 issue of Information and Computation. An extended abstract of this revision, entitled Aliasing Models for Object Migration, appeared as Distinguished Paper in Amestoy, Berger, Daydé, Duff, Frayssé, Giraud and Daniel, editors, 5th International Euro-Par Conference, EURO-PAR ’99 Proceedings, LNCS 1685, 1999, pages 1353–1368, which in turn is a revised part of another paper called Migration = Cloning ; Aliasing that appeared in Cardelli, editor, Foundations of Object-Oriented: 6th International Conference, FOOL6 Informal Proceedings, 1999 and as such supersedes the corresponding part of the earlier BRICS report RS-98-33.

RS-99-43 Uwe Nestmann. What is a ‘Good’ Encoding of Guarded Choice? December 1999. ii+34 pp. To appear in a special EXPRESS ’97 issue of Information and Computation. This revised report supersedes the earlier BRICS report RS-97-45.

RS-99-42 Uwe Nestmann and Benjamin C. Pierce. Decoding Choice Encodings. December 1999. ii+62 pp. To appear in Journal of Information and Computation. An extended abstract appeared in Montanari and Sassone, editors, Concurrency Theory: 7th International Conference, CONCUR ’96 Proceedings, LNCS 1119, 1996, pages 179–194.

RS-99-41 Nicky O. Bodentien, Jacob Vestergaard, Jakob Friis, Kåre J. Kristoffersen, and Kim G. Larsen. Verification of State/Event Systems by Quotienting. December 1999. 17 pp. Presented at Nordic Workshop in Programming Theory, Uppsala, Sweden, October 6–8, 1999.

RS-99-40 Bernd Grobauer and Zhe Yang. The Second Futamura Projection for Type-Directed Partial Evaluation. November 1999. Extended version of an article to appear in Lawall, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’00 Proceedings, 2000.

RS-99-39 Romeo Rizzi. On the Steiner Tree \frac{3}{2}-Approximation for Quasi-Bipartite Graphs. November 1999. 6 pp.