# Semantics of Objects as Processes

Basic Research in Computer Science ¡§ BRICS NS-98-5 Huttel & Nestmann (eds.): SOAP ¡¯98 Proceedings

BRICS

Proceedings of the Workshop on

Semantics of Objects as Processes SOAP ¡¯98

Aalborg, Denmark, July 18, 1998

¡§ Hans Huttel Uwe Nestmann (editors)

BRICS Notes Series ISSN 0909-3206

NS-98-5 June 1998

Copyright c 1998,

BRICS, Department of Computer Science University of Aarhus. All rights reserved. Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Notes Series publications. Copies may be obtained by contacting: BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK¨C8000 Aarhus C Denmark Telephone: +45 8942 3360 Telefax: +45 8942 3255 Internet: BRICS@brics.dk BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs: http://www.brics.dk ftp://ftp.brics.dk This document in subdirectory NS/98/5/

Proceedings of the Workshop on Semantics of Objects as Processes SOAP ¡¯98 July 18 Aalborg, Denmark

Hans H¡§ttel u Uwe Nestmann (editors)

Preface

One of the most widespread programming paradigms today is that of objectoriented programming. With the growing popularity of the language C++ and the advent of Java as the language of choice for the World Wide Web, object-oriented programs have taken centre stage. Consequently, the past decade has seen a ?urry of interest within the programming language research community for providing a ?rm semantic basis for object-oriented constructs. Recently, there has been growing interest in studying the behavioural properties of object-oriented programs using concepts and ideas from the world of concurrent process calculi, in particular calculi with some notion of mobility. Not only do such calculi, as the well-known ¦Ð-calculus by Milner and others, have features like references and scoping in common with objectoriented languages; they also provide one with a rich vocabulary of reasoning techniques ?rmly grounded in structural operational semantics. The process calculus view has therefore proven to be advantageous in many ways for semantics and veri?cation issues. On the one hand, the use of encodings of object-oriented languages into existing typed mobile process calculi enables formal reasoning about the correctness of programs; on the other hand, using standard techniques from concurrency theory in the setting of calculi for objects may help in reasoning about objects, e.g. by ?nding appropriate and mathematically tractable notions of behavioural equivalences. Encodings may also help clarify the overlap and di?erences of objects and processes, and suggest how to integrate them best in languages with both. The aim of the one-day SOAP workshop, which is a satellite workshop of ICALP 98, has been to bring together researchers working mainly in this area, but in related ?elds as well, where other process models or calculi are used as a basis for the semantics of objects. Among the submitted abstracts, six were recommended by the programme committee (Mart? Abadi, Hans H¡§ ttel, Josva Kleist, and Uwe Nestmann) ?n u and are presented in these proceedings. According to the more informal character of the workshop, there was no formal refereeing process. It is expected that the abstracts presented in these proceedings will appear elsewhere at other conferences or in journals. We would like to thank the organizers of ICALP ¡¯98 for helping us set up the SOAP workshop and BRICS for the publication of these proceedings.

June 1998 3

Hans H¡§ ttel u Uwe Nestmann

4

Table of Contents

The workshop will be held in Aalborg Congress and Culture Centre on July 18, 1998, in the order appearing in these proceedings. Carlos Herrero, Javier Oliver Object-Oriented Parallel Label-Selective ¦Ë-calculus Claudia Balzarotti, Fiorella De Cindio, Lucia Pomello Observation equivalences for type and implementation inheritances Ant?nio Ravara, Pedro Resende, Vasco Vasconcelos o Towards an Algebra of Dynamic Object Types Andrew D. Gordon, Paul Hankin A Concurrent Object Calculus: Summary of the Operational Semantics Silvano Dal-Zilio Quiet and Bouncing Objects: Two Migration Abstractions in a Simple Distributed Blue Calculus Hans H¡§ ttel, Josva Kleist, Uwe Nestmann, Davide Sangiorgi u Surrogates in ?jeblik: Towards Migration in Obliq

7

17

25

31

35

43

5

6

Object-Oriented Parallel Label-Selective

-calculus3

Carlos Herrerox Javier Oliverx

x

DSIC, UPV, Camino de Vera s/n, Apdo. 22012, 46022 Valencia, Spain. E-mail: cherrero,fjoliver@dsic.upv.es.

Abstract

LCEP is a calculus for modelling concurrent systems. The eorts to use it to represent object oriented features have been successfully treated in this paper. We present an operational semantics for a parallel object-oriented programming language by means of a phrase-by-phrase translation from the language into an extension of LCEP in which only a few changes from the original LCEP are made. Keywords: Concurrency, Extensions of -calculus, Object-Oriented, Process Algebras.

1

Introduction

We can nd many studies in computation to produce an elegant semantics which correctly denes languages with concurrent features. The role played by the -calculus in computation theory is well-known but while it was adopted by D.S. Scott and C. Strachey as a semantic basis for programming languages, it cannot be successfully used with concurrence features. In 1980, R. Milner proposed CCS, [7], which is a calculus for modelling concurrent systems. His contribution was to view computational entities as agents whose interaction is the basic behavioural unit. This calculus was the basis for the -calculus [8] which emerged as a renement of CCS with two primitive notions as foundations: the name and the agent. A name is used to provide access to agents. Specically, two agents that share a name can interact by using it. In addition, an agent can send a name in an interaction, and therefore one agent can transfer its ability to interact with other agents to the other. On the other hand, with the label-selective -calculus of H. A t-Kaci [1] the distinction between terms and channels appears. A term plays the role of an agent of the -calculus and a channel (numeric or symbolic labels) represents the way through which terms can send information. With the extension of this calculus to LCEP [6] (Parallel Label-Selective calculus) we have a complete calculus for modelling concurrency by using numeric and/or symbolic labels and parallel operators, and also by representing polyadic functions. Among the proposed approaches to parallel programming, the disciplines which are characteristic of parallel object-oriented programming have many desirable features. However, providing adequate semantics for these languages is very complex. The family of POOL languages is outstanding among the works in this eld. This is the starting point for this work. In particular, the operational semantics of a member of this family of languages appeared in [2] and was later expanded by the denotacional semantics [3] based on metric spaces. Moreover, there are other semantics available which are associated to the family of POOL languages using process algebras [10]. The nature of the language suggests that correct models are complicated. More precisely, attempts to discern a clear vision of the central concept (i.e. the object) is very complex, although already important advances have been made in this direction. In this article, we show a semantics in LCEP of a slightly modied version of POOL, via a phrase-by-phrase translation. Each syntactic entity is represented as a parameterized agent. The representation of composite entities is constructed by using the operators of the calculus. In particular, we are interested in modelling

3 This

work was partially supported by CICYT, TIC 95-0433-C03-03.

7

the communication, the invocation of methods, and the transfer of results between objects. An object is represented as a composed term which is able to interact with others by asking for the execution of a certain method. The remainder of the work is organized as follows. In Section 2, LCEP is brie
y dened. In Section 3, the POOL language is described. In Section 4, we show the translation function of the dierent instructions from POOL into LCEP. In Section 5, we present an example of a POOL program translation. Finally, Section 6 presents some concluding remarks.

2 The Parallel Label-Selective

-calculus

