BRICS RS-98-33 Hüttel et al.: Migration = Cloning ; Aliasing BRICS

Basic Research in Computer Science

Migration = Cloning ; Aliasing

(Preliminary Version)

Hans Hüttel Josva Kleist Uwe Nestmann Massimo Merro

BRICS Report Series RS-98-33

ISSN 0909-0878 December 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, 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/98/33/

Migration = Cloning ; Aliasing (preliminary version)

To appear in: Informal Proceedings of FOOL6, January 1999.

Hans Hüttel^{∗} Josva Kleist^{†} Massimo Merro^{‡}

Uwe Nestmann^{§}

December 22, 1998

Abstract

In Obliq, a lexically scoped, distributed, object-based programming language, object migration was suggested as creating a (remote) copy of an object’s state at the target site, followed by turning the (local) object itself into an alias, also called surrogate, for the just created remote copy. There is no proof that object migration in Obliq is safe in any sense.

We consider the creation of object surrogates as an abstraction of the above-mentioned style of migration. We introduce Øjeblik, a distribution-free subset of Obliq, and provide two formal semantics, one in an intuitive configuration style, the other in terms of π-calculus. The intuitive semantics shows why surrogation is neither safe in Obliq, nor can it be so in full generality in Repliq (a repaired Obliq). The π-calculus semantics allows us to prove that surrogation in Øjeblik is safe for certain well-identified cases, thus suggesting that migration in Repliq may be safe, accordingly.

1 Motivation: From migration to surrogation

Øjeblik^{1} is an object-based language that is not only inspired by Obliq [Car95], but rather represents its concurrent core. Obliq is a lexically scoped, distributed, object-based programming language. 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 site at which execution takes place.

∗hans@cs.auc.dk †kleist@cs.auc.dk ‡Massimo.Merro@sophia.inria.fr §uwe@cs.auc.dk 1Danish for moment, ‘blink of the eye’.

It can be advantageous, for example for efficiency improvements, to migrate an object from one site to another, which is also called for in Obliq. Here, however, mutable values in general are never sent over the network; instead, only network references are transmitted. Accordingly, migration of objects is carried out in Obliq by creating a copy of the object at the target site and then modifying the original (local) object such that it forwards all future requests to the new (remote) object. Since Obliq is lexically scoped, we may safely ignore the aspects of distribution, so in Øjeblik we concentrate on just the concurrent aspects: surrogation of an object a can be described as creating a copy b of a and then turn a itself into a proxy for b, i.e., which forwards all future request for methods of a to b.

2 Øjeblik, a language for serialized concurrent objects

In this section, we present Øjeblik as an untyped language (types can be added in a straightforward manner), but we sometimes refer to types when we think it helps us in explaining our design decisions or it eases the understanding. For the sake of simplicity, compared to Obliq we

1. omit ground values, data operations, and procedures,

2. restrict field selection to just method invocations,

3. restrict multiple cloning to single cloning,

4. omit flexibility of object attributes,

5. replace field aliasing with object aliasing,

6. omit explicit distribution (sites, engines, name-servers),

7. omit exceptions and advanced synchronization,

so we get a still non-trivial, but more feasible language. The set L of Øjeblik-expressions is given by the grammar in Figure 2, where the l represent method labels.

An object [l_{j}=m_{j}]_{j∈J} consists of a finite collection of named methods l_{j}=m_{j}, more generally called fields, for pairwise distinct labels l_{j}.

In a method ς(s, x̃)b the letter ς is a binder for the self variable s and argument variables x̃ (a tuple x_{1}. . x_{n}) within the method body b. In order to invoke a method, we are required to supply a number of actual parameters:

a, b ::= 𝕆  object
| a.l⟨ a_{1}. . a_{n} ⟩  method invocation
| a.l⇐m  method update
| a.alias⟨b⟩  object aliasing
| a.clone  shallow copy
| let x = a in b  local definition
| s, x, y, z  variables
| fork(a)  thread creation
| join(a)  thread destruction
𝕆 ::= [l_{j}=m_{j}]_{j∈J}  object record
m ::= ς(s, x̃)b  method

Figure 1: Syntax of Øjeblik expressions

a, b ::= … | v | wait_{v ::= o | t}_{m ::= ς(s, x̃)b}_{𝕆 ::= [l_{j}=m_{j}]_{j∈J}} r ::= 𝕆

| o.l⟨ ṽ ⟩
| o.l⇐m
| o.alias⟨o′⟩
| o.clone
| let x = v in b
| fork(a)
| join(t)
| wait

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

Figure 2: Syntax of Øjeblik run-time expressions usually, a.l⟨ a_{1}. . a_{n} ⟩ with field l containing the method ς(s, x̃)b results in the body b with the enclosing object a bound to the self variable s, and the actual parameters a_{1}. . a_{n} of the invocation bound to the formal parameters x̃. The expression a.l⇐m updates the content of the named field l in a with method m and evaluates to the modified object.

Every object in Øjeblik comes equipped with special methods for cloning and aliasing, which cannot be overwritten by the update operation. The operation a.clone creates an object with the same fields as the original object and initializes the fields to the same values as in the original object. The operation a.alias⟨b⟩ replaces the object a with a pointer to b, regardless of whether a is already a pointer or still an object record^{2}. Thus, like cloning, the aliasing operation itself is not subject to aliasing. Consequently, the behavior of an Øjeblik-object can only be changed directly via method update or else indirectly by aliasing.

As usual, an expression let x = a in b (only non-recursive) first evaluates a, binding the result to x, and then evaluates b within the scope of the new binding. Moreover, a; b abbreviates let x = a in b, where x does not occur free in b.

To create a new concurrent thread we use the fork command. The expression fork(a) returns a thread identifier to denote a new thread evaluating a. To get the result of a computation in a fork’ed thread the join command is used. If a evaluates to a thread identifier, then join(a) either returns the value that the thread denoted by a has evaluated to, blocks until the thread finishes and then returns the resulting value, or blocks forever if a join on the a thread has already been performed^{3}.

Self-Infliction The current method of the current thread is the last method invoked in it that has not yet completed. The current self is the self of the current method. Operations on Øjeblik-objects can happen in two ways: a self-inflicted operation is an operation that is performed on the current self; an operation is external if it is not self-inflicted.

Serialization 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—it prevents recursion. Based on the notion of thread as a strand of activity, so-called reentrant mutexes 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 self-serialization 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 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.

2Note that this is consistent with re-aliasing in Obliq.

3In Obliq, an exception will be raised.

Protection Based on the notion of self-infliction, objects can be protected against external modifications in a natural way: for protected objects, updates, cloning, and aliasing, are only allowed, if these operations are selfinflicted.

Note that in Obliq, the programmer specifies by means of keywords whether an object is protected or serialized. In this document, however, we assume for simplicity that all Øjeblik-objects are both protected and serialized.

3 An operational semantics for Øjeblik

We give a transitional semantics for Øjeblik terms that closely follows 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. We adapt the basic setup to our restricted variant Øjeblik.

3.1 Concepts

The semantics performs changes on run-time configurations, which are mappings from references R to run-time entities. More precisely, a configuration ℭ maps task references t ∈ R_{T} and object references o ∈ R_{O} to tasks T and objects O, respectively, which we introduce below. We write t, o ∈ ℭ, if t, o are in the domain of ℭ, and ↑ for undefined references.

A run-time expression a is generated from the extended Øjeblik grammar as in Figure 2, where we introduce references as values v, 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 𝕆 as generated by the extended grammar, or a pointer ≫o to an object reference o ∈ R_{O}.

A run-time task T is a triple ⟨ f, s, a ⟩ ∈ R_{T} × R_{O} × L_{R} that refers to a father f, a current self s, and a run-time Øjeblik expression a that remains to be evaluated. By the partial functions s_{ℭ}(t) and f_{ℭ}(t), we refer to the—also possibly undefined—current self and father of the task associated with reference t in ℭ. As a well-formedness condition, we will only consider configurations, where each task is the father of at most one other task (fathers and children are unique), and if a task has a father reference, then this father is associated with a task within the configuration.

Alias chains Let the partial function ali_{ℭ} : R_{O} ⇀ R_{O} with

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

compute the endpoint of an alias chain (starting at reference o), which is associated with an object record if it exists.

Threads We formalize the notion of thread derived from a task as the task’s ancestors, similar to a call-stack in an implementation. Let his_{ℭ} : R_{T} → R_{T}^{∗} with

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

be the history of a task t, where · denotes concatenation of strings of references, and ϵ the empty string.

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

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

be the trace of a task, which represents the string of all object references that occur as the current self of the task and its ancestors. For example, with

ℭ = {t_{0} := ⟨↑, ↑, a_{0}⟩, t_{1} := ⟨t_{0}, s_{1}, a_{1}⟩, t_{2} := ⟨↑, ↑, a_{2}⟩},

we get his_{ℭ}(t_{1}) = t_{1}t_{0} and trc_{ℭ}(t_{1}) = s_{1}. A task t̂ is current in a configuration ℭ, if it is defined in ℭ, but not the father of any other task in ℭ. The threads of a configuration ℭ are identified as the set of 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 two threads {t_{1}t_{0}, t_{2}}. Finally, a task is active, if its expression is not a value.

