Sung-Shik T Q Jongmans
email: jongmans@cwi.nl

Christian Krause

Farhad Arbab

Encoding Context-Sensitivity in Reo into Non-Context-Sensitive Semantic Models

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Over the past decades, coordination languages have emerged for modeling and implementing interaction protocols between two or more software components. One example is Reo [START_REF] Arbab | Reo: A channel-based coordination model for component composition[END_REF], a language for compositional construction of connectors. Connectors are software entities that coordinate the communication between components; they constitute the glue that holds components together, and become, once considered at a higher level of abstraction, components themselves.

Connectors have several behavioral properties; for instance, they may manipulate data items that pass through them. Another property is context-dependency or context-sensitivity: whereas the behavior of a context-insensitive connector depends only on its own state, the behavior of a context-sensitive connector depends also on the presence or absence of I/O-requests at its ports-its context. To illustrate context-sensitivity, we consider the LossySync connector, which coordinates the interaction between two components: a writer and a taker. If the taker is prepared to receive data, LossySync properly relays a data item from the writer to the taker. If the taker, however, refuses to receive, LossySync loses the data item sent by the writer. Since LossySync's behavior depends on the taker's willingness to receive data, that is, the presence or absence of a request for input, LossySync exhibits context-dependent behavior.

Several formal models for describing the behavior of Reo connectors exist, but not all of them have constructs for context-dependency. For example, the early models (e.g., an operational model based on constraint automata [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF]), although attractive because of their simplicity, lack such constructs. These models implement context-sensitivity as non-determinism. In an attempt to mend this deficiency, more recent models incorporate constructs for context-dependency, but at the cost of more complex formalisms (e.g., the 3-coloring model [START_REF] Clarke | Connector colouring I: Synchronisation and context dependency[END_REF]). As a result, the algorithms for their simulation and verification suffer from a high computational complexity, which makes these models less attractive in practice.

In this contribution, we show that context-dependency in fact can be captured in simple semantic models, namely the 2-coloring model [START_REF] Clarke | Connector colouring I: Synchronisation and context dependency[END_REF] and constraint automata: we define an operator that transforms a connector with 3-coloring semantics to one with 2-coloring semantics, while preserving its context-sensitive behavior. Furthermore, we prove the transformation's correctness, and, to illustrate its merits, we show how our approach enables the verification of contextdependent connectors with the Vereofy model checker (impossible up to now). Other applications of our approach include context-sensitive connector decomposition [START_REF] Pourvatan | Decomposition of constraint automata[END_REF], and, as we speculate, an improved implementation of Reo's interpreter.

The paper is organized as follows. In Section 2, we briefly discuss Reo and connector coloring. In Section 3, we present the transformation from 3-coloring models to 2-coloring models. In Section 4, we present an application of our approach to Vereofy. We discuss related work in Section 5. Section 6 concludes the paper.

Reo Overview

In this section, we discuss connectors in Reo and the coloring models for describing their behavior. A comprehensive overview appears in [START_REF] Arbab | Reo: A channel-based coordination model for component composition[END_REF][START_REF] Costa | Formal Models for Component Connectors[END_REF].

The simplest connectors, called primitives, consist of a number of input and output nodes to which components can connect and at which they can issue write and take requests for data items. Data items flow through a primitive from its input node(s) to its output node(s); if data flow through a node, this node fires. The semantics of a primitive specifies its behavior by describing how and when data items flow through the primitive's nodes. To illustrate this, we now present some common primitives and sketch their semantics informally.

The Sync primitive consists of an input node and an output node. Data items flow through this primitive only if these nodes have pending write and take requests. The LossySync primitive behaves similarly, but, as described in Section 1, loses a data item if its input node has a pending write request, while its output node has no pending take request. In contrast to the previous two

Sync

LossySync FIFO1 (Empty)

FIFO1 (Full) A B A B A B A B 2-Col. 3-Col.
memoryless primitives, primitives can have buffers to store data items in. Such primitives exhibit different states, while the internal configuration of Sync and LossySync always stays the same. For instance, the FIFO 1 primitive consists of an input node, an output node, and a buffer of size 1. In the EMPTY state, a write request on the input node of FIFO 1 causes a data item to flow into the buffer (i.e., the buffer becomes full), while a take request on its output node remains pending. Conversely, in the FULL state, a write request on its input node remains pending, while a take request on its output node causes a data item to flow from the buffer to the output node (i.e., the buffer becomes empty).

The first row of Table 1 depicts the three primitives discussed. In general, we define primitives as follows. Let N ode be a denumerable set of nodes.

Definition 1 (Primitive). A primitive P of arity k is a list (n j1 1 , . . . , n j k k ) such that n i ∈ N ode, j i ∈ {"i", "o"}, and

[if i = i , then n i = n i ] for all 1 ≤ i, i ≤ k.
One can construct complex connectors from simpler constituents using composition. In this view, a connector consists of a set of nodes, a set of primitives connecting these nodes, and a subset of boundary nodes on which components can perform I/O-operations. Although primitives have only boundary nodes, this generally does not hold for composed connectors. For instance, composing LossySync and FIFO 1 , by joining the former's output node with the latter's input, causes their shared node to become internal to the composed connector. This connector, called LossyFIFO 1 , appears in the top-left cell of Table 2. We proceed with the formal definitions.

Definition 2 (Connector

). A connector C is a tuple N, B, E such that N is the set of nodes occurring in C, ∅ = B ⊆ N is a set of boundary nodes, and E is a set of primitives. Definition 3 (Composition of connectors). Let C 1 = N 1 , B 1 , E 1 and C 2 = N 2 , B 2 , E 2 be connectors such that E 1 ∩ E 2 = ∅. Their composition, denoted C 1 ×C 2 , is defined as: C 1 ×C 2 = N 1 ∪N 2 , (B 1 ∪B 2 )\(B 1 ∩B 2 ), E 1 ∪E 2 .
Thus, to compose two connectors, we merge their sets of nodes, compute a new set of boundary nodes, and merge the primitives that constitute them.

LossyFIFO1

M(LossyFIFO 1 )

A B C A B C A B C 2-Col. 2-Coloring 3-Col.
Thus far, we presented only the structure of connectors; next, we focus on their behavior. More specifically, we discuss connector coloring [START_REF] Clarke | Connector colouring I: Synchronisation and context dependency[END_REF], the most relevant model to this paper, in some detail; we mention other models in Section 5. Connector coloring works by assigning colors to the nodes of a connector. These colors specify whether data items may flow at a node. For instance, when using two colors, one color expresses that data can flow at a node (i.e., the flow-color:

), while the other expresses the opposite (i.e., the no-flow color:

). We call a total map from the nodes of a connector to colors a coloring. Definition 4 (Coloring [START_REF] Clarke | Connector colouring I: Synchronisation and context dependency[END_REF]). Let N ⊆ N ode and Colors a set of colors. A coloring over N , denoted c, is a total map N → Colors. We denote c's domain by dom(c).

To model a connector's different behavior in different states, we use coloring tables. A coloring table consists of a number of colorings and corresponds to a configuration of a connector; each coloring describes one way in which nodes can fire synchronously in this configuration.

Definition 5 (Coloring table [START_REF] Clarke | Connector colouring I: Synchronisation and context dependency[END_REF]). A coloring table, denoted T , is a set of colorings with mutually equal domains, denoted dom(T ), and co-domains.

When certain nodes fire synchronously, a connector's configuration may change (e.g., a full FIFO 1 can become empty). We use next functions, which describe transitions from one coloring table to the next, to model this change.

Definition 6 (Next function [START_REF] Costa | Formal Models for Component Connectors[END_REF]). Let S be a set of coloring tables such that dom(T 1 ) = dom(T 2 ) for all T 1 , T 2 ∈ S. A next function over S, denoted η, is a map S × {dom(S) → Colors} → S in which dom(S) = [dom(T ) for any T ∈ S] is the domain of any coloring in T ∈S T .

Coloring tables that consist of 2-colorings for the previously discussed primitives appear in the third row of Table 1. For instance, the top coloring of Sync denotes the presence of flow between A and B; its bottom coloring denotes the absence of flow. The middle coloring of LossySync denotes that data items flow only at A, causing them to get lost before reaching B.

To compute the behavior of a composed connector whose constituents have coloring tables and next functions as semantic model, we use the composition operators for coloring tables and next functions. The formal definitions appear below; shortly, we discuss an example (LossySync).

Definition 7 (Composition of colorings [START_REF] Clarke | Connector colouring I: Synchronisation and context dependency[END_REF]). Let c 1 and c 2 be colorings such that c 1 (n) = c 2 (n) for all n ∈ dom(c 1 ) ∩ dom(c 2 ). Their composition, denoted c 1 ∪ c 2 , is defined as:

c 1 ∪ c 2 = n → κ n ∈ dom(c 1 ) ∪ dom(c 2 ) and κ = c 1 (n) if n ∈ dom(c 1 ) c 2 (n) otherwise
Definition 8 (Composition of coloring tables [START_REF] Clarke | Connector colouring I: Synchronisation and context dependency[END_REF]). Let T 1 and T 2 be coloring tables. Their composition, denoted T 1 • T 2 , is defined as:

T 1 • T 2 = c 1 ∪ c 2 c 1 ∈ T 1 and c 2 ∈ T 2 and c 1 (n) = c 2 (n) for all n ∈ dom(c 1 ) ∩ dom(c 2 )
Definition 9 (Composition of next functions [START_REF] Costa | Formal Models for Component Connectors[END_REF]). Let η 1 and η 2 be next functions over sets of coloring tables S 1 and S 2 , respectively, and let

