# Subtyping and Matching for Mobile Objects

In ICTCS 2001, Lecture Notes in Computer Science, 2202:235{255, c Springer, 2001.

Subtyping and Matching for Mobile Objects

1 Dipartimento di Informatica Univ. \Ca' Foscari", Venezia, Italy

?

Michele Bugliesi1 , Giuseppe Castagna2, and Silvia Crafa1 2

;

2 Departement d'Informatique Ecole Normale Superieure, Paris, France

1 Introduction

Abstract. In BCC00], we presented a general framework for extending calculi of mobile agents with object-oriented features, and we studied a typed instance of that model based on Cardelli and Gordon's Mobile Ambients. Here, we re ne our previous work and de ne a new calculus which is based on Remote Procedure Call as the underlying protocol for method invocation, and a di erent technique to type method bodies. The new type system is equipped with both a subtyping and a matching relation. The combination of matching and subtyping provides new insight into the relationship between ambient opening in the new calculus and method overriding in object-oriented calculi.

Calculi of mobile agents are receiving increasing interest in the programming language community as advances in computer communications and hardware enhance the development of large-scale distributed programming. Agents are e ective entities that perform computation and interact with other agents: the term \mobile" implies that agents are bound to locations and that this binding may vary over time; agent interaction, in turn, is achieved using resources such as communication channels Independently of the new trends in communication technology, object-oriented programming has established itself as the de-facto standard for a principled design of complex software systems. Drawing on our preliminary work on the subject BC00,BCC00], in this paper we study a formal calculus that integrates object-oriented constructs into calculi of mobile agents. The resulting framework provides foundations for a computation model for distributed applications, where conventional client-server technology |based on remote exchange of messages between static sites| and mobile agents coexist in a uniform way. The model results from extending the structure of named agents in the style of Mobile Ambients CG98] with method de nitions and primitives for dealing with message passing and self denotations. The extension has interesting payo s, as it leads to a principled approach to structuring agents. In particular, introducing methods and message passing as primitives, rather than encoding them on top of the underlying calculus of agents leads to a rich and precise notion of agent interface and type. Furthermore, it opens the way to reusing the advances in type system of object-oriented programming and static analysis.

? Work partially supported by MURST Project 9901403824 003, by CNRS Program Telecom-

munications : \Collaborative, distributed, and secure programming for Internet", and by Galileo Action n. 02841UD

With respect to our previous work BC00,BCC00] this paper brings two main contributions: the introduction of a Remote Procedure Call (RPC)1 primitive for message passing and method invocation and, foremost, a non trivial blend of matching and subtyping relations. Method invocation based on RPC ts nicely the design of a typed distributed calculus as it allows method bodies to be type checked locally, in the object where they are de ned, independently of the caller. As a consequence, the choice of RPC as the underlying semantics of method invocation yields a notion of interface type for our mobile objects that is substantially simpler and more tractable than the corresponding notion de ned in BC00,BCC00]. Matching is employed in the type system to ensure sound typing of ambient (or object) opening in the presence of methods residing within objects2 . As it turns out, the combination of subtyping and matching conveys new insight into the relationship between method overriding in objectoriented calculi and the open capability in our mobile objects.

Plan of the paper In Section 2 we describe the calculus of mobile objects, named MA++ , based on the calculus of Mobile Ambients (henceforth MA) of Car99,CG98]. Section 3 describes various examples of the expressive power of the calculus. Speci cally, we show that it is possible to encode primitives like method overriding distinctive of object calculi, various forms of process communication, as well as di erent primitives of method execution3 . In Section 4 we study the type theory of our calculus, and state relevant properties. Possible further extension are discussed in Section 5. The presentation of related work in Section 6, and nal remarks in Section 7 conclude our presentation.

2 MA++

2.1 Syntax

The syntax of MA++ is the same as that of mobile objects de ned in BC00,BCC00], and it results from generalizing the structure of ambients to include interfaces, as in a I ; P ] , where P is a process and I is a list of method de nitions, de ned by the following productions: Processes

P ::= 0 inactivity ? P P parallel composition ? a I ; P ] ambient ? ( x)P restriction ? M:P action

j

1 Remote Proceduce Call is often referred to as Remote Method Invocation (RMI) in this context. 2 Note that under this aspect the type system in BCC00] contained a aw. 3 Here, and throughout the paper, we use the terms \encode" and \encoding" in a somewhat

loose sense: we should in fact use \simulate" and \simulation" as we don't claim these encodings to be \atomic" |i.e. free of interferences| in all possible contexts.

Interfaces Patterns

I ::= `(x) . & (z )P method ? I :: J sequence ? ? empty interface

x ::=

?

x

variable (x1 ; : : : ; x ) tuple (n > 1)

n

The syntax of processes is a generalization of the combinatorial kernel of the Ambient Calculus: 0 denotes the inactive process, P Q the parallel composition of two processes P and Q, a I ; P ] denotes the object named a with interface I and enclosed process P , ( x)P restricts the name x to P , and nally M:P performs the action described by the term M and then continues as P . Interfaces are lists of labels with associated processes: the syntactic form `(x) . & (z )P denotes a method labeled ` whose associated body is the process P where the & -bounded variable z represents the self parameter distinctive of object calculi, i.e. the method's host object. Finally, the pattern x is the tuple of input parameters for P .

j

Terms

M; N ::= a; b; : : : ; x; y : : : ? (M1 ; : : : ; M ) ? M:M ? " ? in a ? out a ? open a ? a send ` M

n

h

i

name/variable tuple (n > 0) path empty path enter a exit a open a remote invocation

h i

