% $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<int> 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<int> 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<int>} 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<int> t1 = freeze {
    int x1 = r1.f1(a); 
    int y1 = r1.g1(a, x1); 
    int z1 =  r1.h1(a, y1); 
    thunk<int> 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<MyObj> b1 = serialize(a);
  ser<MyObj> b2 = serialize(a);
  ser<MyObj> b3 = serialize(a);
  thunk<int> 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<MyObj> 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<int> 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<int> 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
    i<n}l_i[F_i])$ with 
  $F_i = (P_i,\store_i,\ct_i)$, and assuming $0\leq j<n$, $i\neq j$
  where required, we define property $\inv[r]$ as a set of networks
  which satisfy the condition $r$ (with $1\leq r\leq 16$) as defined below.
\end{defn}

The majority of these properties fall into one of three important
categories: \emph{class availability}, \emph{locality} and
\emph{linearity}. Each invariant has a clear operational (and arguably
engineering) meaning.

\bfsubsubsection{Class availability} \label{subsec:classavailability}
\begin{invenum}{}
\setlength{\itemsep}{0mm}%
\item\label{def:invariants:fct-in-ct}%
  $\fct\subseteq\ct_i$%
\item\label{def:invariants:class-availability}%
  $P_i\equiv E[\enew{C}{\vec{v}}]\PAR Q_i\implies \COMPLETE{C}{\ct_i}$
\item\label{def:invariants:shared-classes-share-defn}%
$C\in\DOM{\ct_i}\cap\DOM{\ct_j}\implies$\\
$\begin{array}{ll}    
 \quad \quad  &\ct_i(C)=\ct_j(C)%
    \lor\ct_i(C)=\ct_j(C)\SUBS{\vec{D}^{l_i}}{\vec{D}}\\
\quad\quad    & \text{with}~\FCL{\ct_i(C)}=\{\vec{D}\}%
 \end{array}
$
\end{invenum}
Key invariant properties in the presence of distribution are those of
\emph{class availability}.  For example when a class is needed, it and
all its superclasses must be present in the local class table. This
requirement eliminates erroneous networks containing locations such
as: $l[E[\enew{C}{\vec{v}}],\store,\emptyset]$ where class $C$ is not
present in $l$'s empty class table, so the initial step of execution
will cause a crash.  Note that even if $C$ is present, if its
superclass $D$ is not then this is also an unexpected state. For
example, in our system \ref{def:invariants:class-availability} says
that if we attempt to instantiate $C$, we need to have all its
superclasses.

\label{classinvariants}
\ref{def:invariants:shared-classes-share-defn} models the strict
default class version control of the Java serialisation API. For
example suppose we serialise an instance of the following class:
\begin{lstlisting}
class A implements java.io.Serializable {
  private int i;
  private int j = 0;
  A(int i) { this.i = i; }
}
\end{lstlisting}
If we then pass this to a remote consumer who has also has a class
\java{A}, then deserialisation is not guaranteed to succeed, even if they
have a binary compatible copy of the class:
\begin{lstlisting}
class A implements java.io.Serializable {
  private int i;
  A(int i) { this.i = i; }
}
\end{lstlisting}
This is because it is impossible to
recreate the original \java{A} at the new site
without special low level programming.    
Moreover 
the \java{serialVersionUID}---a long integer hash value computed from the
structure of a class file---will differ between the serialised object
and the version of \java{A} held by the consumer \cite{javaRMI}.\footnote{It is possible
to override this value at the programmer level, however we do not
consider such advanced techniques for versioning serialised objects.}

\bfsubsubsection{ Locality} \label{subsec:locality}
\begin{invenum}{resume}
\setlength{\itemsep}{0mm}%
\item\label{def:invariants:thread-variables-in-scope}%
  $\FV{P_i}\subseteq\DOM{\store_i}\subseteq\{\vec{u}\}$%
%\item\label{def:invariants:thread-variables-not-shared}%
%  $\FV{P_i}\cap\FV{P_j}=\emptyset$%
\item\label{def:invariants:store-variables-not-shared}%
  $\DOM{\store_i}\cap\DOM{\store_j}=\emptyset$%
\item\label{def:invariants:shared-oids-are-remote}%
  $o\in\FN{F_i}\cap\FN{F_j}\implies\exists !k. \ \store_k(o)=(C,\dotso)\land\REMOTE{C}$ 
\item\label{def:invariants:local-oids-in-scope}%
  $o\in\FN{F_i}\land\exists k.\ \store_k(o)=(C,\dotso)\land\LOCAL{C}\implies k=i$%
\item\label{def:invariants:remote-oids}%
  $o\in\FN{F_i}\implies\exists k \ 1 \leq k \leq n. \ o\in\DOM{\store_k}$%      