S 1 * S 2 = { T 1 • T 2 | T 1 ∈ S 1 and T 2 ∈ S 2 }.
Their composition, denoted η 1 ⊗ η 2 , is defined as:

η 1 ⊗ η 2 = (T 1 • T 2 , c 1 ∪ c 2 ) → η 1 (T 1 ) • η 2 (T 2 ) T 1 • T 2 ∈ S 1 * S 2 and c 1 ∪ c 2 ∈ T 1 • T 2
The expressiveness of connector coloring depends on the instantiation of Colors in Definitions 4, 5, and 6. With two colors, we obtain 2-coloring models in which Colors = { , }. Whereas 2-coloring models can express synchronization, they cannot express context-dependency: to model contextsensitive connectors, three colors seem necessary. With three colors, we obtain 3-coloring models in which Colors = { , , }. Instead of one noflow color as in 2-coloring models, two colors to express the absence of flow exist in 3-coloring models. As a result, in 3-coloring models, one can express why data does not flow, whereas in 2-coloring models, one can express only that data does not flow. More precisely, in 3-coloring models, the direction of the arrow of the no-flow colors indicates where the reason for the absence of flow comes from. Loosely speaking, an arrow pointing in the same direction as the flow indicates that a node has no pending write requests, while an arrow pointing in the opposite direction indicates that a node has no pending take requests. In text, we associate with the former case and with the latter. We prefix "coloring" by "2-" (respectively, "3-") if Colors in Definitions 4, 5, and 6 accords with 2-coloring (respectively, 3-coloring) models.

To illustrate the previous, 3-colorings for Sync, LossySync and FIFO 1 appear in the fourth row of Table 1, and composed 2-coloring and 3-coloring tables for LossyFIFO 1 appear in the two bottom-left cells of Table 2. The middle coloring in the 2-coloring table of the empty LossyFIFO 1 describes an inadmissible behavior: if A fires, but B does not, LossySync loses a data item between Table 3. M-transformation of common primitives.

M(Sync) M(LossySync) M(FIFO1) (Empty) M(FIFO1) (Full) A B A B A B A B A B A B A B A B

2-Colouring

A and B despite the empty buffer. Such a coloring does not exist in the 3coloring table of the empty LossyFIFO 1 . Thus, 3-coloring models can capture context-dependency-through the propagation of the reason for the absence of flow-whereas 2-coloring models cannot. Finally, we define colored connectors (respectively, 2-colored, 3-colored connectors), which are connectors whose semantics are defined in terms of a coloring model (respectively, 2-coloring model, 3-coloring model), and their composition operator, which preserves well-formedness by Proposition 3.3.5 in [START_REF] Costa | Formal Models for Component Connectors[END_REF].

Definition 10 (Colored connectors).

A colored connector over a set of coloring tables S, denoted C Col , is a tuple C, η in which C = N, B, E is a connector, and η is a next function over S such that dom(S) = N .

Definition 11 (Composition of colored connectors). Let

C Col 1 = C 1 , η 1 and C Col 2 = C 2 , η 2 be colored connectors. Their composition, denoted C Col 1 ×C Col 2 , is defined as: C Col 1 × C Col 2 = C 1 × C 2 , η 1 ⊗ η 2 .
3 From Three to Two Colors

In the literature, 2-coloring models are considered not expressive enough to capture context-dependency of connectors. In this section, however, we show the converse: at the expense of making the models of the primitives more complex, we encode context-dependent behavior using only two colors (and without altering the existing composition operators for coloring models). Our encoding comprises a generic transformation from 3-colored connectors to 2-colored connectors. Essentially, we trade a more complex semantic model-i.e., 3-coloring-with simple primitives for a simpler semantic model-i.e., 2-coloring-with more complex primitives. We start by introducing our transformation operator, denoted M, which we liberally overload for different types of arguments for notational convenience. In Section 3.1, we prove the correctness of the transformation by showing that flow through nodes of a 3-colored connector C Col implies corresponding flow through its transformation M(C Col ) (a 2-colored connector); in Section 3.2, we discuss the distributivity properties-important for compositionality-of M.

We begin with the M-transformation for connectors. Informally, this transformation clones all nodes in a connector and inverts the direction of the flow through these clones. The latter facilitates the backwards propagation of the reason for the absence of flow in case the connector lacks appropriate take requests (in a similar spirit as the color). Henceforth, we call a node n of the original connector a base node and its unique clone, denoted n, a context node. Base and context nodes correspond one-to-one, and we consider them each other's duals. Next, let N be a set of base nodes. We define its Mtransformation, denoted M(N ), as M(N ) = n∈N {n, n}, that is, the set of base nodes and their duals. Finally, let inv be the inverse map of "i" and "o", that is, inv = {"i" → "o", "o" → "i"}. We can now define M for connectors, starting with a definition of M for primitives.

Definition 12 (M-transformation of primitives). Let P = (n j1 1 , . . . , n j k k ) be a primitive. Its M-transformation, denoted M(P ), is defined as:

M(P ) = n j1 1 , . . . , n j k k , n inv(j1) 1 , . . . , n inv(j k ) k . Definition 13 (M-transformation of connectors). Let C = N, B, E be a connector. Its M-transformation, denoted M(C), is defined as: M(C) = M(N ), M(B), M(E) in which M(E) = { M(P ) | P ∈ E }.
One can straightforwardly show that M for primitives yields primitives, that is, preserves well-formedness with respect to Definition 1 [START_REF] Jongmans | Encoding context-sensitivity in Reo into non-context-sensitive semantic models[END_REF]. The same holds for M for connectors (the proof uses preservation of well-formedness by M for primitives).

Proposition 1 (M-transformation of primitives and connectors preserves well-formedness). M-transforming a primitive yields a primitive. Mtransforming a connector yields a connector.

The M-transformations of Sync, LossySync, and FIFO 1 appear in the first row of Table 3, while the top-right cell of Table 2 depicts the M-transformation of LossyFIFO 1 . The figures exemplify that data flow in the opposite direction through context nodes when compared with the direction of the flow through base nodes. As mentioned before, this resembles how the 3-coloring model communicates the reason for no-flow backwards through the connector. Furthermore, context nodes nowhere communicate with base nodes: they form a context circuit that influences the behavior of the base circuit and vice versa, but data items cannot flow from one of these circuits to the other. The M-transformation of LossySync exemplifies this influence: the new dotted arrow tangent to the original dashed arrow indicates that data may disappear between A and B iff data flow through B.

To describe the behavior of M-transformed connectors, we proceed with the definition of M for colorings, coloring tables, and next functions. We first present their formal definitions, and clarify these afterwards.

Definition 14 (M-transformation of colorings). Let c be a 3-coloring. Its M-transformation, denoted M(c), is defined as:

M(c) = n∈dom(c)    { n → , n → } if c(n) = { n → , n → } if c(n) = { n → , n → } if c(n) =
Definition 15 (M-transformation of coloring tables). Let T be a 3-coloring table. Its M-transformation, denoted M(T ), is defined as:

M(T ) = { M(c) | c ∈ T }.
Definition 16 (M-transformation of next functions). Let η be a next function over a set of 3-coloring tables S. Its M-transformation, denoted M(η), is defined as:

M(η) = { (M(T ), M(c)) → M(η(T, c)) | T ∈ S and c ∈ T }.
Informally, M applied to a 3-coloring c clones its domain (similar to the way M for connectors clones nodes) and maps each node in the new domain to either or . The idea behind these mappings follows below.

-If c maps n to , M(c) also maps n to , while it maps n to . This ensures that data never flow through the same parts of the base and the context circuits synchronously. If we would allow such synchronous flow, for instance, data items could flow between the base nodes and through the context circuit of a LossySync (i.e., this LossySync has pending write and take requests) at the same time. This would mean, however, that this LossySync may lose the data item flowing through its base circuit without reason (because of the pending take request). This is inadmissible behavior.

-If c maps n to (i.e., the no-flow color indicating that n lacks take requests), M(c) maps n to (because flow cannot appear out of nowhere), while it maps n to (because the absence of pending take requests may cause lossy channels to lose data items).

-If c maps n to (i.e., the no-flow color indicating that n lacks write requests), M(c) maps n to (because flow cannot appear out of nowhere), and the same holds for n (because the absence of pending write requests may never cause loss of data).

Next, we discuss preservation of well-formedness [START_REF] Jongmans | Encoding context-sensitivity in Reo into non-context-sensitive semantic models[END_REF]. Let c be a 3-coloring. We make two observations: (i) because context nodes correspond one-to-one to base nodes, M(c) maps all nodes in M(dom(c)) exactly once, and (ii) M(c) maps all nodes in its domain to either or . Hence, M(c) defines a 2coloring over the set M(dom(c)). Well-formedness of M for 3-coloring tables then follows immediately. Finally, we argue that M for next functions preserves well-formedness; let η be a next function over a set of 3-coloring tables S. Since M for 3-colorings (respectively, 3-coloring tables) yields well-formed 2-colorings (respectively, 2-coloring tables), and since S is a set of 3-coloring tables, M(η) defines a map from [2-coloring tables and 2-colorings] to 2-coloring tables. Hence, M(η) defines a next function over a set of 2-coloring tables.

Proposition 2 (M-transformation of colorings, coloring tables, and next functions preserves well-formedness). M-transforming a 3-coloring c yields a 2-coloring over M(dom(c)). M-transforming a 3-coloring table yields a 2-coloring table. M-transforming a next function over a set of 3-coloring tables S yields a next function over a set of 2-coloring tables M(S) = { M(T ) | T ∈ S }, and dom(M(S)) = dom(M(T )) for any T ∈ S.