Terms include the capabilities distinctive of Mobile Ambients. In addition, mobile objects are equipped with a capability for remote method invocation: a send ` M invokes the method labeled ` residing on the object denoted by a with arguments M. In the following we use P; Q; R; : : : to range over processes, I; J to range over (possibly empty) interfaces, and lower case letters to range over generic names, preferring when possible a; b; : : : for agent names, and x; y; : : : for parameters. Method names, denoted ` range over a disjoint alphabet and have a di erent status: they are xed labels that may not be restricted, abstracted upon, nor passed as values (they are similar to eld labels in record-based calculi). We omit trailing or isolated 0 processes and empty interfaces, using M , a I ] , a P ] , and a ] as shorthands for, respectively, M:0, a I ; 0 ] , a ? ; P ] , and a ? ; 0]] .

2.2 Operational Semantics

We de ne the operational semantics of the calculus by means of a structural congruence and a reduction relation. As usual, the former is used to rearrange a term in order to apply the latter.

Structural Congruence Structural congruence for agents is de ned in terms of an equivalence relation I over interfaces, given in Figure 1. This relation allows method suites to be reordered without a ecting the behavior of the enclosing agent: reordering of methods, in turn, is used to de ne the reduction of method invocation.

(Eq Meth Assoc) (I :: J) :: L I I :: (J :: L) (Eq Meth Comm) I :: m(xm ) . P ; `(y` ) . Q I I :: `(y` ) . Q :: m(xm ) . P (Eq Meth Over) I :: `(x) . P :: `(x) . Q :: I I I :: `(x) . Q

` 6= m

Fig. 1. Equivalence for Methods

De nitions for methods with di erent name and/or arity maybe freely permuted (Eq Meth Comm); instead, if the same method has multiple de nitions, then the right-most de nition overrides the remaining ones (Eq Meth Over). Similar notions of equivalence between method suites can be found in the literature on objects: in fact, our de nition is directly inspired by the bookkeeping relation introduced in FHM94]. Structural congruence of processes is de ned as the smallest congruence on processes that forms a commutative monoid with product and unit 0, and is closed under the rules in Figure 2, where the set fn of free names is de ned by a standard extension of the de nition in Car99].

j

(Struct Res Dead) (Struct Res Res) (Struct Res Par) (Struct Res Agent) (Struct Path Assoc) (Struct Empty Path) (Struct Cong Agent Meth)

( x)0 0 ( x)( y)P ( y)( x)P ( x)(P j Q) P j ( x)Q ( p)a I ; P ] a I ; ( p)P ] (M:M ):P M:M :P ":P P I I J ) a I; P ] a J; P ]

0 0

x 6= y x 62 fn(P ) p 62 fn(I) fag

Fig. 2. Structural Congruence for Agents

The rst block of clauses are standard (they are the rules of the -calculus). The rule (Struct Path Assoc) is a structural equivalence rule for the Ambient Calculus, while the rule (Struct Res Agent) modi es the rule for agents in the Ambient calculus to account for the presence of methods. Rule (Struct Cong Agent Meth) establishes agent equivalence up to reordering of method suites. In addition, we identify processes up to renaming of bound names: ( p)P = ( q)P p := q if q fn(P ).

f g 62

Reduction Relation The reduction semantics of the calculus is given by the context rules in Figure 3, plus the notions of reduction collected in Figure 4, that we comment below P P

0

P; P ? Q; Q Q ) P ? Q ) ( x)P ? ( x)Q

0

0

?

Q

0

P P

? ?

Q ) a I; P ] ? a I; Q] Q)P jR?QjR

Fig. 3. Structural Rules for Reduction

(in) b I ; in a:P j Q ] j a J ; R ] (out) a I ; b J ; out a:P j Q ] j R ] (open) open a:P j a Q ] ? P j Q

?

a I; R j b J; P j Q] ] ? b J; P j Q] j a I; R]

(update) b I ; open a:P j a J ; Q ] j R ] ? b I :: J ; P j Q j R ] for J 6= " (send) b I ; a send `hM i:P j Q ] j a J :: `(x) . & (z)R ; S ] ? b I ; P j Q ] j a J :: `(x) . & (z )R ; Rfz; x := a; M g j S ]

Fig. 4. MA++ reduction rules

The rst three rules are exactly the same as the corresponding rules for the Mobile Ambients. Rule (update ) is a direct generalization of the open rule to handle the case when the opened ambient contains a non-empty interface. In this case, open a may only be reduced within an enclosing ambient. After the opening, the local process of a is unleashed within b and the interfaces of the opening and the opened ambients are merged. The nal (send ) rule handles the new syntactic construct for method invocation, implementing the Remote Procedure Call (more precisely, Remote Method Invocation) model. The notation R z; x := a; M indicates simultaneous substitution in R of a for z and of M for x. The result of the ambient b sending message ` to its sibling a, is thus the activation of the corresponding method body on the receiver side where actual parameters are substituted for formal ones and the self parameter is dynamically bound to the (name of the) receiver.

f g

3 Expressive power

In this section, we discuss a number of protocols and constructs that can be expressed within MA++ . Some of these examples have been already presented in our previous work BC00,BCC00] where, however, they were de ned in terms of a di erent semantics for method invocation based on Code On Demand.

Having chosen Remote Procedure Call as our primitive protocol, it is interesting to try to encode other alternatives, and see how an object could send messages to its parent or its children, as well as to invoke its own methods as shown in Figure 5. As it turns out, these alternative invocation modes can all be encoded.

(downsend) a downsend `hM i:P j a I :: `(x) . & (z)Q ; R ] ? P j a I :: `(x) . & (z )Q ; R j Qfz := a; x := M g ] (upsend) a I :: `(x) . & (z)Q ; R j b J ; a upsend `hM i:P ] ] ? a I :: `(x) . & (z )Q ; R j Qfz := a; x := M g j b J ; P ] ] (local) a I :: `(x) . & (z)Q ; a local `hM i:P1 j P2 ] ? a I :: `(x) . & (z )Q ; Qfz; x := M; ag j P1 j P2 ]

