% $Id: re24-ahern.tex,v 1.6 2005/08/16 09:37:40 aja Exp $ \documentclass[times,preprint]{sig-alternate-yoshida} \usepackage{mathptmx} \usepackage{courier} \usepackage[scaled=.90]{helvet} \usepackage[dvipsnames]{xcolor} \usepackage{amsmath} \usepackage{amssymb} \usepackage{mathptmx} \usepackage{enumitem} \usepackage{subfigure} \usepackage{dj-oopsla} % Listings package settings \lstset{% language=Java, % float=hbp,% basicstyle=\ttfamily\small, % identifierstyle=\color{Black}, % keywordstyle=\bfseries\color{blue}, % stringstyle=\color{Violet}, % commentstyle=\itshape\color{RedViolet}, % columns=flexible, % tabsize=2, % frame=single, % extendedchars=true, % showspaces=false, % showstringspaces=false, % numbers=left, % numberstyle=\tiny, % breaklines=true, %x breakautoindent=true, % xleftmargin=15pt,% Stops line numbers being in the middle captionpos=b,% mathescape=true,% morekeywords={thunk,freeze,eager,lazy,defrost,ser,serialize,deserialize},% escapeinside={(*@}{@*)}% } %================================= %\title{Need to Make Distributed Runtime Explicit} %\subtitle{Formal Analysis of RMI and Code Mobility} \title{Formalising Java RMI with Explicit Code Mobility} %\subtitle{Formal Analysis of RMI and Code Mobility} \numberofauthors{2} \author{% \alignauthor Alexander Ahern\email{aja@doc.ic.ac.uk} \alignauthor Nobuko Yoshida\email{yoshida@doc.ic.ac.uk} \sharedaffiliation \affaddr{Department of Computing}\\ \affaddr{Imperial College London}\\ \affaddr{180 Queen's Gate, London SW7 2AZ, UK}} % \pagestyle{plain} \def\sharedaffiliation{% \end{tabular} \begin{tabular}{c}} % \pagestyle{plain} \begin{document} \conferenceinfo{OOPSLA'05,}{October 16--20, 2005, San Diego, California, USA.} \CopyrightYear{2005} \crdata{1-59593-031-0/05/0010} \maketitle %\input{abstract} \begin{abstract} This paper presents a Java-like core language with primitives for object-oriented distribution and explicit code mobility. We apply our formulation to prove the correctness of several optimisations for distributed programs. Our language captures crucial but often hidden aspects of distributed object-oriented programming, including object serialisation, dynamic class downloading and remote method invocation. % It is defined in terms of an operational semantics that concisely models the behaviour of distributed programs using machinery from calculi of mobile processes. Type safety is established using invariant properties for distributed runtime configurations. We argue that primitives for explicit code mobility offer a programmer fine-grained control of type-safe code distribution, which is crucial for improving the performance and safety of distributed object-oriented applications. % \end{abstract} \category{D.3.1}{Programming Language}{Formal Definitions and Theory} \category{D.3.3}{Programming Language}{Language Constructs and Features} \category{F.3.2}{Theory of Computation}{Semantics of Programming Languages} \terms{Languages,Theory} \keywords{Distribution, Java, RMI, Types, Optimisation, Runtime, Code mobility} \pagestyle{plain} %\input{introduction_alex} %\input{introduction_first} %\input{introduction} \section{Introduction} % The purpose of this paper is to argue for the need of the formal % semantics % for distributed object-oriented programs which expose, at an appropriate level % of abstraction, run-time features including code mobility, with % concrete applications to justification of communication-oriented % optimisation of typical RMI-based programs. \noindent Language features for distributed computing form an important part of modern object-oriented programming. It is now common for different portions of an application to be geographically separated, relying on communication via a network. Distributing an application in this way confers many advantages to a programmer such as resource sharing, load balancing, and fault tolerance. However this comes at the expense of increased complexity for that programmer, who must now deal with concerns---such as network failure---that did not occur in centralised programs.% Remote procedure call mechanisms attempt to simplify such engineering practice by providing a seamless integration of network resource access and local procedure calls, offering the developer a programming abstraction familiar to them. Java Remote Method Invocation \cite{RMI} (RMI) is a widely adopted remote procedure call implementation for the Java platform, building on the customisable class loading system of the underlying language to further hide distribution from the programmer. When objects are passed as parameters to remote methods, if the provider of that method does not have the corresponding class file, it may attempt to obtain it from the sender. Such code mobility is important as it reduces the need for strong coupling between communicating parties, while preserving the type safety of the system as a whole. The implicit code mobility in RMI allows almost transparent use of remote objects and services. However when rigorously analysing the dynamics of distributed programs, or when providing programmers with source-level control over code distribution \cite{Christ00}, it becomes essential to model their behaviour explicitly. This is because elements such as distribution, network delay and partition crucially affect the behaviour and performance of programs and systems. As an example, communication-oriented RMI optimisations, often called \emph{batched futures} \cite{BogleLiskov94} or \emph{aggregation} \cite{YeungKelly03,YeungPhD}, use code distribution as their central element. To analyse these optimisations formally, or to make the most of them in applications, explicit primitives for code mobility are essential. This paper proposes a Java-like distributed object-oriented core language with communication primitives (RMI) and distributed runtime. The formalism exposes hidden runtime concerns such as code mobility, class downloading, object serialisation and communication. % The operational semantics concisely models this behaviour using machinery from calculi of mobile processes \cite{MilnerR:calmp1,SangiorgiD:expmpa,HondaK:ocac}. One highlight is the use of a \emph{linear} type discipline \cite{KPT96,Honda96,YBH} to ensure correctness of remote method calls. Another is the application of several invariant properties. These are conditions that hold during execution of distributed programs, and they allow type safety to be established. Our language supports \emph{explicit code mobility} by providing primitives that allow programs to communicate fragments of code---closely related to closures in functional languages---for later execution. This subsumes the standard serialisation mechanism by sending not only object graphs but also executable code. Code passing offers a programmer fine-grained control of type-safe code distribution, improving the safety and performance of their distributed applications. For example, a program fragment accessing a resource remotely could be frozen into a closure. This code could then be passed to the remote site, co-locating it with that resource. This effectively turns remote accesses into local accesses, reducing latency and increasing available bandwidth \cite{Christ00,BogleLiskov94,YeungKelly03,YeungPhD}. As an application of our formalism, we show that the RMI \emph{aggregation} optimisations proposed in \cite{YeungKelly03,YeungPhD} are type- and semantics-preserving. The generality of the primitive we introduce plays an essential role in this analysis: one optimisation relies on the use of second-order code passing, i.e. passing code that in turn passes code itself. % Similar optimisations naturally arise whenever latency and bandwidth are a limiting factor in the performance of distributed programs, suggesting a wide applicability of this primitive in similar endeavours. We summarise our major technical contributions below. \begin{itemize} \setlength{\itemsep}{-0.48mm}% \item Introduction of a core calculus for a class based %Java-like typed object-oriented programming language with primitives for concurrency and distribution, including RMI, explicit code mobility, thread synchronisation and dynamic class downloading. %(\S~3, \S~4). \item A technique to systematically prove type safety for distributed networks using distributed invariants. %(\S~6). Not only are they essential for proving type safety but also they are a useful analytical tool for developing consistent typing rules. %(\S~5.2.2). \item Justification of several inter-node RMI optimisations employing explicit code mobility, using a semantically sound syntactic transformation of the language and runtime. The analysis also demonstrates the greater control that explicit code mobility offers to programmers. %(\S~7.2). \end{itemize}% In the remainder, Section 2 informally motivates the present work through concrete examples of RMI optimisations. Section 3 introduces the syntax of the language. Sections 4 and 5 respectively discuss the dynamic semantics (reduction) and static semantics (typing) of the language. Section 6 establishes type safety and progress properties using the invariants. Section 7 studies contextual congruence of the core language and applies the theory to justify the optimisations in Section 2. Section 8 discusses related work. Section 9 concludes the paper with further topics. Due to space limitations, the detailed definitions and proofs, as well as many examples, are left to the full technical reports \cite{dcblfull,oopslafull} available from: {\texttt{{http://www.doc.ic.ac.uk/\~{ }aja/dcbl.html}}}. %\input{examples} \section{Motivation: representing and justifying RMI optimisation} \label{sec:examples} \noindent The RMI optimisations introduced in this section are used as running examples, culminating in their justification by the behavioural theory in \S~\ref{sec:behaviour}. These are (arguably) typical inter-node optimisations of distributed object-oriented programs. Just as inter-procedure or inter-module optimisations are hard to analyse, RMI optimisation poses a new challenge to the semantic analysis of distribution. They also motivate the use of explicit code mobility for fine-grained control of distributed behaviour and to improve performance. \bfpara*{Original RMI program 1} In optimisations for sequential languages, we can aim to improve execution times by removing redundancy and ensuring our programs exploit features of the underlying hardware architecture. In distributed programs these are still valid concerns, but other significant optimisations exist, in particular how latency and bandwidth overheads can be reduced. One typical example of this sort, centring on Java RMI \cite{Flanagan00} but which is generally applicable to various forms of remote communication, is \emph{aggregation} \cite{BogleLiskov94,YeungKelly03,YeungPhD}. We explain this idea using a simple program. \begin{lstlisting} int m1(RemoteObject r, int a) { int x = r.f(a); int y = r.g(a, x); int z = r.h(a, y); return z; } \end{lstlisting} This program performs three remote method calls to the same remote object \java{r} with eight items transferred across the network (counting each parameter and return value as one). \java{x} is returned as the result of the call to \java{f} from the remote server, but is subsequently passed back to the server during the next call. The same occurs with the variable \java{y}. These variables are unused by the client, and are merely returned to the remote object \java{r} (where they were created) as parameters to the next call. We can immediately see that there is no need for \java{x} or \java{y} to ever be passed back to the client at all. Hence these three calls can be \emph{aggregated} into a single call, reducing by a factor of three the network latency incurred by the method \java{m1} and approximately reducing by a factor of four the amount of data that must be shipped across the network. This optimisation methodology is implemented in the Veneer virtual Java Virtual Machine (vJVM) \cite{YeungKelly03,YeungPhD}, where sequences of adjacent calls to the same remote object are grouped together into an execution \emph{plan} in bytecode format. This is then uploaded to and executed by the server, with the result of the computation being returned to the client. This simple idea---remote evaluation of code \cite{StamosGrifford}---can speed up distributed programs significantly, especially when operating across slower networks or when significant amounts of data may be transmitted otherwise. As a concrete example, in \cite{YeungKelly03} the authors reported that over a moderate bandwidth and moderate latency ADSL connection, call aggregation yields a speedup over a factor of four for certain examples \cite{Flanagan00}. \bfpara*{Optimised program 1} Call aggregation implicitly uses code passing: we first collect all the code that can be executed at a remote site and then send it, in one bundle, for execution there. This aspect is hidden as the transfer of bytecode in the implementation of \cite{YeungKelly03,YeungPhD}, but requires explicit modelling if one wishes to discuss its properties or show that it preserves the original program semantics. For this purpose we introduce two primitives, \java{freeze} and\\ \java{defrost}. These mimic primitives found in well-known functional languages, for example the quotation and evaluation of code in Scheme, or the higher-order functions found in ML and Haskell. We illustrate these primitives using the optimised version of the code above. \begin{lstlisting} // Client int mOpt1(RemoteObject r, int a) { thunk t = freeze { int x = r.f(a); int y = r.g(a, x); int z = r.h(a, y); z; }; return r.run(t); } // Server int run(thunk x) { return defrost(x); } \end{lstlisting} \begin{framefig}[tbp] \centering \subfigure[Aggregation]{\label{fig:examples:diag:a} \includegraphics{diagrams/aggregation.mps}} \subfigure[Server forwarding]{\label{fig:examples:diag:b}\includegraphics{diagrams/forwarding.mps}} \newline% \begin{tabular}[c]{ll} \emph{Pale arrows}& Original calls in the unoptimised program.\\% \emph{Dashed arrows}& Returns from remote calls.\\% \emph{Thick arrows}& Represent code mobility.% \end{tabular} \flushleft We annotate call arrows with the method invocation and return arrows with the name of the variable the client will use to store the return value of the method. \caption{Example optimisations} \label{fig:examples:agg} \end{framefig} Here the client uses the \java{freeze} expression of the language to create a frozen representation of three calls with a closure of free variable \java{a}, sending the resulting ``thunk'' to the server. \java{thunk} says the frozen code contains an expression of type \java{int}. We now make only one call across the network to send the frozen expression, by \java{r.run(t)}. When the server receives the thunked code, it evaluates it and returns the result typed by \java{int} to the client, again across the network. In \figref{examples:diag:a} we show a diagram of the situation. As can be seen, the original sequence of calls (the paler arrows) requires 6 trips across the network. By aggregating the calls at the server, where they effectively become local, we see that only two trips are required (the thicker arrows). \bfpara*{Original RMI program 2} A more advanced form of communication-oriented optimisation, which reduces latency and uses bandwidth intelligently, is the idea of \emph{server forwarding} \cite{YeungKelly03,YeungPhD}. It takes advantage of the fact that servers typically reside on fast connections, whilst the client-server connection can often be orders of magnitude slower. Consider the following program. \begin{lstlisting} int m2(RemoteObject r1, RemoteObject r2, int a) { int x1 = r1.f1(a); int y1 = r1.g1(a, x1); int z1 = r1.h1(a, y1); int x2 = r2.f2(z1); int y2 = r2.g2(z1,x2); int z2 = r2.h2(z1,y2); return z2; } \end{lstlisting} The results of the first three calls are used as arguments to methods on another remote object \java{r2} in a second server. It would be better for the first server to communicate directly with the second. In \figref{examples:diag:b} we give a diagram of the situation. \bfpara*{Optimised program 2} Server forwarding again uses code passing as an execution mechanism. We use closure passing for representing this optimised code, in which thunked code is \emph{nested}, i.e. we are using higher-order code mobility. \begin{lstlisting} int mOpt2(RemoteObject r1, RemoteObject r2, int a) { thunk t1 = freeze { int x1 = r1.f1(a); int y1 = r1.g1(a, x1); int z1 = r1.h1(a, y1); thunk t2 = freeze { int x2 = r2.f2(z1); int y2 = r2.g2(z1, x2); int z2 = r2.h2(z1, y2); z2; }; r2.run(t2); }; return r1.run(t1); } \end{lstlisting} \bfpara*{Original RMI program 3} The semantics of RMI is different from normal, local method invocation. Passing a parameter to a remote method (or accepting a return value) can involve many operations hidden from the end-user; these runtime features make automatic semantic-preserving optimisation of RMI much harder, in particular, when calls contain \emph{objects as arguments}. To observe this, let us change the type of \java{a} from \java{int} to class \java{MyObj} as in the following code: \begin{lstlisting} int m3(RemoteObject r, MyObj a) { int x = r.f(a); int y = r.g(a, x); int z = r.h(a, y); return z; } \end{lstlisting} Here we have two cases: \begin{description}[style=sameline,noitemsep] \item[\java{MyObj} is \emph{remote}] i.e.~when \java{MyObj} implements the \java{java.rmi.Remote} interface and is therefore remotely callable. In this situation, \java{a} is effectively passed by \emph{reference}. \item[\java{MyObj} is \emph{local}] i.e.~when \java{MyObj} is not remotely callable (it does not implement the \java{Remote} interface), \java{a} is automatically \emph{serialised} and passed to the server where it is automatically \emph{deserialised}. In this situation, \java{a} is effectively passed by \emph{value}. \end{description} \noindent Sending a serialised value to a remote consumer can be thought of as passing an object by \emph{value}. Informally, the serialisation process explores the graph under an object in local memory, copying all objects directly or indirectly referred to. %For instance, assuming %that \java{A}, \java{B} and \java{C} are local classes, consider the %following program: %\begin{lstlisting} %class A { % B b; C c; % A (B b, C c) { this.b = b; this.c = c; } %} %serialize(new A(new B(), new C())); %\end{lstlisting} %The serialisation operation here would create an accurate copy of the %object \java{a} by first copying its fields \java{b} and \java{c} %recursively. When passing such local objects as parameters to remote methods, the Java RMI system automatically performs this copying. %Here the syntax %\java{serialize} as shorthand for the idiom in the real Java language %that involves writing objects to an instance of the %\java{ObjectOutputStream} class. Similarly, we write %\java{deserialize} in place of reading from an %\java{ObjectInputStream}. %We make use of explicit serialisation to preserve the meaning of %programs transformed to use code passing. In particular, any remote %method call that passes local objects as parameters must be treated %with care, as we shall explain. %Consider the method \java{m3} above: if the call \java{r.f} performs %an operation that side-effects its parameter \java{a} then in the %original program there is no problem. The version of \java{a} supplied %to the next method \java{r.g} is still just a copy of the initial %\java{a} held in the client's memory, which has not changed. %If we na\"ively apply code passing optimisations to the problem, we might rewrite %method \java{m3} to look a lot like \java{mOpt1}. Unfortunately now %the next call \java{r.g} no longer has a copy of the original \java{a} %to work on: it instead receives the version modified by \java{r.f}, %potentially altering the meaning of the program and rendering the %optimisation incorrect. Consider the method \java{m3} above: if the call \java{r.f} performs an operation that side-effects the parameter \java{a}, then in the original program this side-effect is lost. The version of \java{a} supplied to the next method \java{r.g} is still just a copy of the initial \java{a} held in the client's memory, which has not changed. If we na\"ively apply code passing optimisations to the problem, we might rewrite method \java{m3} to look much like \java{mOpt1}. Unfortunately now the next call \java{r.g} no longer has a copy of the original \java{a} to work on: it instead receives the version modified by \java{r.f}, potentially altering the meaning of the program and rendering the optimisation incorrect. By applying explicit serialisation we can simulate the original program behaviour. By insisting each method call in the server operates on a fresh copy of the original \java{a}, we regain correctness as is shown below. %I propose to move this sentence to the conclusion. %The question is whether the original copying semantics of %Java RMI are easy to understand for the programmer: %through our code freezing primitive we can allow %side-effects at the server side in sequences of remote calls. \bfpara*{Optimised program 3} We show the case when \java{MyObj} is a local class. If there are no call-backs from the server to the client (discussed next), then the original RMI program has the same meaning as passing the following code. First the client creates three copies of serialised object \java{a} by applying the explicit serialisation operator \java{serialize}. We write \java{serialize} as shorthand for the idiom in Java that involves writing objects to an instance of \java{ObjectOutputStream}. The server immediately deserialises the arguments, creating three independent object graphs, thus avoiding problems with methods that alter their parameters (we write \java{deserialize} in place of reading from an\\ \java{ObjectInputStream}). \begin{lstlisting} // Client int mOpt3(RemoteObject r, MyObj a) { ser b1 = serialize(a); ser b2 = serialize(a); ser b3 = serialize(a); thunk t = freeze { int x = r.f(deserialize(b1)); int y = r.g(deserialize(b2), x); int z = r.h(deserialize(b3), y); z }; return r.run(t); } \end{lstlisting} In the above code, the declaration \java{ser b1} says that \java{b1} is a serialised representation of an object of class \java{MyObj}. \bfpara*{Two further problems} We have seen that code passing primitives can help us to cleanly represent communication-based optimisation of RMI programs. Analysis of the code above immediately suggests two further problems that must be addressed. %before we can give a precise semantic account of RMI optimisation. \begin{description} \setlength{\itemsep}{-1mm}% \item[1. Sharing between objects and call-backs:] the above copying\\ method should not be applied na\"ively, since marshaling should preserve sharing between objects. It also may not be applicable if a call by the client to the server results in the server calling the client. \item[2. Overhead of class downloading:] if the server location does not contain the byte-code for \java{MyObj}, RMI automatically invokes a class downloading process to obtain the class from the network. In addition, verifying that the received class is safe to use may require the downloading of many others (such as all superclasses of \java{MyObj} and classes mentioned in method bodies and so on), which may incur many trips across the network, increasing the risk of failures and adding latency. \end{description} To illustrate the first problem, consider the following simple code with \java{r} remote and \java{x} and \java{y} local: \begin{lstlisting} x.f = y; r.h(x, y); \end{lstlisting} The content of \java{y} is shared with \java{x} in the original code, but if we apply the copying method then the server creates independent copies of \java{x} and \java{y}, breaking the original sharing structure. %For the second point of (1), suppose, in the original RMI code 3, %\aja{serialisation of \java{a} in line 3 occurs when the call %\java{r.f} in line 2 is made,} i.e.~\java{r.f} invokes a call-back %from the server to the client, and this behaviour directly or %indirectly conspires to modify \java{a} in the client; then the %optimised program 2 is no longer correct since \java{a} is serialised %in line 4 before \java{r.f} in line 7 is performed. For the second point of (1), imagine that the body of remote method \java{f} invoked at line 2 of the original program involves some communication back to the local site. Then it is possible for the value of \java{a} to be modified at the client side and so the optimised program is no longer correct: because in our optimised program, \java{a} is serialised in line 4 before \java{r.f} is performed, any effect that a call-back would have on \java{a} is lost, when it \emph{should} be visible to the call \java{r.g}. The second problem, class downloading, is more subtle from the communication-based optimisation viewpoint. Although the aim of this optimisation is to reduce the number of trips across the network, if there is a deep inheritance hierarchy above \java{MyObj}, sending code may not yield the performance benefit that the programmer expects. This is because many requests over the network may be required to obtain all the required classes. As an example, if \java{MyObj} has a chain of $n$-superclasses such that \java{MyObj}\ $\subtypes$\ \java{MyObj2} \ $\subtypes\dotsb\subtypes$ \ \java{MyObjn}, and none of these are present at the server, there are at least $n$ class downloads even with ``verification off'' in the framework of type safe dynamic linking \cite{aja:liang98dynamic,aja:qian00formal}. With ``verification on'', this could be even more. These hidden features of RMI make reasoning about the behaviour of a program, and establishing a clear optimisation, hard. \bfpara*{Challenges} Having provided the source-level presentation of several features necessary to discuss RMI optimisations, we may ask the following questions: \begin{enumerate}[label=Q{\arabic*}.] \item\label{int:q1} How can we precisely model this dynamic runtime behaviour, including code passing, serialisation and class downloading? \item\label{int:q2} How can we verify the correctness of the optimised code, in the sense that the original code and the optimised code have the same contextual behaviour? \item\label{int:q3} Having studied the optimisations above, can we improve our code mobility primitives to make them generally useful to application programmers? %%% NY original %Does the semantic account of these optimisations %guide us to design and articulate newly %proposed language constructs on the basis of clear semantic %foundations for distribution? \end{enumerate} %It should be noted that A satisfactory solution to \ref{int:q1} is a prerequisite for \ref{int:q2} due to the interleaving of communication events which affect the observational behaviour of distributed programs. % For example, Various elements inherent in distributed computing make the semantic correctness of optimisations more subtle than in the sequential setting. The behaviour, hence the final answer, may differ depending on sharing of objects, timing and class downloading strategies, as well as network failure. In our paper, \ref{int:q1} will be answered by giving a clean formal semantics for distributed object-oriented features usually hidden from a programmer. We shall distill key runtime features, including class downloading and serialisation, so that important design choices (for example various class downloading and code mobility mechanisms) can be easily reflected in the semantics. \ref{int:q2} will be answered by semantic justification of the above optimisations using the theory of mobile processes \cite{MilnerR:calmp1,SangiorgiD:expmpa,HondaK:ocac}. For \ref{int:q3}, we summarise our proposal below. \bfpara*{Optimised program 4} Class downloading is a fundamental mechanism in distributed object-oriented programming. Yet so far we have treated it as a behind-the-scenes feature and left it as an implementation detail. However, by augmenting our primitives with a mechanism to control class downloading, a programmer is able to write down different strategies explicitly. This explicit control allows us to mitigate some of the problems class downloading induces that were explained in the previous section. %Shifting code mobility to the user level primitive, %this explicit presentation in turn is essential for improving %the state of the art of distributed object-oriented languages. %This explicit presentation in turn is essential for semantic %discussions of code mobility in the presence of exceptions and network failure %\cite{YeungKelly03,YeungPhD} and for performance prediction. For example, to represent one basic strategy of class downloading, we attach the tag \java{eager} to \java{freeze} in the original code 3. \begin{lstlisting} // Client int mOpt4(RemoteObject r, MyObj a) { ... // as in mOpt3 thunk t = freeze[eager] { ... // as in mOpt3 } \end{lstlisting} The tag \java{eager} in \java{freeze[eager]} controls the amount of class information sent along with the body of the thunk by the user. With \java{eager}, the code is automatically frozen together with all classes that \emph{may} be used. In the above case all classes appearing in \java{MyObj} and all their superclasses are shipped together with the code (see \S~\ref{subsec:thunk} for the definition). Another option is for the user to select \java{lazy} which essentially leaves class downloading to the existing RMI system. Further the user might write a list of specific classes $\vec{C}$ to be shipped. For example, the following program %instead of relying on the standard Java lazy policy %(which has no knowledge of execution environment), is able to notice when it is in a high latency situation and act accordingly. \begin{lstlisting} // Client thunk t; if (pingTime() > 1000) {// milliseconds t = freeze[eager] {...}; } else { t = freeze[lazy] {...}; } \end{lstlisting} If we imagine that the latency is very high, then it may be the case that the time to iteratively download all the superclasses exceeds the actual execution time of the frozen code being sent to the server. Because of this, the program is able to switch to the \java{eager} mode of class downloading, allowing improved performance. Moreover, from a point of view of failure there are fewer trips across the network with the eager policy, reducing the risk of a transient problem, such as a temporary network partition, disrupting the class downloading process. The formal semantics for both implicit and explicit code mobility is given from the next section as part of the core language. %\input{syntax} \section{Language}\label{sec:syntax} \subsection{User syntax}\label{subsec:usersyntax} \noindent The syntax of the core language, which we call \DJ, is an extension of FJ \cite{FJ} and MJ \cite{MJ}, augmented with basic primitives for distribution and code-mobility, along with concurrent programming features that should be familiar to Java programmers. The syntax comes in two forms, and is given in \figref{syntax}. The first form is called \emph{user syntax}, and corresponds to terms that can be written by a programmer as source code. The second form is called \emph{runtime syntax}. It extends the user syntax with constructs that only appear during program execution, and these are distinguished in the figure by placing them in shaded regions. We briefly discuss each syntactic category below. \begin{framefig*}[tbp] \centering \[\begin{array}[c]{rrl@{}rrl} \multicolumn{6}{l}{% \text{Syntax occurring only at runtime appears in \rtsyntax{\text{shaded}} regions.}% }% \\% [3mm] \text{(Types)}& T ::=& \tbool~~|~~\tunit~~|~~C~~|~~T\rightarrow U\\% \text{(Returnable)}& U ::=& \tvoid ~~|~~ T\\% % [1mm] \text{(Classes)}& L ::=& \lclassdefault&% \text{(Constructors)}& K ::=& \kcon{C}{\vec{T}\vec{f}}{\mathtt{super}(\vec{f});\efldvec{\ethis}{f} = \vec{f}}\\% % [1mm] \text{(Methods)}& M ::=&\multicolumn{4}{l}{\mmethoddefault}\\% % [1mm] \text{(Expressions)}& e ::=&% \multicolumn{4}{l}{% v~~|~~x~~|~~\ethis~~|~~\econd{e}{e}{e}~~|~~\ewhile{e}{e}~~|~~\efld{e}{f}~~|~~% e;e~~|~~x=e~~|~~\efld{e}{f} = e~~|~~\enew{C}{\vec{e}}% }\\% &|&\multicolumn{4}{l}{% \emeth{e}{m}{e}~~|~~T~x=e~~|~~\ereturn{e}~~|~~\ereturn{}~~|~~% \efreeze[t]{T~x}{e}~~|~~\edefrost{e}{e}% }\\% &|&\multicolumn{4}{l}{% \efork{e}~~|~~\esync{e}{e}~~|~~\ewait{e}~~|~~\enotify{e}~~|~~\enotifyall{e}% }\\% &|&\multicolumn{4}{l}{% \rtsyntax{\enew{C^l}{\vec{e}}~~|~~\edownload{\vec{C}}{l}{e}~~|~~% \eresolve{\vec{C}}{l}{e}~~|~~\eawait{c}~~|~~\esandbox{e}}% }\\% &|&\multicolumn{4}{l}{% \rtsyntax{\einsync{o}{e}~~|~~\eready{o}{n}~~|~~\ewaiting{c}{n}~~|~~\error} }\\% % [1mm] \text{(Tags)}& t ::=& \eager~~|~~\lazy~~|~~\vec{C}\\% % [1mm] \text{(Values)}& v ::=&% \multicolumn{4}{l}{% \vtrue~~|~~\vfalse~~|~~\vnull~~|~~\vunit~~|~~\rtsyntax{o~~|~~\vfrozen{T~x}{\vec{u}}{l}{e}{\store}{\ct}% ~~|~~\epsilon}}\\% % [1mm] \text{(Class Sig.)}& \csig ::=&\multicolumn{4}{l}{\emptyset~~|~~\csig\cdot C:\csigentryboth{D}}\\% % [1mm] \text{(Identifiers)}& u ::=& x~~|~~\rtsyntax{o~~|~~c}\\% % [1mm] \text{(Threads)}& P ::=&% \multicolumn{4}{l}{% \rtsyntax{% \NIL~~|~~P_1 \PAR P_2~~|~~(\NEW u) P~~|~~\eforked{e}~~|~~\egowith{e}{c}~~|~~\ewith{e}{c}% ~~|~~\egoto{e}{c}~~|~~\ereturn[c]{e}~~|~~\error% }% }\\% % [1mm] \text{(Configurations)}& F ::=& \rtsyntax{(\NEW\vec{u})(P,\store,\ct)}&% \text{(Networks)}& N ::=& \rtsyntax{\NIL~~|~~l[F]~~|~~N_1 \PAR N_2~~|~~(\NEW u) N}\\% % [1mm] \text{(Stores)}& \store ::=& \rtsyntax{\emptyset~~|~~\store\sapp\sentry{x}{v}~~|~~% \store\sapp\sentry{o}{\sobj{C}{\vec{f}:\vec{v}}{n}{\{\vec{c}\}}}}&% \text{(Class tables)}& \ct ::=& \rtsyntax{\emptyset~~|~~\ct\cdot[C\mapsto L]}% \end{array}\] \caption{The syntax of the language \DJ.} \label{fig:syntax} \end{framefig*} \paragraph*{\textsf{Types}} $T$ and $U$ range over types for expressions and statements, which are explained in \S~\ref{sec:typing}. $C,D,F$ range over class names. $\vec{f}$ denotes a vector of fields, and $\vec{T}\vec{f}$ is short-hand for a sequence of typed field declarations: $T_1 f_1;\dotsc;T_n f_n$. We assume sequences contain no duplicate names, and apply similar abbreviations to other sequences with $\epsilon$ representing the empty sequence. $T\rightarrow U$ denotes an \emph{arrow type}, which is assigned to frozen expressions that expect a parameter of type $T$ and return a value of type $U$. We abbreviate the type of thunked frozen expressions as $\tthunk{U}\EQDEF\tunit\rightarrow U$. We associate the type $\tser{U}$ with frozen \emph{values}. If a value $v$ has type $U$ is frozen then the result has the type $\tser{U}$. \paragraph*{\textsf{Expressions}} The syntax is standard, including the standard synchronisation constructs of the Java language, except for two code passing primitives. The first primitive, $\efreeze[t]{T~x}{e}$ takes the expression $e$ and, without evaluating it, produces a flattened value representation parameterised by variable $x$ with type $T$. Any parts of the local store required by the expression (such as the information held in variables free in $e$) are included in this new value, along with class information it may need for execution. The tag $t$ is a flag to control the amount of this information sent along with $e$ by the user. If he specifies $\eager$, then the code is automatically frozen together with all classes that \emph{may} be used. If the user selects $\lazy$, it is the responsibility of the receiving virtual machine to obtain missing classes. The third option is called \emph{user-specified} information, and allows the programmer to supply a list of class names. Only these classes and their dependents (such as superclasses) are included with the frozen value. Dual to freezing, the action $\edefrost{e_0}{e}$ expects the evaluation of expression $e$ to produce a piece of frozen code. This code is then executed, substituting its parameter with the value obtained by evaluating $e_0$, much like invoking a method. We abbreviate freeze and defrost expressions that take no parameters as $\efreeze[t]{}{e}\EQDEF\efreeze[t]{\tunit~x}{e}$, $x\notin\FV{e}$ and $\edefrost{}{e}\EQDEF\edefrost{\vunit}{e}$ respectively. Note that $\vunit$ denotes a constant of $\tunit$ type. To simplify the presentation, we only allow single parameters to methods and to frozen expressions. This does not restrict the expressiveness of programs written in \DJ, as there is a semantics and type-preserving mapping from programs with multiple parameters to this subset. See \S~\ref{sec:behaviour} for the formal proofs. For clarity, we introduce two \emph{derived} constructs that are syntactic sugar for serialisation and deserialisation. \[\begin{array}[c]{rcl} \eser{e}&\EQDEF&\efreeze[\lazy]{}{e}\\% \edeser{e}&\EQDEF&\edefrost{}{e}% \end{array}\] \paragraph*{\textsf{Class Signatures}} A class signature $\csig$ is a mapping from class names to their interface types (or signatures). We assume $\csig$ is given globally, as a minimum agreed interface between remote parties, unlike class tables which are maintained on a per-location basis. Attached to each signature is the name of a direct superclass, as well as the declaration ``$\mathtt{remote}$'' if the class is remote. For a class $C$, the predicate $\REMOTE{C}$ holds iff ``$\mathtt{remote}$'' appears in $\csig(C)$; otherwise $\LOCAL{C}$ holds. Class signatures contain only the types of fields and expected method signatures, not their implementation. This provides a lightweight mechanism for determining the type of remote methods. \subsection{Runtime syntax} \noindent Runtime syntax extends the user syntax to represent the distributed state of multiple sites communicating with each other, including remote operations in transit. \paragraph*{\textsf{Expressions}} Location names are written $l,m,\dotsc$ and can be thought of as IP addresses in a network. $\enew{C^l}{\vec{v}}$, $\edownload{\vec{C}}{l}{e}$ and $\eresolve{\vec{C}}{l}{e}$ define the machinery for class downloading, which will be explained along with the operational semantics in \S~\ref{subsec:expression} and \S~\ref{subsec:classloading}. The key expression is $\enew{C^l}{\vec{e}}$, indicating that the definition of class $C$ can be obtained from a location called $l$ should it need to be instantiated. We write $C^{\_}$ when the treatment of class name $C$ is independent of whether it is labelled or not. $\eawait{c}$ is fundamental to the model of method invocation and can be thought of as the return point for a call. $\esandbox{e}$ represents the execution environment of some code $e$ that originated from a frozen expression. $\einsync{o}{e}$ denotes that expression $e$ has previously acquired the lock on object $o$. When an expression contains $\eready{o}{n}$ as a sub-term it indicates that it is ready to re-acquire the lock on object $o$. The expression $\ewaiting{c}{n}$ denotes an expression waiting for notification on channel $c$, at which point it may try to re-acquire a lock it was holding. $n$ indicates the number of times that this waiting thread had entered its lock before yielding. Finally, the expression $\error$ denotes the null-pointer error. \paragraph*{\textsf{Values}} $v$ is also extended with runtime terms. Object identifiers $o$ denote references to instances of classes as well as the destination of RMI calls. We shall often write ``o-id'' for brevity. Channels $c$ are fundamental to the mechanism of method invocation and determine the return destination for both remote and local method calls, as illustrated in the operational semantics later. We call $o$ and $c$ \emph{names}. The most interesting extended value is a \emph{frozen expression}, a piece of code or data that can be passed between methods as a value. Later, it can be ``defrosted'' at which point it is executed to compute a value. $\vfrozen{T~x}{\vec{u}}{l}{e}{\store}{\ct}$ denotes an expression $e$ frozen with class table $\ct$ created at $l$. Expression $e$ is parameterised by variable $x$ with type $T$, and $\store$ contains data local to the expression that was stored along with it at ``freezing time''. The identifiers $\vec{u}$ correspond to the domain of $\store$. $\ct$ ships class bodies that may be used during the execution of $e$. If it is empty and the party evaluating $e$ lacks a required class, it should attempt to download a copy from $l$. If $\store$ or $\ct$ is empty, then we shall omit writing them entirely for clarity. Finally, the value $\epsilon$ serves as a constant that appears at runtime as the return value of $\tvoid$ methods. \paragraph*{\textsf{Threads}} $P\PAR Q$ says $P$ and $Q$ are two threads running in parallel, while $(\NEW u)P$ restricts identifier $u$ local to $P$. $\NIL$ denotes an empty thread. This notation comes from the $\pi$-calculus \cite{MilnerR:calmp1}. It also includes $\error$ which denotes the result of class downloading and communication failure. The expression $\eforked{e}$ says that expression $e$ was previously forked from another thread. The remaining constructs of $P$ are used for representing the RMI mechanism, and are illustrated when we discuss the operational semantics in \S~\ref{sec:os}. \paragraph*{\textsf{Configurations and Networks}} $F$ represent an instance of a virtual machine. A configuration $(\NEW\vec{u})(P,\store,\ct)$ consists of threads $P$, a store $\store$ containing local variables and objects, and a class table $\ct$. Networks are written $N$, and comprise zero or more located configurations executing in parallel. $\NIL$ denotes the empty network. $l[F]$ denotes a configuration $F$ executing at location $l$. $N_1\PAR N_2$ and $(\NEW\vec{u})N$ are understood as in threads. A \emph{store} $\store$ consists of a mapping from variable names to values, written $\sentry{x}{v}$, or from object identifiers to store objects, written $\sentry{o}{\sobj{C}{\vec{f}:\vec{v}}{n}{\{\vec{c}\}}}$. This indicates an identifier $o$ maps to an object of class $C$ with a vector of fields with values $\vec{f}:\vec{v}$. The set of channels $\{\vec{c}\}$ contains identifiers for threads currently waiting on $o$, i.e. those that have executed $\ewait{o}$ and have not received notification. The number, $n$, indicates how many times the lock on this object has been entered by a thread. Finally, class tables $\ct$, are a mapping from unlabelled class names to class definitions (metavariable $L$ in \figref{syntax}). Throughout the paper we write $\fct$ for the \emph{foundation class table} that contains the common classes that every location in the network should possess, roughly corresponding to the \java{java.*} classes. %\input{semantics} \newpage \section{Operational Semantics}\label{sec:os} \noindent This section presents the formal operational semantics of \DJ, extending the standard small step call-by-value reduction of \cite{PierceBC:typsysfpl,MJ}. There are two reduction relations. The first is defined over configurations executing within an individual location, written $F\RED[l]F'$, where $l$ is the name of the location containing $F$. The second is defined over the networks, written $N\RED N'$. $F\RED[l] F'$ promotes to $l[F]\RED l[F']$. Both relations are given modulo the standard structural equivalence rules of the $\pi$-calculus \cite{MilnerR:calmp1}, written $\equiv$. We define \emph{multi-step} reductions as: $\MRED\EQDEF(\RED\cup\equiv)^{*}$ and $\MRED[l]\ \EQDEF\ (\RED[l]\cup\equiv)^{*}$. The reduction rules not introduced in this section are left to the the Appendix. \subsection{Local expressions} \label{subsec:expression} \noindent The rules for the sequential part of the language are standard \cite{FJ,MJ}. We list only the rules for object creation in \figref{obj-creation}. \begin{framefig}[tbp] \centering \begin{align*} &\inferrule[\rulelabel{red-new}{New}]{% \fields(C)=\vec{T}\vec{f}\\% C\in\DOM{\ct}% }{% \enew{C^\_}{\vec{v}},\store,\ct\RED[l](\NEW o)(o,\store\sapp\sentry{o}{\sobj{C}{\vec{f}:\vec{v}}{0}{\emptyset}},\ct)% }\\% &\inferrule[\rulelabel{red-newr}{NewR}]{% C\notin\DOM{\ct}% }{% \enew{C^m}{\vec{v}},\store,\ct\RED[l]\edownload{C}{m}{\enew{C}}{\vec{v}},\store,\ct% }% \end{align*} \caption{Rules for object creation} \label{fig:obj-creation} \end{framefig} \noindent When allocating a new object by \ruleref{red-new}, we explicitly restrict identifiers, which represents ``freshness'' or ``uniqueness'' of the address in the store. The auxiliary function $\fields(C)$ examines the class signature and returns the field declarations for $C$. Tagged class creation takes place in \ruleref{red-newr}. This rule is applied whenever execution attempts to instantiate an object of a tagged class whose body is not present in the local class table. Instead of immediately allocating a new object, it first attempts to download the actual body of the class from the labelled location. This is discussed in detail in \S~\ref{subsec:classloading}. To reduce the number of computation rules, we make use of the evaluation contexts in \figref{evaluation-contexts}. Contexts contain a single hole, written $[~]$ inside them. $E[e]$ represents the expression obtained by replacing the hole in context $E$ with the ordinary expression $e$. The evaluation order of terms in the language is determined by the construction of these contexts. \begin{framefig}[tbp] \begin{align*} E &::= [~]~~|~~\econd{E}{e}{e}~~|~~\efld{E}{f}~~|~~E;e~~|~~x=E\\% &|~~\efld{E}{f}=e~~|~~\efld{o}{f}=E~~|~~\enew{C^{\_}}{\vec{v},E,\vec{e}}~~|~~% \emeth{E}{m}{e}~~|~~\emeth{o}{m}{E}\\% &|~~T~x = E~~|~~\edefrost{e}{E}~~|~~\edefrost{E}{v}\\% &|~~\esync{E}{e}~~|~~\ewait{E}~~|~~\enotify{E}~~|~~\enotifyall{E}\\% &|~~\esandbox{E}~~|~~\einsync{o}{E}~~|~~\eforked{E}~~|~~\egowith{E}{c}\\% &|~~\ewith{E}{c}~~|~~\egoto{E}{c}~~|~~\ereturn[c]{E}% \end{align*} \caption{Evaluation contexts} \label{fig:evaluation-contexts} \end{framefig} \subsection{Class downloading}\label{subsec:classloading} \noindent Class mobility is very important in Java RMI systems, since it reduces unnecessary coupling between communicating parties. If an interface can be agreed, then any class that implements the interface can be passed to a remote consumer and type-safety will be preserved. However this only works if sites are able to dynamically acquire class files from one another. This hidden behaviour is omitted from known sequential formalisms, as it is not required in the single-location setting, and so the formalisation of class downloading is one of the key contributions of \DJ. The rules for class downloading in \DJ\ are given in \figref{marshal} and approximately model the lazy downloading mechanism found in JDK 1.3 without verification \cite{aja:drossopoulou02manifestations}. The \emph{download} expression is responsible for the transfer of class table entries from a remote site. \ruleref{red-download} defines the semantics for this operation. For a download request $\edownload{\vec{C}}{l}{e}$ we first produce $\vec{D}$ by removing the names of any classes locally available (and thus eliminating duplication). We then compute vector $\vec{F}$ from all the {\em free class names} mentioned in the bodies of the classes in $\vec{D}$. Finally, the classes named in $\vec{D}$ are downloaded and added to the local class table. $\FCL{\ct_2(\vec{D})}$ denotes the union of free class names in class $D_i$. A class name $C$ is \emph{free} if it is the subject of an instantiation operation (written $\enew{C}{\dotso}$), or if it appears as the class of an object in stores ($[o \mapsto (C,...)] \in \store$). The function $\mathsf{fcl}$ is defined over expressions, threads, stores and class table entries. %\footnote{At first glance it may appear %strange that computation occurs at both sides of the network in %\ruleref{red-download}. However we choose to abstract from the finer %mechanics of requesting a class for download in this paper.} Any occurrence of a member of $\vec{F}$ in a newly downloaded class body is tagged with the name of the remote site ($l_2$ in this case). \emph{Resolution}, defined by \ruleref{red-resolve}, is the process of examining classes for unmet dependencies and scheduling the download of missing classes. Informally this amounts to downloading immediate superclasses. The \ruleref{red-download} and \ruleref{red-resolve} rules work together to iteratively resolve all class dependencies for a given object. Once all dependencies have been met, normal execution continues after \ruleref{red-dnothing}. \begin{framefig}[tbp] \centering \begin{align*} &\inferrule[\rulelabel{red-resolve}{Resolve}]{% \ct(C_i)=\lclass{C_i}{D_i}{\vec{T}\vec{f}}{K}{\vec{M}}% }{% \eresolve{\vec{C}}{l'}{e},\store,\ct %\\\\% \RED[l]% \edownload{\vec{D}}{l'}{e},\store,\ct% }\\% &\inferrule[\rulelabel{red-download}{Download}]{% \{\vec{D}\}=\{\vec{C}\}\setminus\DOM{\ct_1}\\% \{\vec{F}\}=\FCL{\ct_2(\vec{D})}\\% \ct'=\ct_2(\vec{D})[\vec{F}^{l_2}/\vec{F}]% }{% l_1[E[\edownload{\vec{C}}{l_2}{e}]\PAR P,\store_1,\ct_1]\PAR l_2[P_2,\store_2,\ct_2]\\\\% \RED\\\\% l_1[E[\eresolve{\vec{D}}{l_2}{e}]\PAR P,\store_1,\ct_1\cup \ct']\PAR l_2[P_2,\store_2,\ct_2]% }\\% &\inferrule[\rulelabel{red-dnothing}{DNothing}]{% }{% \edownload{\vec{C}}{l'}{e},\store,\ct\RED[l] e,\store,\ct% }\qquad C_i\in\DOM{\ct}\\% &\inferrule[\rulelabel{err-classnotfound}{Err-ClassNotFound}]{% \exists C_i\in\vec{C}.C_i\notin\DOM{\ct_1}\cup\DOM{\ct_2}% }{% l_1[E[\edownload{\vec{C}}{l_2}{e}]\PAR P,\store_1,\ct_1]\PAR l_2[P_2,\store_2,\ct_2]\\\\% \RED% l_1[E[\error]\PAR P,\store_1,\ct_1]\PAR l_2[P_2,\store_2,\ct_2]% }% \end{align*} \caption{Rules for class resolution and downloading} \label{fig:marshal} \end{framefig} We model a failure in this process by the last rule. The rule \ruleref{err-classnotfound} approximates \java{ClassNotFoundException} that would occur in the case of the site $l_2$ not possessing some class requested by $l_1$. In this case, the code attempting the download will reduce to the $\error$ expression. In this paper we chose the option of class loading without verification as it allows significantly simpler presentation. However, our formalisation is modular: we can model different class loading mechanisms by adjusting the reduction rules for downloading and resolution and the class graph algorithm introduced in \defref{class-graph}. For example, in rule \ruleref{red-resolve} the vector $\vec{D}$ is constructed from the direct superclasses of the classes being resolved. One aspect of Java verification is that it checks subtypes for method arguments. By inspecting the body of methods in the classes being resolved, we could extend $\vec{D}$ to reflect these checks as a first approximation. Following on from this we observe that , with verification \emph{on}, the overhead induced by Java's lazy class loading policy is increased---since verifying a class typically requires the loading of more classes than just the direct superclass---making an even stronger case for eager code passing. \subsection{Serialisation and deserialisation}\label{subsec:serialisation} \noindent One of the contributions of \DJ\ is a precise formalisation of the semantics of serialisation, using the frozen expressions which are detailed in \S~\ref{subsec:thunk} (for the encoding, see \S~\ref{subsec:usersyntax}). Serialisation occurs in two instances. In the first, the expressions $\eser{e}$ and $\edeser{e}$ allow explicit flattening and re-inflation of objects by the programmer, whereas the second instance occurs when values must be transported across the network. $\eser{e}$ and $\edeser{e}$ must appear automatically as runtime expressions to serialise parameters and return values of remote method invocations. This is because instances of local classes---those classes without the $\mathtt{remote}$ keyword in their signature---are incapable of remote method invocation, and so cannot be passed by reference as parameters or as return values to remote methods. Should this occur, the remote party would receive the identifier of an unreachable object. Avoiding this problem involves making a deep clone of the local object, and we see this in action in \S~\ref{subsec:RMI}. \subsection{Method invocation}\label{subsec:RMI} \noindent Unlike centralised formalisms, \DJ\ describes \emph{remote method invocation}. To accommodate RMI, the rules for method call take a novel form employing concepts from the $\pi$-calculus, representing the context of a call by a local linear channel. While this technique is well-known in the $\pi$-calculus \cite{MilnerR:calmp1}, \DJ\ may be the first to use it to faithfully capture the semantics of RMI in a Java-like language. Among other benefits, it allows us to define the semantics of local and remote method calls concisely and uniformly: a method call is local when the receiver is co-located with the caller; whereas it becomes remote when the receiver is located elsewhere. Remote calls also differ from local ones because of the need for parameter serialisation, which is reflected as several extra reduction steps. We summarise the general picture of a remote method invocation in \figref{methodinvocation:pic}, which starts from dispatch of a remote method and ends with delivery of its return value. The corresponding formal rules are given in \figref{methodinvocation:rules}. We start our illustration from local method calls. For a method call $\emeth{o}{m}{v}$, if $o\in\DOM{\store}$ then the rule \ruleref{red-methlocal} is applied. A new channel $c$ is created to carry the return value of the method; the return point of the method call is replaced with the term $\eawait{c}$ corresponding to a receiver waiting for the return value supplied on channel $c$. The method call itself is spawned in a new thread as $\ewith{\emeth{o}{m}{v}}{c}$ carrying channel $c$. \begin{framefig} \centering \subfigure[Evaluation steps for a remote call]{\label{fig:methodinvocation:pic} \includegraphics[scale=0.8]{diagrams/go-with-to.mps}} \subfigure[Reduction rules]{\label{fig:methodinvocation:rules} \begin{minipage}[c]{0.5\textwidth} \begin{align*} &\inferrule[\rulelabel{red-methlocal}{MethLocal}]{% c~\text{fresh},o\in\DOM{\store}% }{% E[\emeth{o}{m}{v}]\PAR P,\store,\ct% \RED[l](\NEW c)(E[\eawait{c}]\PAR\ewith{\emeth{o}{m}{v}}{c}\PAR P,\store,\ct)% }\\% &\inferrule[\rulelabel{red-methremote}{MethRemote}]{% c~\text{fresh},o\notin\DOM{\store}% }{% E[\emeth{o}{m}{v}]\PAR P,\store,\ct\\\\% \RED[l]% (\NEW c)(E[\eawait{c}]\PAR\egowith{\emeth{o}{m}{\eser{v}}}{c}\PAR P,\store,\ct)% }\\% &\inferrule[\rulelabel{red-methinvoke}{MethInvoke}]{% \store(o)=\sobj{C}{\dotso}{}{}\\%(C,\dotso)\\% \mbody{m}{C}{\ct} = (x,e)% }{% \ewith{\emeth{o}{m}{v}}{c},\store,\ct\\\\% \RED[l](\NEW x)(e[o/\ethis][\ereturn[c]{}/\ereturn{}],\store\sapp\sentry{x}{v},\ct)% }\\% &\inferrule[\rulelabel{red-await}{Await}]{}{% E[\eawait{c}]\PAR\ereturn[c]{v},\store,\ct\RED[l] E[v],\store,\ct% }\\% &\inferrule[\rulelabel{red-retser}{SerReturn}]{% c\notin\FN{P}% }{% l[\ereturn[c]{v}\PAR P,\store,\ct]\RED l[\egoto{\eser{v}}{c}\PAR P,\store,\ct]% }\\% &\inferrule[\rulelabel{red-leave}{Leave}]{% o\in\DOM{\store_2}% }{% l_1[\egowith{\emeth{o}{m}{v}}{c}\PAR P_1,\store_1,\ct_1]\PAR l_2[P_2,\store_2,\ct_2]\\\\% \RED% l_1[P_1,\store_1,\ct_1]\PAR l_2[\ewith{\emeth{o}{m}{\edeser{v}}}{c}\PAR P_2,\store_2,\ct_2]% }\\[2mm]% &\inferrule[\rulelabel{red-return}{Return}]{% c\in\FN{P_2}% }{% l_1[\egoto{v}{c}\PAR P_1,\store_1,\ct_1]\PAR l_2[P_2,\store_2,\ct_2]\\\\% \RED% l_1[P_1,\store_1,\ct_1]\PAR l_2[\ereturn[c]{\edeser{v}}\PAR P_2,\store_2,\ct_2]% }\\% &\inferrule[\rulelabel{messagelossleave}{Err-LostCall}]{% }{% \egowith{\emeth{o}{m}{v}}{c},\store,\ct \ % \RED[l]% \ \error,\store,\ct% }\\% &\inferrule[\rulelabel{messagelossreturn}{Err-LostReturn}]{% }{% \egoto{v}{c},\store,\ct \ % \RED[l]% \ \error,\store,\ct% }% \end{align*} \end{minipage}} \caption{Remote method invocation} \label{fig:methodinvocation} \end{framefig} The next stage is the application of the method invocation rule \ruleref{red-methinvoke}. Both remote and local invocations apply this rule. The auxiliary function $\mbody{m}{C}{\ct}$ looks up the correct method body in the local class table. It returns a pair of the method code and the formal parameter name. The receiver is substituted $[o/\ethis]$ and a new store entry $x$ is allocated for the formal parameter $v$. We apply the substitution $[\ereturn[c]{}/\ereturn{}]$ to indicate that the return value of the method must be sent along channel $c$. The rule \ruleref{red-await} is used to communicate the return value to its caller. When $o\notin\DOM{\store}$ the method invocation is \emph{remote}. The rule \ruleref{red-methremote} is applied, with care being taken to automatically serialise any local object identifiers in the vector of parameters $\vec{v}$. We note that frozen values are also transferred to the remote location without modification (like base values). After serialisation, we are left with a thread of the form\\ $\egowith{\emeth{o}{m}{w}}{c}$ where $w$ is the serialised representation of the original parameter $v$. At this point, the network level rule \ruleref{red-leave} triggers the migration of the calling thread to the location that holds the receiving object in its local store. After transfer over the network, the parameters are automatically deserialised and \ruleref{red-methinvoke} applied. Again, the return value must be automatically serialised using \ruleref{red-retser}. Then it crosses the network by application of \ruleref{red-return}. After returning to the caller site, it is again deserialised. The last two rules present instances of network failure. In the case of \ruleref{messagelossleave}, the network becomes partitioned such that a remote method call attempting to reach its destination cannot. Likewise, in \ruleref{messagelossreturn}, the return value from a remote method call is lost. Both cases reduce to $\error$. \subsection{Direct code mobility}\label{subsec:thunk} \noindent Frozen expressions offer a direct way to manipulate code and data. They permit the storing of unevaluated terms that can, for example, be shipped to remote locations for evaluation or merely saved for future use. As we have seen in \S~\ref{subsec:usersyntax}, our formulation of the primitives subsumes the serialisation operations found in Java that were explained in \S~\ref{subsec:serialisation}. As introduced in \figref{syntax}, there are two operations associated with frozen values---for their creation and use---called \emph{freezing} and \emph{defrosting} respectively. Their rules are given in \figref{thunking}. \begin{framefig}[tbp] \centering \begin{align*} &\inferrule[\rulelabel{red-freeze}{Freeze}]{% \{\vec{y}\} = \FV{e}\setminus\{x\}\\% \store_y = \bigcup\store(y_i) \\\\\vspace*{1mm}% \store' = \OG{\store}{\FN{e}\cup\FN{\store_y}}\cup\store_y\\% \{\vec{u}\} = \DOM{\store'}\\\\\vspace*{1mm}% \mbox{$% \ct'=% \begin{cases}% \CG{\ct}{\FCL{e}\cup\FCL{\store'}} & t = \eager\\% \CG{\ct}{\vec{C}}&t=\vec{C}\\% \emptyset & t = \lazy% \end{cases}$}% }{% \efreeze[t]{T~x}{e},\store,\ct\RED[l]\vfrozen{T~x}{\vec{u}}{l}{e}{\store'}{\ct'},\store,\ct% }\\% &\inferrule[\rulelabel{red-defrost}{Defrost}]{% \{\vec{C}\}=\FCL{e}\setminus\DOM{\ct'}\\% \{\vec{F}\}=\FCL{\store'}\setminus\DOM{\ct'}% }{% \edefrost{v}{\vfrozen{T~x}{\vec{u}}{m}{e}{\store'}{\ct'}},\store,\ct\\\\% \RED[l]%\\\\% (\NEW x\vec{u})(\edownload{\vec{F}}{m}{\esandbox{e[\vec{C^m}/\vec{C}]}},\\\\% \store\cup\store'\sapp\sentry{x}{v},\ct\cup\ct')% }\\% &\inferrule[\rulelabel{red-sandbox}{LeaveSandbox}]{% }{% \esandbox{v},\store,\ct\RED[l]v,\store,\ct% }% \end{align*} \caption{Rules for creating and executing frozen expressions} \label{fig:thunking} \end{framefig} Freezing is given by \ruleref{red-freeze}, and has modes $\lazy$, $\eager$, and \emph{user-specified}. Its operation is divided into two steps. The first step in any mode is to determine the store locations used by the expression $e$. We do this by examining the expression for any free variables, excluding the formal parameter $x$. The store entries for each variable are copied, $\store_y$. Next, we search for all the free object identifiers in $e$, written $\FN{e}$. Because variables may hold references to objects, we must then examine the store fragment $\store_y$ for any object identifiers held in the co-domain of variable mappings. Finally, objects have internal structure, so we apply the object graph function given in \defref{object-graph} to copy all local objects transitively referenced by $e$ or its variables, resulting in $\store'$. Base values stored in variables are copied ``as-is''. In the second step the freezing mode matters because it directly affects the amount of class information included in $\ct'$. For the $\lazy$ case, no extra classes are provided with the expression, so the result of applying \ruleref{red-freeze} is a value of the form $\vfrozen{T~x}{\vec{u}}{l}{e}{\store}{\emptyset}$. When the case is $\eager$, the creator of the frozen expression takes responsibility for including \emph{all} classes that $e$ and $\store'$ depend upon. In the case that the user specifies a list of classes $\vec{C}$, only those classes and their dependencies are included. In either situation, we must use the class graph algorithm in \defref{class-graph} to determine the classes that the expression (or the user-specified classes) depends upon. %The application of this algorithm in \ruleref{red-freeze} is written\\ %$\ct'=\CG{\ct}{\FCL{e}\cup\FCL{\store'}}$ where %$\FCL{e}\cup\FCL{\store'}$ denotes the union of the \emph{free class %names} in expression $e$ and $\store'$. A class name $C$ is %\emph{free} if it is the subject of an instantiation operation %(written $\enew{C}{\dotso}$), or if it appears as the class of an %object in $\store'$. The function $\mathsf{fcl}$ is defined over %expressions, threads, stores and class table entries. \begin{defn}%[Object graph] \label{def:object-graph} \em The function $\OG{\store}{v}$ which computes the object graph of value $v$ in store $\store$ is defined as follows. \begin{align*}% \OG{\store}{v}&=% \begin{cases}% \emptyset & \hspace{-5em}\text{if~}v\notin\DOM{\store}\lor\REMOTE{C}\\% \sentry{v}{\sobj{C}{\vec{f}:\vec{v}}{0}{\emptyset}}\bigcup\OG{\store_i}{o_i}&\text{otherwise}% \end{cases}% \end{align*} where $\store(v)=\sobj{C}{\vec{f}:\vec{v}}{n}{\{\vec{c}\}}$, $\{\vec{o}\}=\FN{\vec{v}}$, $\store_1=\store\setminus\{v\}$ and $\store_{i+1}=\store_i\setminus\DOM{\OG{\store_i}{o_i}}$. \end{defn} The object graph is defined as the set of all mappings from object identifier to store object for every local object transitively referenced by local object identifier $v$. The lock count, $n$, for each object is reset to zero when copied and the blocked set $\vec{c}$ emptied to preserve linearity. If the value $v$ refers to a remote object, or a base value such as a boolean, then the object graph is empty. In the full Java language, fields may be marked $\mathtt{transient}$. Such fields are never serialised (for example they may contain a value that can be derived from other fields, or a reference to a non-serialisable object). Similarly, the Emerald language \cite{Emerald} supports a qualifier called ``$\mathtt{attached}$'' that indicates which of an object's fields should be brought along it when it is copied. To support these extra features in \DJ\ would involve the straightforward extension of syntax and a trivial modification to the object graph algorithm. \begin{defn}%[Class graph] \label{def:class-graph} \em The function $\CG{\ct}{T}$ computes the class graph of type $T$ in class table $\ct$ as follows: \[\begin{array}[c]{ll} % \CG{\ct}{\tbool}=\CG{\ct}{\tvoid}=\CG{\ct}{C^l}=\emptyset\\ \CG{\ct}{\vec{M}}\ = \ \bigcup{\CG{\ct}{\FCL{e_i}}}~\text{with}~M_i=\mmethod{U_i}{m_i}{C_i~x_i}{e_i}\\[1mm] \CG{\ct}{C} \ = \ \begin{cases} \emptyset & \text{if~}C\notin\DOM{\ct}\lor C\in\DOM{\fct}\\ \CG{\ct}{\ct(C)} & \text{otherwise} \end{cases}\\[1mm] \CG{\ct}{\vec{C}} \ = \ \bigcup\CG{\ct}{C_i}\\ % \quad \quad \CG{\ct}{e}\ = \ \CG{\ct}{\FCL{e}}\\% \CG{\ct}{\lclassdefault}\\ \quad\quad =\ \CG{\ct\setminus C}{D} \cup~\CG{\ct\setminus C}{\vec{M}}\\\quad\quad\cup[C\mapsto\lclassdefault]% \end{array}\] \end{defn} A small example of the freezing process is as follows: \begin{lstlisting} class A { int f; B g; A(int f, B g) { this.f = f; this.g = g; } } class B { } // Program: int y = 6; A o1 = new A(5, new B()); freeze[B](int x){x + y + o1.f}; \end{lstlisting} After executing the above program at location $l$, we should obtain a frozen expression of the form: \begin{align*} &\vfrozen{\mathtt{int}~x}{o_1,o_2,y}{l}{x+y+\efld{o_1}{f}}{\store_1}{\ct_1}\\% \text{where}~&\store_1=\sentry{o_1}{\sobj{A}{f:5,g:o_2}{0}{\emptyset}}\sapp% \sentry{o_2}{\sobj{B}{\epsilon}{0}{\emptyset}}\sapp\sentry{y}{6}\\% \text{and}~&\ct_1=[B\mapsto\dotso]% \end{align*} To defrost a frozen value $\vfrozen{T~x}{\vec{u}}{l}{e}{\store_1}{\ct_1}$ we use \ruleref{red-defrost}. Firstly, any classes supplied with the frozen value are appended to the current class table. Any class names appearing free in $e$ are tagged with their originating location: $\enew{C}{\vec{e}}$ becomes $\enew{C^l}{\vec{e}}$. During execution of the newly defrosted code, when an expression such as the above $\enew{C^l}{\vec{v}}$ is encountered then \ruleref{red-newr} is applied if the body of $C$ has not been downloaded to the execution location. The second stage is to merge the data shipped with the value, $\store_1$, into the local store. It is not possible to merely append this to the local store, since this could cause a name clash (for example two entries for variable $x$ in the same scope). Therefore we create new memory locations for the formal parameter of the frozen expression, as well as for every element in the domain of the accompanying store entries. This is written $(\NEW x\vec{u})$. It is then safe to append the new store and allocate space for the formal parameter. We write the new store at the location as $\store\cup\store_1\sapp\sentry{x}{v}$. The final aspect of the defrost rule is to download the classes for all the objects added to the store in the previous step, because we may have added instances of classes not present at this location. This means instead of immediately evaluating $e$ we call $\edownload{\vec{F}}{l}{\esandbox{e}}$. This accurately mimics the mechanism employed by the \java{RMIClassLoader} class used in RMI. When sending marshaled objects, RMI implementations annotate the data stream for classes with a codebase URL. This is a pointer to a remote directory that the \java{RMIClassLoader} can refer to download classes that are not available at the current location. After class downloading has completed, we are left with an expression of the form $\esandbox{e}$. Execution inside the sandbox then proceeds until a value is computed, which is then propagated to the enclosing scope according to the rule \ruleref{red-sandbox}. Take the frozen expression computed in the example previously and call it $t$. We now give another example of defrosting this time at a location $m$, where it is important to notice that a variable $y$ is already in scope: here the $\NEW$-operator will be used to avoid collision of bound variables. We abbreviate $\mathtt{download}$ to $\mathtt{dl}$ and $\mathtt{sandbox}$ to $\mathtt{sb}$ in the following: \begin{align*} &\edefrost{5}{t},\sentry{y}{\vtrue},\ct\\% \RED[m]&(\NEW x,o_1,o_2,y_2)(\edownloadshort{A}{l}{\esandboxshort{x + y_2 + \efld{o_1}{f}}},\store_2,\ct_2)\\% \text{with}~&\store_2=\sentry{y}{\vtrue}\sapp\sentry{o_1}{\sobj{A}{f:5,g:o_2}{0}{\emptyset}}\sapp\\% &\phantom{\store_2=}\sentry{o_2}{\sobj{B}{\epsilon}{0}{\emptyset}}\sapp\sentry{y_1}{6}\sapp\sentry{x}{5}\\% \text{and}~&\ct_2=\ct\sapp[B\mapsto\dotso]\\% \RED[m]&(\NEW x,o_1,o_2,y_1)(\eresolve{A}{l}{\esandboxshort{x + y_1 + \efld{o_1}{f}}},\store_2,\ct_3)\\% \text{with}~&\ct_3=\ct_2\sapp[A\mapsto\dotso]% \end{align*} Assuming that the superclass of $A$ is \object, this should already be present in the local class table. \begin{align*} \RED[m]&(\NEW x,o_1,o_2,y_1)(\edownloadshort{\object}{l}{\esandboxshort{x + y_1 + \efld{o_1}{f}}},\store_2,\ct_3)\\% \RED[m]&(\NEW x,o_1,o_2,y_1)(\esandboxshort{x + y_1 + \efld{o_1}{f}},\store_2,\ct_3)\\% \MRED[m]&\esandboxshort{16},\sentry{y}{\vtrue},\ct_3 \ \ \RED[m] \ 16,\sentry{y}{\vtrue},\ct_3% \end{align*} In the final steps, we garbage-collect the store entries added by the frozen expression since they are now no longer required. %nor reachable from any other part of the store. We do not model %garbage collection of class data, even though this is subject to the %same garbage collection as any other object in the JVM. To illustrate the different class loading mechanisms, we change the above example as follows and investigate the cases when we change \java{B} in \java{freeze} to \java{eager} or \java{lazy}. \begin{lstlisting} class A extends C{ ...} class B { } class C {D d(){return new D()}} class D { } \end{lstlisting} \begin{itemize} \item In the case of \java{eager}, the frozen expression ships all classes (\java{A,B,C,D}). Hence there is no downloading required after \java{defrost}. \item In the case of \java{lazy}, the frozen expression ships no classes. When defrosting, it downloads \java{A} and \java{B}. When resolving them at the next step, \java{A}'s superclass \java{C} is called to be downloaded. After \java{C} is downloaded, the final class table becomes $\ct_5= \ct_3\cdot [C \mapsto \mathtt{class}\ C \ \{ D \ \mathtt{d}() \{ \ereturn{\enew{D^l}{}} \} \} ]$. Note that \java{D} is \emph{not} downloaded: hence it is renamed to \java{D}${}^l$ so that if \java{D} requires instantiation, \ruleref{red-newr} will be applied and \java{D} downloaded from $l$. \end{itemize} \subsection{Correctness of graph algorithms}\label{subsec:graph} \noindent In this subsection we show the correctness of the graph algorithms that are used in the proof of the results in \S~\ref{sec:invariant}. The reader may safely skip this subsection if they wish. \sfpara*{Object graph algorithm} %First we show that the object graph algorithm is correct %, and to do this we introduce the preliminary %notion of \emph{reachability}. The predicate $\REACHABLE{\store}{o}{o'}$ holds if there exists a path in store $\store$ from the object with identifier $o$ to the object with identifier $o'$. This can be an immediate link (when $o'$ is stored in a field of $o$), or it can be via the fields of one or more intermediaries. This is defined below, where $\store(o)=\sobj{C}{\vec{f}:\vec{v}}{\dotso}{}$: \begin{multline*} \REACHABLE{\store}{o}{o'} \iff\\% (o'\in\FN{\vec{v}}\lor\exists o''\in\FN{\vec{v}}.\REACHABLE{\store}{o''}{o'})% \end{multline*} With this predicate, $RCH(\store)$ which contains all reachable pairs of objects in a store $\store$, is defined below. \begin{align*} RCH(\store) = \{(o,o')~|~\forall o,o'\in\DOM{\store}.o\neq o'\land\REACHABLE{\store}{o}{o'}\}% \end{align*} Our object graph algorithm must, to be correct, preserve the tree structure of the store when copying objects, hence it must preserve this reachability relation. %To determine correctness of the above algorithm, %we introduce the notion of a \emph{complete object graph} as follows. For a store $\store$ and an object graph $\store_g$ computed from that store, the predicate $\OGCOMPLETE{\store}{\store_g}$ (\emph{completeness of object graph}) holds if the computed graph preserves the reachability relation for all object identifiers in its object domain. Given $RCH({\store})$ and $RCH({\store_g})$, we define: \begin{align*} \OGCOMPLETE{\store}{\store_g} & ~\text{if for all } o\in\DOM{\store}\cap\DOM{\store_g}, \\% &(o,o')\in RCH({\store}) \iff (o,o')\in RCH({\store_g})% \end{align*} This property ensures all links are correctly copied to the graph $\store_g$, and no new links are created. %An interesting point is The algorithm used to compute the class graph can safely add extra objects into $\store_g$ without violating this property iff those objects are \emph{unreachable} from any other that should be in the graph. %Intuitively, safety is preserved since the recipient %of such an object graph will merely add an unreachable element to %its store (which could be immediately garbage collected). \sfpara*{Class graph algorithm} The correctness of the class graph algorithm relies upon the definition of the following predicate: \begin{align*} \COMPLETE{C}{\ct}\EQDEF \forall D~C\subtypes D.D\in\DOM{\ct} \end{align*} which is read: class table $\ct$ is \emph{complete with respect to} class $C$. When $C$ is actually used, the class table $\ct$ at that location should be complete w.r.t. $C$. We extend the notion of completeness to entire class tables: we say a class table $\ct$ is \emph{complete} if the following predicate holds: \begin{align*} \CTCOMPLETE{\ct}\EQDEF\forall D\in \DOM{\ct}.\ \COMPLETE{D}{\ct} \end{align*} This means for every class $D\in\DOM{\ct}$, every superclass of $D$ is also available in $\ct$. With these preliminaries dealt with, we have the following lemma: \begin{lemma}\emph{(Correctness of algorithms)} \ % \label{lem:graphs:complete-cg}\label{lem:graphs:og-complete} \setlength{\itemsep}{-1mm}% \begin{enumerate} \item $\store'=\OG{\store}{v}$ implies $\OGCOMPLETE{\store}{\store'}$.% \item $\CTCOMPLETE{\ct}$ and $\ct'=\CG{\ct}{C}$ imply $\CTCOMPLETE{\ct'\cup\fct}$. \end{enumerate} \end{lemma} %\input{typing} \section{Typing System}\label{sec:typing} \noindent This section presents the key typing rules for \DJ, focusing on the linear channel types and the use of invariants for typing runtime expressions and the new primitives. First we introduce the syntax of types and environments in \figref{types-syntax}. \begin{framefig}[htb] \begin{align*} T &::=\tbool ~|~ \tunit ~|~ C ~|~ T\rightarrow U &% &\text{(Types)}\\% U &::=\tvoid ~|~ T&% &\text{(Returnable types)}% \intertext{Extended types not appearing in program text:}% S &::= U ~|~ \tret{U}&% &\text{(Return types)}\\% \tau &::=\tchan ~|~ \tchani{U} ~|~ \tchano{U}&% &\text{(Channel types)}\\% \teenv &::=\emptyset ~|~ \teenv,x:T ~|~ \teenv,o:C ~|~ \teenv,\ethis:C&% &\text{(Expression environment)}\\% \tcenv &::=\emptyset ~|~ \tcenv,c:\tau&% &\text{(Channel environment)}% \end{align*} \caption{Syntax of types and environments} \label{fig:types-syntax} \end{framefig} $T$ represents expression types: booleans, class names, frozen expressions that take a parameter of type $T$ and return elements of type $U$ and the $\tunit$ type. The metavariable $U$ ranges over the same types as $T$ but is augmented with the special type $\tvoid$ with the usual empty meaning. We write $C\subtypes D$ when class $C$ is a subtype of class $D$. Our notion of subtyping is mostly standard (we assume $\subtypes$ causes no cycle as in \cite{FJ,MJ}), and is judged on the class signature. The arrow type is standard. Two runtime types (which do not appear in programs) are newly introduced. \emph{Return types} are ranged over by $S$ are used to denote the type of value returned by a method invocation ($\mmethoddefault$ is well-typed if $e$ has the type $\tret{U}$). \emph{Channel types} are ranged over by metavariable $\tau$ and represents the types for channels used in method calls, which is explained in the next subsection. There are two different kinds of environment. The environment for typing expressions, written $\teenv$, is a finite map from variables, o-ids and $\ethis$ to types ranged over by $T$. $\tcenv$ is a finite map from channel names to channel types, and appears in judgements for method calls and those involving multiple threads and locations. We often omit empty environments from judgements for clarity of presentation. \subsection{Linear channel types} \label{subsec:lineartype} \noindent One of the key tasks of the typing rules is to ensure \emph{linear} use of channels. This means that for every channel $c$ there is exactly one process waiting to input from $c$ and one to output to $c$. In terms of \DJ, this ensures that a method receiver always returns its value (if ever) to the correct caller, and that a returned value always finds the initial caller waiting for it. In \figref{types-syntax}, $\tchani{U}$ is \emph{linear input} of a value of type $U$; $\tchano{U}$ is the opponent called \emph{linear output}. The type $\tchan$ is given to channels that have matched input and output types. $\tchani{U}$ is assigned to $\mathtt{await}$, while $\tchano{U}$ is to threads with/to $c$ (either $\ereturn[c]{e}$, $e \ \mathtt{with}/\mathtt{to} \ c$, or $\mathtt{go} \ e \ \mathtt{with}/\mathtt{to} \ c$). To see the use of linear types, consider the following network; the return expression cannot determine the original location if we have two $\mathtt{await}$s at the same channel $c$, violating the linearity of $c$. \begin{align} &l_1[E_1[\eawait{c}],\sigma_1,\ct_1]% \PAR l_2[E_2[\eawait{c}],\sigma_2,\ct_2]\PAR\nonumber\\% &l_3[\egoto{v}{c},\sigma_3,\ct_3]\label{eq:net2}\\% \intertext{The uniqueness of the returned answer is also lost if return channel $c$ appears twice.}% &l_1[\ereturn[c]{e_1},\sigma_1,\ct_1]% \PAR l_2[\ereturn[c]{e_2},\sigma_2,\ct_2]\label{eq:net3}% \end{align} The aim of introducing linear channels is to avoid these situations during execution of runtime method invocations. The following binary operation $\asymp$ is used for controlling the composition of threads and networks. \begin{defn}%[Channel environment composition] \label{def:composition} \em The commutative, partial, binary composition operator on channel types, $\odot$, is defined as $\tchani{U}\odot\tchano{U}\EQDEF\tchan$. Then we define the composition of two channel environments $\tcenv[1]\odot\tcenv[2]$ as: \begin{align*} \tcenv[1]\odot\tcenv[2]\EQDEF&\{\tcenv[1](c)\odot\tcenv[2](c)~|~c\in\DOM{\tcenv[1]}\cap\DOM{\tcenv[2]}\}\\ &\cup\tcenv[1]\setminus\DOM{\tcenv[2]}\cup\tcenv[2]\setminus\DOM{\tcenv[1]}% \end{align*} Two channel types, $\tau$ and $\tau'$ are \emph{composable} iff their composition is defined: $\tau\asymp\tau'\iff\tau\odot\tau'~\text{is defined}$. Similarly for $\tcenv[1]\asymp\tcenv[2]$. \end{defn} \noindent Note that $\odot$ and $\asymp$ are partial operators. Hence the composition of other combinations is not allowed. Once we compose linear input and output types, then it is typed by $\tchan$, hence it becomes uncomposable because $\tchan\not\asymp\tau$ for any $\tau$. Intuitively if $P$ is typed by environment $\tcenv[1]$ and $Q$ by $\tcenv[2]$, and if $\tcenv[1]\asymp\tcenv[2]$, then we can compose $P$ and $Q$ as $P\PAR Q$ safely, preserving channel linearity. Hence \eqref{eq:net2} is untypable because of $\tchani{U}\not\asymp\tchani{U}$ at $c$. \eqref{eq:net3} is too by $\tchano{U}\not\asymp\tchano{U}$ at $c$. \subsection{Value and expression typing} \label{typing:val} \noindent Types are assigned to values and expressions using only the expression environment $\teenv$. They have judgements of the form: \begin{align*} \teenv\proves e:\alpha&&\text{$e$ has type $\alpha$ in expression environment $\teenv$.}% \end{align*} where $\alpha$ ranges over $T$, $U$ and $S$. The judgement is lightweight or local in the sense that it does not require the current global or local class table $\ct$ such as $\teenv\proves_{\ct} e:U$; this approach is not suitable for \DJ\ since during execution, new classes may be downloaded or discovered. The lightweight judgement is possible by the use of the class signatures and invariants as explained below. \vspace{15pt} % Needed to get freeze and defrost into the new column \bfsubsubsection{Freeze and Defrost} \noindent First we focus on the key typing rule for frozen expressions: \begin{align*} &\inferrule[\rulelabel{tv-frozen}{TV-Frozen}]{% \teenv,x:T,\vec{u}:\vec{T}'\proves e:U\\% \teenv,\vec{u}:\vec{T}';\emptyset\proves\store:\ok\\% \proves\ct:\ok% }{% \teenv\proves\vfrozen{T~x}{\vec{u}}{l}{e}{\store}{\ct}:T\rightarrow U% }% \end{align*} The rule for typing a frozen expression is given in \ruleref{tv-frozen}. In order for such a value to be well-typed we must ensure that the store $\store$ and $\ct$ are well-typed, and that the expression $e$ computes a result of the expected type when supplied its formal parameter. The simplicity of this rule comes from the assumption that runtime values are created under the invariants defined in \S~\ref{sec:invariant}. By combining with the invariants, we shall see: \begin{itemize} \setlength{\itemsep}{0mm}% \item Instances of remote classes are not contained in $\store$, i.e.~if $o\in\DOM{\store}$, then we have $\store(o)=\sobj{C}{\dotso}{}{}$ with $\LOCAL{C}$. This is guaranteed by the combination of invariants from \ref{def:invariants:thread-variables-in-scope} to \ref{def:invariants:remote-oids} in \S~\ref{subsec:locality}. \item The closure contains no free variables and no local object-identifiers: for example, by the combination of the invariants from \ref{def:invariants:thread-variables-in-scope} to \ref{def:invariants:fieldstores-are-closed} in \S~\ref{subsection:others}, we know $\store(o_i)=v_i$ is closed so that we can ensure that the resulting frozen value is closed again. \end{itemize} The assumption for the class table is more complicated as shall be explained in the next section. We now show the typing rules for the freezing and defrosting operations: \begin{align*} &\inferrule[\rulelabel{te-freeze}{TE-Freeze}]{% \teenv,x:T\proves e:U% }{% \teenv\proves\efreeze[t]{T~x}{e}:T\rightarrow U% }&% &\inferrule[\rulelabel{te-defrost}{TE-Defrost}]{% \teenv\proves e_0:T'\\% T'\subtypes T\\\\% \teenv\proves e:T\rightarrow U% }{% \teenv\proves\edefrost{e_0}{e}:U% }%% \end{align*} \bfsubsubsection{Locality for field and thread synchronisation} \label{subsub:locality} \noindent There are two important restrictions which we should impose in correspondence with the current Java implementation. The first constraint is to disallow field access and assignment to a remote object in a different location. Hence the following should be prohibited even if class $C$ is remote. \begin{eqnarray} \label{invalidfield} l[E[\efld{o}{f}]|P, \store_1, \ct_1]\PAR m[Q, \store_2\sapp\sentry{o}{\sobj{C}{\dotso}{}{}},\ct_2] \end{eqnarray} However we wish to allow to type the following with class $C$ remote: \begin{eqnarray} \label{validfield} l[E[\efld{o}{f}]|P, \store_1\sapp\sentry{o}{\sobj{C}{\dotso}{}{}},\ct_1]\PAR m[Q, \store_2, \ct_2] \end{eqnarray} An early version of the work simply replaced the typing rule for field access with one that prevented it on any instance of a remote class. While safe this was overly restrictive, since even at the location where the remote object was held in store, no update to any of its fields could ever take place, hence \eqref{validfield} above was untypable. In order to propose a typing rule to prevent remote field access statically but allow field access on remote objects locally, we require a combination of the locality invariants in \S~\ref{subsec:locality}, the rule \ruleref{te-fld} and also the initial conditions explained in \defref{initial}. The rule \ruleref{te-fld} restricts field accesses only for local classes if $e$ is neither $\ethis$ or $o$. The special expression $\ethis$ is allowed to have a remote class because $\ethis$ is always instantiated by an object identifier $o$ that is present in the local store (see \ruleref{red-methinvoke}). This constraint, together with our initial conditions guarantees that field access is always local. The second restriction with respect to Java implementation is on thread synchronisation: performing thread synchronisation on a remote object is undefined behaviour. In Java it is possible to synchronise on the \emph{stub} to a remote object, but this is not the same as synchronising on the actual remote object, since it does not acquire the lock on the underlying object held at the remote site and does not prevent other clients in the network from accessing that resource. Suppose we have the remote class which contains synchronised methods \java{set} and \java{get} in location 1 and two clients in locations 2 and 3. \begin{lstlisting} // Client 1 in Location 2 // ... import reference to r via RMI registry synchronized (r) { r.set(1); return r.get(); } // Client 2 in Location 3 // ... import reference to r via RMI registry synchronized (r) { r.set(2); return r.get(); } \end{lstlisting} %Despite both clients referring to the same remote object, they are %in fact local stub objects in the stores of location "client1" and %"client2" respectively. In this example the clients happen to be aware that their server is providing a shared resource, so they try to guarantee a ``transaction'' by ``locking'' the remote object. However this only locks the local stub objects, and does not prevent interleaving of operations: hence it is possible for client 1 to return $2$ and client 2 to return $1$. To avoid this situation by type-checking, we can just put the same condition as the field access as defined in \ruleref{te-sync}. Combining the invariants of locality, then we can now detect the above situation. \begin{align*} &\inferrule[\rulelabel{te-fld}{TE-Fld}]{% \teenv\proves e:C\\\\% e\neq\ethis,o% \implies \LOCAL{C}\\\\% \fields(C)=\vec{T}\vec{f}% }{% \teenv\proves \efld{e}{f_i}:T_i% }&% \inferrule[\rulelabel{te-sync}{TE-Sync}]{% \teenv\proves e_1:C\\\\% e_1\neq\ethis,o\implies\LOCAL{C}\\\\% \teenv\proves e_2:S% }{% \teenv\proves\esync{e_1}{e_2}:S% } \end{align*} To implement a server-side locking solution would require engineering effort and an agreed protocol between clients. For instance, we consider a semaphore-style arrangement to guarantee the atomicity of a ``transaction'' in the following toy example: \begin{lstlisting} // Client 1 in Location 2 // ... import reference to r via RMI registry r.down(); r.set(1); int v = r.get(); r.up(); return v; // Client 2 in Location 3 // ... import reference to r via RMI registry r.down(); r.set(2); int v = r.get(); r.up(); return v; \end{lstlisting} This would require synchronised \java{down()} and \java{up()} methods to be installed in the remote object \java{r}, and would be very fragile since it relies on the good behaviour of clients to correctly signal the semaphore upon leaving the critical section. This option would be typable by our system, since it does not require synchronisation on the remote object \java{r}. \subsection{Thread and network typing}\label{sub:parallel} \noindent Threads, configurations and networks are assigned types under both the expression environment $\teenv$ and the channel environment $\tcenv$. The judgements take the following forms: \begin{align*} &\teenv;\tcenv\proves P:\tthread&&% P~\text{is a well-typed $\tthread$ in environment $\teenv;\tcenv$.}\\% &\teenv;\tcenv\proves F:\tconf&&F~\text{is a wt. configuration in environment $\teenv;\tcenv$.}\\% &\teenv;\tcenv\proves N:\tnet&&N~\text{is a wt. network in environment $\teenv;\tcenv$.}% \end{align*} Key typing rules are given below. The most important rule for threads is \ruleref{tt-par}; we type a parallel compositions of threads if a composition of their respective channel environments preserves the linearity of channels. This is checked by $\tcenv[1]\asymp\tcenv[2]$. We must make a similar check in \ruleref{tc-conf}, since the blocked queue of threads waiting for locks requires the use of a channel environment to type the store $\store$. A configuration is then well-typed in an environment $\teenv;\tcenv[1]\odot\tcenv[2]$ if its threads, $P$, are well typed in the environment $\teenv;\tcenv[1]$ and its store $\store$ is well-typed under $\teenv;\tcenv[2]$ with $\tcenv[1]\asymp\tcenv[2]$. The class table must also be well-formed, and must contain a copy of the foundation classes $\fct$. The rule \ruleref{tn-conf} promotes configurations to the network level. \[\begin{array}[c]{cc} \inferrule[\rulelabel{tt-par}{TT-Par}]{% \teenv;\tcenv[i]\proves P_i:\tthread\\% \tcenv[1]\asymp\tcenv[2]% }{% \teenv;\tcenv[1]\odot\tcenv[2]\proves P_1\PAR P_2:\tthread% }&% \inferrule[\rulelabel{tn-conf}{TN-Conf}]{% \teenv;\tcenv\proves F:\tconf% }{% \teenv;\tcenv\proves l[F]:\tnet% }\\% [5mm] \multicolumn{2}{c}{% \inferrule[\rulelabel{tc-conf}{TC-Conf}]{% \teenv;\tcenv[1]\proves P:\tthread\\ \teenv;\tcenv[2]\proves\store:\ok\\\\% \proves\ct:\ok\\% \fct\subseteq\ct\\% \tcenv[1]\asymp\tcenv[2]% }{% \teenv;\tcenv[1]\odot\tcenv[2]\proves P,\store,\ct:\tconf% }% }% \end{array}\] %\input{invariants} \section{Network Invariants and Type Soundness} \label{sec:invariant} \noindent This section presents the main technical results of the present paper. We first introduce several runtime invariants and show that if an initial network satisfies certain conditions then reductions always preserve these runtime invariants. Next we establish subject reduction by the use of invariants. Finally combining subject reduction and invariants, we derive progress and other safety guarantees. \subsection{Network invariants and initial networks} \noindent We start from the definition of a property over networks, given in \defref{property}. \begin{defn}\em %[Properties] \label{def:property} Let $\Prop$ denote a property over networks (i.e.~$\Prop$ is a subset of networks). We write $N\models\Prop$ if $N$ satisfies $\Prop$ (i.e.~if $N\in\Prop$); we also write $N \not\models \Prop$ if $N$ does not satisfy $\Prop$. We define the error property $\Err$ as the set of the networks which contain $\error$ as subexpression, i.e.~$\Err=\{N~|~N\equiv(\NEW\vec{u})(l[E[\error]\PAR P,\store,\ct]\PAR N')\}$. We say $\Prop$ is a \emph{network invariant with an initial property} $\Prop_0$ if $\Prop=\{N~|~\exists N_0.(N_0 \models\Prop_0,~N_0\MRED N,~N\not\models\Err)\}$ \end{defn} \noindent In order to ensure the correct execution of networks and the preservation of safety, we require certain properties to remain invariant. \begin{defn}%[Network invariants] \label{def:networkinvariants} \em Given network $N\equiv(\NEW\vec{u})(\prod_{0\leq i0$ \item\label{inv:queue}% $P_i\equiv E[\ewaiting{c}{n}]\PAR Q_i$\\ \hspace*{1cm} $\implies \exists !o.c\in\BLOCKED{\store_i}{o}\land\INSYNC{o}{E}\land n > 0$ % \item\label{inv:counter}% % $\forall o.\GETLOCK{\store_i}{o}\geq 0$ \end{invenum} \end{description} \noindent The \emph{closedness} invariants ensure that values and store entries do not contain any unbound variables. This is important to guarantee that newly created frozen expressions are similarly closed. The \emph{lock} invariants ensure the correct behaviour of the locking primitives at runtime. \ref{inv:ready} ensures that a thread that is ready to reacquire a lock will set that lock's count to a non-zero number. \ref{inv:queue} ensures that a thread does not wait for a non-existent lock. %and finally \ref{inv:counter} says that all objects %must have a non-negative lock counter. %The following definition formally states the above class invariant and %others. Below $\DOMV{\sigma}$ (resp.~$\DOMO{\sigma}$) denotes %variables (resp.~o-ids) of the domain of $\sigma$. Also Before proving the network invariant, we define the initial network configurations. Roughly speaking an initial configuration contains no runtime values and expressions except o-ids. It can, however, contain parallel threads distributed among locations; these have been generated by compiling multiple user-defined main programs. \defref{initial} states these conditions formally. \begin{defn}%[Initial network]\em \label{def:initial}% \em We call network $N\equiv(\NEW\vec{u})(\prod_{0\leq i}) tells the consumer little about the behaviour of the code he is about to execute, which can be dangerous \cite{GGMobile,BogleLiskov94}. In Java, the \java{RMISecurityManager} can be used with an appropriate policy file to ensure that code downloaded from remote sites has restricted capability. By extending DJ with principals, we can examine the originator of a piece of code to determine suitable privileges prior to execution \cite{aja:wallach97extensible}. To ensure the integrity of resources we can dynamically check invariants when code arrives (e.g.~by adding constraints in \ruleref{red-defrost}), or we could allow static checking by adding more fine-grained information about the accessibility of methods in class signatures, along the lines of \cite{Yoshida04}. The second direction is to extend the syntax and operational semantics to allow complex, structured, communications. For this purpose we have been studying \emph{session types} \cite{honda.vasconcelos.kubo:language-primitives,vasconcelos.ravara.gay:session-types-functional-multithreading} for ensuring correct pattern matching of sequences of socket communications, incorporating a new class of channels at the user syntax level. Our operational semantics for RMI is smoothly extensible to model advanced communication protocols. Session types are designed using class signatures, and safety is proved together with the same invariance properties developed in this paper. Study of the semantics of failure and recovery in our framework is an important topic. So far we have incorporated the possibility of failures in class downloading and remote invocation due to network partition (defined by \textbf{Err}-rules in \S~4). When a message is lost, some notion of time-out is generally used to determine whether to re-transmit or fail. Such error recovery can be investigated by defining different invocation semantics (for example at-most-once \cite{RMI}) and adding runtime extensions to DJ. This point is also relevant when we consider socket-based communication instead of RMI. We have implemented an initial version of our new primitives for code mobility \cite{Tejani05}. This takes the form of a source-to-source translator, compiling the \java{freeze} and \java{defrost} operations into standard Java source. Eager class loading via RMI requires modification to the class loading mechanism, which is achieved by installing a custom class loader working in conjunction with our translated source. This approach has the advantage that we can use an ordinary Java compiler and existing tools, and that the JVM would not need modification. However a more direct approach (for example extending the virtual machine) may yield better performance. The examples in \S~\ref{sec:examples} and the transformation rules in \S~\ref{sec:behaviour} lead to the question of how to automatically translate from RMI source programs to programs exploiting code mobility for added efficiency. Developing a general theory and an integrated tool is non-trivial due to an interplay between inter node- and procedure optimisations. Furthermore we need to formalise a cost theory for distributed communication with respect to the distance of the locations and the size of code and class tables transferred. DJ can be used as a reference model to define efficiency since it exposes distributed runtime explicitly by means of syntax and reduction rules. For example, we can put marshaling cost in rule \ruleref{red-freeze} with respect to the size of the frozen expression; we can investigate the cost of class downloading with respect to the size of a downloaded class table $\ct'$ and a distance between location $l_1$ and location $l_2$, using rule \ruleref{red-download}. An interesting further topic is an application to DJ of the cost-preoder theory developed for process algebra \cite{Arun-Kumar92} to compare program performance. %Study along this line would %be worthwhile for %articulations and comparisons of newly %proposed language constructs; and %development of automatic varification tools %for more advanced optimisations of RMI interaction %patterns \cite{YeungKelly03} %on the basis of formal semantic foundations. %the non-interfernece property %to identify the commands which has no dependency with the remote proceedure %calls to reduce a size and a number of transfer of the frosen expression. %Before considering this point, %One obvious way to combine the exisiting methods %to identy the commands %which satisify non-interference property. %More interesting approach is to %or how we can major the efficiency in the pre %expressiveness between serialisation and freezing %constructs: are these optimised programs semantically equivalent in the %sense that all executions which do not involve an error state, can %derive the same result? As ongoing work, we are investigating %the correctness of the source-to-source translation used in %the implimentation %using the technique established in the $\pi$-calculus \cite{HondaK:redbps}. %Study along this line would %be worthwhile for %articulations and comparisons of newly %proposed language constructs; and %development of automatic varification tools %for more advanced optimisations of RMI interaction %patterns \cite{YeungKelly03} %on the basis of formal semantic foundations. \bfpara*{Acknowledgements} We deeply thank Paul Kelly for his discussions about the Veneer vJVM and the RMI optimisations in \cite{YeungKelly03,YeungPhD}. Comments from the anonymous reviewers helped to revise the submission. We thank Luca Cardelli, Susan Eisenbach, Kohei Honda, Andrew Kennedy and members of the SLURP and ToCS groups at Imperial College London for their discussions, Farzana Tejani and Karen Osmond for their work on implementation. We thank Mariangiola Dezani, Sophia Drossopoulou and Uwe Nestmann for their comments on an earlier version of this paper. The first author is partially supported by an EPSRC PhD studentship and the second author is partially supported by EPSRC Advanced Fellowship (GR/T03208/01), EPSRC GR/S55538/01 and EPSRC GR/T04724/01. %-------------------------------------------------------------- % bibliography %-------------------------------------------------------------- \bibliographystyle{abbrv} { %\footnotesize %\scriptsize \small \begin{thebibliography}{10} \bibitem{Acute} Acute home page. \newblock \url{www.cl.cam.ac.uk/users/pes20/acute}. \bibitem{AbadiCardelli96} M.~Abadi and L.~Cardelli. \newblock {\em A Theory of Objects}. \newblock Springer-Verlag, 1996. \bibitem{oopslafull} A.~Ahern and N.~Yoshida. \newblock Full version of this paper. \newblock \url{www.doc.ic.ac.uk/~aja/dcbl.html}. \bibitem{dcblfull} A.~Ahern and N.~Yoshida. \newblock {F}ormal {A}nalysis of a {D}istributed {O}bject-{O}riented {L}anguage and {R}untime. \newblock Technical Report 2005/01, Department of Computing, Imperial College London: {A}vailable at: \url{www.doc.ic.ac.uk/~aja/dcbl.html}, 2005. \bibitem{aja:ancona02simplifying} D.~Ancona, G.~Lagorio, and E.~Zucca. \newblock Simplifying types in a calculus for {J}ava exceptions. \newblock Technical report, DISI - Univ. di Genova, 2002. \bibitem{Arun-Kumar92} S.~Arun-Kumar and M.~Hennessy. \newblock An efficiency preorder for processes. \newblock {\em Acta Inf.}, 29(8):737--760, 1992. \bibitem{MJ} G.~Bierman, M.~Parkinson, and A.~Pitts. \newblock {MJ}: An imperative core calculus for {J}ava and {J}ava with effects. \newblock Technical Report 563, Univ. of Cambridge Computer Laboratory, April 2003. \bibitem{BogleLiskov94} P.~Bogle and B.~Liskov. \newblock Reducing cross domain call overhead using batched futures. \newblock In {\em OOPSLA'94}, pages 341--354. ACM Press, 1994. \bibitem{NestmannFMOODS} S.~Briais and U.~Nestmann. \newblock Mobile objects ``must'' move safely. \newblock In {\em FMOODS'02}, pages 129--146. Kluwer, 2002. \bibitem{aja:cardelli94obliq} L.~Cardelli. \newblock {Obliq}: {A} language with distributed scope. \newblock Technical Report 122, Systems Research Center, Digital Equipment Corporation, 1994. \bibitem{Christ00} R.~Christ. \newblock San{F}rancisco {P}erformance: A case study in performance of large-scale {J}ava applications. \newblock {\em IBM Systems Journal}, 39(1), 2000. \bibitem{aja:drossopoulou02manifestations} S.~Drossopoulou and S.~Eisenbach. \newblock Manifestations of {D}ynamic {L}inking. \newblock In {\em USE 2002}, M\'alaga, Spain, June 2002. \bibitem{aja:drossopoulou03flexible} S.~Drossopoulou, G.~Lagorio, and S.~Eisenbach. \newblock Flexible {M}odels for {D}ynamic {L}inking. \newblock In P.~Degano, editor, {\em ESOP'03}, volume 2618 of {\em LNCS}, pages 38--53. Springer-Verlag, April 2003. \bibitem{Flanagan00} D.~Flanagan. \newblock {\em Java Examples in a Nutshell}. \newblock O'Reilly UK, 2000. \bibitem{aja:gordon99concurrent} A.~D. Gordon and P.~D. Hankin. \newblock A concurrent object calculus: Reduction and typing. \newblock Technical Report 457, Univ. of Cambridge Computer Laboratory, February 1999. \bibitem{aja:gordon01typing} A.~D. Gordon and D.~Syme. \newblock Typing a multi-language intermediate code. \newblock In {\em POPL'01}, pages 248--260. ACM Press, 2001. \bibitem{javaRMI} T.~Greanier. \newblock Discover the secrets of the {J}ava {S}erialization {API}. \newblock \url{java.sun.com/developer/technicalArticles/Programming/serialization/}. \bibitem{Honda96} K.~Honda. \newblock Composing processes. \newblock In {\em POPL'96}, pages 344--357, 1996. \bibitem{HondaK:ocac} K.~Honda and M.~Tokoro. \newblock An object calculus for asynchronous communication. \newblock In {\em Proceedings of ECOOP'91}, volume 512, pages 133--147, 1991. \bibitem{honda.vasconcelos.kubo:language-primitives} K.~Honda, V.~T. Vasconcelos, and M.~Kubo. \newblock Language primitives and type disciplines for structured communication-based programming. \newblock In {\em ESOP'98}, volume 1381 of {\em LNCS}, pages 22--138. Springer-Verlag, 1998. \bibitem{HondaK:redbps} K.~Honda and N.~Yoshida. \newblock On reduction-based process semantics. \newblock {\em TCS}, 151(2):385--435, 1995. \bibitem{FJ} A.~Igarashi, B.~C. Pierce, and P.~Wadler. \newblock Featherweight {J}ava: a minimal core calculus for {J}ava and {GJ}. \newblock {\em ACM Trans. Prog. Lang. and Sys.}, 23(3):396--450, 2001. \bibitem{Jeffrey00} A.~Jeffrey. \newblock {A} {D}istributed {O}bject {C}alculus. \newblock In {\em FOOL}. ACM Press, 2000. \bibitem{Jones93} C.~Jones. \newblock Constraining interference in an object-based design method. \newblock In {\em TAPSOFT'93}, volume 668 of {\em LNCS}, pages 136--150. Springer-Verlag, 1993. \bibitem{Emerald} E.~Jul, H.~Levy, N.~Hutchinson, and A.~Black. \newblock Fine-grained mobility in the emerald system. \newblock {\em ACM Trans. Comput. Syst.}, 6(1):109--133, 1988. \bibitem{Jumbo} S.~Kamin, L.~Clausen, and A.~Jarvis. \newblock Jumbo:run-time code generation for java and its applications. \newblock In {\em CGO'03}. IEEE, 2003. \bibitem{KPT96} N.~Kobayashi, B.~C. Pierce, and D.~N. Turner. \newblock Linearity and the pi-calculus. \newblock {\em ACM Trans. Program. Lang. Syst.}, 21(5):914--947, 1999. \bibitem{aja:krintz99reducing} C.~Krintz, B.~Calder, and U.~H\"olzle. \newblock Reducing transfer delay using {J}ava class file splitting and prefetching. \newblock In {\em OOPSLA'99}, pages 276--291. ACM Press, 1999. \bibitem{aja:liang98dynamic} S.~Liang and G.~Bracha. \newblock Dynamic class loading in the {J}ava virtual machine. \newblock In {\em OOPSLA'98}, pages 36--44. ACM Press, 1998. \bibitem{GGMobile} G.~McGraw and G.~Morrisett. \newblock Attacking malicious code: a report to the infosec research council. \newblock {\em IEEE Software}, 17(5):33--44, 2000. \bibitem{aja:merro02mobile} M.~Merro, J.~Kleist, and U.~Nestmann. \newblock Mobile objects as mobile processes. \newblock {\em Inf. \& Comp.}, 177(2):195--241, 2002. \bibitem{MilnerR:calmp1} R.~Milner, J.~Parrow, and D.~Walker. \newblock A calculus of mobile processes, parts {I} and {II}. \newblock {\em Inf.~\&~Comp.}, 100(1), 1992. \bibitem{Nestmann02} U.~Nestmann, H.~H\"uttel, J.~Kleist, and M.~Merro. \newblock Aliasing models for mobile objects. \newblock {\em Inf. \& Comp.}, 177(2):195--241, 2002. \bibitem{ohorikatopopl93} A.~Ohori and K.~Kato. \newblock Semantics for communication primitives in a polymorphic language. \newblock In {\em POPL'93}, pages 99--112. ACM Press, 1993. \bibitem{PierceBC:typsysfpl} B.~C. Pierce. \newblock {\em Types and Programming Languages}. \newblock MIT Press, 2002. \bibitem{aja:qian00formal} Z.~Qian, A.~Goldberg, and A.~Coglio. \newblock A formal specification of {J}ava class loading. \newblock In {\em OOPSLA'00}, pages 325--336. ACM Press, 2000. \bibitem{Reynolds78} J.~C. Reynolds. \newblock Syntactic control of interference. \newblock In {\em POPL'78}, pages 39--46. ACM Press, 1978. \bibitem{SangiorgiD:expmpa} D.~Sangiorgi. \newblock {\em Expressing Mobility in Process Algebras: First-Order and Higher Order Paradigms}. \newblock PhD thesis, Univ. of Edinburgh, 1992. \bibitem{StamosGrifford} J.~W. Stamos and D.~K. Gifford. \newblock Implementing remote evaluation. \newblock {\em IEEE Trans. Softw. Eng.}, 16(7):710--722, 1990. \bibitem{RMI} {Sun Microsystems Inc.} \newblock Java {R}emote {M}ethod {I}nvocation ({RMI}). \newblock \url{java.sun.com/products/jdk/rmi/}. \bibitem{METAML} W.~Taha and T.~Sheard. \newblock Multi-stage programming with explicit annotations. \newblock In {\em PEPM'97}, pages 203--217. ACM Press, 1997. \bibitem{Tejani05} F.~Tejani. \newblock Implementation of a distributed mobile {J}ava. \newblock Master's thesis, Imperial College London, 2005. \bibitem{vasconcelos.ravara.gay:session-types-functional-multithreading} V.~T. Vasconcelos, A.~Ravara, and S.~Gay. \newblock Session types for functional multithreading. \newblock In {\em CONCUR'04}, volume 3170 of {\em LNCS}, pages 497--511. Springer-Verlag, 2004. \bibitem{aja:vitek98javaseal} J.~Vitek, C.~Bryce, and W.~Binder. \newblock Designing {J}ava{S}eal or how to make {J}ava safe for agents. \newblock {\em Electronic Commerce Objects}, 1998. \bibitem{aja:wallach97extensible} D.~S. Wallach, D.~Balfanz, D.~Dean, and E.~W. Felten. \newblock Extensible security architectures for {J}ava. \newblock In {\em SOSP'97}, pages 116--128. ACM Press, 1997. \bibitem{YeungPhD} K.~Yeung. \newblock {\em Dynamic performance optimisation of distributed Java applications}. \newblock PhD thesis, Imperial College London, 2004. \bibitem{YeungKelly03} K.~Yeung and P.~Kelly. \newblock Optimizing {J}ava {RMI} programs by communication restructuring. \newblock In {\em Middleware'03}, volume 2672 of {\em LNCS}, pages 324--343. Springer-Verlag, 2003. \bibitem{Yoshida04} N.~Yoshida. \newblock Channel dependency types for higher-order mobile processes. \newblock In {\em POPL'04}, pages 147--160. ACM Press, 2004. \newblock Full version available at \url{www.doc.ic.ac.uk/~yoshida}. \bibitem{YBH} N.~Yoshida, M.~Berger, and K.~Honda. \newblock Strong {N}ormalisation in the $\pi$-{C}alculus. \newblock In {\em LICS'01}, pages 311--322. IEEE, 2001. \newblock The full version in \emph{Journal of Inf.~\& Comp.}., 191 (2004) 145--202, Elsevier. \bibitem{dodNet04} D.~Yu, A.~Kennedy, and D.~Syme. \newblock Formalization of generics for the {.NET} common language runtime. \newblock In {\em POPL'04}, pages 39--51. ACM Press, 2004. \bibitem{aja:zhao04scoped} T.~Zhao, J.~Noble, and J.~Vitek. \newblock Scoped types for real-time {J}ava. \newblock In {\em RTSS'04}, 2004. \bibitem{Zook04} D.~Zook, S.~S. Huang, and Y.~Smaragdakis. \newblock Generating {A}spect{J} {P}rograms with {M}eta-{A}spect{J}. \newblock In {\em GPCE'04}, volume 3286 of {\em LNCS}, pages 1--19. Springer-Verlag, 2004. \end{thebibliography} } \appendix %\input{extra} { \small This appendix contains the reduction rules for \DJ\ that were not introduced in the main body of the paper. Several auxiliary definitions are omitted due to space limitations, but these can be found in the long version of this paper \cite{oopslafull}. \begin{center} \textlbl{Field lookup} {\small \begin{align*} \inferrule{% }{% \fields(\object)=\bullet% }&&% \inferrule{% \csig[C]=\csigentry{D}\\\\% \fields(D)=\vec{T}'\vec{f}'% }{% \fields(C)=\vec{T}'\vec{f}',\vec{T}\vec{f}% }% \end{align*} } \textlbl{Method type lookup} {\small \[\begin{array}[c]{cc} \inferrule{% % \scriptstyle {\csig[C]=\csigentryboth{D}} }{% \mtype{m_i}{C}=C'_i\rightarrow U'_i% } \\% \\% \inferrule{% % \scriptstyle {\csig[C]=\csigentryboth{D}}\quad m\notin\{\vec{m}\} }{% \mtype{m}{C}=\mtype{m}{D}% }% \end{array}\] } \textlbl{Method body lookup} {\small \begin{align*} \inferrule{% \scriptstyle {\ct(C)=\lclassdefault}\\\\% \mmethoddefault\in\vec{M}% }{% \mbody{m}{C}{\ct}=(x,e)% }&&% \inferrule{% \scriptstyle {\ct(C)=\lclassdefault}\\\\% \mmethoddefault\notin\vec{M}% }{% \mbody{m}{C}{\ct}=\mbody{m}{D}{\ct}% }% \end{align*} } \end{center} \noindent\textbf{[Expression]} \begin{align*} &\inferrule[\rulelabel{red-var}{Var}]{% }{% x,\store,\ct\RED[l]\store(x),\store,\ct% }\\% &\inferrule[\rulelabel{red-cond}{Cond}]{% }{% \econd{\vtrue}{e_1}{e_2},\store,\ct\RED[l] e_1,\store,\ct\\\\% \econd{\vfalse}{e_1}{e_2},\store,\ct\RED[l] e_2,\store,\ct% }\\% &\inferrule[\rulelabel{while}{While}]{% }{% \ewhile{e_1}{e_2},\store,\ct\\\\% \RED[l]\econd{e_1}{e_2;\ewhile{e_1}{e_2}}{\epsilon},\store,\ct% }\\% &\inferrule[\rulelabel{red-fld}{Fld}]{% \store(o)=\sobj{C}{\vec{f}:\vec{v}}{n}{\vec{c}}% }{% \efld{o}{f_i},\store,\ct\RED[l]v_i,\store,\ct% }\\% &\inferrule[\rulelabel{red-seq}{Seq}]{% e_1,\store,\ct\RED[l](\NEW\vec{u})(v,\store',\ct')% }{% e_1;e_2,\store,\ct\RED[l](\NEW\vec{u})(e_2,\store',\ct')% }~~\vec{u}\notin\FN{e_2}\cup \FV{e_2}\\% &\inferrule[\rulelabel{red-ass}{Ass}]{}{% x=v,\store,\ct\RED[l] v,\store\sentry{x}{v},\ct% }\\% &\inferrule[\rulelabel{red-fldass}{FldAss}]{% \store'=\store\sentry{o}{\store(o)\sentry{f}{v}}% }{% \efld{o}{f} = v,\store,\ct\RED[l]v,\store',\ct% }~~o\in\DOM{\store}\\% &\inferrule[\rulelabel{red-dec}{Dec}]{}{% T~x=v; e,\store,\ct\RED[l] (\NEW x)(e,\store\cdot\sentry{x}{v},\ct)% }~~x\notin\DOM{\store}\\% &\inferrule[\rulelabel{red-cong}{Cong}]{% e,\store,\ct\RED[l](\NEW\vec{u})(e',\store',\ct')% }{% E[e],\store,\ct\RED[l](\NEW\vec{u})(E[e'],\store',\ct')% }~~\vec{u}\notin\FN{E}\cup \FV{E}% % \end{align*} The predicate $\INSYNC{o}{E}$ is true if there exist $E_1$ and $E_2$ such that $E=E_1[\einsync{o}{E_2[~]}]$. We also use the following functions. Let $\store(o)=\sobj{C}{\vec{f}:\vec{v}}{n}{\{\vec{c}\}}$. \[\text{read/update the counter}% \begin{cases} \SETLOCK{\store}{o}{n'}&=\store\sentry{o}{\sobj{C}{\vec{f}:\vec{v}}{n'}{\{\vec{c}\}}}\\% \GETLOCK{\store}{o}&=n% \end{cases}\] \[\text{read/update the queue}% \begin{cases} \BLOCKED{\store}{o}&=\{\vec{c}\}\\% \BLOCK{\store}{o}{c}&=% \store\sentry{o}{\sobj{C}{\vec{f}:\vec{v}}{n}{\{\vec{c}\}\cup\{c\}}}\\% \UNBLOCK{\store}{o}{\vec{c}'}&=% \store\sentry{o}{\sobj{C}{\vec{f}:\vec{v}}{n}{\{\vec{c}\}\setminus\{\vec{c}'\}}}% \end{cases}\] \noindent\textbf{[Synchronisation]}% \begin{align*} &\inferrule[\rulelabel{fork}{Fork}]{% }{% E[\efork{e}]\PAR Q,\store,\ct\RED[l]E[\epsilon]\PAR \eforked{e} \PAR Q,\store,\ct }\\% &\inferrule[\rulelabel{threaddeath}{ThreadDeath}]{% }{% \eforked{v},\store,\ct\RED[l]\NIL,\store,\ct% }\\% &\inferrule[\rulelabel{sync}{Sync}]{% \GETLOCK{\store}{o}=% \mbox{$\begin{cases}% 0&\SETLOCK{\store}{o}{1}=\store'\\% n>0&\INSYNC{o}{E}\implies\SETLOCK{\store}{o}{n+1}= \store'% \end{cases}$}% }{% E[\esync{o}{e}],\store,\ct\RED[l]E[\einsync{o}{e}],\store',\ct% }\\% &\inferrule[\rulelabel{wait}{Wait}]{% \INSYNC{o}{E}\\% \GETLOCK{\store}{o}=n\\\\% \SETLOCK{\store}{o}{0}=\store''\\% \BLOCK{\store''}{o}{c}=\store'% }{% E[\ewait{o}]\PAR Q,\store,\ct\RED[l](\NEW c)(E[\ewaiting{c}{n}]\PAR Q,\store',\ct)% }\\% &\inferrule[\rulelabel{notify}{Notify}]{% \INSYNC{o}{E}\\% c\in\BLOCKED{\store}{o}\\% \UNBLOCK{\store}{o}{c}=\store'% }{% E[\enotify{o}] \PAR E_1[\ewaiting{c}{n}],\store,\ct \RED[l] E[\epsilon] \PAR E_1[\eready{o}{n}],\store',\ct% }\\% &\inferrule[\rulelabel{notifyall}{NotifyAll}]{% \INSYNC{o}{E}\\% \BLOCKED{\store}{o}=\{\vec{c}\}\\% m\geq0\\% \UNBLOCK{\store}{o}{\vec{c}}=\store'% }{% E[\enotifyall{o}]\PAR E_1[\ewaiting{c_1}{n_1}]\PAR\dotsb\PAR E_m[\ewaiting{c_m}{n_m}],\store,\ct\\\\% \RED[l]E[\epsilon]\PAR E_1[\eready{o}{n_1}]\PAR\dotsb\PAR E_m[\eready{o}{n_m}],\store',\ct% }\\% &\inferrule[\rulelabel{notifynone}{NotifyNone}]{% \INSYNC{o}{E}\\% \BLOCKED{\store}{o}=\emptyset% }{% E[\enotify{o}],\store,\ct\RED[l]E[\epsilon],\store,\ct% }\\% &\inferrule[\rulelabel{ready}{Ready}]{% \GETLOCK{\store}{o}=0\\% \SETLOCK{\store}{o}{n} = \store'% }{% \eready{o}{n},\store,\ct\RED[l]\epsilon,\store',\ct% }\\% &\inferrule[\rulelabel{leavecritical}{LeaveCritical}]{% \GETLOCK{\store}{o}=n\\% \SETLOCK{\store}{o}{n-1} = \store'% }{% \einsync{o}{v},\store,\ct\RED[l]v,\store',\ct\\\\% \einsync{o}{\ereturn[c]{v}},\store,\ct,\RED[l]\ereturn[c]{v},\store',\ct% }% \end{align*} \begin{align*} % \intertext{\textbf{[Errors]}} &\inferrule[\rulelabel{red-err}{Err-Null}]{% }{% \efld{\vnull}{f},\store,\ct \RED[l] \error,\store,\ct\\\\% \efld{\vnull}{f}=v,\store,\ct \RED[l] \error,\store,\ct\\\\% \emeth{\vnull}{m}{v},\store,\ct \RED[l] \error,\store,\ct% }\\% &\inferrule[\rulelabel{err-monitor}{Err-Monitor}]{% \lnot\INSYNC{o}{E}% }{% E[\enotify{o}],\store,\ct\RED[l]E[\error],\store,\ct\\\\% E[\enotifyall{o}],\store,\ct\RED[l]E[\error],\store,\ct\\\\% E[\ewait{o}],\store,\ct\RED[l]E[\error],\store,\ct% }\\% % \intertext{\textbf{[Threads]}} % &\inferrule[\rulelabel{red-par}{RC-Par}]{% P_1,\store,\ct\RED[l](\NEW\vec{u})(P'_1,\store',\ct')% }{% P_1\PAR P_2,\store,\ct\RED[l](\NEW\vec{u})(P'_1\PAR P_2,\store',\ct')% }~~\vec{u}\notin\FN{P_2}\cup \FV{P_2}\\% &\begin{array}{ll} \inferrule[\rulelabel{red-str}{RC-Str}]{% F\equiv F_0\RED[l] F_0'\equiv F'% }{% F\RED[l]F'% }% &\inferrule[\rulelabel{red-res}{RC-Res}]{% (\NEW\vec{u})(P,\store,\ct)\RED[l](\NEW\vec{u}')(P',\store',\ct')% }{% (\NEW u\vec{u})(P,\store,\ct)\RED[l](\NEW u\vec{u}')(P',\store',\ct')% }% \end{array} \end{align*} \noindent\textbf{[Network]} \[\begin{array}[l]{lll} \inferrule[\rulelabel{red-conf}{RN-Conf}]{% F\RED[l] F'% }{% l[F]\RED l[F']% }&% \inferrule[\rulelabel{red-npar}{RN-Par}]{% N\RED N'% }{% N\PAR N_0\RED N'\PAR N_0% }&% \inferrule[\rulelabel{red-nres}{RN-Res}]{% N\RED N'% }{% (\NEW u)N \RED (\NEW u)N'% }\\% \\% \inferrule[\rulelabel{red-nstr}{RN-Str}]{% N\equiv N_0 \RED N'_0\equiv N'% }{% N\RED N'% }% \end{array}\] } \end{document}