Self-Infliction According to the need to test for the either self-inflicted or external character of operations on objects, we introduce some suitable notation. An object reference o is idle in ℭ, if it is not the current self of any task in ℭ.

Idle_{ℭ}(o) =^{def} _{⋀t∈R_{T}∩ℭ} (o ≠ s_{ℭ}(t))
Avail_{ℭ}(o, t) =^{def} Idle_{ℭ}(o) ∨ (o = s_{ℭ}(t))

An object reference o is available for task t in ℭ, if o is either idle or identical with the current self of task t.

Evaluation Figure 2 contains grammars for generating redexes r and evaluation contexts e[·], which we use to control the evaluation of (the expression part of) run-time tasks. The contexts are designed such that evaluation proceeds leftmost-innermost. A simple algorithm can compute for every runtime expression a ∉ R a unique pair of redex r and context e[·] such that a = e[r].

Behaviors The semantics [[[ a]]] of a closed Øjeblik term a ∈ L is given by assigning {t_{m} := ⟨ ↑, ↑, a ⟩} as its initial configuration. Note that the task associated with t_{m} is both current and active; it represents the start of a main thread. The behavior of configurations is generated from the transition rules in Figures 3–6. 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, the notation ℭ{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.

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

Figure 3: Local transitions

\frac{\begin{matrix}ℭ(t) = ⟨ f, s, e[o.alias⟨o′⟩] ⟩ s = o \\ o ∈ ℭ o′ ∈ ℭ \end{matrix}}{ℭ ⟶ ℭ\{t := ⟨ f, s, e[o′] ⟩, o := ≫o′\}}  (Ali)
\frac{\begin{matrix}ℭ(t) = ⟨ f, s, e[o.clone] ⟩ s = o \\ o ∈ ℭ o′ ∉ ℭ \end{matrix}}{ℭ ⟶ ℭ\{t := ⟨ f, s, e[o′] ⟩, o′ := ℭ(o)\}} (Cln)
\frac{ℭ(t) = ⟨ f, s, e[o.l⇐m] ⟩ ali_{ℭ}(o) = ô = s ℭ(ô) = [l_{j}=m_{j}]_{j∈J}  l = l_{k} for k∈J}{ℭ ⟶ ℭ\{ \begin{matrix}t := ⟨ f, s, e[ô] ⟩ \\ o := [l_{k}=m, l_{j≠k}=m_{j}]_{j∈J}\} \end{matrix}} (Upd)

Figure 4: Protected transitions

\frac{ℭ(t) = ⟨ f, s, e[o.l⟨ ṽ ⟩] ⟩  ali_{ℭ}(o) = ô ℭ(ô) = [l_{j}=ς(s_{j}, x̃)b_{j}]_{j∈J} l = l_{k} for k∈J Avail_{ℭ}(ô, s)  t′ ∉ ℭ}{ℭ ⟶ ℭ\{ \begin{matrix}t := ⟨ f, s, e[wait] ⟩ \\ t′ := ⟨ t, ô, b_{k}\{^{ôṽ}/_{sx̃}\} ⟩\} \end{matrix}} (Inv)
\frac{\begin{matrix}ℭ(t) = ⟨ f, s, e[wait] ⟩ \\ ℭ(t′) = ⟨ t, s′, v ⟩ \end{matrix}}{ℭ ⟶ ℭ\{t := ⟨ f, s, e[v] ⟩, t′ := ↑\}}  (Ret)

Figure 5: Method transitions

\frac{ℭ(t) = ⟨ f, s, e[fork(a)] ⟩ t′ ∉ ℭ}{ℭ ⟶ ℭ\{t := ⟨ f, s, e[t′] ⟩, t′ := ⟨ ↑, ↑, a ⟩\}} (Fork)
\frac{\begin{matrix}ℭ(t) = ⟨ f, s, e[join(t′)] ⟩ \\ ℭ(t′) = ⟨ ↑, ↑, v ⟩ \end{matrix}}{ℭ ⟶ ℭ\{t := ⟨ f, s, e[v] ⟩, t′ := ↑\}}  (Join)

Figure 6: Concurrency transitions

The rules in Figure 3 describe the local activity in a single task t in a straightforward manner; recall that let is not recursive and that the value v is either a task or an object reference whose actual run-time entity is accessible through ℭ, when needed.

The rules in Figure 4 have in common that they address protected operations, which can only happen if they are self-inflicted—so the premise o = s is required. Note also that the effects of (Ali) and (Cln) do not depend on whether the current object is aliased or non-aliased, while this is important for (Upd), where the check for self-infliction is only carried out on the endpoint ô of a (possible) alias chain starting with o. The intermediate nodes are thus treated in a rather liberal manner w.r.t. protection and serialization (cf. the detailed discussion in § 4 below).

The rules in Figure 5 formalize the protocol of synchronous method invocation, where each call creates a subtask as a child of the current task and blocks the father—by means of wait—until the subtask t′ signals its completion to its father t in rule (Ret). Note the use of the predicate Avail_{ℭ}(o) in rule (Inv) which is capturing the fact that a method call can be enabled—again checked for the endpoint ô of an alias chain—either externally or by means of self-infliction.

The rules in Figure 6 exhibit that the interplay of fork-and-join is dual to the invoke-and-return game: in rule (Join), it is the father who knows his child by name, while in rule (Ret), it is the child knowing his father by name. This distinction is crucial since we derive the notion of thread by collecting references along the father pointers. Forked tasks do not know their father, so they represent initial tasks of new threads.

Finally, note that for simplicity we have not generated run-time errors in the above semantics for the cases of invalid access to protected operations; here, the calls to such operations will just block forever.

3.2 Theory

Based on the operational semantics, we may now formally define—and prove—in a straightforward manner the concept of self-serialization for Øjeblik expressions. We may also define a behavioral notion of program equivalence. Definition 3.1 (Serializability). 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 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}).

Serialization 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.

Let ⟶^{∗} denote the reflexive-transitive closure of the transition relation on Øjeblik-configurations.

Proposition 3.2 (Soundness). For each Øjeblik term a, whenever [[[ a]]] ⟶^{∗} ℭ, then ℭ is self-serialized.

Proof. By induction on the length of transition sequences, exploiting the premises concerning self-infliction and availability of objects. The fact that the self or father of a task once added in a configuration is never changed, is also used.

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) and (Join), 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.

Based on a may-variant^{4} of convergence [Mor68], we will define a contextual notion of program equivalence.

Definition 3.3 (Convergence). If a is an Øjeblik term, then a⇓ if [[[ a]]] ⟶^{∗} ℭ with ℭ(t_{m}) = ⟨ ↑, ↑, v ⟩ for some v.

Note that this notion of convergence does not mean that the whole computation of a terminates, but rather that the main thread 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 other fork’ed computations that were not join’ed and might still be running, possibly forever.

In order to define a contextual notion of program equivalence, we also need a general notion of program context that differs from the notion of evaluation context given earlier. More specifically, according to Figure 3.2, an object context C[·] has a single hole [·] that may be filled with an Øjeblik term that possibly evaluates to an object; in particular, the hole must not be filled with a term that evaluates to a thread identifier. So, a composition C[a]

4In the context of a concurrent language with fork, where threads may nondeterministically affect the outcome and convergence of evaluation, and with respect to our goal of reasoning about surrogation, we regard must-variants of convergence as too strong.

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

Figure 7: Øjeblik object contexts

of an object context C[·] and an object expression a is well-formed^{5}, if a does not evaluate to a thread identifier. In the following, we implicitly consider only well-formed compositions.

Definition 3.4 (Equivalence). Two terms a, b ∈ L are observationally equivalent, written a ≅ b, if for all contexts C[·] with fv(C[a])=fv(C[b])=∅ : C[a] ⇓ iff C[b] ⇓.

3.3 Examples

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

Cycles Note that Øjeblik does not prevent the programmer from introducing self-aliases or alias chains with cycles, e.g.

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

(1)

In the semantics, after carrying out the aliasing operation, by means of the call to x. l⟨y⟩, yielding configuration ℭ, the call to x. k results in the function ali_{ℭ} not returning an argument. As a consequence, every operation on an object in an alias chain with cycles will block unless one of the objects breaks the cycle by means of re-aliasing (see also § 4).

5In a typed variant of Øjeblik, well-typed composition takes over.

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:

C[·] := let x = [ l=ς(s, z)z.clone ] in
let y = [·] in
x.l⟨y⟩

(2)

The behavior of C[x] is error-free: the cloning operation may take place since z is replaced with x such that the call z.clone is self-inflicted (see also § 5.2).

4 Models for alias chains

With respect to the semantics of the alias operation, there is some freedom on how to precisely model serialization and protection in the aliased object. There are several possible variants, some of which we list in order of strength:

• a conservative model that keeps all properties,

• a relaxed model that only partially keeps them,

• an ignorant model that ignores them completely.