3.1 Parent-child and Local communications

Fig. 5. Other Constructs for Method Invocation

Parent-to-child invocation. This form of method invocation can be de ned as follows:

4 a downsend ` M :P = ( p; q) (p a send ` M :q out p ] ] open q:open p:P ) where (p; q = fn(M ) fn(P )). In words, we temporarily create a new ambient p

h i h i j 2

that becomes a sibling of the receiver in order to perform a RPC; we then use the ambient q as a \lock", to guarantee that the ambient p is destroyed only after the receiver has served the invocation. It is a routine check to verify that the desired e ect of the invocation is achieved by a sequence of reduction steps. To ease the notation, we give the reduction steps in the simpli ed case of a method which does not have parameters and does not depend on self (the presence of parameters and the dependency on self does not interfere with the protocol). a downsend `:P a ` . Q ; R ] ( p; q) p a send ` M :q out p ] ] open q:open p:P a ` . Q ; R ] ? ? ( p; q ) p q out p ] ] open q:open p:P a `.Q; R Q] ? ? ( p; q ) p ] q ] open q:open p:P a ` . Q; R Q] ? P a ` . Q; R Q] The coding could be simpli ed by adding coactions, in the style of SA calculus of LS00]. Coactions help serialize the steps of the protocol by means of the capability-cocapability synchronization. The lock ambient q would then be substituted by cocapability coopen p, enforcing the opening of p only after the message has been sent.

j h i j j j j j j j j j j j

Local and Self Invocation. Local method invocation within an ambient a is coded similarly to the previous case. Choosing p; q 2 = fn(M ) fn(P ), one de nes:

4 a local ` M :P = ( p; q) (p out a:a send ` M :in a:q out p ] ] open q:open p:P )

h i h i j

Relying upon this de nition, it is then easy to de ne self-invocation within method bodies. To exemplify, consider the following process: a `1 (x) . & (z )z local `2 x :: `2 (x) . P ; R ] Invoking the method `1 from outside the object a results in the execution of the process P in parallel with R within a. Child-to-parent. We conclude with a form of upward method invocation, whereby an object invokes a method provided by that object's parent. A rst way of de ning it might be:

h i

4 a upsend ` M :P = out a:a send ` M :in a

h i h i

But this is not fully satisfactory because requires a move of the sender. Alternatively, we can encode it by using some auxiliary ambient. Assume that the invocation occurs within an object b enclosed within a: To understand the de nition, simply look at the chain of capabilities inside the ambient p, which corresponds to the steps in the protocol evolution. First, the ambient p leaves its parent ambients b, then a (that contains the method to be invoked), and performs the message send before being destroyed after the opening of the locking ambient q. One problem with the encoding is that it is context-dependent, since it uses the name b of the sender.

4 a upsend ` M :P = ( p; q) (p out b:out a:a send ` M :in a:in b:q out p ] ] open q:open p:P )

h i h i j

3.2 Replication

The behavior of replication in concurrent calculi is typically de ned by a structural equivalence rule establishing that !P !P P . With ambients we can encode a similar construct relying upon the implicit form of recursion inherent in the reduction of method invocation. Let be p; q = fn(P )

j 2

4 !P = ( p; q) (p downsend ! :open q:P p ! . & (z )(q out z:z downsend ! :open q:P ] ) ; ] ) The reduction for the encoding of !P is then the following:

hi j hi

4 !P = ( ?( ?( ?(

p; q) p downsend ! :open q:P p ! . & (z )(q ] ) ; ] ? p; q) open q:P p ! . & (z )(:::) ; q out p:p downsend ! :open q:P ] ] ? p; q) open q:P q p downsend ! :open q:P ] p ! . & (z )(:::) ; ] p; q) (P p downsend ! :open q:P p ! . & (z )(:::) ; ] ) P !P

hi j j hi j hi j j hi j j

Notice that at each reduction step only one capability is ready to be exercised. Furthermore, the process P is activated only after the opening of the ambient q, hence it does not interfere with the protocol. We have then that the described protocol is a \precise" encoding of the replication (free from interferences). Even if we adopted RPC as primitive protocol for remote method invocation, the Code on Demand protocol used in BC00,BCC00] is useful in several situation. The behavior of code on demand (cod) can be described as follows. A client c invokes a method ` on a server s; the server activates the method and then sends it back to the client for the latter to execute it. Formally this correspond to the following reduction rule:

c J ; s send cod`hM i:R j S ] j s I :: `(x) . & (z )Q ; P ] ? c J ; Qfz; x := s; M g j R j S ] j s I :: `(x) . & (z )Q ; P ] The protocol can be encoded by translating the caller and the called ambients as follows:

4 server = s I :: `(u; v; x) . & (z )u out z:in v:Q ] ; P ] 4 client = c J ; ( p)s send `hp; c; M i:open p:R j S ]

3.3 Code on Demand

The protocol relies on the agreement between the server and the client upon the name of the ambient that carries the activated process back to the client. This name is decided locally by the client which passes it as an argument for the call together with its own name. Invoking ` p; c:M spawns a new process on the server that simply carries the ambient p out of the server and back into the client c: once inside c, the transport ambient p is opened thus unleashing the process Q to be executed on the client. Note that, if the second argument passed to the method ` were a path, rather than the client's name, then by slightly modifying the server we could have a more general protocol, where the client can choose where to receive and to execute the requested method (e.g. , in one of its subambients).

h i

Following the standard de nition of method override AC96,FHM94] in formal calculi method updates for ambients can be formulated, informally, as follows: given the ambient a I :: `(x) . & (z )P ; Q ] we wish to replace the current de nition P of ` by the new de nition P 0 to form the ambient a I :: `(x) . & (z )P 0 ; Q ] Updates can be coded using a distinguished ambient as \updater". The updater carries the new method body and enters the updatable ambient a: the updatable ambient is coded as an ambient whose controlling process opens the updater thus allowing updates on its own methods. The coding is de ned precisely below, in an asynchronous setting: a similar encoding can be de ned for synchronous updates. Moreover, we allow only local updates, that is, an ambient

3.4 Updates

may only override methods contained in subambients (of course other kind of updates can be encoded, too) Updates are denoted by a update `(x) . & (z )P , read \the ` method at a gets de nition P ". We de ne their behavior as follows: let rst

4 a update `(x) . & (z )P = upd `(x) . & (z )P ; in a ]

Then de ne an updatable ambient as follows

4 a I; P ] = a I ; !(open upd) j P ]

?

Now, if we form the composition a update `(x).& (z )P 0 a I :: `(x) . & (z )P ; Q ] , the reduction for open enforces the expected behavior:

j

?

a update `(x).& (z )P 0 a I :: `(x) . & (z )P ; Q ]

j

?

?

a I :: `(x) . & (z )P 0 ; Q ]

?

Multiple updates for the same method may occur in parallel, in which case their relative order is established nondeterministically. The protocol, as de ned, relies on the assumption that the name of the updater ambient carrying the new method body is globally known. A more realistic assumption is that updated ambient and the context agree on the name of the updater prior to start the protocol. This can be accomplished with a di erent de nition of updatable ambient, one that assumes that updatable ambients come with an ad-hoc method that sets the appropriate conditions for the actual update to take place. The upd method below serves this purpose.

4 a I; P ] = a I :: upd (u) . & (z )open u ; P ]

?

Now, the updated protocol comprises two steps. First the updated ambient receives the name of the updater, and only then does the update take place:

4 a update `(x) . & (z )P = ( p) (a downsend upd p :p `(x) . & (z )P ; in a ] )

h i

3.5 Encoding the -calculus

A nal example shows that synchronous and asynchronous communication primitives between processes can be encoded. We rst give an encoding of synchronous communication. A similar model of (asynchronous) channel-based communication is presented in CG98] and it is based on the more primitive form of local and anonymous communication de ned for the Ambient Calculus: here, instead, we rely on the ability, distinctive of our ambients, to exchange values between methods. A channel n is modeled by an updatable ambient n, two locks n , and n and an auxiliary ambient n needed for the communication protocol based on RPC. The ambient n contains a method ch: a process willing to read from n installs itself as the body of this method, whereas a process willing to write on n invokes

i o

ch

passing along the argument of the communication.

?

4 (ch n) = n ch(x) . 0 ] n ] 4 n! y :Q = open n :n downsend ch(y):open n:(n ] Q) 4 n?(x):P = open n : n update ch(x) . (n out n:P ] ) :n ] The communication is then the following: a process n! y :Q writing y on n rst attempts to grab the output lock n , then sends the message ch(y) to n, and after the end of the RPC protocol (i.e. after the opening of the carrier ambient n), the process continues as Q releasing the input lock n . At the start of the protocol there are no output locks: hence the process writing on n blocks. A process n?(x):P reading from n rst grabs the input lock n provided by the channel, then installs itself as the body of the ch method in n, and nally releases the output lock. Now the writing process resumes its computation: it sends the message thus unleashing P , and then releases the input lock and continues as Q. Asynchronous communications are obtained directly from the coding above, by a slight variation of the de nition of n! A :Q. We simply need a di erent way of composing Q with the context:

j

i

h i

o i

i

j

o

h i

o

i

i

h

i

4 n! y :Q = (open n :n downsend ch(y):open n:(n ] )) Q

h i

o

i

j

Based on the this technique, we can encode the synchronous (and similarly, the asynchronous) polyadic -calculus in ways similar to what is done in CG99]. Each name n in the -calculus becomes a quadruple of names in our calculus: the name n of the ambient dedicated to the communication, the names n and n of the two locks, and the name n of the auxiliary ambient. Therefore, communication of a -calculus name becomes the communication of a quadruple of ambient names.

i o

h ( n)P i h n!hy i:Q i h n?(x):P i h P j Qi h !P i h i

0

= ( n; n; ni; no )(n ] j n ? ch(x; x; xi; xo) . 0]] j h P i ) n; ni; no62 fn(h P i ) = open no :n downsend ch(y; y; yi; yo):open n:(n ] j Q) = open ni :n update ch(x; x; xi ; xo) . (n out n:P ] ) :n ] = h P i j h Qi = !h P i =0

4 i 4 i 4 o 4 4 4

Fig. 6. Encoding of the synchronous -calculus

The initialization of the ch method in the ambient that encodes the channel n could be safely omitted, without a ecting the operational properties of encoding. However, as given, the de nition scales smoothly to the case of a typed encoding, preserving well-typing.

A compositional encoding of the -calculus channel-based communication in terms of message sends, can be de ned in a way similar to that in LS00], adding to the calculus coactions and relying on their ability to control/synchronize any computational step. See Section 5 for a more detailed discussion.

4 Types and Type Systems

The typing of ambients inherits ideas from existing type systems for Mobile Ambients; however, as we anticipated, the presence of methods enables a more structured (and informative) characterization of their enclosing ambient's interfaces. The grammar productions for types are: Signatures Ambients Capabilities Processes Values Types ::= A ::= C ::= P ::= V ::= T ::= ( ` (V ) ) 2 Amb ] Cap ] Proc ]