%\item\label{def:invariants:store-oids-not-shared}%
%  $\DOM{\store_i}\cap\DOM{\store_j}=\emptyset$% 
\item\label{def:invariants:methodcall}\label{def:invariants:field_read}\label{def:invariants:field_write}%
  Suppose
  \begin{align*}
    R_i&\in\{~\ewith{\emeth{o}{m}{e}}{c},E[\efld{o}{f}],E[\efld{o}{f}=e],E[\esync{o}{e}],\\%
    &\phantom{\in\{~}%
    E[\einsync{o}{e}],E[\enotify{o}],E[\enotifyall{o}],\\%
    &\phantom{\in\{~}%
    E[\ewait{o}],E[\eready{o}{n}]~\}%
  \end{align*}
  \quad \quad Then
  $P_i \LITEQ Q_i\PAR R_i\implies\store_i(o)=(C,\dotso)\land\COMPLETE{C}{\ct_i}$
\end{invenum}
An important property in the system is the locality of store entries
such as local variables and object identifiers, captured by these
invariants. For instance, combining 
\ref{def:invariants:thread-variables-in-scope} and 
\ref{def:invariants:store-variables-not-shared}, 
we can derive $\FV{P_i}\cap\FV{P_j}=\emptyset$, 
which ensures that
local variables are not shared between threads at different
locations. In \ref{def:invariants:methodcall} we ensure that
non-remote operations like field access and thread synchronisation are not
attempted on remote object references. This particular situation
highlights the necessity of the invariants, since we cannot guarantee
this property alone in the typing system as 
we discussed in \S~\ref{typing:val}.

\bfsubsubsection{Linearity invariants}
\noindent Below we say
\emph{thread $P$ inputs at $c$} if $P\equiv E[\eawait{c}]\PAR R$ 
or $P\equiv E[\ewaiting{c}{n}] \PAR R$ 
for some $E$ and $R$; dually \emph{thread $P$ outputs at $c$} if $P\equiv
R\PAR Q$ with $R \equiv \ereturn[c]{e}$ or $R\equiv \mathtt{go} \ e/e \ 
\mathtt{with}/\mathtt{to} \ c$ for some $Q$ and $e$.
\begin{invenum}{resume}
\setlength{\itemsep}{0mm}%
\item\label{def:invariants:linearity_await}%
  $P_i \equiv Q_i\PAR R_i$ 
  and $Q_i$ inputs at $c$\\
   \hspace*{1cm}$\implies$ neither $R_i$ nor 
  $P_j$ inputs at $c$.  
\item\label{def:invariants:linearity_output}%
  $P_i \equiv Q_i\PAR R_i$ and 
  and $Q_i$ outputs at $c$\\
  \hspace*{1cm}$\implies$ neither $R_i$ nor 
  $P_j$ outputs at $c$.  
\end{invenum}
Linearity of channel usage ensures the determinacy of method calls and
returns and also the notification of blocked threads. 
This is ensured by the linear type checking. 

\bfsubsubsection{Other invariants} \label{subsection:others}
\noindent In the following, the predicate $\INSYNC{o}{E}$ is true if
there exist $E_1$ and $E_2$ such that
$E=E_1[\einsync{o}{E_2[~]}]$. Intuitively this means that a thread has
previously acquired the lock on object $o$, although it may have
subsequently released it by calling $\ewait{o}$.

We also use the following functions. Let
$\store(o)=\sobj{C}{\vec{f}:\vec{v}}{n}{\{\vec{c}\}}$. Then to read
the re-entry count for the monitor on $o$ we use\\
$\GETLOCK{\store}{o}=n$. To obtain the queue of threads waiting on the
monitor of $o$ we use the function $\BLOCKED{\store}{o}=\{\vec{c}\}$.
\begin{description}[fullwidth,noitemsep,font=\bfseries]
\item[Closedness]%
  \mbox{}
  \begin{invenum}{resume}
\setlength{\itemsep}{0mm}%
  \item\label{def:invariants:values-are-closed}%
    $P_i\equiv E[v] \PAR Q_i$ then $\FV{v}=\emptyset$%
  \item\label{def:invariants:stores-are-closed}%
    $\store_i(x)=v \implies\FV{v}=\emptyset$%
  \item\label{def:invariants:fieldstores-are-closed}%
    $\store_i(o)=\sobj{C}{\vec{f}:\vec{v}}{\dotso}{}\implies\FV{v_i}=\emptyset$%
  \end{invenum}
\item[Locks]
  \mbox{}%
  \begin{invenum}{resume}
\setlength{\itemsep}{0mm}%
  \item\label{inv:ready}%
    $P_i\equiv E[\eready{o}{n}]\PAR Q_i\implies \INSYNC{o}{E} \land n>0$
  \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<n}l_i[P_i,\store_i,\ct_i])$ an \emph{initial network} if it
  satisfies the following conditions (called \emph{initial
  properties}):
 \begin{itemize}%[fullwidth]
\setlength{\itemsep}{0mm}%
 \item it contains no runtime expressions or values except o-ids and
  parallel compositions of $\ereturn[c]{e}$; and 
  $\efreeze[t]{T\ x}{e}$ does not contain free o-ids,
  i.e.~$\FN{e}=\emptyset$.
\item it satisfies all properties $\inv[i]$ except
  \ref{def:invariants:class-availability},
  which is replaced by:\\ %
  \hspace*{1cm}$\FCL{P_i}\subseteq \DOM{\ct_i}$,\\
  \hspace*{1cm}
  $C\in\FCL{\ct_i}\cup\DOM{\ct_i}\implies\COMPLETE{C}{\ct_i}$ and\\
  \hspace*{1cm}
  $\store_i(o)=(C,\dotso)\implies\COMPLETE{C}{\ct_i}$. 
\item 
  We also strengthen the locality invariant 
  \ref{def:invariants:field_read} by replacing $E$ by the arbitrary context. %\\%  Suppose