According to Cardelli’s intuitive semantics [Car95, Car98], where object aliasing is derived from field aliasing, Obliq adopts the conservative model. A reasonable explanation is that, there, the aliased object still exists unchanged, but only accesses to its fields are redirected. The remainder of this section shall provide some operational understanding of the underlying concepts and differences of the above models.

It is helpful to clarify the structure and requirements of aliased objects in an alias chain. In particular, we try to distinguish the cases of external vs internal requests that need to be dealt with in aliased objects. Note that, in Obliq, there is no doubt about the forwarding of updates and invocations to the alias target, being them internal or external.

4.1 Inside alias chains

Considering the case of internal requests actually means that we look at an alias chain ‘under construction’. In this case, there is at least one nonendpoint node in the chain, where some task is running and has just, in a self-inflicted way, connected itself by means of an alias operation to its current successor. Let this be the case for s in

[figure: s; y]

where it has just connected itself to y. Note the behavior of further possible self-inflicted actions of the current method in s: no update on s may take place since it would already be forwarded to the y (and maybe further). Invocations on s would be treated in the same way, such that they will possibly be serialized in y or beyond. However, self-inflicted cloning and aliasing on s are successful, leading to one of

[figure: s; y; s′; or; s; y; z]

and such changes could continue further as long as the current method remains active. Once the method current in s terminates, the alias s≫y becomes stable, as it can never be changed again in future computations.

[figure: s; y]

Indeed, after an aliasing node has terminated its connection, every future incoming request will necessarily be external:

• for invocations and updates this is immediate, and

• for cloning and aliasing, this follows from the fact that the only possibility to start a self-inflicted cloning or aliasing—after the current method has finished—would be just within a method invoked at s, but any such will be forwarded to a successor of s, so it cannot affect s itself.

4.2 Protection: Countering to the ignorant model

For external protection-critical access, like aliasing or cloning, in aliased objects, both the relaxed and conservative model produce run-time errors. For example, in the case of an external aliasing request to an already aliased object

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

(3)

observe that the first call to x.l⟨y_{1}⟩ causes an internal aliasing operation on x, while the second afterwards tries to re-alias from the outside. While both the conservative and the relaxed model would—intuitively correct—block access to the call to x.alias⟨y_{2}⟩, the ignorant model would grant this external aliasing. This argument clearly suggests that protection should not be dropped completely, thus not to use the ignorant model, so we do not consider it further.

4.3 Serialization

The reason why one should keep serialization at all in aliased objects is, compared to protection, less obvious.

What may happen, when an external request enters a potentially serialized aliased object? Recall that, in Obliq, invocations and updates are always forwarded, while cloning and re-aliasing try to run where they are received. For the latter operations, the conservative and the relaxed model coincide and yield run-time errors. For the former operations, where forwarding is involved, the conservative and the relaxed model differ. It is crucial to clarify the interference between the act of forwarding that takes place in the source and the notion of current method for the moment when the forwarded request arrives at the target.

Forwarding vs current self For handling external requests that are to be forwarded by aliased objects, there are basically three strategies, which essentially rely on different underlying implementations of the object’s mutex:

1. If the request is required to grab the mutex of the aliased object before being forwarded, then we should also assume that, afterwards, the current method is the one holding the mutex in the source.

2. If the request is not required to grab the mutex, then it is natural to assume that the current method after forwarding is the one that sent the request to the source.

3. If the request is just required to be able to touch the mutex, which amounts to grab and immediately release it, then it seems also natural to assume that the current method after forwarding is like in strategy 2.

Strategy 2 may be considered as safe under the assumption that aliasing is only carried out if the set of properties of the target subsume the ones of the source such that serialization and protection may be carried out there, if necessary. Strategy 3 lies in between the other two (cf. Example (5)).

Note further that if a request is self-inflicted at the source, then the current method should be as in strategy 2.

Conservative vs relaxed model Example (4) shows the case of an invocation, which is subject to serialization only:

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

(4)

Observe that, in both models, the call x.l⟨y⟩ results in x turning itself into an alias to y. Then, the call y.l⟨x⟩ results in a call to x.k, which in turn is forwarded by x, now being an alias, back to y. There, it is treated differently:

• In the conservative model, which adopts strategy 1, the request arriving back at object y would be blocked because there is already a method active in it, which is not the current one.

• In the relaxed model, which adopts strategy 2 (cf. rules (Ali), (Fig), and (Upd) in Figures 4 and 5), the request forwarded to y is recognized as being self-inflicted since the current method is still the one active in y.

There may be reasons to prefer either of the possible design decisions. In our semantics, we chose the relaxed model to contrast it with Obliq’s conservative model, over which it has some advantages, as will be explored later on. Yet, also the relaxed model has some deficiencies.

A critique on the relaxed model In the operational semantics of § 3, reminiscent of Talcott [Tal96], we mimic the relaxed model. According to the rules (Inv) and (Upd), invocations and updates are forwarded directly to the endpoint of an alias chain disregarding activities that potentially go on in intermediate nodes, only checking for serialization and protection (for update) in the endpoint. For example, in

let y = [ l=id , k=id ] in
let x = [ l=id , k=s.alias⟨b⟩; … s …] in
fork(x.l); x.a

(5)

we concurrently call two different methods on x, both of which have the same chance of entering the object x.

If the call to x.l is first to enter, then there is no problem with the x.k getting in afterwards.

If, however, x.k is the first to enter, then after performing the aliasing operation resulting in a ‘chain-under-construction’ situation outlined in the beginning of § 4.1, where the other call to x.l might knock on x’s door. If there is no serialization going on in the now aliased object x, then this call might already (enter and) be forwarded, while x is still active in performing operations of the current method k. These operations may be self-inflicted and the programmer of method k might have had in mind that no other method might enter or pass x, as long as method k is active, so there might be inconsistent intermediate states of x that no other thread should be confronted with. To conclude, if the concept of serialization is to be interpreted rather strictly, external requests should be prevented from being processed in an aliased object as long as some computation is going on in it. So, the relaxed model of our semantics is not purely serialized (the semantics is too coarse-grained to exhibit this lack of serialization in a statement as of Definition 3.1).

The above discussion suggests that external requests should only be allowed to enter or pass an aliased object, when it has become stable, i.e., where requests are not in danger of passing the alias ‘under construction’. It is this idea we had in mind when introducing strategy 3. Once the alias is stable, external requests can always touch-and-go.

An relaxed interpretation: preentrant mutexes The relaxed model ignores serialization in intermediate nodes of alias chains since an invocation or update to any of them is directly forwarded to the endpoint of the chain.

Regarding protection, the situation is slightly different. Whereas cloning and aliasing are checked and carried out in the source, updates are forwarded to be checked and carried out at the endpoint. We update Example (4) to this case:

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

(6)

In the conservative model, a forwarded update causes a run-time error. In the relaxed model, the update is forwarded to the endpoint where it is accepted as self-inflicted.

The behavior of the relaxed model in the above two examples could be interpreted as a relaxation of the concept of self-infliction towards reentrant mutexes. A thread may leave its current self behind to enter another object preceding it in an alias chain, from where it is forwarded to the endpoint of the chain. If the endpoint is the current self, then the thread may re-enter. Mutexes that allow this behavior may be called pre-entrant since they allow for self-invocation on endpoints via predecessors in an alias chain.

5 Surrogation in Øjeblik

In Øjeblik-objects, we use the special method surrogate as our abstraction for migration: by calling it, an object is turned into a (local) proxy for a (remote) copy of itself.

a, b, c ::= … | a.surrogate

According to our abstraction from migration to surrogation, Cardelli [Car95] would suggest that the response of Øjeblik objects to the call to a.surrogate can be implemented precisely and uniformly as the method ς(s)SUR⟨s⟩ where:

SUR⟨s⟩ =^{def} let x = s.clone in s.alias⟨x⟩

Since left rather implicit in [Car95], we list the basic properties of surrogation, when implemented as a uniform method:

1. Surrogate methods shall not be updatable.

2. Surrogation shall be permitted for external requests.

3. Surrogation shall be forwarded by aliased objects.

Property 1 is reminiscent of cloning, aliasing, and updating, while properties 2 and 3 rather make it resemble invocation. Their justification is that surrogation mimics migration (although without resorting to explicit distribution), so an object should be surrogatable more than once. In this realm, double-surrogation a.surrogate; a.surrogate should obviously be equivalent to a.surrogate.surrogate. Without forwarding, the migration of an already migrated object would mistakenly migrate the proxy.

\frac{ℭ(t) = ⟨ f, s, e[o.surrogate] ⟩ ali_{ℭ}(o) = ô Avail_{ℭ}(ô, s)  t′ ∉ ℭ}{ℭ ⟶ ℭ\{ \begin{matrix}t := ⟨ f, s, e[wait] ⟩ \\ t′ := ⟨ t, ô, SUR⟨ô⟩ ⟩\} \end{matrix}} (Sur)

Figure 8: Surrogate transitions