i i i I

A C X A C P

j j j j

Signatures convey information about the interface of an ambient, by listing the ambient's method names and input types. The intuitive reading of ambient, capability and process types is as follows: the type Amb ] is the type of ambients with methods declared in ; the type Cap ] is the type of capabilities whose enclosing ambient (if any) has a signature which contains at least the methods included in ; the type Proc ] is the type of processes whose enclosing ambient (if any) contains at least all the methods declared in . The values, used as argument for method invocation, are ambient names and capabilities. The complete syntax of types contains type variables, that are used to deal with the dependency of method bodies on the self parameter. In fact, due to ambient opening, a method residing in an ambient a may be reinstalled inside a new ambient that opens a and that may have a richer interface; thus the type of the self variable may be dynamically rebound to a di erent ambient type. As a consequence, to ensure sound typings of method invocations, method bodies are typed in a context that assumes the so-called MyType Bru94] typing for the self variable, i.e. a match-bounded type variable representing the type of all ambients where the method can be reinstalled, via opening. In particular, we use a restricted form of matching relation Bru94], where a type variable X , representing a self type, may appear in the context only match-bounded by an ambient type (i.e. X< # A ). Furthermore, we syntactically restrict our signatures, and consequently our ambient, capability and process types, to not contain type variables. As a consequence, the type system does not support MyType method specialization Bru94,FHM94], the OO-typing technique that allows methods's types to be specialized when they are inherited (or, in our context, when they are subsumed in an opening ambient). Instead, in our calculus

a method body has always the same type (that is, the one declared in ), independently of the dynamic binding of its self variable. This is not surprising, as our method bodies are processes with no return value, hence they are dealt with essentially as methods with return type unit in imperative object calculi.

4.1 Type System

The typed syntax of the calculus is described by the productions in Figure 7 :

Interfaces I ::= `(x) . & (z)P j I :: I j " Processes P ::= 0 j P jP j a I ; P ] j ( x:A )P j M:P Expressions M ::= x j (M1 ; : : : ; Mn ) j x send `hM i j in x j out x j open x j "

Fig. 7. Typed syntax for ambients

As we said in Section 2, we take method names to be xed labels that may not be passed as values, nor restricted. The rst restriction is justi ed by the fact that method names are part of the structure of ambient (capability and process) types; as a consequence, lifting this restriction would be possible but it would make our types ( rst-order) dependent types. Instead, lifting the second restriction is possible, and in fact not di cult, even though it complicates the format of the typing rules . For this reason we will disregard this issue in what follows. The structure of contexts and judgments is de ned by the productions below, where we assume W to range over the set X; A ; C of extended value types:

f g

Contexts ? ::= ? j ?; x : W j ?; X< #A Judgements J ::= ? ` M : W j ? ` X< #A j ? ` P : P j ? ` T j ? `

Fig. 8. Contexts and typing judgments

The complete set of typing rules is presented in Appendix A; below, we discuss the most interesting ones. Method signatures, associated with ambient types, are traced by the types Cap, of capabilities, to allow an adequate typing of messages, mobility and opening.

? a : Amb ] ? open a : Cap ]

` `

(open)

The rule (open) for opening an ambient requires precise knowledge of the type of the ambient being opened: consequently, the type of the ambient must be an ambient type, not a type variable. An opening is now legal under the condition that the signature of the opening ambient be equal to (in fact, contain, given the presence of subtyping) the signature of the ambient being opened. This condition is necessary, as subject reduction would otherwise fail: as a consequence, opening an ambient may only update existing methods of the opening ambient, and their original typing must be preserved.

? a:W ? W< # Amb `(V 0 ) ] ? M 0 : V 0 ? a send ` M 0 : Cap ] Rule (Message) says that an invocation for method ` on an expression a requires the type of a to match an ambient type containing the method `. Note that the type of a may either be an ambient type matching (i.e. \longer" then) Amb `(V 0 )], or else an unknown type (i.e. a type variable) occurring matchbounded in the context ? . Since the body of the invoked method is not executed

` ` ` ` h i

(Message)

in the same ambient that contains the send capability (due to the RPC semantics), no constraint is imposed on the type of the send capability. Of course, in order for the expression to type check, the message argument and the method parameters must have the same type. 4 (Amb) ( = ( ` (V ) ) 2 ) ? a : Amb ] ?; Z< # Amb ]; z :Z; x :V P : Proc ] ? P : Proc ] ? a (` (x ) . & (z )P ) 2 ; P ] : Proc 0 ] Rule (Amb) types ambients similarly to objects in the object calculi of AC96]: each method is typed under the assumptions that (i) the self parameter has a type that matches the type of the enclosing ambient, (ii) method parameters have the declared type, and (iii) method bodies must be typable with a process type that agrees with the type of the enclosing ambient and that is independent on the type of self (i.e. disallowing MyType method specialization). Moreover, the rule requires the local process to have a process type that agrees with the type of the enclosing ambient. Finally, no constraint is imposed on the signature 0 , associated with the process type in the conclusion of the rule, as that signature is (a subset of) the signature of the ambient enclosing a (if any). Note that the match-binding for the type of the self variable ensures that methods local to ambient a are well-typed also within any other ambient that might eventually open a. Also the rule requires exact knowledge of the true type of the ambient's name; a structural rule allowing the name of the ambient to be typed with a match-bounded type variable would break type soundness, since we would not have a precise control of the openings of that ambient (see rule (open)).