The Parallel Label-Selective -calculus (LCEP) [9] is the calculus that we use for modelling the LCEPOO language, which originated from a previous proposal by H. A t-Kaci (the label-selective -calculus). This calculus is an extension of the -calculus in which function arguments are selected by labels. Symbolic and numeric labels can be used to name the communication channels. This has not been possible in other proposals and it allows for the use of currying and the labeled specication of parameters. It makes the ordering of the actual parameters in a function call independent of the presentation order of the formal parameters in the denition. Let V = fx; y; z; : : :g be a set of variables, and C = fa; b; c; : : :g be a set of constants. P represents a channel name from a set of labels L = IN [ S , where m; n; : : : denote numerical labels taken from IN. S = fp; q; : : :g is a set of symbolic labels. IN \ S = ;. 0 represents the null process. The language of the formal system is M. It is dened as follows: P

M ::= 0 j a j x j P x:M j P M j M k M j M M j (M + M ) j !M b ::= number j symbol

Usually, the terms of this signature are called EP -terms. In concurrent programming, the terms of M represent processes. Operation symbols ; k; +; ! are considered as process constructors. The communication P x: (abstraction or input) and P b (parameter passing or output) are also considered as process constructors, whose eect over a process M is to dene processes (P x:M y P M , respectively) which are involved in functional b applications under certain given conditions. Constants, variables and the null process form the atomic symbols of the language. The interpretation of the process constructors is as follows: sequential composition (): it denes a process M N from the processes M y N . The process N is executed after M ; parallel composition (k): it denes a new process M k N from the processes M and N . Both processes are executed simultaneously; non-deterministic choice (+): M + N shows the capability of M or N (either one or the other) to take part in a communication. A communication can be made by one of them and the other disappears; replicator (!): !M denes a process which produces the multiple generation of M . It acts as a warehouse, where it is possible to take an innite number of the process M . b Operators have the subsequent priority order: ! > P > > P x: > + > k. An occurrence of the variable x is bound in a process M i it is in a term P x:M (for all P 2 L). In any other case, the occurrence of x is free. If x has, at least one free occurrence in M , we say that x is a free variable of M . We call F V (M ) the set of free variables of M . A process is closed if it does not have free variables. The relations between the processes are described in terms of communications. The constructors P x: and P provide the processes M and N with the possibility of communicating through a channel b labelled with P 2 L as follows: constructor of input (P x:): through channel P process P x:M can receive a process which replaces the free occurrences of x in M by the incoming process through b b this channel; constructor of output (P ): process P M can send a process N through channel P . It then becomes inactive. In addition, a partial order relation is dened in the set of labels which we denote as L . It is required as a condition for the relation that the numerical label 0 be the minimum of the ordered set. We use the partial order relation in the set of labels (among others) to represent the

8

application order of the real parameters to the formal parameters of a function, which is analogous to how it is done in the -calculus in order to treat the problem of parameterization in function calls. For more complete information about the calculus, see [9].

3

Parallel Object-Oriented Language (POOL)

When we work with the object-oriented programming style, we always describe a computational system as a collection of self-contained entities possessing data and methods. These entities are called objects. Objects interact by sending messages. There are two kinds of messages: a request by the sender for the receiver to execute one of its methods with its parameters (client to server), and a reply (server to client) in response to such a method invocation. The parameters and the reply are object references. The system evolution depends on the communications, and the creation/destruction of objects is made in computing time. In the variant of POOL considered [2], a program is a sequence of class declarations together with an indicator of which class constitutes the object root. The declaration of a class consists of a sequence of variable and method declarations together with a sentence, the body of the class. Each object is an instance of a class and its creation executes a copy of the body of the class in parallel with all the other existing objects using its own copies of the variables and class methods. The sentences are built by means of the sequential, conditional and iterative operators of the expressions, instructions of assignment and the answer instruction, which means that an object accepts a request of execution of one of its methods. Among the expressions, we can nd new(B), whose evaluation creates a new object of the class B and returns the reference to this object; self, whose evaluation returns a reference to the object in which it happens; and E !M (E1; : : : ; En), whose evaluation implies the left to right evaluation of the E; E1; : : : ; En, expressions, the sending to the object for which the value of E is a request to execute method M with these parameters. The value of the expression is the reference which has been returned by the object owner of the invoked method. The activity of the transmitter is interrupted until this value is received. Therefore, the expressions in POOL, the declaration of variables, and the sentences are: E ::= b j new(B ) j self j X j E !M (E1; : : : ; En) j M (E1; : : : ; En) j j V decs in E j S ; E V decs ::= var X1 : A1 ; : : :; Xn : An S ::= X := E j answer j E j S 1; S 2 j if E then S1 else S2 j while E do S

composition, choice, a

These sentences are

assignment, answer (an object accepts the request), expression, sequential and iteration, respectively. Note that an expression is considered as a sentence. The declaration of methods (Mdec), sequences of method declarations (Mdecs), declarations of class (Cdec), and units (Udec) are given by:

M dec M decs Cdec U dec

::= ::= ::= ::=

method M (Y1 : C1; : : : ; Yp : Cp ) C is E M dec1 ; : : :; M decq class A is V decs; M decs with body S unit U is Cdec1 ; : : :; Cdecr with root A

where C is the resulting method class, Y1 ; : : :; Yp are the formal parameters, and E is the body. The language is strongly typed, and several conditions are imposed. For example, in a unit declaration, A must be the name of one of the classes declared in Cdec1; : : : ; Cdecr and if an expression E !M (E1; : : : ; En) appears in one of the class denitions and the type of E is C , then it must have a class C and a called method M of the appropriate type. The classes are only considered if they fulll all the imposed conditions. See [2] for further details. The language diers from POOL in some small syntactic details. The signicant dierences are that there is a general sentence answer (any method can be invoked) and not a conditional one (answer + select), which allows the exclusion of certain methods, and that the standard class

9

integer

does not appear. These dierences simplify the proposal language and it can be easily translated to LCEP. For further details about the operational semantics of POOL and of the current version of POOL see [2] and [11], respectively.

4

The Translation

It is obvious that each syntactic entity is represented as a EP -term and composite entities are represented by their components. LCEP cannot use multiple parameters as channels. However, we can communicate through numeric channels (using currying we can model polyadic functions) or by sending some processes in parallel. This problem has an easy treatment in -calculus, because we can send names of channels through the channels. In LCEP we have a numeric or symbolic label P , which represents a channel through which we b send a process N from an output P N into an input p x:M , where the occurrences of x in M are replaced by the process N , i.e. every valid EP -term (variables, constants, processes, etc. but not channels). The idea of conversion is to use the name of the channel to substitute the name of the agent. This channel is then used to send the parameters and a EP -term, which works as output of the result instead of the name of the method and the associated parameters. Therefore, the sender process is like an input which is waiting for the reply through the same channel. When we need to send a name or channel, we actually send an output process through this channel. Consider an expression as a variable value or an output process which communicates or starts the expression from the represented channel. In this paper, the process perspective is presented. Therefore, the denition of classes comes from the denition of the objects'behaviour. To simplify the notation, construction blocks are used:

V alue(l; v) N ull(l) W ait(l; l0 ) Return(l; l0; l00)

bv l b0 l l0 v:V alue(l; v) b l00 v:l0 v N ull(l)

Value(l,v) represents the evaluation of an expression or variable. Null(l) put through the channel l of the null term. Wait(l,l0 ) is an abstraction evaluation. Return(l,l0 ,l00) is its complement.

is translated as an out(a waiting) and a later

Simple POOL expressions are translated into LCEP as follows: [new(B )](l; k) [self ](l; v) [Y ](l; y) [V ar Y ](y; v) V ar(y; v)

b(ret x:b x) k l V alue(l; v) b(b 0) y v:V alue(l; v) + b(b v0 ) y v:V alue(l; v) yr yu V ar(y; v) y x1 :(x1 k r x:(b v V ar(y; v)) k u v0 :(b v0 V ar(y; v0 ))) y y

The creation of a new object is modelled as a call to the class and the later reception of the new object identier (Channel). This is the only exception in which we can see a label as a variable. Using a variable is equivalent to updating it or to consulting it. In any case, the declaration of a variable is the parallel composition of two answers. POOL classes'declaration in LCEP is: c ! k x:((x k ret ci) N ewobject(ci )) [Cdec](k) N ewobject(ci ) ([S ] k [V decs](~; ~) k [M decs](m)) yv ~ [M dec1](m1 ) k : : : k [M deci](mi ) [M decs](m) ~ In addition, we are going to make the request for the execution of a remote method into LCEP. First, let us see the translation of an object c0 which requests the execution of a remote method m with only one evaluated parameter.

b b b c [0!M (1 )](l; c0; m) c0 (m 1 m (m x:ret x) ret x:b x) W ait(l; l0 ) l

0

10

In this case, a term is sent to the object (received by an answer into the object body), and then the object waits using Wait(l,l0 ). The term which has been sent will execute three actions: (1) send the parameter to the method; (2) send a term which produces the answer of the method; (3) make a term which stays in the answer and which really sends the result to the Wait(l,l0 ). The declaration of a one-parameter method is:

! M method(m) [M dec](m) M method(m) M handle(m) k [V ar Y1 ](y1; v1 ) k g x:[E ](m) M handle(m) m x:y1 (b x) y1 x:0 m x:(x k b 0) b u g

As you can see, the receipt of a parameter is translated by updating the variable Y1, joined to the parallel composition with the answer sender term and with another that synchronizes with the evaluation of the method body. Now let us see a similar process, but using multiple parameters:

b b b b c [0!M (1 ; : : : ; n)](l; c0; m) c0 (m 1 : : : m n m (m x:ret x)) (ret x:l x) W ait(l; l0 ) b

0

The method declaration into the server object is:

! M method(m) [M dec](m) M method(m) M handle(m) k [V ar Y1 ](y1; v1 ) k : : : k [V ar Yn ](yn ; vn) k g x[E ](m) M handle(m) m x:y1 (b x) y1 x:0 m x:(b x) yb x:0 m x(x k b 0) b u b u g n

If, instead of the evaluated parameters, we have expressions (knowing that a POOL expression must be left-to-right evaluated), we require that the evaluation of an expression Ei not start, since the evaluation of the expresion Ei01 has nished. This eect is successfully represented by:

b b b b d [0!M (1 ; : : : ; i01; Ei; : : : ; En)](l; c0 ; m) c0 (m 1 : : : m i01 li i :m i gi+1 0 : : : ln n :m n m (m x:ret x)) b b c ret x:l x k [Ei](l1 ) k gi+1 x:[Ei+1](li+1 ) k b k : : : k gn x:[En](ln ) W ait(l; l0 )

0

It is easy to see that the treatment of this expression may be similar to the treatment of a local call to execution of a method. Actually, it only diers in one feature. In a remote call, we need to generate a EP -term that really executes the sending of the parameters, and makes the answer to the original object that is waiting in a Wait(l,l0) instruction. In a local call, we do not have an answer because the purpose of a local invocation is execution, and not reply. This is the reason why the EP -term, which results after the evaluation, is the sending of the expression. Therefore, the translation of a local call of one evaluated parameter method is:

b b [M (1)](m; l) m 1 m (m x:b x) l

A multiple evaluated arguments method is as follows:

b b b [M (1; : : : ; n )](m; l) m 1 : : : m n m (m x:b x) l

If we have not evaluated parameters and what we really have are expressions (as in the remote call), then the translation into LCEP is:

b b b d [M (1; : : : ; i01; Ei; : : : ; En)](m; l) (m 1 : : : m i01 li i :m i gi+1 0 : : : ln n :m n m (m x:b x) k [Ei](li ) k b b l k gi+1 x:[Ei+1](li+1 ) k : : : k gn x:[En](ln ))

~ For a local declaration of variables with V decs var Y into an expression, we can model into LCEP as: ~ yv [V decs in E ](l; : : : ; ~; ~) [E ](l; : : :) k [V ar Y](~; ~) yv ~ yv where [V ar Y](~; ~) [V ar Y1 ](y1; v1) k : : : k [V ar Yv ](yv ; vv ).

11

Now, let us see the translation into LCEP of the auxiliary expressions whose denitions were postponed: [W ait( )](l; l0 ) [E ) ](l; : : :) [E; ](l; : : :) [](~; ~) yv [nil](l) [Y := E ](l; : : :; y) [answer](a; l)

W ait(l; l0 ) [E ](l0; : : :) k Return(l; l0; l00) [E ](l; : : :) k [](~; ~) yv V ar(y1 ; v1 ) k : : : k V ar(yn ; vn) N ull(l) [E ](l0; : : :) k l v0 :(b(b v0 ) y v:N ull(l)) yu a x:x N ull(l)

0