%  \begin{align*}
%    P_i&\in\{~\mathcal{C}[\efld{o}{f}],\mathcal{C}[\esync{o}{e'}]~\}%
%  \end{align*}
%  Then $o\in\DOM{\store_i}$ where ${\mathcal{C}}$ is an arbitrary
%  context.
\end{itemize}
We denote the set of networks satisfying these conditions by $\Init$.
\end{defn}
%Note that, by combining \ref{def:invariants:class-availability}$'$,
%the above condition subsumes \ref{def:invariants:field_read}.  
The second extra requirement states that all initial class tables are complete
w.r.t.  classes in the program and stores.  Note that during runs of
programs, the initial properties may \emph{not} be satisfied since
classes can be downloaded lazily.

\subsection{Type soundness and progress properties}
\noindent To prove some cases of the subject reduction theorem, we
require some invariants to hold in the assumptions. Therefore the
proof routine for type soundness is divided into the following three
steps:

\begin{description}
\item[Step 1] We prove one step invariant property for a typed network
starting from the initial properties. This step has two sub-cases:\\[1mm]
{\bf (i)} \emph{Assume $\teenv;\tcenv\proves N_0:\tnet$ and $N_0$
satisfies the initial properties. Then $N_0 \RED N_1$ implies
$N_1\models \inv[r]$ for each $1\leq r\leq 16$ if
$N_1\not\models \Err$.}\\[1mm]
{\bf (ii)} \emph{Assume $\teenv;\tcenv\proves N_m:\tnet \ (m\geq 1)$
and $N_m \models \inv[r]$ for all $1\leq r\leq 16$.  Then $N_m\RED N_{m+1}$
implies $N_{m+1}\models \inv[r]$ for each $1\leq r\leq 16$ if $N_{m+1}\not\models \Err$.}

\item[Step 2] We prove the subject reduction theorem using Step 1,
i.e. $\teenv;\tcenv\proves N:\tnet$ and $N\RED N'$ implies
$\teenv;\tcenv\proves N':\tnet$.

\item[Step 3] Then invariant of $\inv[r]$ is a corollary of Steps 1
and 2.
\end{description}
\noindent The proof of \textbf{Step 1} is non-trivial; it requires key
additional invariants for runtime expressions related to dynamic class
downloading.
Then assuming
\textbf{Step 1} holds, the proof of \textbf{Step 2} proceeds by
induction on the derivation of reduction with a case analysis on the
final typing rule applied. 
Lemma \ref{lem:graphs:og-complete} plays a key role. 
\cite{oopslafull} presents all proofs as well as the use of
invariants.

\newpage
\begin{thm} {\bf (Subject reduction)} 
\label{thm:subject-reduction:e}
\begin{itemize}%
\setlength{\itemsep}{0mm}%
\item Assume $\teenv,\vec{u}:\vec{T}\proves e:\alpha$,
  $\teenv,\vec{u}:\vec{T}\proves\store:\ok$ and $\proves\ct:\ok$.
  Suppose
  $(\NEW\vec{u})(e,\store,\ct)\RED[l](\NEW\vec{u}')(e',\store',\ct')$
  and $e'\not\models \Err$.  Then we have
  $\teenv,\vec{u}':\vec{T}'\proves e':\alpha'$ for some
  $\alpha'\subtypes\alpha$, $\teenv,\vec{u}':\vec{T}'\proves\store':\ok$
  and $\proves\ct':\ok$.
                                %
\item Assume $\teenv;\tcenv\proves F:\tconf$, $F\RED_l F'$ and
  $F'\not\models \Err$.  Then we have $\teenv;\tcenv\proves F':\tconf$.
                                %
\item Assume $\teenv;\tcenv\proves N:\tnet$, $N\RED N'$ and
  $N'\not\models\Err$.  Then we have $\teenv;\tcenv\proves N':\tnet$.
\end{itemize}
\end{thm} 
Note that the above theorem guarantees type safety: if there is
neither a null pointer error nor an unavoidable network error
(i.e.~$N'\not\models\Err$), then the typability ensures that an
execution does not go wrong.  As a corollary we derive:
\begin{cor} {\bf (Network invariant)} 
\label{cor:invariances}
$\wedge_{1 \leq r \leq 16}\  \inv[r]$ 
is a network invariant with the initial network properties 
$\Init$  defined in \defref{initial}.
\end{cor} 

\noindent Finally by each property such as 
availability and linearity, we can derive the following 
advanced progress and linearity properties.  

\begin{defn} \em (Progress invariants)\\
\label{def:progress_invariants}
Given network $N\equiv(\NEW\vec{u})(\prod_{0\leq
i<n}l_i[P_i,\store_i,\ct_i])$, and assuming $0\leq k<n$, we define
property $\prog[r]$ as a set which satisfy the following conditions.

\begin{progenum}{}
\item\label{def:progress_invariants:class-availability}%
  $P_{i}\equiv E[\enew{C}{\vec{v}}]\PAR Q_{i}\implies C\in\DOM{\ct_{i}}$\\%
  {Classes are always available for instantiation}.
                                %
\item\label{def:progress_invariants:download}%
  $P_{i}\equiv E[\edownload{\vec{C}}{l_k}{e}]\PAR Q_{i}$\\
  $\implies \vec{C}\in\DOM{\ct_{i}}\cup \DOM{\ct_{k}}$\\% 
  {Download operations always succeed in retrieving the required
  classes from the specified location.}
                                %
\item\label{def:progress_invariants:resolve}%
  $P_{i}\equiv E[\eresolve{\vec{C}}{m}{e}]\PAR Q_{i}
  \implies \vec{C}\in\DOM{\ct_{i}}$\\%
  {No attempt is made to resolve classes that are not available in the
  local class table.}
                                %
\item\label{def:progress_invariants:field_read}%
  $P_{i}\equiv E[o.\mathtt{f}_i]\PAR Q_{i}\implies 
  [o\mapsto\sobj{C}{\dotso}{}{}]\in\store_{i} \land \fields(C) = \vec{T}\vec{f}$\\%
  {No attempt is made to invoke a field access on the store 
  if the class of the store does not provide that field.}  
                                %
\item\label{def:progress_invariants:field_write}%
  $P_{i}\equiv E[o.\mathtt{f}_i = v]\PAR Q_{i}\implies 
  [o\mapsto\sobj{C}{\dotso}{}{}]\in\store_{i} \land \fields(C) = \vec{T}\vec{f}$\\%  
  {No attempt is made to invoke a field access on the store 
  if the class of the store does not provide that field}.  
                                %
\item\label{def:progress_invariants:variable_read}%
  $P_{i}\equiv E[x]\PAR Q_{i}\implies x \in \DOM{\store_{i}}$\\%
  {Expressions only access variables they are local to.}
                                %
\item\label{def:progress_invariants:variable_write}%
  $P_{i} \equiv E[x = v]\PAR Q_{i}\implies x \in \DOM{\store_{i}}$\\% 
  {Expressions only assign to variables they are local to.}
                                %
\item\label{def:progress_invariants:methodcall}%
  $P_{i}\equiv\ewith{\emeth{o}{m}{v}}{c}\PAR Q_{i}\land
  \store_{i}(o)=\sobj{C}{\dotso}{}{}$\\
   $\implies~\mbody{m}{C}{\ct_{i}}$ defined\\% 
   {No attempt is made to invoke a method on an object of a given
   class if that class does not provide that method.}
                                %
 \item\label{def:progress_invariants:gomethodcall}%
   $P_{i}\equiv\egowith{\emeth{o}{m}{v}}{c}\PAR Q_{i}
   \implies~ \exists ! k.\ o \in \DOM{\ct_k}$\\% 
   {Remote method invocations always refer to a unique live location in
   the network.}
                                %
  \item\label{def:progress_invariants:return}%
    $P_{i}\equiv\egoto{v}{c}\PAR Q_{i}\ \land \ c\in \{\vec{u}\}
    \implies~\exists ! k.\ P_k \equiv E[\eawait{c}]\PAR Q_k$\\%
    {If a method return exists, there must be exactly one
    location waiting for it on that channel.}
  \end{progenum}
\end{defn}
For the case of synchronisation, see \cite{oopslafull}.

\begin{thm} {\bf (Progress, Locality and Linearity)}\\
\label{thm:progress}
\ $\wedge_{1\leq r\leq 10}\ \prog[r]$ 
is a network invariant with the initial network properties 
$\Init$  defined in \defref{initial}.
\end{thm} 
\begin{proof}
Immediately 
\ref{def:progress_invariants:class-availability}
is derived 
from \ref{def:invariants:class-availability}. 
\ref{def:progress_invariants:download} 
is by the monotonicity of the class tables. 
%(Lemma~9.4(1) in \cite{oopslafull}).  
\ref{def:progress_invariants:resolve} is obvious 
by \ruleref{red-download}. 
\ref{def:progress_invariants:field_read} and 
\ref{def:progress_invariants:field_write} 
are proved 
by \ref{def:invariants:field_read}. 
\ref{def:progress_invariants:variable_read} and 
\ref{def:progress_invariants:variable_write} are obvious by 
\ref{def:invariants:thread-variables-in-scope}. 
\ref{def:progress_invariants:methodcall} is derived from 
\ref{def:invariants:methodcall}.   
\ref{def:progress_invariants:gomethodcall} 
is by combining \ref{def:invariants:remote-oids} and 
\ref{def:invariants:store-variables-not-shared}. 
\ref{def:progress_invariants:return} is straightforward 
by combining \ref{def:invariants:linearity_await} 
and \ref{def:invariants:linearity_output}.  
\qed 
\end{proof}

%\input{behaviour}
\section{Justification for optimisations}
\label{sec:behaviour}
\noindent We prove the correctness of the optimised code in 
\S~\ref{sec:examples} using sound 
syntactic transformation rules over programs and runtime.   
The key idea is a use of the following 
{\em noninterference property} 
\cite{Jones93,Reynolds78} 
to justify the correctness of these rules. 
Let us write $N \REDB N'$ for a transformation rule of 
the optimisation from $N$ to $N'$.  
Once we check $N \REDB N'$ is type-preserving and 
satisfies the following noninterference property, then 
$N$ and $N'$ are immediately observationally equal, hence 
the transformation is semantics-preserving. 
\begin{quote}
if $N\RED N_1$ and $N \REDB N_2$, then $N_1 \equiv N_2$ or there exists 
$N'$ such that $N_1 \REDB N'$ and $N_2\RED N'$. 
\end{quote}
For tractable reasoning, we introduce syntactic transformation rules
which satisfy the noninterference property. These equational laws,
that come from those of the linear types of mobile processes
\cite{KPT96,YBH}, allow us to check the optimisations purely
syntactically.

\subsection{Observational congruence}
\noindent We define an observational congruence over the typed
language and runtime by applying the equational theory of process
algebra \cite{HondaK:redbps}.  Hereafter we assume all networks are
typed and started executing from the initial condition $\Init$.

%\begin{definition} \label{def:typedrelation} 
A relation ${\cal{R}}$ over networks 
is {\em typed} when
$\teenv_1;\tcenv_1\proves {N_1} \,{\cal{R}}\, \teenv_2;\tcenv_2\proves {N_2}$ 
implies $\teenv_1=\teenv_2$ and $\tcenv_1=\tcenv_2$.   
We write $\teenv;\tcenv \proves {N_1} \,{\cal{R}} \, N_2$ 
(or ${N_1} \,{\cal{R}} \, N_2$ if $\teenv;\tcenv$ is obvious from
the context) 
when $\teenv;\tcenv\proves {N_1}$ and $\teenv;\tcenv\proves {N_2}$ are
related by a typed relation ${\cal{R}}$. A {\em typed congruence} is a
typed relation ${\cal{R}}$ 
which is an equivalence closed under all typed contexts
and the structure rules, i.e.~$\equiv \subseteq {\cal{R}}$. 
%\end{definition}
%By the subject reduction theorem, we immediately know $\RED$ is 
%a typed relation. 

The formulation of behavioural equality is based on two
conditions: reduction-closedness and an observational predicate.  In
the distributed setting, terms can effectively change meaning (for
example by side-effecting a store), so we define ``equality'' to mean
that two equated programs go to an equated state again.  The second
condition comes from the concept of observation in mobile process
theory \cite{HondaK:redbps}.  For an observation, we take the output
(``$\mathtt{go}$'') to channel $c$.
%\begin{defn}
%%[Reduction-based equality]
%\label{def:reductionclosed}
\begin{itemize}
\item 
A typed congruence ${\cal{R}}$ on networks is
{\em reduction-closed} whenever 
$\teenv;\tcenv \proves N_1 \ \mathcal{R}  \ N_2$, 
$N_1\MRED N_1'\not\models\Err$ implies, for some $N_2'$,\\ 
$N_2\MRED N_2'$ with $\teenv;\tcenv 
\proves{N_1'\ {\cal{R}} \ N_2'}$;  
and its symmetric case. 
\item 
We define the observational predicate $\downarrow_c$ and 
$\Downarrow_c$ as follows. 
%Let $\teenv;\tcenv \proves {N}$ with 
%$c:\tchano{U}\in \tcenv$. Then: 
\end{itemize}
\[ 
\begin{array}{ll}
N\downarrow_{c}
\
& \mbox{if}  \ 
N\equiv (\NEW \vec{u})(l[\egoto{v}{c}\PAR P, \store, \ct] \PAR N') 
\quad \mbox{with $c\not\in \{\vec{u}\}$} \\[1mm]
N\Downarrow_c
\ 
& \mbox{if}  \ 
\exists \ N'\ (N\MRED N' \ \wedge \ N'\downarrow_{c}) 
\end{array}
\]
We say ${\cal{R}}$ respects the observational predicate 
if $\teenv;\tcenv \proves N_1 {\cal{R}} N_2$ 
with $c:\tchano{U}\in \tcenv$ 
implies $N_1\Downarrow_{c}$ 
iff $N_2\Downarrow_{c}$.
% ; and 
% (2) $N_1\MRED N'_1\models \NULLErr$ iff
% $N_2\MRED N'_2\models \NULLErr$ where $\NULLErr$ is 

Now we define the observational congruence. 
\begin{defn}
\em 
A typed congruence ${\cal{R}}$ is {\em sound}  
if it is reduction-closed and respects the observational 
predicate. 
\begin{itemize}
\item We write $\cong$ for the maximum sound equality 
over a network invariant, i.e.~$\cong$ is defined 
over a set which exclude the error states  
$\{N~|~\exists N_0.(N_0 \models\Init,~N_0\MRED
  N,~N\not\models\Err)\}$.  

\item We write $\cong^\bullet$ for the maximum sound equality 
over untyped networks which include error states.
\end{itemize}
\end{defn}

\subsection{Transformation rules}\label{subsec:transe}
\noindent We introduce a set of tractable conversion rules  
which can quickly check the equivalence of distributed networks.  
First we formally introduce the noninterference property.  

\begin{defn}\em 
Let us assume $\REDB$ is a typed relation closed under 
name restriction, parallel composition and the structure rules.  
We say $\REDB$ satisfies a {\em noninterference property}, 
i.e.~ if $N\RED N_1$ and $N \REDB N_2$, then $N_1 \equiv N_2$ or there exists 
$N'$ such that $N_1 \REDB N'$ and $N_2\RED N'$. 
\end{defn}

\begin{lemma}
\label{pro:non-interference}
%Define $\MREDB \ \EQDEF \ \REDB^\ast \cup \equiv$ 
%and  $\EQBETA \ \EQDEF \ (\REDB \cup \REDB^{-1})^\ast \cup \equiv$.  
Suppose $\REDB$ satisfies a noninterference property and 
$\REDB$ respects the observational predicate. 
Then $N_1 \REDB N_2 \not\models\Err$ implies $N_1 \cong N_2$.   
\end{lemma}
%Once we found a conversion from $N_1$ to $N_2$ which satisfies 
%the noninterference property, we can automatically 
%prove that it preserves the semantics. 

%Surprisingly, most of reductions in DJ satisfy 
%the noninterference property. 
%\begin{proposition}
%Suppose $N\REDB N'$ is defined by {\em excluding}  
%variable read {\em ({\bf Var} in \cite{dcblfull})}, assignment 
%{\em ({\bf Ass} in \cite{dcblfull})}, 
%field read {\em ({\bf Fld} in \cite{dcblfull})}, 
%field assignment {\em ({\bf FldAss} in \cite{dcblfull})}, 
%freezing (\ruleref{red-freeze}), 
%the signal from notify to wait {\em ({\bf Notify} in \cite{dj-sync})}, 
%the reduction for entering the monitor {\em ({\bf Sync} in \cite{dj-sync})}  
%and the reduction for leaving the monitor {\em ({\bf Ready} in \cite{dj-sync})}. Then $\REDB$ satisfies the noninterference
%over a set of typed network such that 
%$\{ N\ | \ N \not\models \Err\}$.  
%\end{proposition}

\sfpara*{Code that can move safely}
The transformation rules should reduce the 
number of communications and class downloads preserving meaning. For this, we need to identify 
what kinds of code and programs can safely move from one location to another. 
Below predicate $\REMOTEONLY{\teenv}{e}$ is true if 
$\FV{e}=\emptyset$ and $o\in \FN{e}$ implies $\teenv\proves o:C$ with 
$\REMOTE{C}$; i.e.~$e$ does not contain any free variables 
or local o-ids under environment $\teenv$;  
in addition it does not contain any of the following terms as a subterm
(since they break the locality invariants, see \S~\ref{subsub:locality} 
and \S~\ref{subsec:locality}).    
  \begin{align*}
    & \{\efld{o}{f},\efld{o}{f}=e,\esync{o}{e'},
    \einsync{o}{e'},\\%
    & {~}%
    \enotify{o},\enotifyall{o},\ewait{o},\eready{o}{n}~\}%
  \end{align*}
If $\REMOTEONLY{\teenv}{e}$, $e$ can {\em move} from one location to 
another preserving its meaning.  

\sfpara*{Transformation Rules}
We list the key transformation rules. 
%\begin{defn} \label{def:transformationrules}
%\em 
%\noindent{(Equational laws)} 
Assume the right hand side 
is typed under $\teenv;\tcenv$. We omit surrounding
context where it is unnecessary.\\[1mm] 
\noindent{\bf Linearity}
\mbox{}\\[1mm]
$\begin{array}{rl}
  \text{(l1)}&% 
  \ereturn[c]{E[\esandbox{e_1;\dotsc;e_n}]}\\%
  &\TRANSFORM e_1;\dotsc;\ereturn[c]{E[e_n]}\\%
  [1mm]
  \text{(l2)}&%
  E[\eawait{c}]\PAR\ereturn[c]{e}\TRANSFORM E[e]\\%
  [1mm]
\end{array}$
\\[1mm]
(l1) is standard. 
(l2) means that method body $e$ can be evaluated inline.
This is ensured by linearity of channel $c$.   
\\[1mm]
\noindent{\bf Class}\\[1mm]
$\begin{array}{rl}
  \text{(cm)}&% 
  l[P,\sigma,\ct]\TRANSFORM l[P,\sigma,\ct\cup\ct']
\quad\CTCOMPLETE{\ct'},\ \proves \ct':\ok\\%
\end{array}$
\\[1mm]
(cm) says that a complete class table can always move.  
\\[1mm]
\noindent{\bf Closed}\\[1mm]
$\begin{array}{rl}
  \text{(cr)}&%
  (\NEW x)(E[x]\PAR P,\sentry{x}{v}\cdot\sigma)
\TRANSFORM (E[v],\sigma)~\text{when}~x\notin\FV{P}\cup\FV{E}%
\\[1mm]
  \text{(fr)}&% 
  (\NEW\vec{u})(E[\efreeze[t]{T~x}{e}]\PAR P,\store,\ct)\\%
  &\TRANSFORM(\NEW\vec{u})(E[\vfrozen{T~x}{\vec{u}}{l}{e}{\store'}{\ct'}] \PAR P,\store,\ct)%
\end{array}$\\[1mm]
where in (fr), $u_i\notin\FV{P}\cup\FV{E}$, 
$\FN{\store'}\cup \FV{\store'}\subseteq\DOM{\store'}$  
and 
$\store'$ and $\ct'$ are given following 
\ruleref{red-freeze}. These rules mean 
that the timing of reading a value or of freezing an expression is unimportant, 
provided it shares no information with other parties. 
Note ``$\NEW \vec{u}$'' in (fr) ensures $u_i$ is not shared. 
%\\[1mm]
\newpage
\noindent{\bf Method Invocation}\\[1mm]
$\begin{array}{rl}
  \text{(mi)}&% 
  l[E[\emeth{o}{m}{v}],\store,\ct]\PAR m[Q,\store',\ct']\\%
  [1mm]
  &\TRANSFORM l[E[\edefrost{v}{\vfrozen{T~x}{}{m}{e}{\emptyset}{\emptyset}}],\store,\ct]\PAR m[Q,\store',\ct']%
\end{array}$\\[1mm]
where $\REMOTEONLY{\teenv}{e\SUBS{v}{x}}$,  
$\sentry{o}{\sobj{C}{\dotso}{}{}}\in\store'$,  
$\mtype{m}{C} = T \rightarrow U$, 
and $\mbody{m}{C}{\ct'}=(x,e)$. 
This rule means we can fetch a closure of the mobile method body 
from the remote site safely. 
\\[1mm] 
We leave other rules to \cite{oopslafull}.  The transformation rule
$N\TRANSFORM N'$ is defined as a binary relation generated by the
above rules and closed under parallel composition, name restriction and
structure rules.

\begin{thm}\label{thm:equation}
\mbox{}
\begin{enumerate}
\setlength{\itemsep}{-0.5mm}%
\item {\bf (noninterference)} \ 
$\TRANSFORM$ satisfies a noninterference property and 
respects the observational predicate under
a network invariant.  

\item {\bf (type preservation)} \ 
Assume $\teenv;\tcenv\proves N : \tnet$ and 
$N \not\models \Err$.  
Then $N\TRANSFORM N'$ 
implies $\teenv; \tcenv \proves N' :\tnet$. 
\item {\bf (semantic preservation)} \ 
$N\TRANSFORM N'$ implies $N \cong N'$. 
\end{enumerate}
\end{thm}
\begin{proof}
(1) and (2) are mechanical. (3) uses (1) and (2) together with 
Lemma \ref{pro:non-interference}.
\end{proof}
Note that by Definition \ref{def:property}, 
Theorem \ref{thm:equation} excludes the error statement. 
This is because the transformation is {\em not} sound 
{\em if an error occurs during execution}, as we shall discuss 
in the next subsection. More formally, 
$N\TRANSFORM N'$ does not always imply $N \cong^\bullet N'$. 

\begin{proposition}
  \mbox{}
  \begin{enumerate}
\setlength{\itemsep}{-0.5mm}%
  \item $\efreeze[t]{T~x}{e}\cong\efreeze[t']{T~x}{e}$.
  \item There is a fully abstract embedding $\CSMAP{N}{}{}$ of
  networks $N$ that contain methods $\mathtt{m}(\vec{e})$ 
and frozen expressions $\efreeze[t]{\vec{T}~\vec{x}}{e}$ with multiple
  parameters into networks with methods and frozen expressions with
  only single parameters. 
  \end{enumerate}
\end{proposition}
\begin{proof}
(1) Use Lemma~\ref{pro:non-interference} and (cm). (2) A translation
of $\mathtt{freeze}$ is standard by currying. We encode methods
with multiple parameters into those with just a single parameter in
the most intuitive manner. Each method, instead of taking a vector
$\vec{T}~\vec{x}$ of parameters, takes a single parameter of a newly
created class $C$. $C$ contains fields $T_1~f_1;\dotsc;T_n~f_n;$ where
field $f_i$ corresponds to the $i$th parameter of the original method
definition. Then, all call sites for a particular method are replaced
with a constructor call to an instance of the correct ``parameter
class'', so $\emeth{o}{m}{\vec{v}}$ becomes
$\emeth{o}{m}{\enew{C}{\vec{v}}}$ for some $C$. We then prove that
$N\cong\CSMAP{N}{}{}$. See \cite{oopslafull} for the detailed proofs.
\qed
\end{proof}

\subsection{Correctness of the optimisations}
\noindent We now prove the correctness of the 
optimised programs in \S~2. 
We transform one program to another 
using the transformation rules defined above. 

We first demonstrate how to 
transform the optimised program 1 (Opt1) to 
the original program 1 (RMI1).  
Let us assume $e$ is a program from line 2 to 4 in 
(RMI1). 
%i.e.~$e=\mathtt{int}\ x= \ ... \ z= r.\mathtt{h}(a,y)$. 
We omit the surrounding context as there is no class loading in this example. 
After the method invocation by 
$\ewith{\emeth{o}{mOpt1}{r,n}}{c}$,  
(Opt1) becomes:
\begin{align*}
%F \ \EQDEF \ 
%(\NEW a)(&\tthunk{\tint}~t=\efreeze[t]{}{e;z};\\%
%  &\quad\quad\ereturn[c]{\emeth{r}{run}{t},\sentry{a}{n}})%  
(\NEW a)(\tthunk{\tint}~t=\efreeze[t]{}{e;z};
\ereturn[c]{\emeth{r}{run}{t},\sentry{a}{n}})%  
\end{align*}
Let $v=\vfrozen{
\tunit~x}{a}{l}{e;z}{\sentry{a}{n}}{}$. Then the above configuration 
is transformed to: 
\[\begin{array}{ll@{~}l}
  \TRANSFORM&(\NEW a)(\tthunk{\tint}~t=v;\ereturn[c]{\emeth{r}{run}{t},\sentry{a}{n}})&(\text{fr})\\%
  \MREDB&(\NEW t)(\ereturn[c]{\emeth{r}{run}{t}},\sentry{t}{v})\\%
  \TRANSFORM&\ereturn[c]{\emeth{r}{run}{v}},\emptyset&(\text{cr})\\%
  \TRANSFORM&\ereturn[c]{}~
\edefrost{v}{\vfrozen{T~x}{}{l}{\edefrost{}{x}}{\emptyset}{\emptyset}},\emptyset&(\text{mi})\\%
  \MREDB&(\NEW a)(\ereturn[c]{\esandbox{e;z}},\sentry{a}{n})&(\star)\\%
  \TRANSFORM&(\NEW a)(e;\ereturn[c]{z},\sentry{a}{n})&(\text{l1})%
\end{array}\]
The last line is identical to (RMI1) after 
the method invocation by $\ewith{\emeth{o}{m1}{r,n}}{c}$. 
Note that $\mathtt{defrost}$ and $\mathtt{sandbox}$ do 
not affect other parties, 
so that the reduction at ($\star$) satisfies a noninterference 
property, hence this reduction preserves the semantics. Because we have
$\REMOTEONLY{\emptyset}{v}$,  
we can apply (mi) in the forth line.  
Hence (Opt1) is transformed to (RMI1). 

The correctness of (Opt2) is also straightforward 
by repeating the same routine twice. 

We show (RMI3) is equivalent with (Opt3) 
under the assumption there is no call-back.\footnote{
%The paper does not treat a call-back explained in \S~2. 
The equation holds if there is no call-back as explained in \S~2.
Our framework 
can also justify the incorrectness of the optimisation between 
(RMI3) and (Op3) in the presence 
of call-back. However, since most RMI programs do not use call-backs,
we do not investigate them.}
%Let us assume $v_i = \lambda a.(l,a, \sigma_i)$ is a 
%result of serialisation of $a$ at the line $i$ ($3\lei) . 
%Then we can seria
Then the body of (Opt3) is equivalent to 
\ $\ereturn[]{r.\mathtt{run}(\mathtt{freeze}(e\SUBS{\VEC{e}'}{\VEC{b}};z))}$ 
\ and $e_i' = \mathtt{deserialize}(v_i)$ 
\ where $v_i = \lambda(\tunit~x).
(\NEW \vec{u})(l,a, \sigma_i)$ is a serialised value at line 
$i$ in (Opt3) ($3 \leq i \leq 5$). 
Then we apply %(sg) and (sf). By 
a similar transformation with the above to 
derive (RMI3).  
Hence (RMI3) is equivalent to (Opt3).  

Note that our freezing preserves  
sharing between objects (Point 1 in (Opt3) in \S~2), 
hence we can prove the following equation: 
\begin{center}
$x.\mathtt{f} = y; r.\mathtt{h}(x, y)$ \ $\cong$ \ 
$x.\mathtt{f} = y; r.\mathtt{run}(\mathtt{freeze}(r.\mathtt{h}(x, y)))$. 
\end{center}
%\[ 
%\begin{array}{l}
%  \tthunk{\mathtt{int}}\ t \ =\  \mathtt{freeze}(\\
%   \quad \mathtt{int}\ x\ = \ r.\mathtt{f}(\mathtt{deserialize}
%(\lambda a.(l, a,\sigma_1)));\\
%   \quad \mathtt{int}\ y\ = \ 
%r.\mathtt{g}(\mathtt{deserialize}(\lambda a.(l,a, \sigma_2)),\ x);\\ 
%   \quad \mathtt{int}\ z\ = \ r.\mathtt{h}
%(\mathtt{deserialize}(\lambda a.(l,a, \sigma_3)),\ y);\\ 
%    \ z);\\
%  \ereturn[]{r.\mathtt{run}(t);} 
%\end{array}
%\] 
%Then together with (sg) and (sf), we can derive (Opt3) is 
%observational congruent with (RMI3). 

Finally by (erase), we can derive (Opt4) from (Opt3), 
hence (Opt4) is equivalent to (RMI3). 

Not all equations are valid if 
a network error occurs during executions. 
For example, $\eager$ and $\lazy$ are 
not equal in the presence of \ruleref{err-classnotfound}, hence 
(erase) is not applicable. See \cite{oopslafull} for the full proofs. 
To summarise, we have: 


\begin{thm} {\em\bf (Correctness of the Optimisations)}
\begin{enumerate}
\setlength{\itemsep}{-1mm}%
\item {\em (RMI1)} and {\em (Opt1)} are equivalent up to $\cong$. 
\item {\em (RMI2)} and {\em (Opt2)} are equivalent up to $\cong$. 
\item {\em (RMI3)} and {\em (Opt3)} are equivalent up to $\cong$   
without call-back. 
\item {\em (Opt3)} and {\em (Opt4)} are equivalent up to $\cong$, 
hence {\em (RMI3)} and {\em (Opt4)} are equivalent up to $\cong$ 
without call-back.  
\item None of them are equivalent up to $\cong^\bullet$. 
\end{enumerate}
\end{thm}   

%\input{related}
\section{Related Work}
\bfpara*{Class loading and downloading}
Class loading and downloading are crucial to many useful Java RMI
applications, offering a convenient mechanism for distributing code to
remote consumers.  The class verification and maintenance of type
safety during linking are studied in
\cite{aja:liang98dynamic,aja:qian00formal}.  Our formulation of class
downloading is modular, so it is adaptable to model other linking
strategies
\cite{aja:drossopoulou02manifestations,aja:drossopoulou03flexible},
see \S~\ref{subsec:classloading}.  We set the class invariant
$\ref{def:invariants:shared-classes-share-defn}$ in Definition
\ref{def:networkinvariants}. This is because  the Java serialisation
API imposes the strict default class version control discussed in
\S~\ref{classinvariants}. Another solution is to explicitly
model the Java exception \java{InvalidClassException} to check for
mismatch between downloaded and existing classes.  This dynamic
approach leads to the same invariant to prove the subject reduction
theorem.  

Most of the literature surrounding class loading in practice takes the
lazy approach. As we discussed earlier, in the setting of remote
method invocation laziness can be expensive due to delay involved in
retrieving a large class hierarchy over the network. Krintz et al
\cite{aja:krintz99reducing} propose a class splitting and pre-fetching
algorithm to reduce this. Their specific example is applet loading: if
the time spent in an interactive portion of an applet is used to
download classes that may be needed in future, we can fetch them ahead
of time so that the user does not encounter a large delay, sharing the
motivation for our (eager) code mobility primitive. The partly eager
class loading in their approach is implicit, but requires control flow
information about the program in question to determine where to insert
instructions to trigger ahead-of-time fetching. This framework may be
difficult to apply in a general distributed setting, since clients may
not have access to the code of a remote server. Also their approach
merely mitigates the effect of network delay rather than removing it;
it still requires the sequential request of a hierarchy of
superclasses. We believe an explicit thunk primitive as we proposed in
the present work may offer an effective alternative in such
situations.

\bfpara*{Distributed objects} 
Obliq \cite{aja:cardelli94obliq} is a distributed object-based,
lexically scoped language proposed by Cardelli.  One key feature of
the language is that methods are stored within objects---there is no
hierarchy of tables to inspect as in most class-based languages. 
Merro et al \cite{aja:merro02mobile} encode a core part of Obliq into
the untyped $\pi$-calculus.  They use their encoding to show a flaw in
part of the original migration semantics and propose a repair.  Later
Nestmann et al \cite{Nestmann02} formalised a typing system for a core
Obliq calculus and studied different kinds of object aliasing. Briais
and Nestmann \cite{NestmannFMOODS} then strengthened the safety result
in \cite{aja:merro02mobile} by directly developing the must
equivalence at the language level (without using the translation into
the $\pi$-calculus).  They also apply a noninterference property to
show the two terms (with and without surrogation) are must-equivalent.
\DJ\ models two important concerns in distributed class-based
object-oriented languages missing from Obliq, that is object
serialisation and dynamic class downloading associated with
inheritance in Java (note that the same term ``serialisation'' used in
\cite{aja:cardelli94obliq} refers to one in the sense of transaction
theory). These features require a consistent formulation of dynamic
deep copying of object/class graphs. As we have seen in 
\S~\ref{sec:behaviour}, detailed analysis of these
features is required to justify the correctness of the optimisation
examples in \S~\ref{sec:examples}. The proof method using syntactic
transformations in \S~\ref{sec:behaviour} is also new.

Emerald \cite{Emerald} is another example of a distributed
object-based language. It supports classes represented as objects,
however there is no concept of class loading as in \DJ---information
about inheritance hierarchies is discarded at compile-time. Objects in
Emerald may be \emph{active} in that they are permitted their own
internal thread of control that runs concurrently with method
invocations on that object. Such objects may explicitly move
themselves to other locations by making a library call.  In \DJ\ the
fundamental unit of mobility is arbitrary higher-order expressions:
this general code freezing primitive can represent object mobility
similar to Emerald when it is combined with standard Java
RMI. Finally, there has been no study of the formal semantics of
Emerald.

Gordon and Hankin \cite{aja:gordon99concurrent} extend the object
calculus \cite{AbadiCardelli96} with explicit concurrency primitives
from the $\pi$-calculus.  Their focus is synchronisation primitives
(such as fork and join) rather than distribution, so they only use a
single location.  Jeffrey \cite{Jeffrey00} treats an extension of
\cite{aja:gordon99concurrent} for the study of locality with static
and dynamic type checking.  The concurrent object calculus is not
class-based, hence neither work treats dynamic class loading or
serialisation (though \cite{Jeffrey00} treats transactional
serialisation as in \cite{aja:cardelli94obliq}), which are among the
key elements for analysis of RMI and code mobility in Java.

\bfpara*{Scope and runtime formalisms for Java} 
Zhao et al \cite{aja:zhao04scoped} propose a calculus 
with primitives for explicit memory management,  
called SJ, for a study
of containment in real-time Java. 
The SJ calculus proposes a typing discipline based on the
idea of \emph{scoped types}---memory in real-time applications is
allocated in a strict hierarchy of scopes. Using the existing Java
package structure to divide such scopes, their typing system
statically prevents some scope invariants being broken. 
Their focus is on real-time concurrency in a single
location, while ours is on dynamic distribution of code in multiple
locations. \DJ\ also guarantees similar scoping properties by
invariants, for example 
$\ref{def:invariants:shared-oids-are-remote}$ in Definition
\ref{def:networkinvariants} ensures that identifiers for local objects
do not leak to other locations in the presence of 
synchronisation primitives.  

The representation of object-oriented runtime 
in formal semantics is not limited
to distributed programs, as found in study of 
execution models of the .NET CLR
by Gordon and Syme \cite{aja:gordon01typing}
and Yu et al \cite{dodNet04}.

The JavaSeal \cite{aja:vitek98javaseal} project is an implementation
of the Seal calculus for Java. It is realised as an API and run-time
system inside the JVM, targeted as a programming framework for
building multi-agent systems. The semantics of these APIs depend on
distributed primitives in the implementation language, which are
precisely the target of the formal analysis in the present paper.
JavaSeal may offer a suggestion for the implementation and security
treatment of higher-order code passing proposed in the present paper.

\bfpara*{Functions with marshaling primitives} 
Ohori and Kato \cite{ohorikatopopl93} extend a purely functional part
of ML with two primitives for remote higher-order code evaluation via
channels, and show that the type system of this language is sound with
respect to a low-level calculus.  The low-level calculus is equipped
with runtime primitives such as closures of functions and creation of
names. Their focus is pure polymorphic functions, hence they treat
neither side-effects nor (distributed) object-oriented features.
Acute \cite{Acute} is an extension of OCaml equipped with type-safe
marshaling and distributed primitives.  By using flags called
marks, the user can control dynamic loading of a sequence of modules
when marshaling his code.  This facility is similar to our lazy and
eager class loading.  The language also provides more flexible way to
rebind local resources and modules.  
An extension of our freeze operator for fine-grained rebinding 
is an interesting topic, though 
as we discussed in \S~\ref{classinvariants}, 
it is not suitable in practice due to 
the Java serialisation API. 
%An extension of our freeze operator for fine-grained rebinding 
%would be possible by dropping the 
%class invariant as discussed in dynamic linking and shipping multiple
%class tables annotated by locations, guided by a technique in
%\cite{Acute}. 

\bfpara*{Staged computation and meta-programming}
Taha and Sheard \cite{METAML} give a dialect of ML containing staging
annotations to generate code at runtime, and to control evaluation
order of programs. The authors give a formal semantics of their
language, called MetaML, and prove that the code a well-typed program
generates will itself be type-safe. 

The \java{freeze} and \java{defrost} primitives in \DJ\ can be thought
of as staging annotations, and also guarantee that frozen expressions
should be well-typed in any context. However we study distribution and
concurrency in an imperative setting, with strong emphasis on runtime
features. These features are not discussed in MetaML as it is a
functional language, nor the problems associated with
classloading we address.

Kamin et al \cite{Jumbo} extend the syntax of Java with
staging annotations and provide a compiler for a language called
Jumbo. They allow creation of classes at runtime, focusing on
single-location performance optimisation: there is no discussion of
use in distributed applications, a main focal point of our work. They
give no static guarantees about type safety of generated code, nor do
they allow code to be generated in fragments smaller than an entire
class. They 
do not consider higher-order quotation, permitting only one level of
quotation and anti-quotation.

Zook et al \cite{Zook04} propose Meta-AspectJ as a
meta-programming tool for an aspect-oriented language. They implement
a compiler that takes code templates---containing quoted Aspect-J
code---and turns them into aspect declarations that can be applied as
normal to Java programs. Their system is more focused on compile-time
code generation, and offers weaker static guarantees: well-typed
generators do not guarantee type safety of the generated aspects. 

%\input{conclusion}
\section{Conclusions and Further Work}
\noindent 
This paper introduced a Java-like core language for RMI with
higher-order code mobility. It models runtime for distributed
computation including dynamic class downloading and object
serialisation. Using the new primitives for code mobility, we subsumed
the existing serialisation mechanism of Java and were able to
precisely describe examples of communication-based optimisations for
RMI programs 
on a formal foundation.
% in the formal system. 
We established type soundness and
safety properties of the language using distributed
invariants. Finally, by the behavioural theory developed in
\S~\ref{sec:behaviour}, 
we were able to systematically prove the correctness of the examples
in \S~\ref{sec:examples}. 


Explicit code mobility as a language primitive gives powerful control
over code distribution strategies in object-oriented distributed
applications.  
This is demonstrated in the examples in \S~\ref{sec:examples}. 
In \cite{BogleLiskov94,YeungKelly03,YeungPhD}, these
optimisations are informally described as implementation details.
Not only is source-level presentation necessary for their semantic
justification, but also explicit treatment of code mobility gives programmers
fine-grained control over the evaluation order and location of executing code. It also opens the potential for
source-level verification methodologies for access control, secrecy and other
security concerns, as briefly discussed below.
Note current customised class downloading mechanisms do not offer
active code mobility and algorithmic control of
code distribution (as in the last example of \S~\ref{sec:examples}).

Further, the fine-grained control of code mobility has a 
direct practical significance: 
the optimisation strategy in \cite{YeungKelly03,YeungPhD}
cannot aggregate code in which new object generation is inserted,
such as:
\begin{lstlisting}
int m3(RemoteObject r, MyObj a) {
  int x = r.f(a); 
  int y = r.g(new MyObj(x));
  int z = r.h(a, y); 
  return z; 
}
\end{lstlisting}
where \java{MyObj} is a local class in the client.
This is because we need active class code delivery if this code is to
be executed in a remote server. In contrast, the freeze primitive in
our language can straightforwardly handle aggregation of this code.  We
also believe that, in comparison with direct, byte-code level
implementation in \cite{YeungKelly03,YeungPhD}, the use of our
high-level primitives may not jeopardise efficiency but rather can
even enhance it by e.g.~allowing more flexible inter-procedure optimisation.

%This paper introduced a Java-like core language for RMI with
%constructs for distribution including dynamic class loading and
%serialisation and presented its formal semantics and typing system.  A
%new language primitive for distribution, higher-order code mobility,
%was proposed, subsuming the serialisation mechanism.  Type soundness
%and safety properties of the language were established through the use
%of distributed invariants.  Finally the correctness of RMI
%optimisation in Section 2 is proved by syntactic transformation of the
%language and runtime.  The primitive for explicit code mobility was
%used to model the optimised code at runtime, which was crucial for
%this analysis.  At the user level, this primitive assists programmers
%to be able to write fine-graind control of distribution as a program
%text, with clear semantics.

%One of the key issues in the optimisation in \cite{} 
%is cost to identify non-dependent 
%commands from a user text alone 
%in order to make a batch of a number of remote calls. 
%a number of communication. One of 
%As such, using this primitive 

%depending on the bandwidth and latency. 
%improving the state of the art in the distributed 
%object-oriented programs.  
%The invariants can be used as a ``prescription'' of global and local 
%state of a language and runtime which a system 
%designer expects to be guaranteed; if it is not satisfied by his 
%implementation, he can correct or strengthen the typing rules 
%or relax the prescription itself. See \S~\ref{subsub:locality} 
%for the examples demonstrated in the paper. 
%See \ref{} for examples we discussed. 
%For example, to make the field access local, 
%we modified the standard field access 
%and synchronisation typing rules  
%by adding one constraint 
%($e\neq\ethis,o\implies\LOCAL{C}$), 
%guided by the value and object identifiers invariants in 
%Section \ref{sec:invariant}. 

The complexity of the third program optimisation poses the
question of whether the original copying semantics of Java RMI are
themselves correct in the first place: making a remote call can entail
subtly different invocation semantics to calling a local method. Our
code freezing primitive allows us to make the call semantics explicit,
and also allows us to support more traditional ideas about object
mobility \cite{Emerald,aja:cardelli94obliq}, such as side-effects in
calls at the server side.

The class-based language considered in the present work does not
include such language features as casting \cite{FJ,MJ}, exceptions
\cite{aja:ancona02simplifying} and parametric polymorphism
\cite{FJ}; although these features can be represented by
extension of the present syntax and types, their precise interplay 
with distributed language constructs requires examination.

An important future topic is enrichment of the invariants and type
structures to strengthen safety properties (e.g. for security).  Here
we identify two orthogonal directions. The first concerns mobility. As
can be seen in the second example in \S~\ref{sec:examples}, the
current type structure of higher-order code (e.g.~\java{thunk<int>})
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}