i i i I

`

i

i ` I

i

`

`

i

i

i

i

4 In fact, since capability types can be subtyped, the type of the arguments can be subtypes

of the type of the formal parameters.

(Match Amb)

`

i i i

? Amb (` (V )) 21 + ]< # Amb (` (V )) 21 ]

::n k i i i ::n

?

`

(Sub Cap)

0

(Sub Proc)

0

Cap ] Cap 0 ] Proc ] Proc 0 ] Non-trivial subtyping is de ned for capability and process types: speci cally, a capability (resp. process) type Cap ] (resp. Proc ]) is a subtype of any capability (resp. process) type whose associated signature (set theoretically) contains . The resulting notion of subtyping is reminiscent of the notion of subtyping in width distinctive of type systems for object and record calculi. Width subtyping must be disallowed over ambient types to ensure sound uses of the open capability: intuitively, when opening an enclosed ambient, one again needs exact knowledge of the contents of that ambient, (speci cally, of its method suite) so as to ensure that all the overriding that takes place upon exercising the capability, be traced in the types. Nevertheless, we have matching relation between ambient types, that ensures sound typing of methods even when they are merged, via opening, in a \larger" ambient. The complete set of subtyping and matching rules includes the standard rules for re exivity and transitivity (not shown). Also, as customary, the subtyping relation is endowed in the type system via a subsumption rule.

We conclude the description of the basic type system with a proof of subject reduction. The proof is rather standard, and only sketched due to lack of space.

4.2 Subject Reduction and Type Soundness

Lemma 1 (Substitution). 1. If ?; x:W P : P and ? M : W , then ? P x: = M : P . 2. If ?; Z< # A ; z :Z P :P and ? a:A 0 , ? A 0 < #A, then ? P z : = a :P .

` ` ` f g ` ` ` ` f g

Proof. By induction on the derivation of the rst judgment in hypothesis.

Proposition 1 (Subject Congruence).

1. If ? ` P : Proc ] and P Q then ? ` Q : Proc ]. 2. If ? ` P : Proc ] and Q P then ? ` Q : Proc ]. Proof. By simultaneous induction on the derivations of P

` ` `

Q and Q P .

Lemma 2 (Bounded Weakening). 1. If ?; x : W P : P and ? W 0 W then ?; x : W 0 P : P . 2. If ?; Z< # A ; z :Z P :P and ? A 0 < # A then ?; Z< # A 0 ; z :Z P :P .

` ` `

Proof. By induction on the derivation of the rst judgment in hypothesis. If ? ` P : Proc ] and P ?Q then ? ` Q : Proc ]. Proof. By induction on the derivation of P ?Q, and a case analysis on the last applied rule. Besides being interesting as a meta-theoretical property of the type system, subject reduction may be used to derive a soundness theorem ensuring the absence of run-time (type) errors for well-typed programs. As we anticipated, the errors we wish to statically detect are those of the kind \message not understood" which are distinctive of object calculi. With the current de nition of the reduction relation such errors may not arise, as not-understood messages simply block: this is somewhat unrealistic, however, as the result of sending a message to an object (a server) which does not contain a corresponding method should be (and indeed is, in real systems) reported as an error. We thus introduce a new reduction to account for it a I ; P j b send `hM i:Q ] j b J ; R ]

?

Theorem 1 (Subject Reduction).

a I; P

j

ERR ]

j

b J; R]