The rule in Figure 8 precisely formalizes the semantics of surrogate according to the above properties as a uniform partially protected method in objects. The overall semantics of Øjeblik is still sound and also the definition of convergence and equivalence carries over smoothly.

The following statement is a first attempt to rephrase the title of this paper in terms of a formal semantics. The idea is that an object should behave the same in all contexts before and after surrogation, so we state an equation using the previously introduced notion of program equivalence.

Guess 5.1 (Safety of surrogation). Let a be an Øjeblik term. Then a ≅ a.surrogate.

It turns out that this guess is rather naive and indeed wrong with our current semantics, so in the following paragraphs we narrow down the above equation in a way such that it becomes true, and provably so. Along the way, we give a few examples that highlight various problems of surrogation. Note that the following discussion also generalizes to migration in a distributed lexicallyscoped setting, like Obliq.

The simplest case of Guess 5.1 is, where a is an Øjeblik object 𝕆. In this case the surrogation is surely safe because (1) the process of surrogation is carried out correctly since 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 in exactly the same way by 𝕆.surrogate and after surrogation nobody has access to the previous 𝕆.

In the general case, however, neither of the two above arguments holds. In order to simplify the discussion, note that by means of a ≅ let x = a in x and the fact that the notion of equivalence takes all Øjeblik contexts into account, the statement of Guess 5.1 can be reduced to the equation x ≅ x.surrogate, thus reducing the problem to surrogation on variables. It is easy to see that x⇓ iff x.surrogate⇓ since neither of them converges. Similarly, C[x]⇓ iff C[x.surrogate]⇓ for all contexts C[·] that do not bind x. This implies that the interesting contexts are the ones binding x.

For the safety of surrogation, it is decisive, whether or not the call x.surrogate is an external or a self-inflicted one. Note that this is an undecidable problem, so we can only at run-time observe which case applies. In the following series of examples, we consider both cases separately.

5.1 External surrogation

The main message of this subsection is that, even with respect to our weak semantics based on may-convergence:

External surrogation in Øjeblik is not safe! Migration in the Obliq [Car] is not safe!

… at least if the semantics or implementation is based on either the conservative or the relaxed alias chain model.

Countering to the conservative alias model The following object context C[·], a variant of Example (4), distinguishes an object variable x and its surrogated counterpart x.surrogate in Cardelli’s conservative alias model for Obliq:

C[·] := let x = [ k=id , l=ς(s, z)z.k ] in
let y = [·] in
y.l⟨x⟩

(7)

Regarding C[x] both the conservative and the relaxed model yield a (even must-) convergent computation since the call to y.l⟨x⟩ is transformed to a self-inflicted call to x.k.

In contrast, for C[x.surrogate], then this call arises from object y different from object x and comes back to y as a forwarded call. For the same reason as in Equation (4), the relaxed model still yields (must-) convergence, in accordance with C[x], while the conservative model blocks this call, always preventing the whole term from proper termination.

Countering to the relaxed alias model The following example, a variant of Example (2), distinguishes an object variable x and its surrogated counterpart x.surrogate in Talcott’s relaxed alias model for Obliq:

C[·] := let x = [ l=ς(s, z)z.clone ] in
let y = [·] in
y.l⟨x⟩

(8)

As already motivated in Example (2), the term C[x] converges since the cloning inside x is self-inflicted. This, however, is not the case for the term C[x.surrogate], for reasons similar to the previous Example (7): The call in the surrogation target y to clone its predecessor x is external to x.

Promoting the forwarder model The previous counterexamples obviously suggest that aliasing of objects should yield pure forwarders for external requests, not only for invocations, surrogations, and updates, but also—instead of generating run-time errors—for cloning and aliasing. In particular, like in the relaxed model, these external requests should be forwarded without affecting the identity of the current method. Otherwise, a surrounding context can be constructed that distinguishes variables x from their externally surrogated counterparts x.surrogate.

In comparison with the relaxed model, the forwarder model represents a proper generalization for the handling of external requests. For internal requests that enter aliased objects, i.e., as sketched at the end of Section 4, the situation is not different compared to the relaxed model. Note that the critique on the relaxed model that we articulated in § 4.3, and its correction by adopting forwarding strategy 3, is orthogonal to the generalization to the forwarder model, so the critique also applies to the latter.

If we want to adapt the operational semantics of § 3 to the forwarder model with strategy 3, we have to model

1. that for (Cln) and (Ali) forwarding to a non-endpoint successor—the current self—must be considered, and

2. that forwarding in (Cln), (Ali), (Upd), and (Inv), is only allowed via stable alias nodes.

We omit the straightforward formalization.

5.2 Self-inflicted surrogation

A particular class of examples is represented by objects that perform surrogation in a self-inflicted 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 is not completely safe, even in a forwarder model. We classify two different sets of examples depending on whether they exhibit problems with access to a self-surrogated source or the target thereof.

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

C[·] := [ k=ς(s)let y = [·] in y.clone ].k

yields

C[s] ⇓ and C[s.surrogate] ⇓̸.

(9)

In C[s] the cloning of y is allowed, while in C[s.surrogate] the corresponding call is blocked due to a run-time error.

Source problems Similar to the previous example, a problem arises by externally sending a request to the surrogation target, but now via the surrogation source, e.g., for updates:

C[·] := [ k=ς(s)let y = [·] in s.k⇐id ].k

yields

C[s] ⇓ and C[s.surrogate] ⇓̸.

(10)

By sending an update to itself after having surrogated, as in C[s.surrogate], the update of y is blocked and results in a run-time error, 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 after self-inflicted surrogation.

C[·] := let x = [ l=Ω , k=Ω ] in
let z = [ l=id , k=ς(s) \begin{matrix}let & y = [·] \\ in & s.alias⟨x⟩; y.l ].k \end{matrix}

yields

C[s] ⇓̸ and C[s.surrogate] ⇓.

(11)

Whereas C[s] diverges since the alias call to s also affects y in that case, the counterpart C[s.surrogate] converges since the re-aliasing of s does not affect the target y.

Note that it is the programmer of an object who is responsible for potential problems caused by self-inflicted surrogation. A programmer will hardly cause problems using self-surrogation if, in the current method, the self-variable s is neither copied (to prevent from target problems), nor used after surrogation in a self-inflicted way for calls to state-changing methods (to prevent from source problems). The safest way to prevent from problems of self-inflicted surrogation is to use the self-variable in the current method for nothing else but surrogation.

5.3 A safety theorem

Apparently, since internal surrogation in Øjeblik cannot be safe in general, we concentrate our efforts on x ≅ x.surrogate for the case that the surrogate operation is external to x. According to Definition 3.3, this means that the best safety theorem we can expect in Øjeblik is:

for all C[·] with [·] “external for” x:

C[x]⇓ iff C[x.surrogate]⇓.

(12)

Since self-infliction of method calls is statically undecidable, unless the hole [·] is at top-level (i.e., in redex position), how can we state that the contexts under consideration shall be the ones that render the call to x.surrogate external?

1. Give a “dynamic” definition based on evaluation of contexts according to an operational semantics.

2. Give a sound syntactic definition of “external” contexts that provides a reasonably complete approximation.

Both attempts will fail based on our current operational semantics. Even if we manage to cut down the number of contexts under consideration, we do not see that a proof of the safety of surrogation based on our definition of convergence in the operational semantics is tractable. The main reasons are: (1) this semantics only works for closed terms, so only convergence of these can be investigated; (2) the semantics is not sufficiently compositional;

(3) the semantics is in a non-syntactical configuration style such that derived configurations after some steps do not allow to reconstruct a corresponding term, thus it is impossible to describe the evaluation of contexts.

In previous work on Abadi and Cardelli’s Imperative Object Calculus (IOC) [AC96a], equivalence between IOC terms is defined in a contextual way [GHL97] similar to Definition 3.3. It turned out that in many cases it is simpler to use a semantics by translation into a π-calculus to establish the equivalence between terms. The main advantage is the large number of equivalences and algebraic laws to reason about expressions. Building on these experiences we choose a similar path—IOC is a concurrency-free subset of Øjeblik—for establishing the safety of external surrogation.

6 π-calculus background

In the next section we give the semantics of Øjeblik as an encoding into some π-calculus. In Figure 9, we introduce a monadic asynchronous πcalculus [HT92, Bou92], equipped with: (i) name testing; (ii) labeled values, called variants, used recently for encoding objects [San98]; (iii) a case destructor construct over variants values; (iv) a wrong construct used to indicate that a run-time error has occurred.

Substitutions, ranged over by σ, are functions from names to values; for an expression e which could be either a process or a value, eσ is the result of applying σ onto e, with the usual renaming to avoid captures of bound names. Substitutions have a tighter syntactic precedence than the process operators. Parallel composition has the lowest precedence among the operators.

Names

p, q, r, x, y, z, m, s, i, t Variant Tags

l Values

v ::= x  name
| l v  variant value

Processes

P ::= 0  nil process
| p(x). P  input
| \overline{p}v  output
| P | P  parallel
| (νx) P  restriction
| ! p(x). P  replicated input
| if [p=q] then P else Q name testing
| case v of {l (x) : P }^{∗} case destructor
| wrong  wrong