Finally, we present the M-transformation of colored connectors. Both the definition and its preservation of well-formedness turn out straightforwardly. To M-transform a colored connector, we take the M-transformations of its constituents; preservation of well-formedness then follows from Propositions 1 and 2.

Definition 17 (M-transformation of colored connectors). Let C Col = C, η be a colored connector over a set of 3-coloring tables. Its M-transformation, denoted M(C Col ), is defined as:

M(C Col ) = M(C), M(η) .
Proposition 3 (M-transformation of colored connectors preserves well-formedness). M-transforming a colored connector over a set of 3-colorings yields a colored connector over a set of 2-colorings.

Correctness of M

In this subsection, we show the correctness of M for colored connectors. To define "correctness" in this context, we first introduce the concept of paintings, which are, essentially, (infinite) executions of a colored connector.

Definition 18 (Painting). Let C Col = C, η be a colored connector over S and T 0 ∈ S the coloring table corresponding to its initial configuration. A painting of C Col is a sequence [T 0 , c 0 , T 1 , c 1 , . . .] such that c i ∈ T i , and T i+1 = η(T i , c i ) for all i ≥ 0. The set of all C Col 's paintings is denoted Painting(C Col ).

We call M for colored connectors correct if, for each painting of C Col , there exists a corresponding painting of M(C Col ) and vice versa; paintings correspond if, for all indexes, (i) the respective colorings assign flow to the same shared nodes-i.e., nodes that occur in both of the colored connectors-and (ii) the respective coloring tables correspond to the same configuration. We formulate our correctness theorem more formally below; a proof follows shortly.

Theorem 1 (Correctness of M). Let C Col = C, η be a colored connector over a set of 3-coloring tables S and M(C Col ) = M(C), M(η) a colored connector over a set of 2-coloring tables M(S) (by Proposition 3). Then:

i. if: [T 0 , c 0 , . . .] ∈ Painting(C Col ) then: [M(T 0 ), M(c 0 ), . . .] ∈ Painting(M(C Col )) such that for all 0 ≥ i : { n | c i (n) = } = { n ∈ dom(c i ) | (M(c i ))(n) = } ii. if: [M(T 0 ), M(c 0 ), . . .] ∈ Painting(M(C Col )) then: [T 0 , c 0 , . . .] ∈ Painting(C Col ) such that for all 0 ≥ i : { n | c i (n) = } = { n ∈ dom(c i ) | (M(c i ))(n) = }
Later, we sketch a proof by induction that establishes the theorem. For the sake of conciseness, however, we first move large parts of the inductive step to the following two lemmas. Lemma 1 states that M for next functions over 3-coloring tables preserves the flow behavior of the connector. That is, if an untransformed coloring assigns flow to some base node, the M-transformed coloring (i) exists, and (ii) also assigns flow to this base node. The same must hold in the opposite direction. Lemma 2 states that M for next functions preserves transitions from one configuration to the next. Note that these two lemmas correspond to the two conditions for "correspondence" given above. Finally, given the previous two lemmas, we sketch a proof of Theorem 1.

Proof (Of Theorem 1; Sketch). Both i. and ii. follow from induction on the length of a painting's prefix. The base case (prefix of length 1) follows from preservation of well-formedness of M for next functions (recall M(S) = { M(T ) | T ∈ S }), and because T 0 ∈ S by Definition 18. To prove the inductive step, first, suppose there exists a painting with prefix of length 2j -1 on which the theorem holds, for some j ≥ 1 (note that the (2j -1)-th element is a coloring table). Next, apply Lemma 1 to establish that there exists a painting with a prefix of length 2j on which the theorem holds (note that the (2j)-th element is a coloring). Finally, apply Lemma 2 to establish that there exists a painting with a prefix of length 2j + 1 = 2(j + 1) -1 on which the theorem holds.

Distributivity of M

Previously, we showed that by applying M to a 3-colored connector, we obtain a corresponding 2-colored connector. Though an essential result, it not yet suffices: to properly construct a complex 2-colored connector from context-dependent constituents, we still must compose a corresponding 3-colored connector from 3-colored primitives first. Only thereafter, we can apply M to obtain the desired 2-colored connector. Instead, we would prefer (i) to apply M only once to the 3-colored primitives (yielding, among others, the primitives in Table 3), and (ii) to construct context-dependent 2-colored connectors by composing these M-transformed primitives. We prefer this approach, because we speculate that an implementation of Reo that operates on 2-coloring models can compute connector composition more efficiently than an implementation that operates on 3-coloring models. In this section, we develop the theory that accommodates this: we show the compositionality of M. This means that it does not matter whether we (a) first apply M to 3-colored connectors and then the composition operator on the resulting 2-colored connectors, or (b) first apply the composition operator on 3-colored connectors and then M to the resulting composition. Specifically, we show that M distributes over composition of connectors (Definition 2) and composition of next functions (Definition 9). Distributivity over composition of colored connectors (Definition 10) then follows straightforwardly. We start, however, with a proposition stating that M for sets of nodes (defined in the second paragraph of Section 3) distributes over the set operators ∪, ∩, and \. Our complete proof [START_REF] Jongmans | Encoding context-sensitivity in Reo into non-context-sensitive semantic models[END_REF] consists of a series of straightforward applications of the definitions and the distributivity laws of these operators, while making use of the one-to-one correspondence between base and context nodes.

Proposition 4 (M for sets of nodes distributes over ∪, ∩, \ for sets). Let N 1 , N 2 ⊆ N ode be sets of nodes. Then:

M(N 1 ) ∪ M(N 2 ) = M(N 1 ∪ N 2 ), M(N 1 ) ∩ M(N 2 ) = M(N 1 ∩ N 2 ), and M(N 1 ) \ M(N 2 ) = M(N 1 \ N 2 ).
We proceed with a compositionality lemma that concerns M for connectors.

Lemma 3 (M for connectors distributes over × for connectors). Let C 1 and C 2 be connectors. Then:

M(C 1 ) × M(C 2 ) = M(C 1 × C 2 ). Proof. Suppose C 1 = N 1 , B 1 , E 1 and C 2 = N 2 , B 2 , E 2 (
without loss of generality). Applying Definition 13 of M for connectors and Definition 2 of × to rewrite the above equation, we obtain the following:

M(N 1 ) ∪ M(N 2 ), M(B 1 ) ∪ M(B 2 ) \ M(B 1 ) ∩ M(B 2 ), M(E 1 ) ∪ M(E 2 ) = M(N 1 ∪ N 2 ), M(B 1 ∪ B 2 \ B 1 ∩ B 2 ), M(E 1 ∪ E 2 ) (i) (ii) (iii)
Sub-equations (i) and (ii) follow from Proposition 4. Sub-equation (iii) holds because, by Definition 13 of M for sets of primitives:

M(E 1 ) ∪ M(E 2 ) = { M(P ) | P ∈ E 1 } ∪ { M(P ) | P ∈ E 2 } = { M(P ) | P ∈ E 1 ∪ E 2 } = M(E 1 ∪ E 2 ) = M(E 1 ∪ E 2 ).
To show that M distributes over composition of next functions, we, as before, start with a proposition. More specifically, Proposition 5 states that M distributes over composition of colorings and coloring tables. We consider our complete proofs [START_REF] Jongmans | Encoding context-sensitivity in Reo into non-context-sensitive semantic models[END_REF], though rather technical and detailed, straightforward. They rely on the following observations: (i) context nodes correspond one-to-one to base nodes, (ii) the colors assigned to a base node and its dual context node by an M-transformed 2-coloring uniquely define the color assigned to the base node by the 3-coloring (by Definition 14 of M for 3-colorings), and (iii) each context node that corresponds to a base node in the domain-intersection of two untransformed 3-colorings occurs in the domain-intersection of their M-transformations.

Proposition 5 (M for colorings and coloring tables distributes over ∪ for colorings and • for coloring tables). Let c 1 and c 2 be 3-colorings. Then, M(c 1 ) ∪ M(c 2 ) = M(c 1 ∪ c 2 ). Let T 1 and T 2 be 3-coloring tables. Then,

M(T 1 ) • M(T 2 ) = M(T 1 • T 2 ).
We proceed with a compositionality lemma that concerns M for next functions.

Lemma 4 (M for next functions distributes over ⊗ for next functions).

Let η 1 and η 2 be next functions over sets of 3-coloring tables S 1 and S 2 . Then:

M(η 1 ) ⊗ M(η 2 ) = M(η 1 ⊗ η 2 ).
Proof. Follows from Table 4.

Finally, we present the compositionality theorem of M, which states that M distributes over composition of colored connectors. As mentioned before, this result follows straightforwardly from the previous lemmas.

M(C Col 1 ) × M(C Col 2 ) = M(C Col 1 × C Col 2 ). Proof. Suppose C Col 1 = C 1 , η 1 and C Col 2 = C 2 , η 2 (

without loss of generality).

Applying Definition 17 of M for 3-colored connectors and Definition 11 of × to rewrite the above equation, we obtain the following:

M(C 1 ) × M(C 2 ), M(η 1 ) ⊗ M(η 2 ) = M(C 1 × C 2 ), M(η 1 ⊗ η 2 ) (i) (ii)
Sub-equation (i) follows immediately from Lemma 3, while sub-equation (ii) follows from Lemma 4.

Table 4.