(` J)

62

together with the rules that propagate errors in every context. The intuitive reading of the reduction is that a not-understood message causes a local error | for the sender of that message| rather than a global error for the entire system. The rule above is meaningful also in the presence of multiple ambients with equal name, as our type system (like those of CG99,CGG99,LS00]) ensures that ambients with the same name have also the same type. Therefore if a message ` is absent from a given ambient b, it will also be absent from all ambients named b. If we assume that ERR is a distinguished process, with no type, it is easy to verify that no system containing an occurrence of ERR can be typed in our type system. Absence of run-time errors may now be stated follows:

Theorem 2 (Soundness). For every ? , P , if ? P : T , then P

` 6

?

ERR.

5 Adding coaction: SA++

In LS00], Levi and Sangiorgi show that the calculus of Mobile Ambients can be re ned in order to have a richer algebraic theory and prove useful properties. To that end, they de ne the Safe Ambients calculus, where each MA's capability is combined with a dual cocapability, and where a computational reduction step is the result of a capability-cocapability synchronization. Thus an interaction between two ambients only happens when both ambients agree on their intentions. Following their work it is not di cult to add cocapabilities to MA++ calculus we presented here, obtaining what we call SA++ . In particular, the SA++ calculus contains a cocapability listen a, that is the dual of the capability a send ,

and whose meaning is that the ambient a is ready to serve an invocation to one of its methods. For reasons of space, we do not describe this extension in full details, but we want nevertheless to point out its advantages by showing how it allow us to derive a simpler and compositional encoding of the -calculus.

h n?(x):P i h n!hxi i h ( x)P i h P j Qi

= ( p)(n ch(x) . p out n:coopen p: h P i ] ; listen n:coout n ] j open p) = n downsend chhxi = ( x) h P i = h P i j h Qi h !P i = ! h P i h 0i = 0 h ni = n

4 4 4 4 4 4 4

h Ch(T ) i

= Amb ch( h T i )]

4

Fig. 9. Encoding of the asynchronous -calculus

Every input on a channel n generates a new ambient named n, waiting to synchronize with an output on n. Having received input, the transport ambient p carries (the encoding of) P out of n. Once outside n, p is dissolved thus unleashing the continuation process P . It is instructive to notice that the ambient n is left without capabilities after having let the transport p out. As such, after synchronization, n is unavailable for interactions with the context, and thus behaviorally equivalent to the null process and garbage collectable. Note also that, dealing only with the processes yielding from the encoding of -calculi processes, the parent-to-child invocation protocol is guaranteed to be executed without interferences.

6 Related work

In the literature on concurrent object oriented programming, papers can be distinguished in two basic categories. The rst class contains works that provide semantics to objects by encoding them into process calculi. Works in the second class study calculi where primitives for objects and for concurrent processes coexist. Systematic translations of objects into -calculus can be found, for instance, in Wal95,HK96,San98,KS98]. Works that belong to the second approach are much closer to what we do here. Among these it is worth to mention the approaches of Vas94,PT95,FMLR00] which, given a name-passing calculus, build high-level constructors distinctive of object-oriented languages. A complementary approach is followed by GH98] and DBF96] since they add primitives for concurrency to the imperative object-oriented calculus of, respectively, AC96]

and FHM94]. Aspects of distribution are taken into account in NHKM99,Jef00]. We present next a detailed discussion on works most related to our.

The conc& calculus. In GH98] the authors present a concurrent object calculus (conc& ) that consists of Abadi and Cardelli's imperative object calculus extended with primitives for parallel composition, restriction and synchronization via mutexes. They also show that existing type systems for the underlying object calculus can be smoothly and soundly extended to accommodate concurrency. The basic di erence between this work and that we presented, is the fact that GH98] does not deal with process mobility. In GH98] distribution aspects are absent, while in our framework objects may move through a hierarchy of nested locations, and communication (method invocation) often requires mobility. Moreover, in our framework, due to the interplay between the dynamic nesting structure and the communication primitives, more method invocation styles can be modeled. On the other hand, the semantics of method invocation in GH98], as well as in our work, is based on the idea of self-substitution distinctive of AC96]. As in the work presented here, in GH98] objects are explicitly named, thus what gets substituted for the self variable is the name of the object rather then the object itself. A distinctive feature of GH98] is the fact that the syntax of conc& includes sequential composition of expressions that return results. This contrasts with what happens in most formalisms based on processes ( Vas94,PT95,Wal95,KS98]), where the operation of returning a result is translated into sending a message on a result channel. Even though we did not explicitly address the problem of returning a result, it is easy to extend our framework by endowing agent interfaces not only with methods, but also with elds whose invocation returns an expression. A distributed version of conc& is studied in Jef00], where the syntax of the calculus is enriched with a notion of location, and threads are allowed to migrate between locations. Contrary to our framework, in Jef00] the author considers a very simple, xed at set of locations, with no routing information, no dynamic location creation or hierarchy of locations. Moreover, in Jef00] only a subset of objects (serializable objects) can be sent across the network, and only the so-called located objects can be accessed via remote threads. The Ojeblik calculus. In NHKM99] authors present Ojeblik, an object-based language that represents the concurrent core of Obliq ( Car95]), Cardelli's lexically scoped distributed programming language. In this setting, mobility of objects is rendered via a migration mechanism that is carried out by creating a copy of the object at the target site and then modifying the original (local) object such that it forwards future requests to the new (remote) object. Moreover, lexical scoping of Obliq permits to safely ignore aspects of distribution. Migration is then correct if the behavior of an object is transparent to whether the object has migrated or not.

Our approach is very di erent since, in a way similar to that of Ambient Calculus, we assume that the process a I ; P ] is an abstraction for both an agent (client) and an object (server). This implies that in our framework mobile objects move without the burden of future obligations at the source location. A client agent willing to invoke a method of a server object, in turn, must approach the server in order to start the communication protocol. In addition, while the work on Ojeblik does not address typing issues, we developed a rich type theory showing how advances in type system for objectoriented languages can be reused in the context of calculi of mobile agents. MA++ is a core calculus on the top of which many other extensions, besides the one with coactions and single threaded types LS00] can be de ned. A rst example is the addition of elds. Unlike what happens in object calculi, where elds can be obtained as parameter-less methods, here elds cannot be encoded. Calling a method does not return a value, but instead spawns a process. The solution is to explicitly add new syntax for elds, which operationally instead of triggering a process returns terms. A di erent possibility is to extend the calculus so that method names have not a distinguished status but are dealt with as ordinary names. This would allow one to restrict them, thus obtaining private methods, and to communicate them, thus obtaining dynamic messages. This is a straightforward modi cation in the untyped calculus but it is quite problematic in the typed case since the possibility of communicating method names would naturally give rise to dependent types. Finally we could imagine to de ne security policies for MA++ and try to apply it to specify and verify real case examples.

7 Future Work

References

AC96] BC00]

M. Abadi and L. Cardelli. A Theory of Objects. Springer, 1996. M. Bugliesi and G. Castagna. Mobile objects. In 7th Workshop on Foundation of Object-Oriented Languages, Boston, 2000. Electronic Proceedings. BCC00] M. Bugliesi, G. Castagna, and S. Crafa. Typed mobile objects. In Proceedings of CONCUR 2000 (11th. International Conference on Concurrency Theory), number 1877 in Lecture Notes in Computer Science, pages 504{520. Springer, 2000. Bru94] B. Bruce, K. A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of Functional Programming, 1(4):127{206, 1994. Car95] L. Cardelli. A language with distributed scope. Computing Systems, 8(1):27{59, 1995. Car99] L. Cardelli. Abstractions for mobile computations. In Secure Internet Programming, number 1603 in Lecture Notes in Computer Science, pages 51{94. Springer, 1999. CG98] L. Cardelli and A. Gordon. Mobile ambients. In Proceedings of POPL'98. ACM Press, 1998. CG99] L. Cardelli and A. Gordon. Types for mobile ambients. In Proceedings of POPL'99, pages 79{92. ACM Press, 1999. CGG99] L. Cardelli, G. Ghelli, and A. Gordon. Mobility types for mobile ambients. In Proceedings of ICALP'99, number 1644 in Lecture Notes in Computer Science, pages 230{239. Springer, 1999.

DBF96] P Di Blasio and K. Fisher. A calculus for concurrent objects. In CONCUR '96, number 1119 in Lecture Notes in Computer Science, pages 655{670. Springer, 1996. FHM94] K. Fisher, F. Honsell, and J. C. Mitchell. A Lambda Calculus of Objects and Method Specialization. Nordic Journal of Computing, 1(1):3{37, 1994. FMLR00] Cedric Fournet, Luc Maranget, Cosimo Laneve, and Didier Remy. Inheritance in the Join Calculus. In Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lecture Notes in Computer Science. Springer, December 2000. GH98] A. Gordon and P. D Hankin. A concurrent object calculus: reduction and typing. In Proceedings HLCL'98, Elsevier ENTC, 1998. Also Technical Report 457, University of Cambridge Computer Laboratory, February 1999. HK96] H. Huttel and J. Kleist. Objects as mobile processes. Technical Report Research Series RS-96-38, BRICS, 1996. Presented at MFPS '96. Jef00] A. Je rey. A distributed object calculus. In 7th Workshop on Foundation of Object-Oriented Languages, Boston, 2000. Electronic Proceedings. KS98] J. Kleist and D. Sangiorgi. Imperative objects and mobile processes. In PROCOMET '98 (IFIP Working Conference on Programming Concepts and Methods). North-Holland, 1998. LS00] F. Levi and D. Sangiorgi. Controlling interference in Ambients. In POPL '00, pages 352{364. ACM Press, 2000. NHKM99] U Nestmann, H. Huttel, J. Kleist, and M. Merro. Aliasing models for object migration. In Proceedings of Euro-Par'99, number 1685 in Lecture Notes in Computer Science, pages 1353{1368. Springer, 1999. PT95] B.C. Pierce and D.N. Turner. Concurrent objects in a process calculus. In Takayasu Ito and Akinori Yonezawa, editors, Theory and Practice of Parallel Programming, Sendai, Japan (Nov. 1994), number 907 in Lecture Notes in Computer Science, pages 187{215. Springer, April 1995. San98] D. Sangiorgi. An interpretation of typed objects into typed -calculus. IC, 143(1):34{73, 1998. Vas94] V.T. Vasconcelos. Typed concurrent objects. In M. Tokoro and R. Pareschi, editors, ECOOP '94, number 821 in Lecture Notes in Computer Science, pages 100{117. Springer, 1994. Wal95] D.J Walker. Objects in the -calculus. Information and Computation, 116(2):253{ 271, 1995.

A Typing rules

Context formation

(Env-empty) (Env-x)

?

`

? W x = Dom(? ) ? X = Dom(? ) ?; x : W ?; X< #A

` 2 ` 2 ` `

(Env-X )

Type formation

? ?; X< #A ;? 0 ?; X< # A ; ? X ? Amb ]

0

` ` ` `

(Type X)

(Type Amb) (Type Cap) (Type Proc)

? Cap ]