Figure 9: Syntax of π-calculus

The labeled transition system is the usual one in the early style [ACS98], extended with straightforward rules for case analysis and wrong [KS98].

Transitions are of the form P ⟶^{μ} P′, where action μ is: τ (interaction), pv (free input), \overline{p}v (free output), or \overline{p}⟨(νx) v⟩ (bound output, i.e., the emission of value v containing a private name x at p). In these actions, p is the subject and v the object part. Free and bound names (fn, bn) of actions and processes are defined as usual.

The relation ⟹ is the reflexive-transitive closure of ⟶^{τ}. Moreover, we recall standard notions for weak transitions:

μ̂ ; \begin{matrix}− \\ − \end{matrix} → =^{def} \{ \begin{matrix}\begin{matrix}− \\ − \end{matrix}^{μ} → & if μ ≠ τ \\ \begin{matrix}− \\ − \end{matrix}^{τ} → ∪ = & if μ = τ \end{matrix}  \begin{aligned}μ̂ ; {= \atop =} ⇒ & =^{def} & ⟹ μ̂ ; \begin{matrix}− \\ − \end{matrix} → ⟹ \\ {= \atop =}^{μ} ⇒ & =^{def} & ⟹ \begin{matrix}− \\ − \end{matrix}^{μ} → ⟹ \end{aligned}

They are direct generalizations to our extended calculus.

6.1 Behavioral Equivalences

In an asynchronous scenario, it makes sense to provide a notion of observability that considers only output actions [ACS98]. Process P has a barb at name q, written P ↓_{q}, if P can perform an output action whose subject is name q. We write P ⇓_{q}, if there exists a P′ with P ⟹ P′ and P ↓_{q}.

As regards behavioral notions of equivalence, we focus on bisimulationbased behavioral equivalences, precisely on barbed bisimulation [MS92]. It is well-known that barbed bisimilarity represents a uniform mechanism for defining behavioral equivalences in any process calculus possessing (i) a reduction relation and (ii) an observability predicate which simply detects the possibility of performing some observable action. Barbed bisimulation equips a global observer with a minimal ability to observe actions and/or process states but it is not a congruence. By closing barbed bisimulation under contexts we obtain a much finer relation.

Definition 6.1 (Barbed bisimulation/congruence). Barbed bisimulation, written ˙≈, is the largest symmetric relation on processes s.t. P ˙≈ Q implies:

1. If P ⟶^{τ} P′, then ∃ Q′ with Q ⟹ Q′ and P′ ˙≈ Q′.

2. If P ↓_{p} then Q⇓_{p}.

Processes P and Q are barbed congruent, written P ≅_{bc} Q, if for each context C[·] it holds that C[P] ˙≈ C[Q].

The main inconvenience of barbed congruence is that it uses quantification over contexts in the definition, and this can make proofs of process equalities heavy. However, there exist several versions of labeled bisimulations, which are defined without context quantification, but which imply barbed congruence, especially in an asynchronous setting [ACS98].

Definition 6.2 (Early bisimulation). Weak early bisimulation, written ≈, is the largest symmetric relation on processes s.t. if P ≈ Q and P ⟶^{μ}P′, with bn(μ) ∩ fn(Q) = ∅, then there exists Q′ s.t. Q \underrightarrow{μ̂} Q′ and P′ ≈ Q′.

6.2 Lπ laws

In the technical part of the paper, we make extensive use of some algebraic properties of the local asynchronous π-calculus, Lπ, due to Merro and Sangiorgi [MS98]. Lπ is a variant of the asynchronous π-calculus, where only the output capability of names may be transmitted, that is, the recipient of a name may use it only in output actions.

Asynchronous names are Lπ names if they cannot be tested and, whenever passed, they may be used by recipients only in output actions. Lπ names have several interesting algebraic properties, of which the following two, Laws (13) and (14), will be useful in our proofs.

Let C[·] be a standard π-calculus process context. Let p and q be two Lπ names with p ≠ q, and p does not appear free in input both in P and C[·]. Then

(νp)(!p(x). \overline{q}x | P) = P \{^{q}/_{p}\}  (13)
(νp)(!p(x). P | C[\overline{p}v]) = (νp)(!p(x). P | C[P \{^{v}/_{x}\}])  (14)

Law 13 is an optimization that allows us to replace a restricted forwarder ! p(x). \overline{q}x with a substitution. Such optimization laws are very useful in compiler environments. Law 14 resembles inline expansion, an optimization technique for functional languages that replaces a function call with a copy of the function body.

As already pointed out in [MS98], the algebraic properties of Lπ can be applied also in calculi where the usage of some names goes beyond the syntax of Lπ. For instance, there could be synchronous names, or names that can be tested for identity. A type system can be used to distinguish between Lπ names and the other names, and the theory of Lπ can then be applied to the former names.

7 A π-calculus semantics for Øjeblik

In addition to the core π-calculus, we introduce some well-known syntactic sugar for presenting the encoding: we use (i) tuples x̃, also in labeled values l ⟨z̃⟩ and patterns l (z̃), and (ii) parameterized recursive definitions. Both can be faithfully represented in our core calculus, tuples in a type-safe manner by means of variants [San98], and recursion up to weak bisimulation in terms of replication [Mil93].

7.1 Concepts

In Figures 10–13, we present an encoding from Øjeblik-terms into π-calcu-lus terms parameterized on two names. In an encoded Øjeblik term [[a]]_{p}^{i_{c}}, the parameters are used for returning its result (p), and for book-keeping its current self (i_{c}).

Objects The basic structure of the encoding is similar to the one for the imperative object calculus IOC by Kleist and Sangiorgi [KS98]: the translation of an object 𝕆, as shown in Figure 10, consists of a message that returns the object’s reference s on some result channel p, a composition of replicated processes that give access to the method bodies [[b_{j}]]_{r}^{i_{c}}, and a new object process new.O_{𝕆}⟨ s, t̃⟩ that connects invocations on s from the outside—via a series of managers—to the method bodies, which are invoked by the trigger names t̃.

Self-Infliction The main new idea of the translation is the distinction between two different self identifiers: an external self s to receive requests, and an internal self i to check for self-infliction. The crux for handling the latter resides on the protocol that each incoming request c carries with it a parameter i_{c} that identifies its current self, i.e., the internal self of the object from where the request originated. This parameter can then be matched against the internal self i of the current object: if [i_{c}≠i], then the request is regarded as external, i.e., originating from a different thread of control and, therefore, will be required to pass some serialization and protection mechanisms.

Serialization The mutual exclusion of activities within an object is implemented by a standard technique: a lock m, i.e., a message on a local mutex channel m that obeys the invariant that at any time there is at most one message on it available. Whenever a new object new.O is created, a new mutex is also created, and initialized.

External requests ([i_{c}≠i]) are forced to grab the mutex before they are forwarded on f to an object manager. After initialization, mutexes are only grabbed by serialization managers SM and released by the managers OM or AM.

We distinguish between object managers (OM) and alias managers (AM) since they behave differently. Before we get into their functionality, we have a look on how standard requests are generated by the clients of objects.

Clients In Figure 11, the current-self parameter i_{c} of encoded terms is ‘used’—just in object position—when clients pass it on together with their requests. In each case, the responsibility for returning a result on channel p is forwarded to the respective object manager. Furthermore, each of the translations obeys the same idea: the involved expressions are evaluated at private locations q, their results are grabbed and then used to forward lowlevel requests to the corresponding object managers. We chose a sequential leftmost-innermost evaluation order for objects and parameters, which also guarantees that i_{c} can only be ‘used’ once at a time.

Object managers We first consider the case of self-inflicted requests c (where [i_{c}=i]) that arrive in OM along name f, where no serialization or protection is required.

The basic functionality of the manager is to invoke the appropriate instances of method bodies (case l_{j} inv: activate the method body bound to l_{j} along trigger name t_{j}), and to carefully administrate updating (case l_{j} upd: install a new trigger name t′). Cloning (case cln) results in the restart of the current object manager in parallel with a new object new.O_{𝕆}⟨ s′, t̃⟩, which can be considered a copy of the former since it uses the same method bodies t̃, but is accessible through a fresh reference s′. Aliasing (case ali) is encoded by starting an appropriate aliased object manager AM instead of re-starting a previous non-aliased OM. Requests for surrogation (case sur) is simply translated in a compositional way as cloning followed by aliasing. Finally, also ping-requests can be handled; they are not generated from clients in Figure 11, but will be introduced later on with the encoding of variables in Figure 12.

If serialization is required, i.e., in the case of external invocation and surrogation, we create a fresh return channel r before we pass on the whole request, with the former result channel p replaced by r. By that, we may block all further requests that need to serialize, until some result y due to the current request is coming back on r. Only then, we are allowed to proceed by forwarding the result y to the intended result channel p and by releasing a signal on the mutex channel m in order to let the next serialized request become active in the object. Note that a triggered method body [[b_{j}]]_{r}^{i} and the externally invoked surrogation body [[SUR⟨s⟩]]_{r}^{i} are both run in the context of the current internal self i, so their further calls to s will be self-inflicted. This is of course essential for surrogation, since cloning and aliasing are only allowed internally.

If protection is required, i.e., in the case of cloning, aliasing, and update, we simply indicate a run-time error, whenever a modification request is attempted externally, and restart the object manager.

Aliased managers In accordance to our discussion in § 4 and 5, we intend to implement a forwarder model with forwarding strategy 3. An encoding in terms of the π-calculus provides just the right amount of granularity to make these ideas operationally precise. All external requests to an alias manager are forwarded—without modification of i_{c}—to the aliasing target s_{a}, its immediate successor.

In the self-inflicted cases, which represent an alias node ‘under construction’, cloning and aliasing are allowed and behave similar to the respective clauses in object managers, using new.A instead of new.O. The requests for update, invocation, and surrogation are forwarded as is to the local alias target s_{a}, where they will be considered external, since they are already selfinflicted in the current alias object.

Variables While the let-construct is encoded in a standard manner (see [KS98]), variables are dealt with in a non-standard way: instead of mapping [[x]]_{p}^{i_{c}} to \overline{p}⟨x⟩, signaling immediately where the object associated with x can be found, in Figure 12, we require variables to briefly interact with the run-time entity that they refer to by sending to it a ping-request. The intuition is that the referred entity simulates the usual signaling protocol, but refines it according to the context of self-infliction and aliasing.

According to our encoding of managers OM and AM, a ping-request is replied immediately if it is self-inflicted, and it is forwarded, when it is external in an alias node. Note that this design possibly delays the signaling protocol for external variable access until the object that it is referring to (via aliasing) has finished its current method. Consequently, it blocks the protocol if this current method diverges.^{6} We defer a further explanation to § 7.2.

6Thus, a variable looks ahead, before it is used in a computation thread: if its referred object is ping’able now, then only concurrent (i.e., fork’ed) computations may prevent its subsequent use for sending requests—in the realm of may-convergence, this tells us that terminating requests sent to the ping’ed variable may converge.

𝕆 =^{def} [l_{j}=ς(s_{j}, x̃)b_{j}]_{j∈J}
SUR⟨s⟩ =^{def} let x = s. clone in s. alias(x)
[[𝕆]]_{p}^{i_{c}} =^{def} (νst̃) ( \overline{p}⟨s⟩ | new.O_{𝕆}⟨ s, t̃⟩ | ∏_{j∈J}! t_{j}(r, i, s_{j}, x̃). [[b_{j}]]_{r}^{i} )
new.O_{𝕆}⟨ s, t̃⟩ =^{def} (νimf) ( \overline{m} | SM_{𝕆}⟨ s, i, m, f ⟩ | OM_{𝕆}⟨ s, i, m, f, t̃⟩ )
new.A_{𝕆}⟨ s, s_{a} ⟩ =^{def} (νimf) ( \overline{m} | SM_{𝕆}⟨ s, i, m, f ⟩ | AM_{𝕆}⟨ s, i, m, f, s_{a} ⟩ )
SM_{𝕆}⟨ s, i, m, f ⟩ =^{def} ! s(c). if [i_{c}=i] then \overline{f}⟨c⟩ else m. \overline{f}⟨c⟩
OM_{𝕆}⟨ s, i, m, f, t̃⟩ =^{def} f(c). if [i_{c}=i]

then case c of cln (p_{c}, i_{c}) : OM_{𝕆}⟨ s, i, m, f, t̃⟩ | (νs′) ( \overline{p_{c}}⟨s′⟩ | new.O_{𝕆}⟨ s′, t̃⟩ )

ali (s_{a}, p_{c}, i_{c}) : AM_{𝕆}⟨ s, i, m, f, s_{a} ⟩ | \overline{p_{c}}⟨s_{a}⟩
l_{j} upd (t′, p_{c}, i_{c}) : OM_{𝕆}⟨ s, i, m, t_{1}. . t_{j−1}, t′, t_{j+1}. . t_{n} ⟩ | \overline{p_{c}}⟨s⟩
l_{j} inv (x̃, p_{c}, i_{c}) : OM_{𝕆}⟨ s, i, m, f, t̃⟩ | \overline{t_{j}}⟨p_{c}, i, s, x̃⟩
sur (p_{c}, i_{c}) : OM_{𝕆}⟨ s, i, m, f, t̃⟩ | [[SUR⟨s⟩]]_{p_{c}}^{i}
ping (p_{c}, i_{c}) : OM_{𝕆}⟨ s, i, m, f, t̃⟩ | \overline{p_{c}}⟨s⟩

else

OM_{𝕆}⟨ s, i, m, f, t̃⟩ | case c of cln (p_{c}, i_{c}) : wrong | \overline{m}
ali (s_{a}, p_{c}, i_{c}) : wrong | \overline{m}
l_{j} upd (t′, p_{c}, i_{c}) : wrong | \overline{m}
l_{j} inv (x̃, p_{c}, i_{c}) : (νr)( \overline{t_{j}}⟨r, i, s, x̃⟩ | r(y). ( \overline{p_{c}}⟨y⟩ | \overline{m}) )
sur (p_{c}, i_{c}) : (νr)( [[SUR⟨s⟩]]_{r}^{i} | r(y). ( \overline{p_{c}}⟨y⟩ | \overline{m}) )
ping (p_{c}, i_{c}) : \overline{p_{c}}⟨s⟩ | \overline{m}
AM_{𝕆}⟨ s, i, m, f, s_{a} ⟩ =^{def} f(c). if [i_{c}=i]

then case c of cln (p_{c}, i_{c}) : AM_{𝕆}⟨ s, i, m, f, s_{a} ⟩ | (νs′) ( \overline{p_{c}}⟨s′⟩ | new.A_{𝕆}⟨ s′, s_{a} ⟩ )

ali (s′_{a}, p_{c}, i_{c}) : AM_{𝕆}⟨ s, i, m, f, s′_{a} ⟩ | \overline{p_{c}}⟨s′_{a}⟩
l_{j} upd (t′, p_{c}, i_{c}) : AM_{𝕆}⟨ s, i, m, f, s_{a} ⟩ | \overline{s_{a}}⟨c⟩
l_{j} inv (x̃, p_{c}, i_{c}) : AM_{𝕆}⟨ s, i, m, f, s_{a} ⟩ | \overline{s_{a}}⟨c⟩
sur (p_{c}, i_{c}) : AM_{𝕆}⟨ s, i, m, f, s_{a} ⟩ | \overline{s_{a}}⟨c⟩
ping (p_{c}, i_{c}) : AM_{𝕆}⟨ s, i, m, f, s_{a} ⟩ | \overline{p_{c}}⟨s⟩
else AM_{𝕆}⟨ s, i, m, f, s_{a} ⟩ | \overline{s_{a}}⟨c⟩ | \overline{m}

Figure 10: Encoding of Øjeblik-objects

[[a. clone]]_{p}^{i_{c}} =^{def} (νq) ( [[a]]_{q}^{i_{c}} | q(y) . \overline{y} cln ⟨p, i_{c}⟩ )
[[a. alias(b)]]_{p}^{i_{c}} =^{def} (νq_{x}q_{y}) ( [[a]]_{q_{y}}^{i_{c}} | q_{y}(y) . ([[b]]_{q_{x}}^{i_{c}} | q_{x}(x) . \overline{y} ali ⟨x, p, i_{c}⟩) )
[[a. l_{j}⇐ς(s, x̃)b]]_{p}^{i_{c}} =^{def} (νq) ([[a]]_{q}^{i_{c}} | q(y) . (νt) ( ! t(r, i, s, x̃). [[b]]_{r}^{i} | \overline{y} l_{j} upd ⟨t, p, i_{c}⟩ ) )
[[a. l_{j}⟨ a_{1}. . a_{n} ⟩]]_{p}^{i_{c}} =^{def} (νq) (νq_{1}⋯q_{n}) ([[a]]_{q}^{i_{c}} | q(y). ([[a_{1}]]_{q_{1}}^{i_{c}} |

q_{1}(x_{1}). (… q_{n}(x_{n}). \overline{y} l_{j} inv ⟨x_{1}…x_{n}, p, i_{c}⟩)))

[[a. surrogate]]_{p}^{i_{c}} =^{def} (νq) ( [[a]]_{q}^{i_{c}} | q(y) . \overline{y} sur ⟨p, i_{c}⟩ )

Figure 11: Encoding of Øjeblik-clients

[[let x = a in b]]_{p}^{i_{c}} =^{def} (νq) ( [[a]]_{q}^{i_{c}} | q(x) . [[b]]_{p}^{i_{c}} )
[[x]]_{p}^{i_{c}} =^{def} \overline{x} ping ⟨p, i_{c}⟩

Figure 12: Encoding of Øjeblik-variables

Concurrency To fork a thread means to create a new activity running in parallel with the current one(s). In the π-calculus, where we have a parallel operator, it suffices in addition to create a fresh self identifier upon thread creation and to implant it as the forked threads’ current self. In Figure 13, we use [[a]]_{q}^{νi} to abbreviate (νi) ([[a]]_{q}^{i}). Note that a fork is never blocking: we immediately return a private name t, which can be used to get back some result (the evaluation of the forked expression a) from the forked thread through interaction with a thread manager TM.

The thread manager is inquired in the translation of join(b) by sending its continuation p to the thread manager along t. Although term b may directly evaluate to some thread identifier, it may also evaluate to a variable that is bound to the thread identifier. In the latter case, the variable does not itself reply along q, but instead is sending a ping-request along t. Therefore, the thread manager has to simulate the variable’s signaling protocol, and then to tell the join’ing thread where to send its continuation to.

[[fork(a)]]_{p}^{i_{c}} =^{def} (νq, t) ( [[a]]_{q}^{νi} | \overline{p}⟨t⟩ | TM⟨q, t⟩ )
TM⟨q, t⟩ =^{def} t(x). case x of
ping (p_{c}, i_{c}) : TM⟨q, t⟩ | \overline{p_{c}}⟨t⟩
join (p_{c}, i_{c}) : TM^{D}⟨t⟩ | q(y). \overline{p_{c}}⟨y⟩
TM^{D}⟨t⟩ =^{def} t(x). case x of
ping (p_{c}, i_{c}) : TM^{D}⟨t⟩ | \overline{p_{c}}⟨t⟩
join (p_{c}, i_{c}) : TM^{D}⟨t⟩ | wrong
[[join(b)]]_{p}^{i_{c}} =^{def} (νq) ( [[b]]_{q}^{i_{c}} | q(t) . \overline{t} join ⟨p, i_{c}⟩ )

Figure 13: Encoding of Øjeblik-concurrency

7.2 Theory

Based on the notion of barbs of § 6, and following the intuition that an encoded term [[a]]_{p}^{i_{c}} eventually tells its result on name p, we may straightforwardly define a new notion of convergence for Øjeblik-terms using the π-calculus encoding.

Definition 7.1 (Convergence). If a is an Øjeblik term, then a⇓ if [[a]]_{p}^{νi}⇓_{p} for any p.

Accordingly, an Øjeblik term converges, if its translation may report its result on the name p. Note that this definition in principle even applies to open Øjeblik terms, e.g., to an Øjeblik variable x. However, our π-calculus semantics is designed to prevent [[x]]_{p}^{νi} from immediately reporting on p; it is required to send a ping-request along x such that a convergence signal is only possible if the ping-request reaches an object, alias, or thread manager.

Immediately, by inserting the π-calculus based notion of convergence into Definition 3.3, we get a π-calculus based notion of equivalence on Øjeblik terms. We may even go further and extend also this notion to open terms since the encoding treats variables carefully, which is important, when we compare variables to their surrogated counterpart.

For the remainder of the paper, the symbol ≅ shall denote the behavioral equivalence based on the notion of convergence that arises from the π-calcu-lus semantics.

7.3 Comparing to the operational semantics

The π-calculus semantics presented in this paper corrects and simplifies our previous approach [HKNS98], which turned out to be too restrictive for expressions that, after having changed an object, keep working on it in a selfinflicted manner, like the examples of self-inflicted surrogation in § 5.2. The current π-calculus semantics implements our proposal for an ideal semantics for Øjeblik, based on the forwarder model for alias chains, together with forwarding strategy 3, as introduce on page 16.

In general, whenever one has two different semantics at hand that address the same language, one should carefully argue—best in a formal way—for their consistence. In the context of the π-calculus the notion of operational correspondence, a kind of mutual simulation between computation steps in the source and target language of the translation, is often used to this end. In the case of our π-calculus semantics, in comparison with some appropriate variant of the operational semantics, we expect such a correspondence to be provable, but we have not yet carried out the necessary work. Here’s an informal sketch of the correspondence:

• Whereas the operational semantics can only be given for closed terms, also the operational correspondence can only address these.

• For a formal correspondence, the operational semantics should also include error-reporting rules instead of just blocking such that also error-cases can be considered.

• The main obstacle for the correspondence arises from the global-state point of view of the operational semantics that allows it to do several forwarding steps along alias chains at once. In contrast, in the π-calcu-lus, each individual forwarding step is a proper computation step. This implies that the occurrence of failures may be delayed in the π-calculus semantics.

Based on the operational correspondence, we conjecture that the two notions of convergence for Øjeblik terms coincide.

8 Proving the safety of external surrogation

In § 3, we derived a notion of behavioral equivalence for Øjeblik terms based on a SOS semantics. In § 7, by translation into π-calculus, we provided a new semantics that closely corresponds to the former. The advantage of a π-calculus semantics is that we can use established proof techniques for reasoning about Øjeblik programs to prove our conjecture.

Conjecture 8.1 (Safety). If we only consider external surrogations, then x ≅ x.surrogate.

This conjecture is not easy to prove, because ≅ still quantifies over Øjeblik contexts, but only the contexts that instantiate x actually need to be considered, as seen in § 5.

A variable x can be bound in three ways: using the let-construct, or using the ς-binder, either as a self-variable or as an ordinary variable in a method. We may want to immediately omit the binding as a self-variable since we do not intend our conjecture does not address internal surrogation. However, x may be bound as a self-variable in a nested way as in C[·] := [ k=ς(x)[ l=ς(s)[·] ] ].k.l, where the surrogate operation would become external. This implies that we should not exclude the binding of x as a selfvariable from the set of contexts that we consider for external surrogations.

Consider C[·] := let x = a in [·]. When the hole [·] is ready to be evaluated, we know that a has reduced to a value. During this evaluation, some concurrent computation could have been started. Note that this computation cannot interfere with the evaluation of x or x.surrogate inserted into [·], because either (i) these concurrent computations enter the object bound to x, then they postpone the evaluation of the hole, or (ii) the hole gets access to the object bound to x, then it blocks access from the concurrent computations. This shows that in let-contexts we may safely restrict our attention to just objects 𝕆 or other variables y as a binding for a, because any computation leading to these will not affect the use of x later on for surrogation; in particular, possibly started concurrent computations of a do not harm.

These consideration lead us to x-instantiating contexts.

Definition 8.2 (x-instantiating contexts). Let x be a variable, 𝕆 an object with x ∉ fv(𝕆), and C[·] an Øjeblik context that does not bind x. Let y and z be fresh variables. Then x-instantiating contexts are defined inductively as:

C_{1}^{x}[·] ::= let x = 𝕆 in C[·]
| [ …, l=ς(. . x. . )C[·] , …].l⟨. . 𝕆. . ⟩
C_{n+1}^{x}[·] ::= let y = 𝕆 in D_{n}^{y→x}[·]
| [ …, l=ς(. . y. . )D_{n}^{y→x}[·] , …].l⟨. . 𝕆. . ⟩
D_{1}^{y→x}[·] ::= let x = y in C[·]
| [ …, l=ς(. . x. . )C[·] , …].l⟨. . y. . ⟩
D_{n+1}^{y→x}[·] ::= let z = y in D_{n}^{z→x}[·]
| [ …, l=ς(. . z. . )D_{n}^{z→x}[·] , …].l⟨. . y. . ⟩

The advantage of x-instantiating contexts is that they have and inductively defined structure which helps us in proofs.

We get a preciser version of Conjecture 8.1.

Theorem 8.3 (Safety). If we only consider external surrogations, then for all x-instantiating Øjeblik contexts C_{n}^{x}[·]

C_{n}^{x}[x] ≅ C_{n}^{x}[x.surrogate]

Proof sketch. (We only mention the crucial points.) At the level of the π-cal-culus semantics, the assumption of considering only external surrogations for an x-instantiating Øjeblik context amounts to a simple syntactic assumption. Let 𝕆 be the object that is bound to x at the moment when the surrogation becomes active, i.e., appears at top-level. Then, at this moment, the mutex of object 𝕆 must be available, too, since this means that there is currently no method active in 𝕆. We exploit this simple condition in the proof below.

base case We have to prove that (i)

let x = 𝕆 in C[x] ≅ let x = 𝕆 in C[x.surrogate]

and (ii)

[ …, l_{j}=ς(s,. . x. . )C[x] , …]. l_{j}⟨. . 𝕆. . ⟩
≅
[ …, l_{j}=ς(s,. . x. . )C[x.surrogate] , …]. l_{j}⟨. . 𝕆. . ⟩

We consider only case (i), because the proof of (ii) is similar. If we put the two processes in a translated Øjeblik context, then they exhibit the same barbs. Then, we essentially carry out a standard bisimulation ‘game’ between left and right hand side of the equation according to the identical context C[·] on both side. We repeat this game, until we expose the context’s hole [·] at top-level, which renders the access to the variable x, and respectively its surrogation, active.

Next, we carry out the surrogation under the assumption that it is external. During this process, we need to exploit some information about serialization, provided by translated contexts, in order to be sure that the surrogation operation is not interfered with by nasty contexts. Here, we exploit the critical fact that the mutex of the object bound to x is currently available, which implies that there can be no other self-inflicted requests arriving from the surrounding derivative of a translated Øjeblik context.

After termination of the two-step surrogation, the overall result follows mainly by applying Laws 13 and 14. inductive step

For using the inductive hypothesis we only need the two following easy results:

\begin{aligned}1. & let x = y in a & ≅ & a\{^{y}/_{x}\} \\ 2. & [ …, l_{j}=ς(x̃)a , …]. l_{j}⟨ ỹ⟩ & ≅ & a\{ỹ/x̃\} \end{aligned}

The reason why, so far, we have only been able to prove that external surrogation is safe for a subset of Øjeblik terms is because ≅, although expressed in terms of π-calculus barbs, quantifies over Øjeblik contexts. The ideal situation would be, if we could show x ≅_{bc} x.surrogate, thereby avoiding the quantification over Øjeblik contexts. Unfortunately, this requires that surrogation is safe (meaning transparent) even for π-calculus contexts, which is not true for the π-calculus semantics that we give in the present paper. For instance, a π-calculus term can easily bypass serialization and start concurrent activities in an object by using the internal self of an object concurrently.

We are currently working on an equivalent, but more robust π-calculus semantics and proving safety even with respect to Lπ contexts. This allows us to reason using Lπ laws and labeled characterizations of barbed congruence. Such a result is obviously much stronger than the above-mentioned one, because it tells us that surrogation is safe even with respect to Lπ attackers, not only translated Øjeblik contexts.

9 Conclusion

Our formal analysis of Øjeblik has proven quite fruitful. By a series of examples, we have shown that object surrogation in Øjeblik, and consequently object migration in Obliq, is not as transparent as one might think in the beginning. We have been able to verify, using the Obliq interpreter, that these examples are indeed examples that show problems with surrogation/migration in Obliq.

Most of the examples were discovered, when trying to prove the safety of surrogation using pi-calculus translations that implemented, first Obliq’s semantics, then Talcott’s semantics. These failed attempts were the ones that led us to the final semantics for Øjeblik. Also working with two different semantics, where the operational semantics is a rather high-level semantics and the π-calculus semantics is closer to an implementation, helped us clarify subtleties in the informal semantics of Obliq, because just the process of keeping two semantics in sync forces one to consider implementation details at different levels of abstraction.

The major “improvement” suggested by our formal semantics is the forwarder model for the treatment of aliasing, based on preentrant mutexes. It seems to be necessary in order to ensure transparency of even only external surrogation. This leads us to the definition of a repaired version of Obliq, aka: Repliq, by adopting the forwarder model.

To us, the major lesson learned from the work presented in this paper, is that concurrent objects need formal analysis. Not because one necessarily should prove properties, but because the formal analysis is a good debugging tool.

Current and future work

Our current statement on the ‘safety’ of migration is not as good as we would like it to be. In particular, we are working on getting rid of x-instantiating contexts by the use of a more robust π-calculus semantics, by which we expect to be able to prove 8.1.

Of course, one more work is required on establishing an operational correspondence between the operational semantics and the π-calculus semantics. Such a result will definitely increase one’s confidence in that the semantics really expresses what we have stated they do.

The π-calculus that we are using can be equipped with a type-system. One could also consider giving a type-system to Øjeblik. By translating types from Øjeblik to types in the π-calculus, we expect to get a proof of subject-reduction for Øjeblik types almost for free.

Now that we have shown that internal surrogation is not safe in general, it would be good to able to give a programmer a better syntactic criteria expressing that if she writes programs like this, then surrogation will be safe.

Finally, we would like to use the semantics to show other, perhaps simpler, properties about Øjeblik. For instance, one could consider showing that join(fork(a))≅a under certain circumstances.

Related work

Apart from Talcott [Tal96], closest to our work and like ours based on Abadi and Cardelli’s object calculus [AC96b], is Gordon and Hankin’s concurrent object calculus [GH98], where concurrency is introduced by means of (not completely commutative) parallel operators. However, no account on object migration has been addressed in their work.

References

[AC96a] M. Abadi and L. Cardelli. An Imperative Object Calculus. Theory and Practice of Object Systems, 1(13):151–166, 1996.

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

[ACS98] R. M. Amadio, I. Castellani and D. Sangiorgi. On Bisimulations for the Asynchronous π-Calculus. Theoretical Computer Science, 195(2):291–324, 1998. An extended abstract appeared in Proceedings of CONCUR ’96, LNCS 1119: 147– 162.

[Bou92] G. Boudol. Asynchrony and the π-calculus (Note). Rapport de Recherche 1702, INRIA Sofia-Antipolis, May 1992.

[Car] L. Cardelli. obliq-std.exe — Binaries for Windows NT. http://www.luca.

demon.co.uk/Obliq/Obliq.html.

[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.

[Car98] L. Cardelli. On the Semantics of Obliq. Personal Communication, 1998.

[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 Electronic Notes in Theoretical Computer Science. 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 Lecture Notes in Computer Science, pages 74– 87. Springer-Verlag, Dec. 1997. Full version available as Technical Report 429, University of Cambridge Computer Laboratory, June 1997.

[HKNS98] H. Hüttel, J. Kleist, U. Nestmann and D. Sangiorgi. Surrogates in Øjeblik: Towards Migration in Obliq. In H. Hüttel and U. Nestmann, eds, Proceedings of SOAP ’98, volume NS-98-5 of BRICS Notes Series, pages 43–50. BRICS, Denmark, 1998.

[HT92] K. Honda and M. Tokoro. On Asynchronous Communication Semantics. In M. Tokoro, O. Nierstrasz and P. Wegner, eds, Object-Based Concurrent Computing 1991, volume 612 of Lecture Notes in Computer Science, pages 21–51. Springer-Verlag, 1992.

[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.

[Mil93] R. Milner. The Polyadic π-Calculus: A Tutorial. In F. L. Bauer, W. Brauer and H. Schwichtenberg, eds, Logic and Algebra of Specification, volume 94 of Series F: Computer and System Sciences. NATO Advanced Study Institute, Springer-Verlag, 1993. Available as Technical Report ECS-LFCS-91-180, University of Edinburgh, October 1991.

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

[MS92] R. Milner and D. Sangiorgi. Barbed Bisimulation. In W. Kuich, ed, Proceedings of ICALP ’92, volume 623 of Lecture Notes in Computer Science, pages 685– 695. Springer-Verlag, 1992.

[MS98] M. Merro and D. Sangiorgi. On Asynchrony in Name-Passing Calculi. In K. G. Larsen, S. Skyum and G. Winskel, eds, Proceedings of ICALP ’98, volume 1443 of Lecture Notes in Computer Science, pages 856–867. Springer-Verlag, July 1998.

[San98] D. Sangiorgi. An Interpretation of Typed Objects into Typed π-Calculus. Information and Computation, 143(1):34–73, 1998. Earlier version published as Rapport de Recherche RR-3000, INRIA Sophia-Antipolis, August 1996.

[Tal96] C. Talcott. Obliq semantics notes. Unpublished note, Jan. 1996.

Recent BRICS Report Series Publications

RS-98-33 Hans Hüttel, Josva Kleist, Uwe Nestmann, and Massimo Merro. Migration = Cloning ; Aliasing (Preliminary Version). December 1998. 40 pp. To appear in 6th International Workshop on the Foundations of Object-Oriented, FOOL6 Informal Proceedings, 1998.

RS-98-32 Jan Camenisch and Ivan B. Damgård. Verifiable Encryption and Applications to Group Signatures and Signature Sharing. December 1998. 18 pp.

RS-98-31 Glynn Winskel. A Linear Metalanguage for Concurrency.

November 1998.

RS-98-30 Carsten Butz. Finitely Presented Heyting Algebras. November 1998. 30 pp.

RS-98-29 Jan Camenisch and Markus Michels. Proving in Zero-Knowledge that a Number is the Product of Two Safe Primes. November 1998. 19 pp.

RS-98-28 Rasmus Pagh. Low Redundancy in Dictionaries with O(1) Worst Case Lookup Time. November 1998. 15 pp.

RS-98-27 Jan Camenisch and Markus Michels. A Group Signature Scheme Based on an RSA-Variant. November 1998. 18 pp. Preliminary version appeared in Ohta and Pei, editors, Advances in Cryptology: 4th ASIACRYPT Conference on the Theory and Applications of Cryptologic Techniques, ASIACRYPT ’98 Proceedings, LNCS 1514, 1998, pages 160–174.

RS-98-26 Paola Quaglia and David Walker. On Encoding pπ in mπ. October 1998. 27 pp. Full version of paper to appear in Foundations of Software Technology and Theoretical Computer Science: 18th Conference, FCT&TCS ’98 Proceedings, LNCS, 1998.

RS-98-25 Devdatt P. Dubhashi. Talagrand’s Inequality in Hereditary Settings. October 1998. 22 pp.

RS-98-24 Devdatt P. Dubhashi. Talagrand’s Inequality and Locality in Distributed Computing. October 1998. 14 pp.

RS-98-23 Devdatt P. Dubhashi. Martingales and Locality in Distributed Computing. October 1998. 19 pp.