Proof: M(η1) ⊗ M(η2) = M(η1 ⊗ η2). M(η1) ⊗ M(η2) = / * By Definition 9 of ⊗ / *    M(T1) • M(T2), M(c1) ∪ M(c2) → (M(η1))(T1, c1) • (M(η2))(T2, c2) M(T1) • M(T2) ∈ M(S1) • M(S2) and M(c1) ∪ M(c2) ∈ M(T1) • M(T2)    = / * By the distributivity of M over ∪ and • in Proposition 5 / *    M(T1 • T2), M(c1 ∪ c2) → (M(η1))(T1, c1) • (M(η2))(T2, c2) M(T1 • T2) ∈ M(S1 • S2) and M(c1 ∪ c2) ∈ M(T1 • T2)    = / * Because, by the definition of M(S) in Proposition 2, M(T ) ∈ M(S) iff T ∈ S,
and because, by Definition 15 of M for 3-coloring tables,

M(c) ∈ M(T ) iff c ∈ T / *    M(T1 • T2), M(c1 ∪ c2) → (M(η1))(T1, c1) • (M(η2))(T2, c2) T1 • T2 ∈ S1 • S2 and c1 ∪ c2 ∈ T1 • T2    = / * Because, by Definition 16 of M for next functions, (M(η1))(T1, c1) = M(η1(T1, c1)) and (M(η2))(T2, c2) = M(η1(T2, c2)) / *    M(T1 • T2), M(c1 ∪ c2) → M(η1(T1, c1)) • M(η2(T2, c2)) T1 • T2 ∈ S1 • S2 and c1 ∪ c2 ∈ T1 • T2    = / * By the distributivity of M over • in Proposition 5 / * M(T1 • T2), M(c1 ∪ c2) → M(η1(T1, c1) • η2(T2, c2)) T1 • T2 ∈ S1 • S2 and c1 ∪ c2 ∈ T1 • T2 = / * By Definition 16 of M for next functions, / * M T1 • T2, c1 ∪ c2 → η1(T1, c1) • η2(T2, c2) T1 • T2 ∈ S1 • S2 and c1 ∪ c2 ∈ T1 • T2 = / * By Definition 9 of ⊗ / * M(η1 ⊗ η2)

Application: Context-Dependency in Vereofy

As an application, we present an implementation of our encoding in a constraint automata based model checker, which is considered as not expressive enough for the verification of context-dependent connectors. Specifically, we extend the Vereofy [START_REF] Baier | Formal verification for components and connectors[END_REF] model checking tool for the analysis of Reo connectors, developed at the TU of Dresden. 3 Vereofy uses two input languages: the Reo Scripting Language (a textual version of Reo) and the guarded command language CARML (a textual version of constraint automata). Vereofy allows the verification of temporal properties expressed in LTL and CTL-like logics and supports bisimulation equivalence checks. Moreover, it can generate counterexamples and provides a GUI integration with the Eclipse Coordination Tools (ECT). Vereofy operates on constraint automata and, thus, does not natively support context-dependent behavior. However, in the previous section, we showed that we can transform 3-colored connectors to 2-colored connectors, while preserving their context-sensitive semantics. Moreover, 2-coloring models and constraint automata correspond to each other (informal arguments appear in [START_REF] Clarke | Connector colouring I: Synchronisation and context dependency[END_REF][START_REF] Costa | Formal Models for Component Connectors[END_REF], while [START_REF] Jongmans | Encoding context-sensitivity in Reo into non-context-sensitive semantic models[END_REF] contains a formal account). Hence, by using the M-transformation, we can construct context-dependent constraint automata as follows. First, we transform the 3-colored primitives to context-dependent 2-colored primitives. Next, we compute the constraint automata corresponding to the resulting 2-colored primitives. Note that the resulting automata can have context-sensitive behavior (because the 2-colored primitives to which they correspond can have such behavior). Finally, we compose the resulting constraint automata to form more complex context-sensitive connectors (possible due to Theorem 2). Although simple and straightforward, this recipe enables the analysis of context-sensitive connectors in Vereofy. For this purpose, we have adapted Vereofy's library of built-in primitives: using the M-transformation, we wrote a new library containing context-dependent versions of the basic Reo primitives. 5 As an example, Figure 1 depicts a listing of the non-deterministic and the context-dependent versions of the LossyFIFO 1 example, and two constraint automata generated from them using Vereofy. For simplicity, we have hidden the internal node M , used a singleton set as data domain, and removed all data constraints in the generated automata. The constraint automata on the left and right correspond to the non-deterministic and the context-dependent versions, respectively. The latter uses our new context-dependent primitives. The crucial difference between the two is that the non-deterministic version contains an illegal transition via port A in the EMPTY state. This corresponds to the connector losing a data item in a situation where the FIFO 1 buffer is empty and should, in any case, accept the data item. In the context-sensitive version, however, this illegal transition does not exists. (Note that if we hide all context nodes-i.e., disregard all gray transitions in Figure 1-we obtain the non-deterministic automaton without the illegal transition.) A more complex example concerns SyncFIFO 1 , a connector with an input node, an output node, and a buffer of size 1. SyncFIFO 1 behaves identically to FIFO 1 , except for the case in which it has an empty buffer and pending I/Orequests on both of its nodes: then, SyncFIFO 1 routes a data item from its input node past its buffer to its output node in one atomic step (thus behaving as a Sync). Instead of modeling SyncFIFO 1 as a primitive without inner structure, we can construct it by composing other primitives as depicted in Figure 2 (left); for reasons of space, we do not discuss the interaction and characteristics of the primitives involved in this composition (more details appear in [START_REF] Jongmans | Encoding context-sensitivity in Reo into non-context-sensitive semantic models[END_REF]).

A first attempt to model SyncFIFO 1 using our library of context-sensitive primitives failed due to the presence of causality loops in the resulting composition. 6 Since one cannot detect and remove causality loops from constraint automata, we removed the colorings that contain causality loops from the composed 3-coloring model of SyncFIFO 1 and, afterwards, applied M to this filtered model. This process yielded a 2-coloring model, whose equivalent constraint automaton we encoded in CARML. In Figure 2, we depict the constraint automaton resulting from the procedure just sketched (bottom-right). Additionally, we depict the constraint automaton that one obtains when composing the ordinary primitives (top-right) instead of the context-sensitive ones. (As before, we hide internal nodes.) At first sight, these automata seem very similar. In fact, if we hide all context nodes in the context-dependent constraint automaton-i.e., disregard its gray transitions-we obtain two identical automata.

The crux of the difference between the two automata, therefore, lies exactly in these context nodes: in contrast to LossyFIFO 1 , SyncFIFO 1 itself exhibits context-dependent behavior (instead of only the primitives that constitute it, namely LossySync). Recall that in the EMPTY state, if output node B lacks a take request, a write request on A causes a data item to flow into the buffer. However, if B has a pending take request, a write request on A causes a data item to flow immediately to node B. The ordinary constraint automaton of Sync-FIFO 1 does not capture this difference, which means that an implementation of this constraint automaton would non-deterministically choose one of these two options in case of a pending write request on A and a pending take request on B. In contrast, an implementation of the context-dependent constraint automaton of SyncFIFO 1 always chooses the appropriate option, because in the absence of a take requests on B, data items with irrelevant content-i.e., signals-flow through B. To illustrate this, we encourage the interested reader to compose SyncFIFO 1 and FIFO 1 in the same way we composed LossySync and FIFO 1 . 7

Related Work

In [START_REF] Arbab | A coinductive calculus of component connectors[END_REF], Arbab et al. introduce a coalgebra-based semantic model-the first-for Reo. Some years later, in [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF], Baier et al. present an automaton-based approach, namely constraint automata (CA), and prove correspondences with the coalgebra-based model. In [START_REF] Clarke | Connector colouring I: Synchronisation and context dependency[END_REF], however, Clarke et al. observe that neither of these models can handle context-sensitivity, and they introduce the 2-coloring and 3-coloring models to mend this deficiency. Since then, other semantic models with the same aim have come to existence. In [START_REF] Costa | Formal Models for Component Connectors[END_REF], Costa introduces intentional automata (IA) as an operational model with constructs for context-dependency. Unlike CA, whose states correspond one-to-one to the internal configurations of connectors, IA have more states than the connectors they model; each state of an IA contains information about not only the configuration of the connector, but also about the nodes that intend to fire (i.e., with a pending I/O-request). Similarly, transition-labels consist of two sets of nodes: those that intend to fire, and those that actually fire. By maintaining information about I/O-request on nodes, IA capture context-dependency. The number of states, however, quickly grows large, whereas our approach yields succinct CA. In [START_REF] Bonsangue | Automata for context-dependent connectors[END_REF], Bonsangue et al. introduce guarded automata (GA) as another automaton-based model for capturing context-dependency. Like CA, the states of GA correspond one-to-one to the configurations of connectors, which makes them significantly more compact than IA. To encode context-sensitivity, every transition-label of a GA consists 7 The constraint automaton that results from composing the ordinary constraint automata of SyncFIFO1 and FIFO1 includes a transition that describes an inadmissible behavior in which, in case both SyncFIFO1 and FIFO1 have empty buffers, the input node of SyncFIFO1 fires and causes its own buffer to become full (while the buffer of FIFO1 remains empty). The constraint automaton that results from composing the context-dependent constraint automata of SyncFIFO1 and FIFO1, in contrast, does not include such a transition: if the input node of SyncFIFO1 fires when both SyncFIFO1 and FIFO1 have empty buffers, the buffer of FIFO1 becomes full (while the buffer of SyncFIFO1 remains empty).