We express the assignment as the parallel composition of two EP -terms: one which evaluates the expression and sends the result through the auxiliary channel l0, and the other which receives the result of the expression from this channel and updates the variable Y by assigning the value of the expression. With regard to the answer which replies to the request of remote invocation of methods, [E0!M (E1; : : : ; En)], we can see that it accepts any request of any ready method, allowing to the replicator of the method to execute a copy of itself. It returns the result (to activate the client process which is in a wait instruction) and later returns a null through its own channel l to nish. Although only the last channel is really dened in the answer, all the others are sent from the b b b c client, as a EP -term like m 1 : : : m n nm (m x:ret x) retx:b x if there is no unevaluated l expression. The fundamental part of the EP -term are the last two terms of the sequence. The second to the last term is a sender through the channel ret of the reply in a method execution. The last one takes that answer and re-sends it to the Wait(l,l') in the other process and it then becomes inactive. The basic expression of the standard class Bool is as follows:

0

[true](l; bk) bb (b(ret x:b x) l x:V alue(l; x)) l k t [false](l; bk ) bb (b(ret x:b x) l x:V alue(l; x)) l k f

0 0

And the standard class [Boolean](bk ) BoolClass(bk ) Bool(b; bk )

Boolean

is:

BoolBody(b) BoolV al(m1 ) BoolN ot(m2 ; m1 )

BoolAnd(m3 ; m1)

(BoolClass(bk ) k Bool(b; bk )) c d c d ! bk x:(x k (t x:(x k ret true 0) k f x:(x k ret false 0))) (! BoolBody(b) k ! BoolV al(m1 ) k ! BoolN ot(m2 ; m1) k k! BoolAnd(m3 ; m1)) b x:x c c m1 x:(m1 x k m1 y:(m1 z:(y k m1 z ))) c c c m2 x:(m1 x m1 (m1 x:m2 x)) m2 x:(x k true y:m2 false 0 k false y:m2 true 0) c d c d c c c c m3 x:(m1 x m1 (m1 x:m3 x)) m3 x:(x k true y:(m3 x:(m1 x c c c d m1 (m1 x:m3 x)) m3 x:(x k truey:(m3 true 0) k k false y:(m3 false 0)) k false y:(m3 z:m3 false 0)) c d c d

0 0 0 0 0

To model the conditional instruction we have: [if E then S1 else S2 ](l) BoolEval(l0 ; l1 ; l2) k [E ](l0) k l1 x:[S1](l) k l2 x:[S2](l) c c l x:b(m1 x (m1 (m1 x:ret x))) BoolEval(l0 ; l1; l2 ) b c (retx:x k true x:lb 0 k false x:lb 0) 1 2

0

With regard to the sequence of sentences, if we have the sentence [S1; S2 ], and we suppose that the sentence S1 is an expression, then: [S1; S2 ](l; : : :) [S1 ](l0; : : :) k l v:[S2 ](l; : : :)

0

where v is a variable which appears in S2 and is a bound variable.

12

CLASS PHILOSOPHERS VAR eat : boolean sig : boolean chopl : CHOPS chopr : CHOPS METHOD ToEat( ) : PHILOSOPHERS BEGIN WHILE not Eat DO sig := true; WHILE sig DO sig := chopl!Takechop( ) OD; sig := chopr!Takechop(); IF sig THEN eat := false; chopl!Leavechop( ) ELSE eat := true FI OD RESULT SELF END; YDOB BODY eat := false; WHILE true DO Toeat( ) Tothink( ) OD METHOD Tothink( ) : PHILOSOPHERS BEGIN chopl!Leavechop( ); chopr!Leavechop( ); eat := false; RESULT SELF END;

CLASS CHOPS VAR freechop : boolean METHOD Takechop ( ) : boolean BEGIN IF freechop THEN freechop := false; RETURN false ELSE RETURN true; FI END; METHOD Leavechop ( ) : CHOP BEGIN freechop := true; RESULT nil END; BODY freechop := true; WHILE true DO answer OD YDOB

Figure 1: The POOL philosophers problem. On the contrary, if the sentence S1 is not an expression, therefore, v is not bound in S2 , and the behaviour of the process is like [S1 ](l0; : : :) [S2 ](l; : : :), with l0 : N ull. Knowing this and using the dual behaviour of expressions and non-expression sentences in the translation to LCEP of iterative instructions, we can nd a new example of the use of the standard class Bool by BoolEval. [while E do S ](l; : : :) Loop(l; l0 ; : : :) k ! l v:Loop(l; l0 ; : : :)

0

If S is an expression then c is a bound variable and therefore: Loop(l; l0 ; : : :) (BoolEval(l 00 ; l1; l2 ) k [E ](l00) k l x:[S ](l0; : : :) k l x:V alue(l; v))

1 2

If S is not an expression, then v is a free variable in S and then: Loop(l; l0 ; : : :) (BoolEval(l 00 ; l1; l2 ) k [E ](l00) k l x:[S ](l0; : : :) k l x:N ull(l))

1 2

5

Example of translation

To re
ect the translation of a POOL program into LCEP, we use an easy variant of the well-known philosophers problem [5], in which we pay attention to the communication between the dierent objects. To model that behaviour in POOL, we consider two object classes: the philosopher class and the chop class. We are basically interested in communication and method invocation. Therefore, we center our attention on the implementation of the classes, and we do not show units or specications in our solution. We are not looking for an ecient solution to the concurrence problem. Therefore, we do not pay attention to aspects such as the non-deterministic choice between left and right chop (we necessarily take the left one before the right one). We can see the POOL example in Fig. 1. From lack of space, we only show some parts of the translation following a similar scheme as in Section 4. The translation of the philosophers'class declaration to LCEP is as follows: [Cphils] ! phils x:((x k ret phili ) N ewobject(phili )) N ewobject(phili ) (BODY phil(phili )) k [V decs](eat; sig; chopl; chopr) k k [M decs](toeat; tothink)) An example of variable declaration is:

0

c

V ar(eat; vb ) eat x1:(x1 k r x:(eat vb V ar(eat; vb)) k k u v0 :(eatvb V ar(eat; vb )))

0

c

13

The invocation of the method takechop of an object as: [chopl ! takechop( )](l; chopl; tchop) [chopr ! takechop( )](l; chopr; tchop)

chop

from a philosopher is modelled in LCEP

0

d d c chopl (tchop (tchop x:ret x) ret x:b x) W ait(l; l ) l0 0 d d c chopr (tchop (tchop x:ret x) ret x:b x) W ait(l; l ) l0

)

Furthermore, the denition of the method takechop(

is:

[M takechopdec](tchop) ! M takechop(tchop) M htakechop(tchop) k g x:[E takechop](tchop) M takechop(tchop) tchop x:(x k b 0) M htakechop(tchop) g An example of a local call appears at the method toeat( ) in a philosopher body: [toeat()](toeat; l0) d toeat(toeat x:b l0

x)

And the declaration of method toeat( ) is: [M toeatdec](toeat) ! M toeat(toeat) M htoeat(toeat) k g x:[E toeat](toeat) M toeat(toeat) toeatx:(x k b 0) M htoeat(toeat) g Our example contains a conditional instruction into the body of method toeat( ) in the class

chop:

IF FI

sig

THEN ELSE

eat := false;

chopl ! Leavechop() eat := true

Therefore: cr [if SIG then S1 else S2 ](l) (BoolEval(l0 ; l1; l2) k (sig (b 0) sig v:V alue(l0 ; v)) k k l1 x:[S1](l) k l2 x:[S2](l)

philosopher:

The following is a practical example of the translation of the loop into the body of object class

WHILE DO OD

true

Toeat( ) Tothink( )

Therefore:

W hile0 (l) [while true do S3 ](l) Loop0 (l; l0) k ! l c:Loop0(l; l0 ) Loop0 (l; l0) (BoolEval(l00 ; l1 ; l2) k [true](l00; bk ) k l1 x:[S3](l0 ) k l2 x:null(l))

0

S3 is the sequential composition of procedures

Toeat()

and

0

Tothink(),

which can be translated as:

[toeat( )](toeat; l0 ) k l v:[tothink( )](tothink; l) [S3](l0 ) 0 d b toeat toeatx:l x) [toeat( )](toeat; l ) d b [tothink( )](tothink; l) tothink tothink x:l x)

0 0

where v is a free variable in [tothink( )](tothink; l).

14

6

Conclusions and future work

An extension of LCEP has been presented. Under a process perspective, this extension can model a simple version of a parallel object-oriented language, LCEPOO. The phrase-by-phrase translation process has been made by modelling object denition, management, communication, and evolution features. The object activities are synchronized by sending messages which contain references to other system objects. Among the characteristics of LCEP, we can not nd the sending of communicating channels. The absence of this feature has not been an obstacle for the modelling of the behaviour of the chosen POOL variant. We have incorporated the possibility of sending variables (channels) only for the modelling of the object generation. As we have shown, LCEP is an eective tool which has sucessfully been used to model parallel and concurrent processes as well as to model object-oriented language features. A translator system from a high level language (ALEPH) into LCEP is already available [4]. By transferring the proposal extension to that system, we can obtain an explicitly parallel high-level language with object-oriented features.

References

1. H. At-Kaci and J. Garrigue. Label-Selective -Calculus: Syntax and Con
uence. In Proc. of the 13th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 761 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1993. 2. P. America, J. de Bakker, J. Kok, and J. Rutten. Operational Semantics of a Parallel ObjectOriented language. In Proc. of the 13th Symposium on Principles of Programming Languages, pages 194{208, 1986. 3. P. America, J. de Bakker, J. Kok, and J. Rutten. Denotational semantics of a parallel object-oriented language. In Information and Computation, volume 83, pages 152{205. 1989. 4. L. Climent, M.L. Llorens, and J. Oliver. LCEP as an Abstract Machine. Technical Report DSICII/38/97, UPV, 1997. 5. E.W. Dijkstra. Cooperating Sequential Processes. In F. Genus, editor, Programming Languages, pages 43{112. Academic Press, London, 1968. 6. S. Lucas and J. Oliver. Parallel label-selective -calculus (LCEP). In M. Alpuente, R. Barbuti, and I. Ramos, editors, Proc. of 1994 Joint Conference on Declarative Programming GULP-PRODE'94, pages 125{139, 1994. 7. R. Milner. A Calculus of Communicating Systems. volume 92 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1980. 8. R. Milner. The polyadic -calculus: A tutorial. In F.L. Brauer, W. Bauer, and H. Schwichtenberg, editors, Logic and Algebra of Specications. Springer-Verlag, Berlin, 1993. 9. J. Oliver. Extensions of the -calculus for Modelling Concurrent Processes. PhD thesis, DSIC (UPV), 1996. 10. F. Vaandrager. A process algebra semantics in POOL. Applications of Process Algebra, Tracts in Theoretical Computer Science, 17:173{236, 1990. 11. D. Walker. Objects in the -calculus. In Information and Computation, volume 116, pages 253{271. 1995.

15

16

Observation equivalences for type and implementation inheritances

Claudia Balzarotti, Fiorella De Cindio, Lucia Pomello Dipartimento di Scienze dell'Informazione, Universit? di Milano via Comelico 39 - 20135 Milano (Italy) e-mail: decindio@dsi.unimi.it, pomello@dsi.unimi.it

EXTENDED ABSTRACT

The main entity of the object-oriented languages is the object, which is generally defined by a class. A fundamental relation between classes is inheritance, that originally indicated a relation is-a among classes. On the other hand, the success of object-oriented programming languages is due to the use of inheritance for code-reuse. As shown in [Ame89], inheritance is often used in these two different ways. Our aim is studying the inheritance relation in concurrent object-oriented languages, formalising these aspects. The integration of object-orientation with concurrency, yielding systems of active objects modelled as concurrent processes, has given the possibility of using theoretical tools, such as the notions of observation equivalences, for the study of inheritance and subtype relations. In particular, the place-transition duality in Petri nets [BRR87] allows the definition of two types of equivalences between nets, based on action observation and on state observation [PRS92]. They have been used for defining the semantics of inheritance relations. Among the various proposals in the literature (see for example [NP92] , [AD95,96]), we take into consideration those proposed by Nierstrasz [Nie93] and van der Aalst and Basten [AB97] for what concerns action observability, while we consider the approach of CLOWN [BCD97] for what concerns the state observability. Nierstrasz?s hypothesis is that the sequences of requests that an object can accept constitute a regular language. Moreover, Nierstrasz defines a preorder based on failures, the Request Substitutability preorder (RS-preorder, ¡ÜRS), and considers this preorder as the semantics of the subtyping relation according to the Wegner and Zdonik?s substitutability principle [WZ88]. Van der Aalst and Basten introduce preorders too, based on the branching bisimulation equivalence and two operators, the encapsulation operator dH and the abstraction operator t I, that, respectively, remove and label as not observable the transitions corresponding to the methods of the subclass not inherited from the superclass. CLOWN uses an inheritance relation based on the State Transformation preorder (STpreorder, ?ST) [PS91], that compares systems with respect to their state space. Preorders are better suited than equivalence notions for modelling the behaviour extension. We consider Elementary Net (EN) systems [BRR87], the basic class of Petri Nets. We denote as LEN systems the labelled EN systems in which the actions are observable. In the following, we discuss through examples the previous approaches.

17

Example 1 This example is taken from Nierstrasz?s paper [Nie93]. In figure 1, the class VAR, that represents a variable, is subclass of the class BUF, that represents a one place buffer. Rephrasing Nierstrasz from CCS to Petri nets, the RS-preorder between the LEN system associated to the class VAR and the LEN system associated to the class BUF is satisfied, i.e. ?VAR ?RS ?BUF. However, we believe that this example is somehow misleading: in fact a variable is not a buffer, but a buffer can be implemented through a variable.

CLASS BUF put

p1 get CLASS VAR q1 put

p2

put q2 get

Figure 1

Example 2 This example is taken from [BCD97]. Figure 2 shows a multiple inheritance hierarchy between printers. In CLOWN, this hierarchy is studied through the ST-preorder, which considers the state (place) observation. however, the exhibited behaviour of objects that are instances of these classes, is better captured by observation of actions, i.e. of transitions. Therefore we would like to build the same hierarchy by using notions based on action observation. Therefore our work aims at giving the semantic characterisation of two forms of inheritance in concurrent context. According to the terminology used in [CHC90], we use the term type inheritance to indicate the subtyping, i.e. the is-a relation between classes, and the term implementation inheritance to denote the code-reuse. In the first case, we study the external observable behaviour of an object, while in the second case we study the internal structure of an object. Therefore, we base the first preorder on failure, since bisimulation distinguishes systems also with respect to some aspect of internal structure, while in the second case we consider ST-preorder. While this latter does not require modifications w.r.t. the original definition, we need to integrate the two approaches by Nierstrasz and van der Aalst and Basten, since the notions defined by them doesn?t deal with all cases where there exists the relation is-a 18

between a subclass and a superclass. To this purpose we define a further operator, namely the renaming operator rR,S, and new preorders based on action observation.

CLASS ROOT create leave unborn alive 1

dead

CLASS MONO PRINTER unborn create 1 load 1 ready print 1 reset done unborn CLASS LOCKER create 1 lock 1 frozen 1 unlock

idle dead leave

unborn

CLASS PRINTER create load 1 1 idle ready 1 reset print

free dead leave

dead

leave

unborn

CLASS LOCK PRINTER create load suspend 1 1 1 idle ready 1 reset print 1 resume stop

dead

leave

Figure 2

Formally, we associate to a class a LEN system ? = (B,E,F,cin,h), where (B,E,F) is an Elementary Net, cin ? B is the initial case, h: E ? L is the labelling function that associates to each event a class method belonging to L. For each R ? L and for each set of labels S such that S?L=? and |S| = |R|, we define a bijective function s : R ? S, that maps each element of R into a new label. Let L' be a superset of S containing L - R, i.e. S ? L' and L - R ? L'. On the basis of the function s we define the renaming function: r : L ? L' that maps each label into a new label in the following way: 19

(1) r(x) = x if x ? R (2) r(x) = y if x ? R, y ? S and s(x) = y. This function r is injective, since the function s is bijective. We define the renaming operator rR,S in the following way: rR,S(?) = ?' such that ?'= (B,E,F,cin,h'), where h'= r ¡ã h.

Now we can give the definitions of four preorders based on the Nierstrasz?s RSpreorder and on the encapsulation, abstraction and renaming operators. In the following, ?A and ?B are LEN systems associated to a class A and a class B, while LA and LB are the sets of event labels associated respectively to ?A and ?B and corresponding to the methods of the classes A and B. The first preorder, the strong substitutability, is equivalent to the RS-preoder.

Definition 1 ?B is less or equal to ?A w.r.t. strong substitutability, denoted ?B ?SF ?A, if and only if there exists a set H ? LB such that: dH(?B) ?RS ?A. If ?B ?SF ?A then an object of class A can be substituted for an object of class B and the environment will not be able to notice the difference, i.e.: if an object of class A may accept after a request sequence w another request a, then an object of class B must accept the request a after the request sequence w, whatever is the reached state. The new methods added in class B are considered as not available through the encapsulation operator dH. The second preorder, the strong substitutability with renaming, is less restrictive than strong substitutability. Definition 2 ?B is less or equal to ?A w.r.t. strong substitutability with renaming, denoted ?B ?SFR ?A, if and only if there exist a set H ? LB, a set R ? LA and a set S ? LB such that: S ? LA = ? and dH(?B) ?RS rR,S(?A). If ?B ?SFR ?A, then an object of class A can be substituted for an object of class B but the environment must make allowance for class A methods that are renamed in class B by the renaming operator rR,S. The third preorder, the weak substitutability, is another extension of the strong substitutability. Definition 3 ?B is less or equal to ?A w.r.t. weak substitutability, denoted ?B ?SD?A, if and only if there exist a set H ? LB and a set I ? LB such that : I ? H = ? and tI ¡ã dH(?B) ?RS ?A.

If ?B ?SD ?A, then an object of class A can be substituted for an object of class B and the environment will not be able to notice the difference since the new methods added in class B are either considered unobservable, through the abstraction operator t I , or considered unavailable, through the encapsulation operator dH.

20

The fourth and last preorder, the weak substitutability with renaming, is the weaker preorder. Definition 4 ? B is less or equal to ?A w.r.t. weak substitutability with renaming, denoted ?B ?SDR ?A, if and only if there exist a set H ? LB, a set I ? LB, a set R ? LA and a set S ? LB such that: I ? H = ?, S ? LA = ? and tI ¡ã dH(?B) ?RS rR,S(?A). If ?B ?SDR ?A, then an object of class A can be substituted for an object of class B and the environment must consider the renamed methods, while the new methods are either considered unobservable, through the abstraction operator tI , or considered unavailable, through the encapsulation operator dH. The formal proofs that these definitions are sound, i.e.: that the relationships so defined are indeed preorders, are in [Bal98]. Figure 3 shows the relations between preorders. strong substitutability (? SF ) strong substitutability with renaming (? SFR) weak substitutability (? SD ) weak substitutability with renaming (? SDR )

Figure 3

Now we can formalise the notion of type inheritance and implementation inheritance. Definition 5 Let ?A and ?B be LEN systems associated to a class A and a class B. Then B is subclass of A with respect to type inheritance if and only if ?B ?SDR ?A. The notion of implementation inheritance is based on the State Transformation preorder (?ST ) [PS91], which compares systems by observing local states and is such that ?A ?ST ?B if and only if the state space of ?A is a substructure of the state space of ?B such that for any observable local state transformation in ?A there is a corresponding observable local state transformation in ?B. Definition 6 Let ?A and ?B be EN systems, associated to a class A and a class B, in which some appropriate places are observable. Then B is subclass of A with respect to implementation inheritance if and only if ?A ?ST ?B. These definitions solve Example 1 and 2 above, as discussed in the following.

21

Example 3 In figure 4, the class BUF represents a one place buffer, while the class V A R represents a variable. The class V-BUF represents a one place buffer implemented through a variable, which inherits from both classes BUF and VAR. The class V-BUF is subclass of BUF with respect to type inheritance, as it preserves the requests that can be accepted from clients: ?V-BUF ?SDR ?BUF . It is subclass of VAR with respect to implementation inheritance: ?BUF ?ST ?V-BUF, as the VAR methods "assign" and "get_item" are used for implementing the buffer's "put" and "get" methods. This captures the intuition that one cell buffer can be implemented with variables.

unborn dead

create

CLASS BUF

CLASS VAR put full get unborn allocate alive dead initialize idle deallocate get_item assign

empty leave

(type inheritance )

unborn create alive put

is-a

CLASS V-BUF get full put leave

(implementation inheritance )

empty leave dead

uses

Figure 4

Example 4 The classes of the printer hierarchy in figure 2 satisfy the type inheritance. That is, the hierarchy is now captured observing methods instead of states, as it was in Example 2.

The open problem is now to remove Nierstrasz's constraint, i.e.: to admit that sequences of requests, that an object can accept, constitute a non-regular language. In this case, the object behaviour would be described by an high-level net, with guards associated to transitions. (In CLOWN, e.g., the class semantics is described by a modular algebraic high level net, which integrates the Superposed Automata nets with the OBJ language). The problem is not easy since the notions of equivalence and preorder between nets are defined in terms of EN or PT systems, i.e. low level systems, while there aren?t equivalences defined for high level models like OBJSA nets.

22

References [AB97] W.M.P. van der Aalst, T. Basten, Life-Cycle Inheritance. A Petri-Net-Based Approach, in P. Az?ma G. Balbo (eds.), Proc. 18th Int. Conf. on Applications and Theory of Petri Nets, LNCS 1248, Springer Verlag, 1997. [AD95,96] G. Agha, F. De Cindio, eds., Proc. of the Workshop on Object-Oriented Programming and Models of Concurrency, 1995 and 1996. [Ame89] P. America, Issues in the Design of a Parallel Object-Oriented Language, in ?Formal Aspects of Computing?, vol. 1, pp. 336-411, 1989. [Bal98] C. Balzarotti, Equivalenze all'osservazione per la caratterizzazione semantica della ereditariet? in linguaggi a oggetti concorrenti, Tesi di laurea, Universit? degli Studi di Milano, 1998. [BCD97] E. Battiston, A. Chizzoni, F. De Cindio, CLOWN as a Testbed for Concurrent Object-Oriented Concepts, G. Agha, F. De Cindio, G. Rozenberg (eds.), Advences in Petri Nets, Springer Verlag (to appear). [BRR87] W. Brauer, W. Reisig, G. Rozenberg, Petri Nets. Central Models and their Properties. Advances in Petri Nets 1986, part 1. Proceedings of an Advanced Course. LNCS 254, Berlin, Springer Verlag, 1987. [CHC90] W.R. Cook, W.L. Hill, P.S. Canning, Inheritance Is Not Subtyping, in Proc. of the ACM Symp. on Principles of Programming Languages, pp. 125-135, 1990. [Nie93] O. Nierstrasz, Regular Types for Active Objects, in ACM Sigplan Notices, 28(10), Proceedings of the 8th annual conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA?93, Washington DC, pp. 1-15, 1993. [NP92] O. Nierstrasz, M. Papathomas, eds., Object based Concurrency and Reuse, Workshop W6, in Proc. 6th European Conf. on Object-Oriented Programming, Springer Verlag, 1992. [PRS92] L. Pomello, G. Rosenberg, C. Simone, A Survey of Equivalence Notions for Net Based Systems, in G. Rosenberg (ed.), ?Advanced in Petri Nets?, LNCS 609, Springer-Verlag, pp. 410-472, 1992. [PS91] L. Pomello, C. Simone, A State Transformation Preorder over a class of EN Systems, in G. Rozenberg (ed.) APN'90, LNCS 483, pp.436-456, 1991. [WZ88] P. Wegner, S. B. Zdonik, Inheritance as an Incremental Modification Mechanism or What Like Is and Isn?t Like, in S. Gjessing and K. Nygaard (eds.), Proc.ECOOP ?88, LNCS 322, Springer Verlag, pp.55-77, 1988.

-----------------------------------------------------------This research has been supported by MURST.

23

24

Towards an Algebra of Dynamic Object Types

Ant
nio Ravara o Pedro Resende

Abstract

Vasco T. Vasconcelos y

We propose an algebra of object types that characterises the semantics of concurrent objects in a process calculus setting where the communication is asynchronous. The types are non-uniform, and provide an internal and synchronous view of the objects that inhabit them. These ideas, along with the algebraic laws, are based on a notion of bisimulation that is unlike other notions in the literature.

1

Introduction

Non-uniform types for concurrent objects constitute the object of study of several authors 7, 2, 3, 6, 8 . The aim is to build type systems capable of ensuring more than the usual safety properties such as subject-reduction; for instance, the absence of some deadlocks. These types re ect a dependency of the interface of an object upon its internal state, conveying information about some dynamic properties of objects. In a process calculus setting such as TyCO 10 , processes denote the behaviour of a community of interacting objects, where each object has a location identi ed by a name. Each process determines an assignment of types to names re ecting a discipline for communication. The usual types-as-records paradigm 11 gives each name a static type that contains information about all the methods of the object, regardless of whether they are enabled or not. Hereby we propose an algebra of object types, where each type is essentially a collection of enabled methods, and it is dynamic in the sense that the execution of a method can change this collection, i.e. the type. Therefore, the type of an object can also be seen as a partial representation of its behaviour. We assume that objects communicate via asynchronous message-passing; nevertheless, types, as de ned in this paper, essentially correspond to a notion of object behaviour as it would be perceived by an internal observer located within an object the object's private gnome. This observer can see methods being invoked and it can detect whether the object is blocked, even though its methods may be internally enabled. Hence, this notion of behaviour is synchronous, as essentially the gnome can detect refusals of methods. The action of unblocking an object, denoted by , cannot be observed by the gnome because it corresponds to an invocation of some method in another object. Thus, this action is similar to Milner's 4 , because it is hidden, but it is external, rather than an internal action. In this paper we de ne a structural operational semantics for the algebra of object types, both for nite and in nite types. We also introduce two behavioural equivalences based on notions of bisimulation that characterise the referred aspects of an object, and show that the two coincide, at least in the case of nite types.

Computer Science Section, Department of Mathematics, Instituto Superior T
cnico. Lisbon, Portugal. e Email: famar,pmrg@math.ist.utl.pt y Department of Computer Science, Faculty of Sciences, University of Lisbon, Portugal. Email: vv@di.fc.ul.pt

1

25

2 Algebra of Finite Object Types

We start by presenting the algebra of nite object types. Objects are records of methods, and we can represent unavailable blocked objects. Assume a countable set of method names l ; m ; n , possibly subscripted or primed. Definition 2.1. The set O of nite types of objects is given by the following grammar. ::= 0 j

X l e :

i 2I i i

i

j

where I and J are non-empty nite indexing sets, with 8i;j2I i 6= j li 6= lj , and, e is a nite sequence of types. We call a term such as l e: a method type. It corresponds to a method with name l and parameters of type e, which behaves as prescribed by . The type composition operator sum P " puts various method types together to form a type of an object that o ers the corresponding U methods. The term 0 is the empty type. The disjoint union j2J j is the type of a blocked object that will behave later according to one of the types j , after being released. Notation 2.2. 1. We abbreviate the type l e:0 to l e, and l to l. 2. We assume the following abbreviations: P a l e: is i2f1g li ei : i ; U b is i2f1g i ; P c l1 e1 : 1 + l2 e2 : 2 is i2f1;2g li ei : i ; U d 1 2 is i2f1;2g i . We de ne a structural operational semantics for the nite types of objects via a labelled transition relation. Definition 2.3. The set of labels is given by the following grammar. The label denotes a silent transition that releasees a blocked object; a label l e denotes a method invocation. Definition 2.4. The labelled transition relation is inductively de ned by the following rules.

j 2J

j

::=

j l e

Act

The axiom Act gives the basic transition: the invocation of a method with name l and parameters of U e results in the type of the body of that method. The axiom Union captures type a side e ect: i2I i is blocked, and one of its behaviours can only become available after an unblocking action occurs. Notation 2.5. Let = denote , , and = denote , +; furthermore, we write 6, when , ! ! ! ! does not hold.

Pi I li ei :

2

i

, e! ,,,

lj

j

j

j 2 I

Union

Ui I

2

i

, !

j

j 2 I

2

26

We want two object types to be equivalent if they have equivalent method types and if after each transition they continue to be equivalent, in a bisimulation style. Furthermore, from the point of view of each object type, transitions of other object types can be regarded as hidden transitions, which would suggest weak bisimulation as the right notion of equivalence for our object types, with playing the role of Milner's . However, we want our types to distinguish an object that immediately makes available a method from one that makes it available only after being unblocked by another object. This is because, although is supposed to be unobservable, we assume that from the point of view of an internal observer the object's gnome it is detectable that the object is blocked. Hence, we would expect l to be di erent from l , but l and l to be equivalent; in both, all the internal observer can see is that the object is blocked, and after being released it can eventually execute the method l . We also want to distinguish l : m from l :m , on the grounds that for the latter a blocking after l cannot be observed. This also discards Milner's observational congruence 4 and rooted bisimulation 1 as possible candidates for object equivalence. A notion such as progressing bisimulation 5 is however too strong because it would distinguish from . These considerations lead to the choice of a notion of equivalence that essentially strengthens weak bisimulation by requiring that if and are bisimilar and o ers a particular method then also o ers that method. Definition 2.6. Bisimilarity on object types. 1. A symmetric binary relation R O O is an object bisimulation if whenever R then e e a ,,! implies 9 ; e; ,,! = and R and eR e1 ; b , implies 9 = and R ; ! 2. Two types and are object-bisimilar, or simply bisimilar, and we write o , if there is an object bisimulation R such that R . The usual properties of bisimilarities hold, namely o is an equivalence relation, and o holds if and only if

l

0

0

l

0

0

0

0

0

0

0

0

e 1. ,,! implies 9 ; e; ,,! = and o and e o e; 2. , implies 9 = and o ; ! We can strengthen this notion of equivalence even more by dropping another double arrow, as follows. Definition 2.7. Strict bisimilarity on object types. 1. A symmetric binary relation R OO is a strict object bisimulation if whenever R then e e a ,,! implies 9 ; e ,,! and R and eR e; b , implies 9 = and R ; ! 2. Two types and are strictly bisimilar, and we write s , if there is a strict object bisimulation R such that R . Again, s is an equivalence relation and s holds if and only if conditions 1a and 1b of the above de nition hold with R replaced by s . Although for an arbitrary labelled transition system the two bisimilarity relations do not coincide, on our particular system they do, as the following result shows. This provides a sense in which our de nition of object type equivalence is robust.

l

0

0

l

e

0

0

0

0

0

0

0

0

l

0

0

l

0

0

0

0

0

0

0

0

def 1 Let 1 k R 1 k =

1R 1

^ ^

kR k.

3

27

Theorem 2.8. Let ;

Proof.

2 O. Then o if and only if s .

l

The right to left implication is immediate. For the other implication we rst remark that our labelled transition system satis es the following conditions:

l l

e1 e2 1. if ,,, 1 and ,,,! 2 then 1 = 2 label determinism; ! e 2. no can have both an and an l transition, i.e., for all either 6, or 6,,!. ! Let o . We will show that e 1. ,,! implies 9 ; e ,,! and o and e o e, 2. , implies 9 = and o ; ! that is, we will prove that o is a strict object bisimulation, which will conclude the proof. The e e second condition is trivial, so let ,,! . There exist e; ; such that ,,! = , with e e o e and o . The condition ,,! in turn implies, together with label determinism, that = with o , for some . All we have to do now is prove that o . If = or = this is immediate. Otherwise we have the following situation:

l

0

0

l

e

0

0

0

0

0

0

0

0

l

0

0

00

l

0

00

0

00

l

0

0

00

00

0

00

0

0

0

00

0

00

0

o

KS

00

0

00

o

000 0 000

0

In this case all the transitions from must be labelled with ; let then , ; it follows that ! = for some such that o , hence also = . Similarly, can only do , and if , ! we can nd such that = and o , which concludes the proof. Therefore, in our type algebra the two equivalences coincide; henceforth we refer to both o and s as object equivalence, and write o. The proof of the theorem relies on the fact that our transition system is deterministic on labels, and no state can have a transition labelled with l and another with . If either of these conditions is violated the theorem no longer holds, as the following examples show:

0 000 00 000 000 000 0 000 0 0 000 000 000 000

Example 2.9.

l

o 6s

? l l ??? l

l

X

o 6s

l

X

l /

l

l

l

Naturally, the counterexamples above are not expressible in our language. Proposition 2.10. Object equivalence is a congruence relation. Proof. Straightforward, since the sum is guarded. 4

28

1. TheP operators +" andP " are commutative; that is, for any permutation : I ! I we have i I li ei : i o i I l i e i : i , and i I i o i I i ; 2. the operator " enjoys a weak form of associativity, i I i o i I i ; ! n o 1 n . 3. if 1 n , + then 1 Proof. The respective bisimulations are straightforward. Notice that law 3 is not really algebraic, but rather it gives us an in nity of laws that express a form of idempotence. For instance, we have 1 n o 1 n 1 1 n 1 m o 1 n 1 m 1 .. .

Proposition 2.11 Algebraic laws.

2 2 2 2 2 2

A more thorough discussion of the algebraic laws will appear in the full version of this report. Remark 2.12. One can easily recognise that what corresponds to the law : : = : of process algebra, namely o , holds in this setting, since it is an instance of the weak associativity law presented above. Notice however that other laws like : = and a: : = a: do not hold. Also, is not associative; e.g., l m n 6o l m n, which means that although is unobservable, sometimes it can be indirectly counted.

3 The Algebra of Object Types

Now we brie y discuss how the algebra of object types can be extended to deal with multiple objects located at the same name with a parallel composition operator and in nite types with recursion. Definition 3.1. Assume a countable set of variables, denoted by t, disjoint from the set of labels. The set O of types of objects is de ned by the following grammar. X l e : j ::= 0 j k j t j t: i i i j j where I and J are non-empty nite index sets, with 8i;j I i 6= j li 6= lj , and e is a nite sequence of types. The parallel composition k" of types denotes the existence of several objects located at the same name in parallel interpreted as di erent copies of the same object, possibly several in di erent states. Definition 3.2. The labelled transition relation is de ned by the rules of De nition 2.4 together with the following rules.

2 2 2

i I

j J

Rpar

This transition system does not satisfy the two conditions that were used in proving the equality of the two notions of bisimilarity in the previous section, as the types lkl and lk l show. However, the counterexamples of Example 2.9 are still not expressible in our language; we are currently checking whether the two bisimilarities coincide in the presence of parallel composition and recursion. Apart from this, it is simple to verify that both o and s are congruences, and that standard algebraic laws hold. For instance, hO= o;s ; k; 0i is a commutative monoid, and t: o;s t: =t .

f g f g

, ! k , !

0 0

k

Lpar

, ! k , k !

0

0

Rec

t: =t , ! t: , !

0

0

5

29

4 Concluding remarks

We propose an algebraic treatment of non-uniform types for concurrent objects, with an operational semantics and a behavioural equivalence. A type characterises the semantics of an object in a concurrent setting with asynchronous message passing. It is an internal view of the object behaviour. Operationally, a type is a state transition system, where the basic transition is an object method execution. A silent hidden transition corresponds to the execution of a method of another object, and is not directly observable. Further work includes the study of in nite processes and the search for a complete axiomatization of the algebra of object types. So far, candidate axiomatic systems tend to be cumbersome; we view this essentially as a consequence of the lack of associativity of . We also expect to apply the ideas described in this paper to the TyCO type system proposed in 9 , and to relate the type algebra to a process calculus, for instance relating type equivalence to a process equivalence.

Acknowledgements

This work is partially supported by FCT, as well as by PRAXIS XXI Projects 2 2.1 MAT 262 94 SitCalc, 2 2.1 MAT 46 94 Escola, PCEX P MAT 46 96 ACL plus 2 2.1 TIT 1658 95 LogComp, and ESPRIT IV Working Groups 22704 ASPIRE and 23531 FIREworks.

References

1 J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. On the consistency of Koomen's fair abstraction rule. Theoretical Computer Science, 51:129 176, 1987. 2 G. Boudol. Typing the use of resources in a concurrent calculus. In Asian Computing Science Conference, volume LNCS 1345, pages 239 253. Springer-Verlag, 1997. 3 J.-L. Colao, M. Pantel, and P. Sall
. A set constraint-based analyses of actors. In 2nd IFIP c e conference on Formal Methods for Open Object-based Distributed Systems, 1997. 4 R. Milner. Communication and Concurrency. C. A. R. Hoare Series Editor Prentice-Hall Int., 1989. 5 U. Montanari and V. Sassone. Dynamic congruence vs. progressing bisimulation for CCS. Fundamenta Informaticae, 16 2:171 199, 1992. 6 E. Najm and A. Nimour. A calculus of object bindings. In 2nd IFIP conference on Formal Methods for Open Object-based Distributed Systems, 1997. 7 O. Nierstrasz. Regular types for active objects. In O. Nierstrasz and D. Tsichritzis, editors, ObjectOriented Software Composition, pages 99 121. Prentice Hall, 1995. 8 A. Ravara and V. Vasconcelos. Behavioural types for a calculus of concurrent objects. In 3rd International Euro-Par Conference, volume LNCS 1300, pages 554 561. Springer-Verlag, 1997. 9 A. Ravara and V. Vasconcelos. A type algebra for concurrent objects. Research report, Department of Mathematics, Instituto Superior T
cnico, Av. Rovisco Pais 1096 Lisboa, Portugal, 1998. e 10 V. Vasconcelos. A Process-Calculus Approach to Typed Concurrent Objects. PhD thesis, Departament of Computer Science, Keio University, Japan, 1994. 11 V. Vasconcelos and M. Tokoro. A typing system for a calculus of objects. In 1st International Symposium on Object Technologies for Advanced Software, volume LNCS 742, pages 460 474. SpringerVerlag, 1993.

6

30

A Concurrent Object Calculus: Summary of the Operational Semantics. Extended Abstract

Andrew D. Gordon Microsoft Research Paul D. Hankin University of Cambridge

A great deal of software is coded in terms of concurrent processes and objects. The purpose of our work is to develop a new formalism for expressing, typing, and reasoning about computations based on concurrent processes and objects. Our concurrent object calculus ? consists of Abadi and Cardelli¡¯s imperative object calculus ? extended with primitives for parallel composition. Our work extends the analysis by Abadi and Cardelli of object-oriented features to concurrent languages. At the heart of their work is a series of type systems able to express a great variety of object-oriented idioms. Given ?, we may smoothly and soundly extend these type systems to accommodate concurrency. There are by now many formalisms capable of encoding objects and concurrency. Our calculus supports Abadi and Cardelli¡¯s type systems, includes sequential composition of expressions. We describe the semantics of ? directly without introducing auxiliary notions of stores, con?gurations or labelled transitions by means of a reduction relation and a structural congruence relation in the style of Milner¡¯s reduction semantics for the -calculus. This is an extended abstract of a full paper, available from the authors. The full paper includes examples, an extension of the calculus to include synchronisation, a collection of type systems, an alternative semantics for the calculus in terms of con?gurations as well as full de?nitions and proofs.

imp

conc

conc

conc

Concurrent Objects

We extend the imperative object calculus by adding names to objects, and adding parallel composition and name scoping operators from the -calculus. Syntax We assume there are disjoint in?nite sets of names, variables, and labels. We let p, q , and r range over names. We let x, y , and z range over variables. We 1

31

let ` range over labels. We de?ne the sets of results, denotations, and terms by the grammars: Syntax of the conc?-calculus

u; v

::=

d ::= `i = ?xi bi i21::n a; b; c ::= u p d u:` u:` ?xb clone u let x=a in b a b

x p

j

results denotations terms

j 7! j j j j

j

pa

Semantics We may interpret a term of our object calculus either as a process or as an expression. A process is simply a concurrent computation. An expression is a concurrent computation that is expected to return a result. In fact, an expression may be regarded as a process, since we may always ignore any result that it returns. A result u is an expression that immediately returns itself. A denomination p `i = ?xi bi i21::n is a process that confers the name p on the object `i = ?xi bi i21::n . We say that the object `i = ?xi bi i21::n is the denotation of the name p. Intuitively, the process represents an object stored at a memory location and the name p represents the address of the object. A method select p:` is an expression that invokes the method labelled ` of the object denoted by p. In the presence of a denomination p `i = ?xi bi i21::n , where ` = `j for some j 1::n, the effect of p:` is to run the expression bj xj p , that is, to run the body bj of the method labelled `, with the variable xj bound to the name of the object itself. A method update p:` ?xb is an expression that updates the method labelled ` of the object denoted by p. In the presence of a denomination p `i = ?xi bi i21::n , where ` = `j for some j 1::n, the effect of p:` ?xb is to update the denomination to be p `j = ?xb; `i = ?xi bi i21::n,fj g , and to return p as its result. A clone clone p is an expression that makes a shallow copy of the object denoted by p. In the presence of a denomination p `i = ?xi bi i21::n , the effect of clone p is to generate a fresh name q with denomination q `i = ?xi bi i21::n and to return q as its result. After a clone, the names p and q denote two copies of the same denotation `i = ?xi bi i21::n ; updates to one will not affect the other. A let let x=a in b is an expression that ?rst runs the expression a, and if it returns a result, calls it x, and then runs the expression b.

7!

g

2

7!

f

7!

2

7!

7!

7!

2

32

A parallel composition a b is either an expression or a process, depending on whether b is an expression or a process. In a b the terms a and b are running in parallel. If b is an expression then a b is an expression, whose result, if any, is the result returned by b. Any result returned by a is ignored. A restriction pa is either an expression or a process, depending on whether a is an expression or a process. A restriction pa generates a fresh name p whose scope is a.

b c a b c a b c b a c pq a q pa pa b a pb pa b pa b let x=let y =a in b in c let y =a in let x=b in c plet x=a in b let x=pa in b a let x=b in c let x=a b in c

a

Structural congruence a b is the least congruence on terms to satisfy:

if p 2 fn a = if p 2 fn b = if y 2 fv c = if p 2 fn b =

For the ?rst three rules, let d = `i = ?xi bi i21::n . p 7! d p:`j ! p 7! d bj fxj pg f g if j 0 p p 7! d p:`j ?xb ! p 7! d if j

clone p let x=p in b b x

p

Reduction a ! b is the least relation on terms to satisfy:

7! d

pa

! pa0 a b ! a0 b b a ! b a0 let x=a in b ! let x=a0 in b a!b

! p 7! d ! f pg f g

q q

7! d

`j = ?xb; `i = ?xi bi i21::n,fj g q if q 2 fn d =

2 1::n 2 1::n, d0 =

if a ! a0 if a ! a0 if a ! a0 if a ! a0 if a a0 , a0

! b0, b0 b

In the full paper, we show that this chemical semantics is equivalent to a more conventional structural operational semantics. Moreover, we identify a deterministic fragment that is closed under reduction and show that it includes Abadi and Cardelli¡¯s imperative object calculus.

3

33

34

Quiet and Bouncing Objects: Two Migration Abstractions in a Simple Distributed Blue Calculus

Silvano Dal-Zilio?

INRIA Sophia-Antipolis

Abstract. In this paper, we study a model of migrating objects based on the blue calculus extended with a very simple system of localities and we show how two migration behaviors can be de?ned, namely those of bouncing and quiet objects. These ¡°migration control abstractions¡± are de?ned separately from other aspects of the object de?nition and can be easily reused, thus providing more ?exibility in the de?nition of ¡°migration constraints¡±.

1 Introduction

The purpose of this extended abstract is to study how the behavior of concurrent objects with respect to migration, can be de?ned orthogonally from other aspects of the object de?nition, such as synchronization constraint for example. To give the reader an intuition: many researches have been conducted on the problem of de?ning synchronization abstractions for concurrent objects [10, 7], likewise, we are interested here in the de?nition of migration abstractions that can be reused to implement distributed objects. To this end, we give two examples of objects that act, respectively, according to the well-known client/server and agent paradigms. We ?rst present the calculus used to de?ne objects, namely a version of the blue calculus [4] enriched with a simple model of localities so that we can deal with migration. In this distributed blue-calculus (D?), objects can be represented ¡°as processes¡± [8]. In particular, we study in Sect. 3, the canonical example of the mutable cell. Then we show, using a slight modi?cation in the process de?nition, how one can mimic two migration behaviors: the object that always resides at the same location and the object that migrates to the location of its clients.

2 The Calculus

The blue calculus (?) is a direct extension of both the and the calculi. In this paper, we consider a very simple distributed version of the original calculus introduced in [4] (see Table 1) obtained by adding locations, located processes ( a :: P ) and a primitive for code transfer (go a:P ). In D? , terms are de?ned using three disjoint kinds of names: references: u; v; w , and localities (or places) a; b; c . The de?nition def D in P (where labels: k; l; m D is a sequence of mutually recursive de?nitions u1 = P1 ; : : : ; un = Pn , with the ui ¡¯s pairwise distinct) is a restricted an replicated version of the declaration hu P i, that can be understood as a resource, located at u, accessible only once. Indeed, the declaration hu xP i

2 R 2 L 2 P

?

Email: Silvano.Dal_Zilio@sophia.inria.fr. Address: INRIA Sophia-Antipolis, BP 93, 2004 route des Lucioles. F-06902 Sophia Antipolis cedex. Fax: +33 492 38 79 98

: : :

35

is the equivalent of the -calculus input guard ux:P . This construct is useful to model processes with a mutable state. An important restriction imposed over terms is that no declaration can be de?ned on an abstracted reference (e.g., uh P i is not a valid process). This restriction, equivalent in to the one that forbids reception on received names, ensures that no new declaration on a given reference can be dynamically created.

u

Table 1 Syntax of the Blue Calculus with Simple Location System: D ?

x P

::= ::=

S

::=

j P P a:P Px h P i u P ; : : : ; u l P P a P S jS S

u

O

P

u a

xP

i

u

go

u

i =

::

1 i n

def

1 = 1 l

n =

Pn in P

u

values processes agents declarations records locations

The model chosen to deal with distribution is very simple. A site is a named box, a :: P , containing a running threads P . For the sake of simplicity, we consider a ?at system of locations (that is located processes are not nested) as in [9, 2]. We consider also the operation: go a:P , that spawns a thread P in the location a and we denote u@a the process go a:u that sends a message at location a. The reduction semantics of D ? is given in a chemical style [3] and uses a structural equivalence ( ). The de?nition of the reduction relation ( ) uses the standard notion of evaluation context (E ), i.e. contexts such that the hole does not occur under a guard1. The de?nition includes three general rules:

!

QP Q

P ! P0 0 ! P

E

P P

! !

P0

E

P0

P a :: P

! !

P0 a :: P 0

We refer the reader to [4, 8] for a full presentation of the reduction semantics for the calculus without localities. Axioms for structural equivalences, see Table 2, are the usual axioms for the -calculus (including scope extrusion) extended with rules to manage application. We have omitted the rules for record selection, P , that acts like application and we refer the reader to [5] for details. We also add two new axioms in the distributed calculus to allow spawning of restricted names over locations: to distribute references restricted by a P statement, and | to distribute de?nition over parallel composition. Note that the equivalent of relation | in the -calculus, is obtained by using a behavioral equivalence. This is the the well-known replication theorem of [11, 12] in the case of channels with output-only capabilities. The reduction relation embeds different mechanisms. ¡°Small¡± reduction (r1),

l

u

1E

::=

:

E

x

E

j P

P j E

u E

def D in E

E

l

36

Table 2 Structural Equivalence

def D in def D in P

0

def P

j j hv i h u i

Q x P

D in P x

def

x

def

P

x

D; D in P x

0

D in

P

Q

x

P

go

a:P x

go

a:P x

def D in go a:P

a ::

u P

D in

| def

P

u :: j def

a Q

go

a:def D in P P

D in P

j

def D in Q

de?nition folding (r2), resource fetching (r3) and record selection (r4):

r1 r2 r3 r4

xP y

def

!

P fy=xg

and l = P ; Q k Q k k = l We also add the reduction rule for the go statement (note that process P cannot execute under the guard go a:P )

l=P;Q

h Pi j u x :::x

u

1

D; u = R; D0 in E u x1 : : : xn

l

!

!

def

D; u = R; D0 in E R x1 : : : xn

u

62

bnE

n

P x1 : : : xn

! 6

!

P

r5

b :: go a:P

Example 1. A typical reduction sequence in D ? is the one such that a message carrying a

jQ j

a :: R

!

b :: Q

j

a :: P

jR

private reference is send remotely.

b :: def u = R in v@a u P a :: v Q

j h i

j

!

b :: go a:def u = R in v u a :: v Q

j j h i

def

u = R in P

fnQ

To conclude, let us just state that, while the blue calculus is a name passing calculus (that is a process can only be applied to a name and not to another process), the ¡°high-order¡± -calculus application can be recovered using the de?nition:

P

j

b :: def u = R in P a :: def u = R in Q u

if u

62

Q =def

def

u = Q in P u

u

62

fnP

fnQ

Moreover this de?nition of application is coherent with our model of distribution since we can prove that go a:P Q go a:P Q.

3 Modeling Objects in the Blue Calculus

In this extended abstract, we will concentrate on a single example of object, namely the ¡°mutable cell¡±. Although it is only an example, it is a representative one, since in [8] we

37

show how to derived a ¡°complete¡± calculus of concurrent objects using cells and extensible records. Thus, the result given for the cell example can be derived for more general objects. The constructs of this object calculus, together with its derived operational rules, are given for information in Sect. 3 (consideration on types are omitted). Let R ob denotes the record: Rob =def get = xo b j x b; put = xo x The cell process with ¡°name ¡° O is de?ned by: CELL O =def def o = bhO Robi in o and the application: CELL O a0, initializes the cell to the value a0. It is easy to see that 2 C ELL a0 j O get r and C ELL a0 j O put a evaluate in a deterministic way: C ELL a0 j O get r def o = bhO Ro bi in hO Ro a0 i j O get r def o = bhO Ro bi in Ro a0 get r def o = bhO R bi in o a j r a C ELL a0 j r a0 o 0 0

! ! !

CELL a0 j O put a def o = bhO Robi in o a CELL a It is interesting to notice the linear use of the reference O in CELL O a. If the cell is invoked, we consume the unique declaration hO R oai. Thus, a unique message o a0, acting like a lock, is freed in the evaluation process, which, in turn, frees a single declaration hO Roa0i. Thus, we have the invariant that there is exactly one resource available at address O, and that this resource keeps the last value passed in a O put call.

!

4 A Concurrent Calculus of Objects

More elaborate objects than the (canonical) example of the mutable cell can be de?ned. In this section, we introduce a calculus of concurrent objects by specifying a set of operators and their operational semantics, and we de?ne these operators (and their associated reduction rules) with an encoding in ?. In the speci?cation of this calculus (Table 3), we distinguish a subset of references (which we call objects names, O; A; B; ) and we use L to denote an ¡°object body¡±: L = l1 = & x1 P1 ; : : : ; ln = & xnPn . An example of object is the one that produces an in?nite copy of itself. Let L be the body: l = & xclonex j x l , then: obj O = L in O l obj O = L in obj A = L in A j O l : : : another example, using method overriding, is: obj O = L in O l = & xx l obj O = l = & xx in O l obj O = l = & xx in O

O 2 O f g ! ? & f g f g ! ? & f g ! ? & f g ! ? & f g

4.1 Interpretation of the Derived Object Constructs

f

Processes modeling objects are inspired from the encoding of the mutable cell. In the definition given in Table 4, an object obj O = li = & xiPi 1in in P , is a cell with an additional ?eld clone to allow object cloning. In this de?nition, a method & xP is an abstraction xP . This function, also called premethod, has one argument: the name of the current object (also called the self-parameter). The cell ¡°memorizes¡± a record of premethods:

g

2

to simplify the examples, we use C ELL to denote C ELLO

38

Table 3 Speci?cation of Operators and Reduction Rules for Objects in ?

& xP n o obj O = li = & xi Pi 1in in P P l O l = & xQ cloneO

Let L =def

l1

method with self parameter x and body P object with n methods l1; : : : ; ln invocation of method l update of method l with body & xP cloning of object O

j

! ? &

= & x1 P1 ; : : : ; ln = & xn Pn

obj O = fLgin E O obj O = fLgin E O obj O = fLg in E cloneO

l

j =

&xP

! ? &

l

! ? &

obj O = flj = & xP; li = & xi Pi i6=j gin E O

obj O = fLgin E Pj fO=xj g

obj O = fLg in obj A = fLg in E A

A

62

bnE

li = xiPi1in , as in the classical recursive records semantics [6]. Note that we restrict the scope of an object name to the de?nition of the object it refers to. Thus we have the invariant that there is a unique declaration for each object names. Moreover, method update returns ¡°a reference¡± to the modi?ed object. This is almost the behaviour of (sequential) objects in the & calculus of Abadi and Cardelli [1]. 2 3 get = xo b j x b O; Sob =def 4 modify = xx o b j O; 5 clone = o b j xclone b

OBJ O

=def

def o = b O

h S b i in o

o

Table 4 De?nition of the Derived Operators for Objects

P l =def P get xx l cloneO =def O clone O l = & xQ =def O modify obo l = xQ ; b o n def xclone = b AOBJ A b j A obj O = li = & xi Pi 1in in P =def in O OBJ O l = x P 1in j P

i

i

i

Another remark is that we use only ?eld selection and application in the de?nition of cloning, method invocation and method update. Thus the de?nition of structural equivalence allows us, for example, to derive the following laws, showing that these (derived) operators acts like application:

def D in P Q

j l

def D in P

l j Ql

39

hu P i l

hu P i

The next result states that there is an operational correspondence between (de?ned in Table 3) and . These properties are proved using a simple induction. Theorem 1 (Operational Equivalence). The speci?cation of the object reduction rules is com0 0 . It is also sound: plete with respect to the encoding of objects in ?:

!

? &

!

implies that Q

!

0 Q

with

P ! ? Q &

0

.

P ! ? P &

P !

P

P ! Q

5 Quiet Versus Bouncing Cells

In our model of distribution, synchronization (rule (r3)) does not extend over location boundaries. Thus communication is local, and, to interact with a remote declaration at location , one has to ?rst spawn a message at . For example, the process :: j :: hu i is inert while :: @ j :: hu i reduces to :: O j :: . Another remark is that the result of the communication is always executed at the location of the declaration. This is reminiscent of the client-server paradigm of computation such that clients ¡°controls¡± the computation, that takes place at the server location, by sending remote messages. The ¡°migration behavior¡± of the mutable cell object and of the declaration hO Ro i are equal. For example, to read the content of the mutable cell from a remote location, one has to (1) move to the location of the cell, then (2) invoke the method read and ?nally (3) fetch the result back. After completion, the cell is still at the same location.

a a b u a P b u a a P b a P b

a :: b ::

CELL

O @a

j j get j

a0 P r @b

!

! Q

a ::

CELL CELL

a0 a0

!

a ::

j j j j j j

r @b

P a0 P b ::

b :: Q

r

a0

Q

Likewise, objects created using the cell also share the same ¡°migration behavior¡±, i.e. they are quiet objects since they never leave the location of their creation. In this section, we de?ne a new migration abstraction, namely the agent behavior, based on a new declaration statement: hu iagt (see Table 6), that can be derived in D ?. Roughly speaking, the result of a remote communication involving hu iagt takes place at the client location instead of the declaration one.

P P

Table 5 Two Distributed Cells

CELL c=s

O

=def def =def def

o

= =

b O b

CELLagt

O

o

h R i hO R i

o b c=s in o o b agt in o

The operational semantics of an agent declaration strongly depends on the distribution of the processes. Indeed in ? (and in ) there are no explicit locations and (therefore) where a communication comes from is not observable. But this information does count in a distributed setting. If we rede?ne the cell object using hO iagt instead of hO i,

::: :::

40

denoting it CELL agt , we obtain a mutable cell bouncing from locations to locations according to communications with the client. :: CELLagt 0 j j ! ! :: j :: @ get j :: C ELL agt 0 j 0 j to sketch the encoding of this new construct, let us just say that remote messages :: @ are translated to :: go (that is the same message with, as extra argument, the ¡°departure location¡±), and that the declaration hu iagt and hu ic=s are de?ned by:

a b a P a b P ! O a r Q a r a Q b u a b a: u b P P

h i h i

u

P

agt =def c=s =def

u

P

h h i

u

ago a:P

i

u

a P

with

a 62

fnP

Other object migration abstractions can be uniformly de?ned by ?rst de?ning a new kind of declaration. For example, an applet object can be interpreted as an object that does not change location but that spawn a copy (or clone) of itself at the location of its client. We can give this behavior to an object using, for its de?nition, a new declaration construct, hu iapplet (see Table 6), that can also be derived in D?. For example hu iapplet can be translated to:

P P

h i

u

P

applet =def def

x

= u

h

ago a:P

j i

x

in x

Table 6 Client/Server, Agent and Applet Communications

0 @

a :: b ::

h i j j

u

P

c=s

R

def

a :: b ::

h i j j

u

P

D in u@a v1 : : : vn

j j j

1 A !

!

a ::

def

D in P v1 : : : vn

j j!

R

Q

b :: Q

agt

R

!

a :: R b ::

j

D in P v1 : : : vn P

def

a :: b ::

h i

u

P

D in u@a v1 : : : vn

Q

applet

j j

R

!

def

! Q

a :: b ::

h i

u

def

applet

j j

R

j j

!

Q

!

def

D in u@a v1 : : : vn

D in P v1 : : : vn

Q

6 Conclusions and Future Work

A challenging problem encountered in the design of programming languages with concurrent objects, is to be able to express the synchronization control of objects in a compositional and reusable way. Now that ¡°network-oriented¡± languages have added functionalities to remotely download code and to migrate objects, a similar problem arises in the description of

41

the migration behavior. In the present paper, we have presented how two abstractions for the de?nition of the migration behavior can be applied to de?ne mutable cell objects that react differently when invoked by a remote client. Using a translation of a calculus of concurrent objects in ? de?ned in [8], we claim that those abstractions can be uniformly applied to every object creation. Moreover, These abstractions can be transposed to other process calculi, and in particular to distributed versions of the -calculus [14, 9, 2], and to other interpretation of objects [13]. The principal advantage of de?ning ¡°standardized behaviors of migration¡±, is that we can de?ne migrating objects from objects designed in an non-distributed language without adding any explicit thread of control, thus providing a ?exible and simple way to automatically add migration features to objects. But further works must be done to de?ne more elaborated behaviors than those presented in this abstract. For example it will be interesting to give an accurate model of the mobile agents behavior as de?ned in T ELESCRIPT [15].

References

1. Mart¨ªn Abadi and Luca Cardelli. A theory of primitive objects: Untyped and ?rst-order systems. Information and Computation, 2(125):78¨C102, March 1996. 2. Roberto Amadio. An asynchronous model of locality, failure and process mobility. In COORDINATION 97, volume 1282 of Lecture Notes in Computer Science, 1997. 3. G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96:217¨C248, 1992. 4. G¨¦rard Boudol. The -calculus in direct style. In Conference Record of POPL ¡¯97: The 24th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 228¨C241, Paris, France, 15¨C17 January 1997. 5. G¨¦rard Boudol. Typing the use of resources in a concurrent calculus. In ASIAN¡¯97, the Asian Computing Science Conference, Lecture Notes in Computer Science, Kathmandu, December 1997. 6. L. Cardelli and J. C. Mitchell. Operations on records. Math. Structures in Computer Science, 1(1):3¨C48, 1991. 7. Denis Caromel. Programming abstractions for concurrent programming. In Technology of Object-Oriented Languages and Systems (TOOLS Paci?c¡¯90), pages 245¨C253, Sydney, November 1990. 8. Silvano Dal-Zilio. Concurrent objects in the blue calculus. (draft) http://www.inria.fr/meije/personnel/Silvano.Dal_Zilio/. 9. Matthew Hennessy and James Riely. Ressource access control in systems of mobile agents. Technical Report 2/98, University of Sussex, February 1998. 10. Satoshi Matsuoka and Akinori Yonezawa. Analysis of inheritance anomaly in object-oriented concurrent programming languages. In Gul Agha, Peter Wegner, and Akinori Yonezawa, editors, Research Directions in Concurrent Object-Oriented Programming, chapter 4, pages 107¨C150. The MIT Press, 1993. 11. Robin Milner. The polyadic -calculus: a tutorial. Technical Report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, University of Edinburgh, 1991. 12. Benjamin Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 11, 1995. 13. Davide Sangiorgi. An interpretation of typed objects into typed -calculus. Technical Report 3000, INRIA, 1996. 14. Peter Sewell. Global/local subtyping for a distributed pi-calculus. Technical Report 435, University of Cambridge, 1997. 15. Jim White. Mobile agent white paper. Technical report, General Magic, 1996.

42

Surrogates in jeblik: Towards Migration in Obliq

Hans Huttel, Josva Kleist, Uwe Nestmann, Davide Sangiorgi BRICS Aalborg University INRIA Sophia-Antipolis June 15, 1998

In Cardelli's lexically scoped, distributed, object-based programming language Obliq, object migration was suggested as creating a remote copy of an objects' state at the target site, followed by turning the local object itself into a surrogate, i.e. a pointer to the just created remote copy. This kind of migration is only safe |migrated objects shall behave the same before and after migration|if it is protected and serialized. Protected objects can only be accessed by clients via selection, and within a serialized object at most one method can be active at any time. Yet, since Obliq does not have a formal semantics, there is no proof of this claim. In this abstract, we consider the act of creating object surrogates as an abstraction of the above-mentioned style of migration. We introduce the language jeblik, a simpli ed distribution-free subset of Obliq, and give its formal semantics in terms of an encoding into the -calculus. This semantics shall provide the ground for proving that surrogation is safe, thus suggesting that migration in Obliq is safe, accordingly.

Abstract

1 Motivation

Our language jeblik for studying surrogation, is an object-based language which is not only inspired by Obliq Car95 , but rather represents its concurrent core. Obliq is a lexically scoped, distributed, object-based programming language. Lexical scoping in distributed settings makes program analysis easier since the binding of variables is only determined by their location in the program text and not by the site at which execution takes place. It can be advantageous to migrate an object from one site to another, which is also called for in Obliq. Here, however, mutable values in general are never sent over the network; instead, only network references are transmitted. Accordingly, migration of objects is carried out in Obliq by creating a copy of the object at the target site and then modify the original local object such that it forwards all future requests to the new remote object. In jeblik, we ignore all distributed aspects of migration|they are not essential for the results of Obliq computations anyway|and concentrate on just the concurrent aspects: surrogation of an object, say: a, can be described as creating a copy b of a and then turn a itself into a `pointer' to b, i.e., which forwards all future request for methods of a to b.

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

1

43

2 Surrogation in jeblik

In this section, we present jeblik as an untyped language1, although we sometimes refer to types when we think it helps us in explaining our design decisions or it eases the understanding. jeblik-expressions are given by the following grammar: a; b; c; : : : ::= fP; S; r; lj =mj j2J g object construction j a:lh a1: : :an i method invocation j a:lm method update j a:aliasb object aliasing j a:clone shallow copy j a:surrogate object surrogation

j j j j

let x = a in b

s; x; y; z

forka joina

local de nition variables thread creation thread destruction

m ::= & s; xb ~ method where method labels l and run-time object references r are taken from disjoint sets. An object fP; S; r; lj =mj j2J g consists of a nite collection of named methods lj =mj , more generally called elds, for pairwise distinct labels lj ; the P and S keywords are optional and re ne how an object reacts to external messages, while the aliasing reference r can be used to forward most requests to another object, so a non-aliased object has just no entry. Note that we introduce object references, actual run-time entities, explicitly in the syntax of jeblik only in order to clarify the semantics of aliasing; an actual user-level language would not need any entry at all. In a method & s; xb the letter & is a binder for the self ~ variable s and argument variables x within the method body b. ~ Let a be a non-aliased object. Methods can only be activated, when also supplying the required actual parameters: a:lh a1: : :an i with l denoting the method & s; xb results ~ in the body b with the enclosing object a bound to the self variable s, and the actual parameters a1 : : : an of the invocation bound to the formal parameters x. The expression ~ a:lm updates the content of the named eld l in a with method m and evaluates to the modi ed object. On aliased objects, by constrast, invocations and updates are forwarded to the aliasing target instead of operating on the aliasing source. Every object in jeblik comes equipped with three special methods for aliasing, cloning, and surrogation, none of which can be overwritten by the update operation, and only one of which is subject to aliasing. In contrast to Obliq, we do not allow aliasing of individual elds, but only aliasing of objects themselves2 : a:aliasb with a = fP; S; r; lj =mj j2J g results in fP; S; b ; lj =mj j2J g, overriding the current alias r with the value b of b, assuming

1 2

Obliq also is an untyped language, although types can be added in a rather straightforward manner. In Obliq, object aliasing called redirection is derived from eld aliasing.

2

44

that evaluates to an object reference with `type' matching that of . Thus, as a special case the aliasing method itself like cloning is not captured by aliasing3. Consequently, the behavior of an jeblik-object can only be changed directly via method update or else indirectly by aliasing. The operation clone creates an object with the same named and optional elds as the original object and initializes the elds to the same values as in the original object. The operation surrogate shall behave as let = clone in alias ; . Here, as usual, the expression let = in rst evaluates , binding the result to , and then evaluates within the scope of the new binding. Moreover, ; abbreviates let = in for 62 fv . Since surrogation is meant to be an abstraction of migration, the correct interpretation of double-surrogation| surrogate; surrogate equivalent to surrogate surrogate|requires that surrogate methods are, in general, subject to aliasing, otherwise the migration of an already migrated object would mistakenly migrate the surrogate. To create a new concurrent thread we use the fork command. The expression fork returns a thread identi er to denote a new thread evaluating . To get the result of a computation in fork'ed thread the join command is used. If evaluates to a thread identi er, then join either returns the value that the thread denoted by has evaluated to, blocks until the thread nishes and then returning the resulting value, or blocks forever if a join on the thread has already been performed4.

b a a: a: x a: a: x x x a b a x b a b x a b x b a: a: a: : a a a a a a

Serialization and Protection based on Self-In iction

The three basic kinds of operation on jeblik-objects|invocation, update, and the special operations|can be performed as either external operations on an object or through self as internal operations. A self-in icted operation is an operation, that is performed on the current self, i.e., the self of the last method invoked in the current thread that has not completed; an operation is external if it is not self-in icted. In concurrent object-based settings, the invariant that at most one thread at a time may be active within an object is called serialization. The simplest way to ensure serialization is to associate with an object a mutex that is locked when a tread enters the object and released when the thread exits the object. However, this approach is too restrictive|it is not possible for a method to call one of its siblings. Instead, self-serialization requires that the mutex is only acquired for external operations. This allows a method to call its siblings through self, but excludes mutual recursion, where a method in an object calls a method in another object , which then tries to call back" to activate a method in . With self-in iction, it is also easy to de ne a sensible method for the protection of objects against external modi cations: for protected objects, updates and the special operations are only allowed, if these operations are self-in icted. Both, protection and selfserialization are used Obliq and also in jeblik: we use the keyword S for self-serialized and the keyword P for protected jeblik-objects.

a b a

3 Note 4 In

that this is consistent with re-aliasing in Obliq.

Obliq, an exception will be raised.

3

45

PP

se

Entry

o

ww pt wwww ww ww ww

;

Protect P

sl m

FF FF F

OB

=

b1

sl FF FF FF F

Serial S

si

MG

t

t1

...

n

bn

Figure 1: Structure of jeblik-objects

3 A formalization using the -Calculus

We give the semantics of jeblik as a translation into the local asynchronous -calculus L of Merro and Sangiorgi MS98 , equipped with matching. This gives us the possibility of using process-algebraic proof techniques to reason about surrogation. Based on previous work e.g. by Kleist and Sangiorgi on the imperative object calculus IOC KS98 , the main new idea of the translation is the distinction between two di erent self identi ers: se to serve external requests, and si to serve internal requests. By this distinction, the requirements of protection and serialization can be decided solely based on the access to the self identi ers. With O := lj =& s; xbj j2J , a non-aliased object is ~ translated into the composition of an object module OB and a pre-processing module PP:

P = se; si phsei j PPO ;Sh se; si i j OBO h se; si i where sc represents the current self of the execution. The OB-module is similar to the encoding of imperative objects: it consists of processes representing the method bodies, and an object manager process MG that deals with the di erent kinds of requests. The PP-module models the re ned functionality for distinguishing and handling requests based on an object's protection and serialization. The structure of the encoding and its code are shown in Figures 1, 2, 3, 4, and 5. In the following paragraphs, we comment on the details.

c

fP; S; ,; O g s p

def

,

Pre-processing

The Entry serves as receptor for external requests; only method invocations are passed on to Serial, all other request are forwarded to Protect. Note that external requests can be grabbed only after some signal has arrived on channel m. This guarantees mutual exclusion not by itself, but in cooperation with Serial, which is to release signals on m concerning the activities between the external and internal interfaces. Protect has a very simple de nition. Note that all incoming requests on channel pt are necessarily external and, due to the behavior of Entry, they can only be requests for updating or one of the special operations. If protection is turned on P=T, all of theses requests lead to a run-time error according to Obliq's informal semantics. Otherwise, incoming requests are simply forwarded to the serialization module. 4

46

P PPO S h s

;

e

;s

i

i

EntryO h s

e

; pt; sl; m i

P ProtectO =T h pt; sl i S SerialO =F h sl; m; s P ProtectO =F h pt; sl i

i

i i

S SerialO =T h sl; m; s

i

= m; sl; pt mhi j EntryO h s ; pt; sl; m i P j ProtectO h pt; sl i S h sl; m; s i j SerialO def = ! m:s x:case x of l inv : : : : slhxi else : pthxi def = ! ptx:wrong def = ! ptx:slhxi , def ~ s hh hp; s ; xii j ~ mhi = ! slh p; s; x: , def = ! slh p; s; x: r s hh hr; s ; xii j ry:phyi j mhi ~ ~

e i e i i i i

def

,

Figure 2: Encoding of jeblik-objects: Pre-processing unify single- and double-selections on records, which helps us to emphasize the essential idea: the label h may range over requests of the form l inv, l upd, as well as ali, cln, and sur, each carrying as parameters at least a result channel r and a current-self identi er s ~ may be empty; Figure 4 shows the generation of such requests by objects' clients. x The main task of Serial|mutual exclusion|is performed by the rather simple and standard technique of using a lock, i.e. a message on some local channel m which obeys the invariant that at any time there is at most one message on it available in the system. If serialization is turned on S=T, we need to extract the return channel p on which the nal result of the invocation is expected at the invoker's side. Here, we create a fresh return channel r, before we pass on the whole request|where the result channel p is replaced with r|to the internal self. Thus, with respect to external requests, which need to serialize, we have now obtained complete local control on the internal self, until some result y of the current externally invoked method is coming back on r. Only then, we are allowed to proceed by forwarding the result y to the intended result channel p and by releasing a signal on the mutex channel m in order to let the next external request enter the object's implementation. If serialization is turned o S=F, then the only obligations are to forward requests to the internal self and, which is important, to immediately signal back on m to the entry module that the next external request shall be allowed to enter. Apart from mutually exclusive access to the internal self s , the serialization module also serves the purpose of authorization: every external request received on s that will be passed on to the object manager on s , gets implanted the new identity s as its self parameter|the former `current self' is discarded. By this mechanism, we will be able to distinguish between authorized external requests, which went through the o cial entrance s , from invalid external ones that somehow see below might have gotten direct access to the internal entrance s .

j j i e i i e i

Serial is not so complicated either. In Figure 2, we use enhanced pattern matching to

5

47

~ OBO h se; si i def t MGO h se; si ; t i = ~

def

j

Q

~ MGO h se; si ; t i = si x:case x of ~ ; s6=si ; : MGO h se; si ; t i j se hxi ~ lj inv r; s=si; x : MGO h se; si; t i j tj hr; si; xi ~ ~ lj upd r; s=si; t0 : MGO h se; si; t1 : : : tj,1; t0; tj+1 : : : tn i j rhsei ali r; s=si ; y : MGA h se ; si ; y i j rhse i O , P;S ~ ~ cln r; s=si : MGO h se ; si ; t i s0 s0 r hs0 i j PPO h s0 ; s0 i j MGO h s0 ; s0 ; t i e i e e i e i s ~ sur r; s=si : MGO h se ; si ; t i j let n = si :clone in si :aliasn; n r MGA h se; si ; sa i def si x:case x of = O ; s6=si ; : MGA h se; si ; sa i j se hxi O lj inv r; s=si; x : MGAh se; si; sa i j sa hxi ~ O lj upd r; s=si; t0 : MGAh se; si; sa i j sa hxi O A h se; si ; y i j rhse i ali r; s=si ; y : MGO , P cln r; s=si : MGA h se ; si ; sa i s0 s0 rhs0 i j PPO ;S h s0 ; s0 i j MGA h s0 ; s0 ; sa i e i e e i O O e i A h se; si ; sa i j sa hxi sur r; s=si : MGO

i

j 2J

!

tj r; s; x: bj s ~ r

Figure 3: Encoding of jeblik-objects: Object manager

Managing The object manager, receiving on the internal self, is the core administrator of an object's functionality, which is either invoked after successful pre-processing for external requests or directly due to internal requests of the aforementioned forms. So, object managers in particular need to deal correctly with self-in iction. To this end, we use an abbreviation that combines the case-construct with a built-in -calculus matching operator for names. The crux for handling self-in iction resides in the matching for the self parameter: if a request reaches the object on the internal self channel si carrying a self parameter di erent from si, then the request is regarded as originating from a di erent thread of control and, thus, is forwarded to the external self se in order to run through the serialization and protection mechanisms. Note that this is necessary for the case `forked extrusion ' of the internal self si , which is explicitly allowed, but needs special treatment: blocking if the extruder waits on the forked results involving invocation of si cf. Car95 . Remember also that external requests that have successfully passed the pre-processing, are explicitly authorized such that they are not mistakenly re-forwarded to the external self. The basic purpose of object managers is to invoke the appropriate instances of method bodies case lj inv: activate the method body bj bound to lj along trigger name tj ; Figure 3 6

48

a: j h a1 : : :an i

l

sc p

def

= q q1 qn = q

,

j

,

i=1n q y :q1 x1 : :qn xn :

a

a: j & s; x b

l

~

sc p

def

sc p s a:clone pc s a:surrogate pc

a:alias b

t ! tr; s; x: b s ~ r j y lj upd hp; sc ; ti , def = qx; qy a sy j b sx j qy y : qxx : y ali hp; sc; xi qc qc , def = q a sc j qy : y cln hp; sci q , def = q a sc j qy : y sur hp; sci q

q y :

a

sc q

y lj inv hp; sc ; x1 : : :xn i

sc q

Q

vi

sc qi

Figure 4: Encoding of jeblik-clients shows that method bodies are run in the context of the current self s and the result channel r, and to carefully administrate updating case lj upd: install a new trigger name t and aliasing case ali such that respective future invocations will be dealt with correctly. We distinguish between aliased MGA and non-aliased MG object managers: aliasing is encoded by starting an aliased object manager instead of re-starting the non-aliased one. The aliased manager makes explicit the forwarding of requests to the aliasing target sa in all cases of invocation, updating, and surrogation, as required. Note that invalid requests those where s6=si are still forwarded to the external self se.5 Cloning results in the restart of the current object manager in parallel with a freshly ~ created copy that uses the same method bodies, i.e. the same access names t to them, so A -part of a new OB-module is installed with the new self parameters. only the MG MG Surrogation is translated as we speci ed earlier as a combined cloning and aliasing, so we have embedded the setting for our main problem in the encoding of jeblik.

0

It is here that the encodings current-self parameter sc is actually used, when clients pass it on together with their requests. In each case, the responsibility for returning a result on channel p is forwarded to the respective object manager. Furthermore, each of the following translations obeys the same idea: the involved expressions are evaluated at private locations, their results are grabbed and then used to forward low-level request to the corresponding object managers. We chose a parallel evaluation order for object and parameters, but the results are grabbed corresponding to CBV-order leftmost-innermost.

Clients

This could be changed to forward the request x to the aliasing target sa instead of the external self se . It would be correct as long as we assume that we never create aliases between objects with di erent protection serialization settings; the required pre-processing is then carried out by the aliasing target. This is always the case for surrogation; for other cases, it can be guaranteed by imposing it in a type system, as we do in the forthcoming long version of the current document. Obliq leaves this rather open.

5

7

49

let x = a in b

sc def p sc p sc p sc p

x

forka joinb

= def = def = def =

q a

phxi

,

sc q

j q x : b

sc p

r phri j a s r sc j q r :r y :phy i q b q

Figure 5: Encoding of miscellaneous jeblik-expressions

Miscellaneous Fork-and-join

Variables and the let-construct is encoded as usual see KS98 .

To fork a thread means to create a new activity running in parallel with the current ones. Since Obliq is making some subtle assumptions about the interplay between the current thread and the other threads, we need to express the concept of threads to some extent. It su ces to create a new unrelated self identi er upon thread creation and to implant it as the forked threads' current self. We use a s to abbreviate s a s . q q Note that a fork is never blocking: we immediately return a linear private name r, which in turn might eventually be used to get some result the evaluation of the forked expression a back from the forked thread. This is achieved by waiting on this implicit return channel, when executing the translation of join. Here, b is an expression that evaluates to some thread identi er|in the translation, the thread is identi ed by the private channel r that has been returned from the corresponding fork-expression. Consequently, we block the continuation of the join-statement until some result is coming back along r from the forked thread and use this result also as the result of the join-expression itself.

4 Current and future work

We are on the verge of proving that Our -calculus semantics preserves typing. Our -calculus semantics implements self-serialization. Surrogation in jeblik is safe a:surrogate a for a suitable .

References

Car95 L. Cardelli. A Language with Distributed Scope. Computing Systems, 81:27 59, 1995. KS98 J. Kleist and D. Sangiorgi. Imperative Objects and Mobile Processes. In Proceedings of PROCOMET '98. IFIP, 1998. To appear. MS98 M. Merro and D. Sangiorgi. On Asynchrony in Name-Passing Calculi. In K. G. Larsen, ed, Proceedings of ICALP '98, volume 1443 of LNCS. Springer, July 1998. To appear.

8

50

Recent BRICS Notes Series Publications

¡§ NS-98-5 Hans Huttel and Uwe Nestmann, editors. Proceedings of the Workshop on Semantics of Objects as Processes, SOAP ¡¯98, (Aalborg, Denmark, July 18, 1998), June 1998. 50 pp. NS-98-4 Tiziana Margaria and Bernhard Steffen, editors. Proceedings of the International Workshop on Software Tools for Technology Transfer, STTT ¡¯98, (Aalborg, Denmark, July 12¨C13, 1998), June 1998. 86 pp. NS-98-3 Nils Klarlund and Anders M?ller. MONA Version 1.2 ¡ª User Manual. June 1998. 60 pp. NS-98-2 Peter D. Mosses and Uffe H. Engberg, editors. Proceedings of the Workshop on Applicability of Formal Methods, AFM ¡¯98, (Aarhus, Denmark, June 2, 1998), June 1998. 94 pp. NS-98-1 Olivier Danvy and Peter Dybjer, editors. Preliminary Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation, NBE ¡¯98, (Gothenburg, Sweden, May 8¨C9, 1998), May 1998. NS-97-1 Mogens Nielsen and Wolfgang Thomas, editors. Preliminary Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL ¡¯97 (Aarhus, Denmark, August 23¨C29, 1997), August 1997. vi+432 pp. NS-96-15 CoFI. CASL ¨C The CoFI Algebraic Speci?cation Language; Tentative Design: Language Summary. December 1996. 34 pp. NS-96-14 Peter D. Mosses. A Tutorial on Action Semantics. December 1996. 46 pp. Tutorial notes for FME ¡¯94 (Formal Methods Europe, Barcelona, 1994) and FME ¡¯96 (Formal Methods Europe, Oxford, 1996). NS-96-13 Olivier Danvy, editor. Proceedings of the Second ACM SIGPLAN Workshop on Continuations, CW ¡¯97 (ENS, Paris, France, 14 January, 1997), December 1996. 166 pp. NS-96-12 Mandayam K. Srivas. A Combined Approach to Hardware Veri?cation: Proof-Checking, Rewriting with Decision Procedures and Model-Checking; Part II: Articles. BRICS Autumn School on Veri?cation. October 1996. 56 pp.