`

?

`

? Proc ]

`

?

`

Matching : Re exivity, Transitivity and the following

? ?; X< #A ;? 2 1 + ]< 0 # Amb (` (V )) 21 ] ?; X< # A ; ? X< # A ? Amb (` (V ))

0

` `

k

(Match X)

(Match Amb)

`

i i

`

i

::n

i

i

i

::n

Subtyping and subsumption : Re exivity, Transitivity and the following

(Sub Cap)

0 0

(Sub Proc)

0 0

(Subsumption)

`

Cap ]

Cap

] Proc ] Proc

]

? A:T T T0 ? A:T0

`

Expressions

? ? M1 : Cap ] ? M2 : Cap ] ? ? M1 :M2 : Cap ] ? x : ? (x) ? " : Cap ]

` ` ` ` ` ` `

(name/var) (")

(path)

? a : Amb ] ? M : W ? W < # Amb ] (M 0 ? open a : Cap ] ? M 0 : Cap 0 ]

` ` ` ` `

(open)

(inout)

2 f

in M; out M g)

(Message)

`

? a:W ? W< # Amb `(V 0 ) ] ? M 0 : V 0 ? a send ` M 0 : Cap ]

` ` ` h i

Processes

(pref)

`

? M : Cap ] ? P : Proc ] ? P : Proc ] ? Q : Proc ] ? M:P : Proc ] ? P Q : Proc ]

` ` ` ` ` j

(par)

? ?; x:A P : Proc ] ? ( x:A )P : Proc ] ? 0 : Proc ]

` ` ` `

(restr)

(dead)

( = ( ` (V ) ) 2 ) ? a : Amb ] ?; Z< # Amb ]; z :Z; x :V P : Proc ] ? P : Proc ] ? a (` (x ) . & (z )P ) 2 ; P ] : Proc 0 ]

(Amb)

`

i i i I i i ` I i

`

`

i

i

i

i