of a guard and a string. Together, they express which nodes can fire (the string), given the presence and absence of requests at certain nodes (the guard). Guarded automata seem very similar to the CA we obtain with our approach: instead of guards that contain negative occurrences of (base) nodes to specify that these nodes have no pending I/O-requests, we make these negative occurrences explicit with the introduction of (flow through) context nodes. Besides Vereofy, other approaches to model checking Reo connectors exist. In [START_REF] Kokash | Verification of context-dependent channelbased service models[END_REF], Kokash et al. employ the mCRL2 toolset, developed at the TU of Eindhoven, for model checking connectors, combined with a translation tool that automatically generates mCRL2 specifications from graphical models of Reo connectors. The tool's original algorithm operated on constraint automata, making it impossible to verify context-dependent connectors using this approach. Later, however, Kokash et al. incorporated (3-)coloring information in the tool, thus facilitating verification of context-dependent connectors. This advantage of mCRL2 over Vereofy, which could not handle context-dependent connectors up to now, seems no longer valid as we have shown how to encode contextsensitivity in Vereofy. An advantage of Vereofy over mCRL2, on the other hand, is its ability to generate counterexamples, which mCRL2 cannot do. In [START_REF] Kemper | SAT-based verification for timed component connectors[END_REF], Kemper introduces a SAT-based approach to model checking timed constraint automata (TCA). In her work, Kemper represents TCA as formulas in propositional logic and uses existing SAT solvers for verification. This approach allows for model checking timed properties of Reo connectors, but it cannot handle context-dependency. In [START_REF] Mousavi | Formal semantics and analysis of component connectors in Reo[END_REF], Mousavi et al. develop a structural operational semantics in Plotkin's style for Reo, encode this semantics in the Maude termrewriting language, and use Maude's LTL model checking module to verify Reo connectors. In [START_REF] Khosravi | Modeling and analysis of Reo connectors using Alloy[END_REF], Khosravi et al. introduce a mapping from Reo to Alloy, a modeling language based on first-order relational logic, and apply the Alloy Analyzer for verification. Although the approach can handle some contextdependent connectors-using a maximal progress rule that removes undesired behavior-Khosravi et al. admit to have considerable performance issues.

Conclusions and Future Work

We showed how to encode context-sensitivity in the 2-coloring model and constraint automata by adding fictitious nodes to primitives, while both these models are considered incapable of capturing context-dependent behavior. Our approach, constituted by the M-transformation, enables the application of tools and algorithms devised for such simpler semantic models to context-dependent connectors. As an example, we demonstrated how Vereofy can model check context-sensitive connectors, which seemed impossible up to now.

With respect to future work, we would like to investigate whether Reo's implementation can benefit from the results presented in this paper. We speculate that algorithms for the computation of connector composition run faster on Mtransformed 2-colored connectors (or their corresponding constraint automata) than on the original 3-colored connectors, because of the simpler semantic model. Furthermore, we would like to study the relation between other formalisms for Reo that facilitate the proper modeling of context-dependent behavior (e.g., intentional automata and guarded automata).

Lemma 1 (

 1 M for colored next functions preserves flow). Let η be a next function over a set of 3-coloring tables S, let M(η) be its M-transformation, that is, a next function over a set of 2-coloring tables M(S) (by Proposition 2), and let n ∈ dom(S) be a node. Then:T ∈ S and c ∈ T and c(n) = iff M(T ) ∈ M(S) and M(c) ∈ M(T ) and (M(c))(n) =Proof. We first prove the left-to-right direction ( only if), and proceed with the right-to-left direction ( if). only if -We start by deriving the first two conjuncts of the right-hand side (RHS) from the first two conjuncts of the left-hand side (LHS). This turns out straightforwardly: T ∈ S implies M(T ) ∈ M(S) by the definition of M(S) in Proposition 2, and c ∈ T implies M(c) ∈ M(T ) by Definition 15 of M for 3-coloring tables. Finally, we derive the RHS's third conjunct from the third conjunct of the LHS. By the premise, c(n) = . Then, by Definition 14 of M for 3-colorings, { n → , n → } ⊆ M(c). Hence, (M(c))(n) = . if -The first two conjuncts of the LHS follow from the first two conjuncts of the RHS similar to the only if case. Next, by the premise, (M(c))(n) = , that is, n → ∈ M(c). By Definition 14 of M for 3-colorings, this happens only if c(n) = . Lemma 2 (M for colored next functions preserves transitions). Let η be a next function over a set of 3-coloring tables S, let M(η) be its Mtransformation, that is, a next function over a set of 2-coloring tables M(S) (by Proposition 2), and let n ∈ dom(S) be a node. Then: T, T ∈ S and c ∈ T and η(T, c) = T iff M(T ), M(T ) ∈ M(S) and M(c) ∈ M(T ) and (M(η))(M(T ), M(c)) = M(T ) Proof. The implication, in both directions, follows from the definition of M(S) in Proposition 2 (first conjunct), Definition 15 of M for 3-coloring tables (second conjunct), and Definition 16 of M for next functions (third conjunct).

Theorem 2 (

 2 Compositionality of M). Let C Col 1 and C Col 2 be colored connectors over sets of 3-coloring tables. Then:

4 1 8 #Fig. 1 .

 481 Fig. 1. Non-deterministic (left) vs. context-dependent (right) LossyFIFO1 in Vereofy.

5Fig. 2 .

 2 Fig. 2. SyncFIFO1: its composition (left), its ordinary constraint automaton (topright), and its context-dependent constraint automaton (bottom-right).

Table 1 .

 1 Common primitives.

Table 2 .

 2 Empty LossyFIFO1 and its M-transformation.

Vereofy homepage: http://www.vereofy.de

ECT homepage: http://reo.project.cwi.nl

Causality loops may occur if a composed connector has one or more circular subcircuits (as in the case of SyncFIFO1) and can cause, among other anomalous phenomena, a reason for the absence of flow to appear out of nowhere. Colorings that contain causality loops, therefore, describe inadmissible behavior. In[START_REF] Costa | Formal Models for Component Connectors[END_REF], Costa proposes an algorithm for the detection of colorings that contain causality loops.

Acknowledgments We are grateful to the Vereofy team for their support.

Supported by the research school in 'Service-Oriented Systems Engineering' at HPI


Seiji Umatani
email: umatani@kuis.kyoto-u.ac.jp

Masahiro Yasugi
email: yasugi@kuis.kyoto-u.ac.jp

Taiichi Yuasa
email: yuasa@kuis.kyoto-u.ac.jp

Abstract Machines for Safe Ambients in Wide-Area and Mobile Networks

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

In recent years, core calculi based on distribution and mobility have been studied extensively, and they are regarded as fundamental models for many programming languages supporting code migration.

The Ambient Calculus (AC) [START_REF] Cardelli | Mobile Ambients[END_REF] is a distributed process calculus with a notion of locations that are known as ambients. Each process belongs to an ambient, and each ambient, except for the topmost ambient, belongs to another ambient. Thus, the ambients form a hierarchical structure, and every process belongs somewhere in the hierarchy. In AC, computation is represented as the combination of three types of primitive operations of ambients-in, which instructs an ambient to enter another ambient; out, which instructs an ambient to exit from another ambient; and open, which provides a way to dissolve the membrane of an ambient so that the content of the ambient can be accessed.

To realize practical programming language systems adaptable to a broad range of heterogeneous distributed and mobile networks, we can adopt AC as the core language of such systems. Several studies have been carried out on the distributed implementation of Ambient-like calculi [START_REF] Cardelli | Mobile Ambient Synchronization[END_REF][START_REF] Fournet | An Asynchronous, Distributed Implementation of Mobile Ambients[END_REF][START_REF] Sangiorgi | A Distributed Abstract Machine for Safe Ambients[END_REF][START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF][START_REF] Phillips | A Distributed Abstract Machine for Boxed Ambient Calculi[END_REF][START_REF] Schmitt | An Abstract Machine for the Kell Calculus[END_REF]. Among these, Pan [START_REF] Sangiorgi | A Distributed Abstract Machine for Safe Ambients[END_REF][START_REF] Giannini | Safe Ambients: Abstract Machine and Distributed Implementation[END_REF] and GcPan [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF][START_REF] Hirschkoff | An efficient abstract machine for Safe Ambients[END_REF] are abstract machines for implementing the Safe Ambients (SA), a variant of AC, in distributed settings.

The implementation technique of Pan and GcPan is simple; it separates the logical distribution of ambients, which is given by the hierarchical structure of ambients, from their physical distribution, which is a mapping from each ambient to a certain computer on which the ambient is running. Pan and GcPan exploit this separation to defer physical movements of an ambient that executes some in or out moves, until the ambient is opened by the target ambient so that it can access the contents of the target ambient, such as files. This implementation technique may eliminate unnecessary communications caused by physical movements, which are typically much more expensive than simple data communications. In particular, when an ambient moves to its target ambient through multiple moves and accesses the contents of the target, physical movements corresponding to intermediate moves could be eliminated entirely. Moreover, if the moving ambient does not access any content of the target, there is no need for physical code migration.

This technique of Pan and GcPan requires all-to-all and permanent connectivity of the underlying network; that is, it assumes that any computer in the network can directly communicate with the other computers at any moment. In particular, the computer to which an ambient has moved through (possibly) multiple in and out moves must be able to communicate with the computer in which the ambient physically resides when the ambient is opened. An ambient may move to any target ambient; hence, any computer can become the target location. Therefore, any computer must be able to communicate with the other computers.

Clearly, the above requirement is not desirable for wide-area distributed environments which consist of several local-area networks or for mobile networks in which mobile devices such as smartphones may be disconnected temporarily or permanently at any moment. Furthermore, deferring the movement of an ambient is not desirable if we want the ambient to move only for using the CPU power of remote computers.

In this paper, we propose novel abstract machines Pan mov , GcPan mov , and GcPan shift for SA in order to support such wide-area and mobile networks. The main ideas of the proposed technique are as follows:

1. We model a wide-area network as a set of network domains, each of which is isolated from other network domains by network boundaries. Computers within a particular network domain can directly communicate with each other. We extend SA's ambient creation construct M [P ], where M is the name of a created ambient and P is its content, to make it clear whether the created ambient belongs to the same network domain as its parent or not; if not, there exists a network boundary between them. 2. We modify the implementation of in and out moves so that an ambient physically moves to the target ambient as soon as the ambient performs a cross-boundary movement. When physical movement of an ambient is performed in Pan (and also in our machines), a special agent called forwarder is created at the original location of the ambient; after that, all messages sent to the ambient from its children are transferred via this forwarder. Thus, our technique guarantees that the content of an opened ambient can always be sent to its parent through a chain of forwarders even if the ambient and its parent belong to different network domains.

The proposed technique is based on the Pan abstract machine. In particular, movements within a single network domain are processed in the same way as they are in Pan. Thus, no physical code migration is performed unless some open action or some cross-boundary movement is executed.

In the proposed abstract machine, every cross-boundary movement causes physical code migration; hence, it requires the creation of more forwarders than Pan, wherein all movements are considered as non cross-boundary movements. Although such an increase of forwarders is inevitable in wide-area networks with boundaries, keeping unused forwarders (i.e., forwarders with no child) alive is a waste of computer resources. Therefore, we have refined the proposed abstract machine so that it can collect and reuse the resources assigned for unused forwarders in the same way as GcPan. Furthermore, to reduce the number of forwarders in use and to prevent erratic behavior related to failures in network communication, the proposed abstract machine relocates ambients that use forwarders so that they can directly send messages to their parents.

We provide a formal description of the proposed machine and we prove its correctness by establishing a bisimilarity between it and Pan. In the formal description, the underlying protocols for implementing ambient (co)capabilities follow the formalization method of Pan. In terms of the correctness of the proposed machine and reusability of the real implementations of Pan (and GcPan), the fact that the proposed machine is a smooth extension of Pan is advantageous.

Cross-boundary communication and code migration are common features of recent distributed systems; hence, we believe that the proposed ideas and techniques can be adapted to such systems.

The remainder of this paper is organized as follows. In Section 2, we provide a brief explanation of SA and Pan. Next, in Section 3, we describe the proposed base abstract machine Pan mov , which does not perform garbage collection. In Section 4, we explain how one of the refined abstract machines, GcPan mov , reduces the resource usage of the underlying computers. In Section 5, we explain how another refined machine, GcPan shift , further reduces the resource usage and improves the fault tolerance of user programs. In Section 6, we prove the correctness of Pan mov . Finally, in Section 7, we provide concluding remarks.

Background

Safe Ambients

Safe Ambients (SA) are ambients that are designed to prevent unintended interference among ambients; whenever an ambient executes some movement action, the target ambient of the movement must execute the corresponding coaction. Thus, the timing of each movement can be controlled by the target ambient, and no unintended interference occurs.

The kinds of processes in SA are the same as those in the original Ambient calculus [START_REF] Cardelli | Mobile Ambients[END_REF]: P 1 | P 2 for parallel composition, (νn)P for restriction, M.P for action prefix, M [P ] for ambient creation, M and (x)P for local communication, and X and rec X.P for recursive processes. The characteristic of SA is found in the existence of coactions in M :

M ::= x | n | in M | in M | out M | out M | open M | open M
where each action (in, out, and open) must be executed along with the corresponding coaction (in, out, and open, respectively). The following are the reduction rules that define the behavior of basic actions in SA processes:

[R-Msg] M | (x)P -→ P {M/x} [R-In] m[in n.P 1 | P 2 ] | n[in n.Q 1 | Q 2 ] -→ n[ m[P 1 | P 2 ] | Q 1 | Q 2 ] [R-Out] m[ n[out m.P 1 | P 2 ] | out m.Q 1 | Q 2 ] -→ n[P 1 | P 2 ] | m[Q 1 | Q 2 ] [R-Open] open n.P | n[open n.Q 1 | Q 2 ] -→ P | Q 1 | Q 2

Pan Abstract Machine

To express how SA can be executed in a network of computers, the Pan abstract machine consists of a flat network of located agents. Intuitively, a located agent h : n[P ] k represents an ambient n whose content process is P , where h is the physical location of n and k is the physical location of its parent ambient. Thus, for example, the logical hierarchical structure of the SA process a

[b[P |c[Q]]|R] is represented by the parallel composition h 1 : a[R] root h 2 : b[P ] h1 h 3 : c[Q] h2
in Pan. Note that ambients in Pan do not need to know the locations of their children. This is because the existence of coactions in SA guarantees that an interaction among ambients is always triggered by a child ambient using an upward request message to its parent, as described below. The precise syntax of Pan is a subset of that of Pan mov , which is given in Section 3.2. The basic actions of SA are simulated in Pan using interactions among ambients, as shown in Figure 1. In the figure, the white boxes represent located agents, and the lines between them represent parent-child relations. The arrows denote messages between them. In Figure 1 (b), for instance, the ambient a, which performs out b.P , sends a request message {out} to b. If b contains an unguarded process out b.Q, these action/coaction match in b, and b sends back to a a completion message {go c}. When a receives the completion message, it updates its parent location with the location of c. The in action is simulated in a similar manner, as shown in Figure 1 (a). It should be noted that these simulations do not change the physical location of a; they update only the local information about the parent location of a, whereas a remains at the same location. On the other hand, in Figure 1 (c), when the ambient a, which performs a open coaction, receives the corresponding completion message {migrate}, it further sends back to b the completion message {register P }, which registers P , the code of a's local processes, into b. This incurs the physical migration of P . After sending the {register P } message, the ambient a becomes a forwarder (depicted as a triangle in the figure), whose role is to transfer messages from its children to b. Such a forwarder is necessary because b cannot access its children; therefore it cannot inform them to send their requests to b instead of a. In the remainder of this paper, we use the textual notation {P } to denote a forwarder. For instance, the final state of Figure 1

(c) is represented as b[ { . . . } ].
By deferring physical code migration until the containing ambient is opened, these simulations eliminate many unnecessary network messages. However, the simulations described above have a serious disadvantage in wide-area distributed environments with network boundaries. A set of in and out moves of an ambient running on a certain computer may logically move into another ambient running on a different computer. If these computers belong to different network domains and if they cannot communicate directly, the former ambient can no longer send messages to its parent, i.e., to the latter ambient, whereas Pan assumes that every computer can communicate directly with any other computers. Consider, for instance, the following code representing the firewalls of two LANs as two sibling ambients f and g:

r[ f[ out f | a[ out f.in g.open a | P ] ] | g[ in g.open a ] ]
where ambients within f cannot communicate with g directly. After a performs out f.in g, it is logically placed in g, whereas it physically remains within f. Then, an attempt to send a message {open} fails. In such a case, the {open} and the following {register P } messages should be transmitted via r, that is, via the path through which a moved.

Furthermore, suppose g is a mobile device that becomes disconnected before it performs open a. Since the code P is not yet delivered to g, some intended behavior of g in P is lost. (This problem is further discussed in Section 5.)

In summary, Pan's assumption of all-to-all and permanent connectivity among computers is not practical in contemporary wide-area and mobile networks; therefore, an alternative technique is required to express ambient movements.

Pan mov : Chaining Forwarders upon Movement

In this section, we propose a novel abstract machine Pan mov , which solves the problem of Pan described in the previous section.

Basic Idea

Pan mov solves the problem using two ideas: [START_REF] Cardelli | Mobile Ambient Synchronization[END_REF] to specify boundaries between network domains, we slightly extend SA's ambient creation construct, and (2) upon each cross-boundary in or out move of an ambient, Pan mov physically moves the ambient into the destination network domain. These ideas are explained in detail below.

Ambient creation with split prefix

To handle network boundaries properly, if a new ambient is created in a different network domain from the domain in which the creating ambient resides, Pan mov places a special kind of forwarder called boundary forwarder between them; that is, the parent of the created ambient is the boundary forwarder, and the parent of the boundary forwarder is the creating ambient. The need for a boundary forwarder at each ambient creation could be automatically determined by an actual implementation if the topology of the underlying network is given, for example, as an external configuration file. However, in this paper, to simplify the formal definition of Pan mov , each ambient creation involving the creation of a boundary forwarder is prefixed with the keyword split (e.g., split a[P ]). If a programmer writes an SA program with split prefixes in accordance with the topology, the program could be executed without any external configuration file. Similarly, a boundary forwarder is placed between each mobile device and its infrastructure.

Besides performing the normal task of forwarding messages, boundary forwarders play several roles in Pan mov , as described below. To distinguish a boundary forwarder from a normal forwarder, we denote the former as • and the latter as • . Sometimes, we simply denote the latter as .

Physical migration upon in and out

In Pan mov , physical migration of ambients upon cross-boundary movements is achieved with a mechanism that is similar to that of Pan with which it performs open actions. The mechanism involves the following steps:

1. If a request message crosses a boundary, the corresponding boundary forwarder marks it with a special tag. 2. When an ambient receives a request message marked with the special tag, it creates an empty clone of the requesting ambient at that location.

3. The receiving ambient sends back to the requesting ambient the {migrate} message, which indicates code migration into the clone. 4. When the requesting ambient receives the {migrate} message, it sends back the {register P } message containing its content, and then, it becomes a forwarder, as in the case of open action.

Following these steps, whenever an ambient moves, a forwarder is created at its original location. Then, even if the ambient repeats several movements, the chain of created forwarders constitutes the path from the original location to the final destination along which all messages sent from its children can always be transmitted.

Note that the physical migration of a moving ambient is performed only when its request message crosses a network boundary. In other words, every movement of an ambient within a single network domain is treated as it is in Pan; hence, physical migration is deferred until it is opened later.

If a request message has crossed a network boundary, the {migrate} message of step 3 and the {register P } message of step 4 must also cross the network boundary. Moreover, at step 4, the requesting ambient cannot send the {register P } message via the boundary forwarder of step 1, which forwards request messages to the parent, because the destination of the {register P } message is not the parent, but its own clone. To remedy these difficulties, the boundary forwarder creates, at step 1, a seed of a boundary forwarder, denoted by •. The {migrate} message sent back from the parent ambient is transmitted backward by this seed. Furthermore, after transmitting the {migrate} message, the seed becomes a new boundary forwarder targeting the appropriate location. For instance, consider the following code:

root[ a[ out a.P | • { b[ out a.Q | c[ R ] ] | S } ] ]
When b's {out} message arrives at a via the boundary forwarder, the state changes to:

root[ a[ P | • | • { b[ Q | c[ R ] ] | S} ] ]
Then, when a's {migrate} message arrives at b via the seed, the state changes to:

root[ a[ P ] | b [ • { b[ Q | c[ R ] ] } ] | • { S } ] ]
where the seed becomes the boundary forwarder targeting b , the clone of b. Finally, b's {register} message is correctly sent to b via the new boundary forwarder, and the state becomes:

root[ a[ P ] | b [ Q | • { • { c[ R ] } } ] | • { S } ] ]
Note that this new boundary forwarder continues to work for its children after these transitions; in the code stated above, all messages from c are forwarded by it.

In the mechanism described above, there is another subtle difficulty at step 2. If a request message is {out}, or if it is {in} without the special tag (i.e., the message did not cross any boundaries), a clone may be allocated at the same domain as the receiving ambient. On the other hand, if the message is {in} marked with the special tag, a clone must be allocated at the same domain as the ambient that sends the {in} message. For instance, in the code:

root[ a[ in c.P | b[ Q ] ] | • { c[ in c.R ] } ]
the clone of a must be created below the boundary forwarder. Here, c cannot predict whether its {in} message crosses any boundary forwarder when it emits the message; hence, the creation of the clone of a in advance by c is inadequate. Therefore, in Pan mov , the clone is created by the boundary forwarder when it receives the completion message from root. In the proposed execution model, the boundary forwarder belongs to both network domains; hence, it can create the clone within the domain below itself. As an alternative, it would be possible to create the clone when the {in} message arrives at the boundary forwarder. However, if no ambient executes the corresponding in action, the created clone will become unnecessary; this is undesirable.

After the movement, the state finally becomes:

root[ • { c[ R | a [ P | • { • { b[ Q ] } } ] ] } ]
The newly created boundary forwarder on the right represents the same network boundary as that on the left; however, it forwards messages in the opposite direction.

Formal Definition

In this section, we formalize the proposed abstract machine Pan mov by the set of reduction rules for network configurations. The definition method basically follows that of Pan [START_REF] Sangiorgi | A Distributed Abstract Machine for Safe Ambients[END_REF]. First, a network configuration of Pan mov is represented using the following syntax: Nets

A ::= 0 | Agent | Msg | A 1 A 2 | (νp)A Agent ::= h : n[P ] k | h B k | h • k, B ::= • | • where n ∈ Names, h, k ∈ Locations,

Messages

Msg

::= ↑ k h {Req} | ↑ h {Compl }, Req ::= R | • R R ::= in n, m | in n, h | out n, m | open n Compl ::= go h | OKin | migrate h | register P | new n, k | • Cin n, m, h, k | • Cout n, h ↑ k h {Req}
::= 0 | P 1 | P 2 | (νn)P | M.P | M [P ] | split M [P ] | M | (x)P | X | rec X.P | wait.P | ↑ h {Req} M ::= x | n | in M | in M | out M | out M | open M | open M
The syntax of the processes is nearly similar to that of SA; the three additional constructs are a cross-boundary ambient creation, split M [P ], a process waiting for the arrival of any message, wait.P , and a request message arriving at its destination ambient, ↑ h {Req}.

The operational semantics of Pan mov is defined as the reduction relation -→ between network configurations. In addition, to express process-level reductions, we use another form of reduction relation,

P k -→ n:h Q Msg, to indicate that
a process P , local to an ambient n that is located at h, and whose parent is located at k, becomes Q, and the message Msg is emitted as a side effect. First, the inference rules for -→ are defined as follows: Inference rules

[Proc-Agent] P k -→ h:n P M Q has no unguarded ambient h : n[P | Q] k -→ h : n[P | Q] k M [Par-Agent] A 1 -→ A 1 A 1 A 2 -→ A 1 A 2 [Res-Agent] A -→ A (νp)A -→ (νp)A [Struct-Cong] A ≡ A A -→ A A ≡ A A -→ A
The rule [Proc-Agent] embeds a process-level reduction step into -→. The side condition about Q ensures that all child ambients of n are activated before any local process-level reduction occurs. The remaining rules are straightforward inference rules about contexts and structural congruence. The definition of structural congruence ≡ is mostly standard; hence, it is omitted.

The other axiomatic rules are classified into six categories according to the stages of ambient interactions. In these rules, when some fields or variables are unimportant, we replace them with -.

Creation

[New-Locamb] h : m[n[P ] | Q] k -→ h : m[Q] k (νl)(l : n[P ] h ), l ∈ FL(P ) [New-Locamb ] h : m[split n[P ] | Q] k -→ h : m[Q] k (νl)(l • h (νl )(l : n[P ] l )), l, l ∈ FL(P ) [New-Res] h : m[(νn)P ] k -→ (νn)(h : m[P ] k ), m = n
In [New-Locamb], an ambient n is created at the fresh location l, whose parent is located at h. In [New-Locamb ], a new boundary forwarder is also created and inserted between m and n. [New-Res] creates a globally unique name for each name restriction.

Emission of request messages

[Req-In] in m.P k -→ h:n wait.P ↑ k h {in m, n} [Req-Coin] in n.P k -→ h:n wait.P ↑ k h {in n, h} [Req-Out] out m.P k -→ h:n wait.P ↑ k h {out m, n} [Req-Coopen] open n.P k -→ h:n wait.P ↑ k h {open n}
These rules are straightforward. For each action or coaction listed above, an ambient sends the corresponding request message to its parent at k. The name n of the requesting ambient is included in the {in} and {out} message so that it can be used for creating a clone of the ambient if the request crosses a boundary. Note that every single-threaded (ST) ambient that sends a request message to its parent simply blocks waiting for any completion message to be sent back from the parent. This fairly simplifies the execution of processes within each ambient.

Transmission of request messages

[Fw-Req] h • k ↑ h l {Req} -→ h • k ↑ k l {Req} [BFw-Req] h • k ↑ h l { -R} -→ h • k (νh )(h • l ↑ k h { • R}) [Loc-Rcv] h : n[P ] k ↑ h l {Req} -→ h : n[P | ↑ l {Req}] k
In [Fw-Req], if a request message reaches a normal forwarder, it is forwarded to k by this normal forwarder. Note that the source location of the message remains l so that the corresponding completion message can be directly sent back to l at the next stage. In [BFw-Req], if a request message reaches a boundary forwarder, it is forwarded to k after being marked with special tag •. Furthermore, the source location of the messages is replaced by the fresh location h , where a new seed attached with l is created so that the corresponding completion message can be sent back via this seed. In [Loc-Rcv], when a request message reaches its destination, it is brought into the destination.

In [Back-New], the condition k = l implies that the agent at l is not the ambient that requested in; it is another boundary forwarder. Thus, the seed simply forwards the {new} message to l, and then, it becomes the boundary forwarder in preparation for the {register} message sent from elsewhere. This boundary forwarder must forward it to l because the new clone will be created beyond l.

In [Back-New ], when a {new} message eventually reaches the same network domain as the ambient that requested in at l, a clone is created at the fresh location k and the seed at h becomes the boundary forwarder targeting k. Furthermore, an OKin message, which notifies the match of in, is sent to l.

Consumption of completion messages

[Compl-Parent] ↑ h {go k} h : n[P | wait.Q] --→ h : n[P | Q] k [Compl-Coin] ↑ h {OKin} h : n[P | wait.Q] k -→ h : n[P | Q] k [Compl-Cin] ↑ h { • Cin -, m, l, l } h : n[P | wait.Q] k -→ h : n[P | Q] k (νh )(h : m[wait.0] l ↑ l {migrate h }) ↑ l {OKin} [Compl-Cout] ↑ h { • Cout m, l} h : n[P | wait.Q] k -→ h : n[P | Q] k (νh )(h : m[wait.0] k ↑ l {migrate h }) [Compl-Migr] ↑ h {migrate k} h : n[P | wait.Q] --→ h • k ↑ k {register P | Q} [BFw-Reg] ↑ h {register R} h • k -→ h • k ↑ k {register R} [Compl-Reg] ↑ h {register R} h : n[P | wait.Q] k -→h : n[P | Q | R] k
In 4 GcPan mov : Garbage Collecting Forwarders

As described in the previous section, chaining forwarders upon each cross-boundary movement in Pan mov removes the need for all-to-all connectivity in the underlying network. However, along with this adaptability to wide-area networks, at least one boundary forwarder and one normal forwarder are created upon each cross-boundary movement. Therefore, continuing the execution of an SA program in Pan mov is likely to result in the accumulation of more unused forwarders and longer chains of forwarders than those in Pan. Clearly, unused forwarders keep occupying resources needlessly, and forwarder chains induce a loss of performance by increasing the number of network messages.

To handle such situations, we enriched Pan mov with the mechanism used in GcPan [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF]; it reclaims unused forwarders and contracts forwarder chains. The following are the basic ideas of GcPan: (1) to detect unused forwarders, every agent is equipped with a reference count. Every time an agent receives a request message, its reference count is decremented. If an agent is a forwarder whose count is zero, it is reclaimed, and (2) to contract forwarder chains, using Tarjan's union-find algorithm [START_REF] Tarjan | Efficiency of a Good But Not Linear Set Union Algorithm[END_REF], every agent is relocated immediately below its parent ambient. For a detailed understanding of GcPan, see [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF].

Enriching Pan mov with GcPan's mechanism is a straightforward process. However, the formal definition of the resulting abstract machine GcPan mov is rather complex. For lack of space, it is provided in [START_REF]GcPan shift webpage[END_REF].

GcPan shift : Proactive Movement

In Pan mov and GcPan mov , an ambient physically moves when it performs a cross-boundary in or out action. However, this implies that its physical movement is still deferred until it sends some request message to its parent. Then, for instance, if an ambient blocks for some reason, e.g., waiting for I/O, forwarders used by the ambient will not be reclaimed or contracted until the ambient resumes and sends some request. Moreover, if a network connection represented by a certain network boundary is broken for some reason (including permanent disconnection of mobile devices), a child ambient whose parent belongs to the other side of the boundary cannot send requests to its parent, and it cannot perform movements anymore.

In order to address the problem described above, there should be a mechanism for enforcing physical movements of ambients in the abstract machines, which Pan and GcPan do not have. Therefore, we added a shift action, which instructs an ambient to move physically below its parent, in Pan mov and Gc-Pan mov . Note that shift performs no logical action at the calculus level; hence, each ambient may perform shift actions periodically. For example, in the state:

h 1 : a[ P ] h2 h 2 • h 3 h 3 • h 4 h 4 • h 5 h 5 : b[ Q ] h6
if a performs a shift action, the state changes to:

h 2 • h 3 h 3 • h 4 h 4 • h 5 h 7 : a[ P ] h5 h 5 : b[ Q ] h6
Moreover, if a has no child or if all of a's children also perform a shift action, the forwarders are reclaimed as in:

h 7 : a[ P ] h5 h 5 : b[ Q ] h6 .
We enrich Pan mov with the shift action described above by adding the following reduction rules:

[Req-Shift] P k -→ h:n wait.P ↑ k h {shift n} [Local-Shift] ↑ l {shift -} - -→ h:- 0 ↑ l {go h} [Local-Shift ] ↑ l {shift • m} - -→ h:- wait.0 ↑ h {Cshift • m, l} [Compl-CShift] ↑ h {Cshift • m, l} h : n[P | wait.Q] k -→ h : n[P | Q] k (νh )(h : m[wait.0] h ↑ l {migrate h })
The formal definition of the abstract machine GcPan shift , which is an extension of GcPan mov with the shift action, is provided in [START_REF]GcPan shift webpage[END_REF].

Correctness

We prove that Pan mov is a correct implementation of SA. The fact that Pan is a correct implementation of SA, i.e., SA and Pan are weak barbed bisimilar, is proved in [START_REF] Sangiorgi | A Distributed Abstract Machine for Safe Ambients[END_REF][START_REF] Giannini | Safe Ambients: Abstract Machine and Distributed Implementation[END_REF]; hence, it suffices to prove that Pan and Pan mov are weak barbed bisimilar. We follow the proof method between Pan and GcPan [START_REF] Hirschkoff | A Correct Abstract Machine for Safe Ambients[END_REF][START_REF] Hirschkoff | An efficient abstract machine for Safe Ambients[END_REF]. Theorem 1. There is a weak barbed bisimulation R between Pan and Pan mov .

Proof. We constructed such a bisimulation relation R. For lack of space, the precise definition of R and the details of the proof is provided in [START_REF]GcPan shift webpage[END_REF].

Due to physical movement of Pan mov , R has several significant differences from the bisimulation relation R between Pan and GcPan, which is described in [START_REF] Hirschkoff | An efficient abstract machine for Safe Ambients[END_REF]. The following are the main differences: (1) each ambient in Pan mov may be at several locations during its lifetime; therefore, the simple correspondence between ambients that are at the same location, which is used in R , does not work. Instead, we established a mapping from the set of ambient locations in a Pan net to the set of ambient locations in the corresponding Pan mov net, and (2) the mapping is updated along with Pan mov 's reductions related to physical movement of ambients so that it can properly map unmoving ambients of Pan to moving ambients of Pan mov . For the correctness of GcPan shift , the proof stated above can be adapted to establish a weak barbed bisimilarity between GcPan shift and GcPan. The correctness of GcPan mov is immediately derived from that of GcPan shift because GcPan mov is a subset of GcPan shift .

Conclusion

In this paper, we proposed novel abstract machines that can handle network boundaries in wide-area and mobile networks. They have the following desirable properties: [START_REF] Cardelli | Mobile Ambient Synchronization[END_REF] No ambients communicate directly with other ambients in different network domains; instead, all inter-domain messages are sent via boundary forwarders, and (2) In GcPan shift , any ambient will go into a stable state in which any ambient inside it can perform SA actions without boundary forwarders. Therefore, we can construct more reliable implementations of SA by using these machines as base implementation models. Formal proofs of these properties are left for future work.

AtJ [START_REF] Fournet | An Asynchronous, Distributed Implementation of Mobile Ambients[END_REF] is a distributed implementation of AC, a translator from AC to Jo-Caml [START_REF] Fournet | The Join-Calculus: a Calculus for Distributed Mobile Programming[END_REF]. Although physical movement is triggered by each execution of in or out, no forwarders are created for this movement in AtJ. This is because any child can send messages directly to its parent at any moment using JoCaml's distributed message transfer mechanism; that is, AtJ relies on JoCaml's all-to-all connectivity. Nonetheless, adapting our technique to AtJ seems relatively easy because a forwarder is created at each open action, as in the case of Pan.

In a distributed abstract machine for the Kell Calculus [START_REF] Schmitt | An Abstract Machine for the Kell Calculus[END_REF], the passivation of a kell is represented as the physical migration of the whole hierarchy (i.e., the kell, its sub-kells, sub-kells of its sub-kells, and so on). Thus, the underlying network need not support all-to-all connectivity. However, such a passivation mechanism seems rather inefficient. Moreover, each kell must keep track of its sub-kells; therefore, the abstract machine is more complex, as compared to the Pan family.

Fig. 1 .

 1 Fig. 1. Simulation of SA actions in Pan.

  [Compl-Parent] and [Compl-Coin], {go} and {OKin} messages are handled appropriately by the destination ambient. In [Compl-Cin] and [Compl-Cout], an ambient that receives a { • Cin} or { • Cout} message creates a clone and sends the appropriate completion messages. In [Compl-Migr], an ambient that receives a {migrate k} message sends the {register} message, which contains the contents of the ambient, to k. Each {register} message reaches the destination ambient through zero or more transmissions of [BFw-Reg]; then, R is merged into the destination in [Compl-Reg].

Corollary 2 (

 2 Adequacy). Let P be an SA process, then [[P ]] mov ≈ P . Proof. [[P ]] R [[P ]] mov can be easily checked; hence, from Theorem 1, [[P ]] ≈ [[P ]] mov . Then, the result follows from the adequacy of Pan [7]: [[P ]] ≈ P .

  and p ∈ Names ∪ Locations. The overall network A consists of parallel compositions ( ) of Agents and Msgs. There are three kinds of agents: h : n[P ] k is a located ambient mentioned earlier, h B k is a forwarder at h, which forwards messages to k, and h • k is a seed of a boundary forwarder at h (the meaning of k is explained later). B in a forwarder indicates whether it is a normal forwarder (•) or boundary forwarder (•).

  represents a request message sent from h to k and ↑ h {Compl } represents a completion message sent to h. When a request message crosses at least one boundary, it is marked with the tag •, e.g., ↑ k h { • R}. The meaning of each kind of R and Compl is described in detail below.

	Processes
	P

These extra steps (local communication) can be omitted in real implementations. In addition, the parameter n of {•Cin n, m, l, l } is used only for the correctness proof (seeSection 6 and [6]).

Acknowledgments. This work was partly supported by MEXT Grant-in-Aid for Young Scientists (B) (21700029).

Local reductions

The other rules express match operations of an ambient for three kinds of movements.

In [Local-In] and [Local-Out], if no request message is marked with the • tag, the appropriate completion messages are sent back, as shown in Figure 1 (a), (b). In [Local-Open], irrespective of the {open} message being marked with •, all opens can be handled as shown in Figure 1 (c).

If an {in} message sent by an ambient at k is marked with •, a clone must be created inside the same network domain as the ambient, as explained in Section 3.1. The message {new m, k} is used for this purpose in [Local-In ], where m is the name of the clone to be created.

On the other hand, if an {in} message does not cross any boundaries, a clone may be created immediately by the parent. However, in our formalization, we cannot express the creation of a located agent at the process level. Instead, we formalized this case as in [Local-In ], where the parent sends the { • Cin} message to itself. The consumption of { • Cin} is a network-level reduction (see [Compl-Cin] below); hence, it can express the creation of a clone. We do the same for out in [Local-Out ]. 1 Transmission of completion messages

The kinds of completion messages that might cross some network boundary are new and migrate; both are forwarded by seeds.

In [Back-Migr], the seed at h changes the argument of {migrate k} to h and forwards it to l, where a requesting ambient or another boundary forwarder is located. At the same time, the seed becomes the boundary forwarder in preparation for the {register} message sent back from l.