<figure><img src="image_1.png" /></figure>

HAL
open science

# Analysis of Deadlocks in Object Groups

Elena Giachino, Cosimo Laneve

► To cite this version:

Elena Giachino, Cosimo Laneve. Analysis of Deadlocks in Object Groups. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. pp.168-182, 10.1007/978-3-642-21461-5_11 . hal-01583328

HAL Id: hal-01583328

https://inria.hal.science/hal-01583328

Submitted on 7 Sep 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Analysis of deadlocks in object groups *

Elena Giachino

Cosimo Laneve

Dipartimento di Scienze dell'Informazione, Università di Bologna

**Abstract.** Object groups are collections of objects that perform collective work. We study a calculus with object groups and develop a technique for the deadlock analysis of such systems based on abstract descriptions of method's behaviours.

# 1 Introduction

Object groups are collections of objects that perform collective work. The group abstraction is an encapsulation mechanism that is convenient in distributed programming in several circumstances. For example, in order to achieve continuous availability or load balancing through replication, or for retrieval services of distributed data. In these cases, in order to keep consistencies, the group abstraction must define suitable protocols to synchronize group members. As usual with synchronization protocols, it is possible that object groups may manifest deadlocks, which are particularly hard to discover in this context because of the two encapsulation levels of the systems (the object and the group levels).

Following the practice to define lightweight fragments of languages that are sufficiently small to ease proofs of basic properties, we define an object-oriented calculus with group operations and develop a technique for the analysis of deadlocks. Our object-oriented language, called FJg, is an imperative version of Featherweight Java [9] with method invocations that are asynchronous and group-oriented primitives that are taken from Creol [10] (cf. the JCoBoxes [19]).

In FJg, objects always belong to one group that is defined when they are created. Groups consist of multiple tasks, which are the running methods of the objects therein. Tasks are cooperatively scheduled, that is there is at most one task active at each time per group and the active task explicitly returns the control in order to let other tasks progress. Tasks are created by method invocation that are asynchronous in FJg: the caller activity continues after the invocation and the called code runs on a different task that may belong to a different group. The synchronization between the caller and the called methods is performed when the result is strictly necessary [10, 21, 3]. Technically, the decoupling of method invocation and the returned value is realized using *future variables* (see [6] and the references in there), which are pointers to values that may be not available yet. Clearly, the access to values of future variables may require waiting for the value to be returned.

In a model with object groups and cooperative scheduling, a typical deadlock situation occurs when two active tasks in different groups are waiting for each other to

<footnote>* The authors are member of the joint FOCUS Research Team INRIA/Università di Bologna.
This research has been funded by the EU project FP7-231620 HATS.</footnote>
return a value. This circular dependency may involve less or more than two tasks. For
example, a case of circularity of size one is

Int fact(Int n){ if (n==0) then return 1; else return n*(this!fact(n-1).get) }

The above FJg code defines the factorial function (for the sake of the example we
include primitive types Int and conditional into FJg syntax. See Section 2.1). The in-
vocation of this!fact(n) deadlocks on the recursive call this!fact(n-1) because
the caller does not explicitly release the group lock. The operation get is needed in
order to synchronously retrieve the value returned by the invocation.

We develop a technique for the analysis of deadlocks in FJg programs based on
*contracts*. Contracts are abstract descriptions of behaviours that retain the necessary
informations to detect deadlocks [12, 11]. For example, the contract of *fact* (assuming
it belongs to the class *Ops*) is G() { Ops.fact⁹: G() } . This contract declares that,
when *fact* is invoked on an object of a group *G*, then it will call recursively *fact* on
an object of the same group *G* without releasing the control – a *group dependency*. With
this contract, any invocation of *fact* is fated to deadlock because of the circularity
between *G* and itself (actually *this.fact(0)* never deadlocks, but the above contract
is not expressive enough to handle such cases).

In particular, we define an inference system for associating a contract to every
method of the program and to the expression to evaluate. Then we define a simple
algorithm – the *dla algorithm* – returning informations about group dependencies. The
presence of circularities in the result of *dla* reveals the possible presence of deadlocked
computations. Overall, our results show the possibility and the benefit of applying tech-
niques developed for process calculi to the area of object-oriented programming.

The paper is organized as follows. Section 2 defines FJg by introducing the main ideas and presenting its syntax and operational semantics. Section 3 discusses few sample programs in FJg and the deadlocks they manifest. Section 4 defines contracts and the inference algorithm for deriving contracts of expressions and methods. Section 5 considers the problem of extracting dependencies from contracts, presents the algorithm *dla*, and discusses its enhancements. Section 6 surveys related works, and we give conclusions and indications of further work in Section 7.

Due to space limitations, the technical details are omitted. We refer the interested
reader to the full paper in the home-pages of the authors.

## 2 The calculus FJg

In FJg a program is a collection of class definitions plus an expression to evaluate. A
simple definition in FJg is the class C in Table 1. This program defines a class C with
a method m. When m is invoked, a new object of class C is created and returned. A
distinctive feature of FJg is that an object belongs to a unique group. In the above case,
the returned object belongs to a new group – created by the operator newg. If the new
object had to belong to the group of the caller method, then we would have used the
standard operation new.
```java
class C { C m() { return newg C() ;} }
class D extends C { C n(D c) { return (c!m()).get ;} }
```

<caption>**Table 1.** Simple classes in FJg</caption>

Method invocations in FJg are asynchronous. For example, the class D in Table 1 defines an extension of C with method n. In order to emphasize that the semantics of method invocation is not as usual, we use the exclamation mark (instead of the dot notation). In FJg, when a method is invoked, the caller continues executing *in parallel with* the callee *without releasing its own group lock*; the callee gets the control by acquiring the lock of its group when it is free. This guarantees that, at each point in time, at most one task may be active per group. The get operation in the code of n constraints the method to wait for the return value of the callee before terminating (and therefore releasing the group lock).

In FJg, it is also possible to wait for a result without keeping the group lock. This is performed by the operation `await` that releases the group lock and leaves other tasks the chance to perform their activities until the value of the called method is produced. That is, `x!m().await.get` corresponds to a method invocation in standard object-oriented languages.

The decoupling of method invocation and the returned value is realized in FJg by using *future types*. In particular, if a method is declared to return a value of type C, then its invocations return values of type Fut(C), rather than values of type C. This means that the value is not available yet; when it will be, it is going to be of type C. The operation get takes an expression of type Fut(C) and returns C (as the reader may expect, await takes an expression of type Fut(C) and returns Fut(C)).

## 2.1 Syntax

The syntax of FJg uses four disjoint infinite sets of *class names*, ranged over by A, B, C, ..., *field names*, ranged over by f, g, ..., *method names*, ranged over by m, n, ..., and *parameter names*, ranged over by x, y, ..., that contains the special name *this*. We write $\bar{C}$ as a shorthand for $C_1, \dots, C_n$ and similarly for the other names. Sequences $C_1 f_1, \dots, C_n f_n$ are abbreviated as with $\bar{C} \bar{f}$.

The abstract syntax of *class declarations* CL, *method declarations* M, and *expressions* e of FJg is the following

CL ::= class C extends C {\bar{C} \bar{f}; \bar{M}}
M ::= C m(\bar{C} \bar{x}){return e; }
e ::= x | this.f | this.f = e | e!m(\bar{e}) | new C(\bar{e}) | e; e
| newg C(\bar{e}) | e.get | e await

Sequences of field declarations $\bar{C} \bar{f}$, method declarations $\bar{M}$, and parameter declarations $\bar{C} \bar{x}$ are assumed to contain no duplicate names.

A program is a pair $(ct, e)$, where the *class table* $ct$ is a finite mapping from class names to class declarations CL and e is an expression. In what follows we always assume a fixed class table $ct$. According to the syntax, every class has a superclass declared with * extends*. To avoid circularities, we assume a distinguished class name
**Field lookup:**

$$ \mathit{fields}(\mathit{Object}) = \bullet \quad \frac{\mathit{ct}(\mathit{C}) = \mathit{class} \ C \ \mathit{extends} \ D \ {\bar{C} \ \bar{f}; \ \bar{M}} \quad \mathit{fields}(\mathit{D}) = \bar{C}' \ \bar{g}}{\mathit{fields}(\mathit{C}) = \bar{C} \ \bar{f}, \ \bar{C}' \ \bar{g}} $$

**Method type lookup:**

$$ \mathit{ct}(\mathit{C}) = \mathit{class} \ C \ \mathit{extends} \ D \ {\bar{C} \ \bar{f}; \ \bar{M}} \\ \mathit{C}' \ \mathit{m} \ ({\bar{C}' \ \bar{x}})\{\mathit{return} \ e; \} \in \bar{M} \qquad \mathit{ct}(\mathit{C}) = \mathit{class} \ C \ \mathit{extends} \ D \ {\bar{C} \ \bar{f}; \ \bar{M}} \\ \mathit{m} \notin \bar{M} \\ \frac{\mathit{mtype}(\mathit{m}, \mathit{C}) = \bar{C}' \to \mathit{C}'}{\mathit{mtype}(\mathit{m}, \mathit{C}) = \mathit{mtype}(\mathit{m}, \mathit{D})} $$

**Method body lookup:**

$$ \mathit{ct}(\mathit{C}) = \mathit{class} \ C \ \mathit{extends} \ D \ {\bar{C} \ \bar{f}; \ \bar{M}} \\ \mathit{C}' \ \mathit{m} \ ({\bar{C}' \ \bar{x}})\{\mathit{return} \ e; \} \in \bar{M} \qquad \mathit{ct}(\mathit{C}) = \mathit{class} \ C \ \mathit{extends} \ D \ {\bar{C} \ \bar{f}; \ \bar{M}} \\ \mathit{m} \notin \bar{M} \\ \frac{\mathit{mbody}(\mathit{m}, \mathit{C}) = \bar{x}.e}{\mathit{mbody}(\mathit{m}, \mathit{C}) = \mathit{mbody}(\mathit{m}, \mathit{D})} $$

**Heap lookup functions:**

$$ \frac{\mathit{H}(o) = (C, G, [\bar{f} : \bar{v}])}{\mathit{class}(H, o) = C \quad \mathit{group}(H, o) = G \quad \mathit{field}(H, o, f_i) = v_i} $$

<caption>**Table 2.** Lookup auxiliary functions (• is the empty sequence)</caption>

Object with no field and method declarations whose definition does not appear in the class table. As usual, `class C { ... }` abbreviates `class C extends Object { ... }`.

Let types T be either class names C or futures Fut(C). Let also `fields(C)`, `mtype(m, C)`, and `mbody(m, C)` [9] be the standard FJ lookup functions that are reported in Table 2. The class table satisfies the following well-formed conditions:

(i) `Object` $\notin$ `dom(ct)`;

(ii) for every C $\in$ `dom(ct)`, `ct(C) = class C ... ;`

(iii) every class name occurring in `ct` belongs to `dom(ct)`;

(iv) the least relation `<:`, called *subtyping relation*, over types T, closed by *reflexivity* and *transitivity* and containing

$$ \frac{C_1 <: C_2}{\mathit{Fut}(C_1) <: \mathit{Fut}(C_2)} \qquad \frac{\mathit{ct}(C_1) = \mathit{class} \ C_1 \ \mathit{extends} \ C_2 \ {\cdots}}{C_1 <: C_2} $$

is antisymmetric;

(v) if `ct(C) = class C extends D { ... }` and `mtype(m, C) = \bar{C}' \to C'` and `mtype(m, D) = \bar{D}' \to D'` then `C' \to D'` and `\bar{D}' \to \bar{C}'`.

It is worth to remark that future types never appear in FJg programs, where types of fields and of methods are always classes. This restriction excludes either to store future values in fields or to invoke methods with future values (that later on may be

## 2.2 Semantics

Below we use an infinite set of *object names*, ranged over by o, o', ..., an infinite set of *group names*, ranged over by G, G', ..., and an infinite set of *task names*, ranged over
by t, t', ... . We assume that the set of group names has a distinguished element D,
associated to the expressions irrelevant for the deadlock analysis, such as this.f.

FJg has an operational semantics that is defined in terms of a transition relation —→ between *configurations* H ⊑ S, where H is the *heap* and S is a set of *tasks*. The heap maps (i) objects names o to tuples (*C*, *G*, [*f̃* : *v̄*]) that record their class, their group, and their fields' values; (ii) group names G to either ⊥ or ⊤ that specify whether the group is unlocked or locked, respectively. We use the standard update operations on heaps H[o ↦ (C, G, [f̃ : v̄])] and H[G ↦ 1] and on fields [f̃ : v̄][f : v] with the usual meanings. Tasks are tuples t : ⊥_o e, where t is the task name, o is the object of the task, 1 is either ⊤ (if the task owns the group lock) or ⊥ (if not), and e is the expression to evaluate. The superscript 1 is omitted when it is not relevant. In the semantic clauses, by abuse of the notation, the syntactic category e also addresses *values*, ranged over by v, which are either object or task names. The set of object and task names in e is returned by the function *names(e)*. The same function, when applied to a set of tasks S returns the object, group, and task names in S. The operational semantics also uses

- the *heap lookup functions class(H, o)*, *group(H, o)*, and *field(H, o, fᵢ)* that respectively return the class, the group and the values of *i*-th field of *o* in *H* (see Table 2);

- evaluation contexts E whose syntax is:

$$
\begin{array}{l}
E ::= [] | E!m(\bar{e}) | \mathit{this}.f = E | o!m(\bar{v}, E, \bar{e}) | \mathit{new} C(\bar{v}, E, \bar{e}) \\
    | \mathit{newg} C(\bar{v}, E, \bar{e}) | E.get | E.await | E; e
\end{array}
$$

The preliminary notions are all in place for the definition of the transition relation that is given in Table 3. It is worth to notice that, in every rule, a task moves if it owns the lock of its group. Apart this detail, the operations of update, object creation, and sequence are standard. We therefore focus on the operations about groups and futures. Rule (INVK) defines asynchronous method invocation, therefore the evaluation produces a future reference *t'* to the returned value, which may be retrieved by a *get* operation if needed. Rule (NEWG) defines *newg C(\bar{v})*, which creates a new group *G'* and a new object *o'* of that group with fields initialized to \bar{v}. This object is returned and the group *G'* is unlocked – no task of its is running. It will be locked as soon as a method of *o'* is invoked – see (LOCK). Rule (RELEASE) models method termination that amounts to store the returned value in the configuration and releasing the group lock. Rule (GET) allows one to retrieve the value returned by a method. Rules (AWAITT) and (AWAITF) model the *await* operation: if the task *t'* is terminated – it is paired to a value in the configuration – then *await* is unblocking; otherwise the group lock is released and the task *t* is blocked. Rule (CONFIG) has standard premises for avoiding unwanted name matches when lifting local reductions to complete configurations.

The initial configuration of a program (*ct*, *e*) is H ⊑ t : ⊤₀ e[°/this] where H = o ↦ (Object, G, []), G ↦ ⊤ (following our previous agreement, the class table is implicit).

*Example 1.* As an example, we detail the evaluation of the expression (newg D())!n(newg D()).get, where the class D is defined in Table 1.

$$
\begin{align*}
H \models t :_{o}^{\top} (\mathit{newg} \ D())!n(\mathit{newg} \ D()).\mathit{get} \\
\rightarrow & H_1 \models t :_{o}^{\top} o_1!n(\mathit{newg} \ D()).\mathit{get} \tag{1}
\end{align*}
$$

$$
\rightarrow H_2 \Vdash t :_o^\top o_1!n(o_2). \text{get} \qquad (2)
$$

$$
\rightarrow H_2 \Vdash t :_o^\top t_1.get, t_1 :_{o_1}^\perp o_2!m().get \quad (3)
$$
<figure><img src="image_3.png" /><figcaption>**Table 3.** The transition relation of FJg.</figcaption></figure>

$$ \rightarrow H_2[G1 \mapsto \top] \vdash t_{:0}^{\top} t1.get, t1_{:01}^{\top} o2!m().get \quad (4) $$

$$ \rightarrow H_2[G1 \mapsto \top] \vdash t_{:0}^{\top} t1.get, t1_{:01}^{\top} t2.get, t2_{:02}^{\top} newg C() \quad (5) $$

$$ \rightarrow H_3 \vdash t_{:0}^{\top} t1.get, t1_{:01}^{\top} t2.get, t2_{:02}^{\top} newg C() \quad (6) $$

$$ \rightarrow H_4 \vdash t_{:0}^{\top} t1.get, t1_{:01}^{\top} t2.get, t2_{:02}^{\top} o3 \quad (7) $$

$$ \rightarrow H_4 \vdash t_{:0}^{\top} t1.get, t1_{:01}^{\top} o3, t2_{:02}^{\top} o3 \quad (8) $$

$$ \begin{array}{l} \text{where } H = o \mapsto (\text{Object}, G, []), G \mapsto \top \qquad H_1 = H[o1 \mapsto (D, G1, []), G1 \mapsto \bot] \\ H_2 = H_1[o2 \mapsto (D, G2, []), G2 \mapsto \bot] \qquad H_3 = H_2[G1 \mapsto \top, G2 \mapsto \top] \\ H_4 = H_3[o3 \mapsto (C, G3, []), G3 \mapsto \bot] \end{array} $$

The reader may notice that, in the final configuration, the tasks t1 and t2 will terminate one after the other by releasing all the group locks.

## 3 Deadlocks

We introduce our formal developments about deadlock analysis by discussing a couple of expressions that manifest deadlocks. Let D be the class of Table 1 and consider the expression `(newg D())!n(new D()).get`. This expression differs from the one of Example 1 for the argument of the method (now it is `new D()`, before it was `newg`
D()). The computation of `(newg D())!n(new D()).get` is the same of the one in Example 1 till step (5), replacing the value of $H_2$ with $H_1[o_2 \mapsto (D, G_1, [ ])]$ ($o_1$ and $o_2$ belong to the same group $G_1$). At step (5), the task $t_2$ will indefinitely wait for getting the lock of $G_1$ since $t_1$ will never release it.

Deadlocks may be difficult to discover when they are caused by schedulers' choices. For example, let $D'$ be the following extension of the class C in Table 1:

```java
class D' extends C {
    D' n(D' b, D' c) {
        return b!p(c); c!p(b); this ;}
    C p(D' c) {
        return (c!m()).get ;}
}
```

and consider the expression `(newg D')!n(newg D', new D')`.get. The evaluation of this expression yields the tasks $t_{o_0}^{\perp} o_1, t_1^{\perp} o_1, t_2^{\perp} o_2, t_3^{\perp} o_3, t_4^{\perp} o_4, t_5^{\perp} o_5$ with $o \in G, o_1, o_3 \in G_1$ and $o_2 \in G_2$. If $t_2$ is completed before $t_3$ grabs the lock (or conversely) then no deadlock will be manifested. On the contrary, the above tasks may evolve into $t_{o_0}^{\perp} o_1, t_1^{\perp} o_1, t_2^{\perp} o_2, t_4^{\perp} o_4, t_3^{\perp} o_3, t_5^{\perp} o_5, t_4^{\perp} o_4, t_5^{\perp} o_5$. `newg C()`, `t_5^{\perp} o_2` `newg C()` that is a deadlock because neither $t_4$ nor $t_5$ will have any chance to progress.

## 4 Contracts in FJg

In the following we will consider plain FJg programs where methods never return fields nor it is possible to invoke methods with fields in the subject part or in the object part. For example, the expressions `(this.f)!m()` and `x!n(this.f)` are not admitted, as well as a method declaration like `C p() { return this.f ; }`. (The contract system in Table 4 and 5 will ban not-plain programs.) This restriction simplifies the foregoing formal developments about deadlock analysis; the impact of the restriction on the analysis of deadlocks is discussed in Section 7.

The analysis of deadlocks in FJg uses abstract descriptions of behaviours, called *contracts*, and an inference system for associating contracts to expressions (and methods). (The algorithm taking contracts and returning details about deadlocks is postponed to the next section.) Formally, *contracts* $\gamma, \gamma', \dots$ are terms defined by the rules:

$$ \gamma ::= \varepsilon \mid C.m : G(\bar{G}); \gamma \mid C.m^g : G(\bar{G}); \gamma \mid C.m^a : G(\bar{G}); \gamma $$

As usual, $\gamma; \varepsilon = \gamma = \varepsilon; \gamma$. When $\bar{\gamma}$ is a tuple of contracts $(\gamma_1, \dots, \gamma_n)$, $\text{seq}(\bar{\gamma})$ is a shortening for the sequential composition $\gamma_1; \dots; \gamma_n$. The sequence $\gamma$ collects the method invocations inside expressions. In particular, the items of the sequence may be empty, noted $\varepsilon$; or $C.m : G(\bar{G})$, specifying that the method m of class C is going to be invoked on an object of group G and with arguments of group $\bar{G}$; or $C.m^g : G(\bar{G})$, a method invocation followed by a get operation; or $C.m^a : G(\bar{G})$, a method invocation followed by an await operation. For example, the contract $C.m:G(); D.n:G'$ defines two method invocations on groups G and G', respectively (methods carry no arguments). The contract $C.m:G(); D.n^g:G'$; $E.p^a:G'$) defines three method invocations on different groups; the second invocation is followed by a get and the third one by an await.

*Method contracts*, ranged over by $G, G', \dots$, are $G(\bar{G})\{\gamma\} G'$, where $G, \bar{G}$ are pairwise different group names – $G(\bar{G})$ is the header –, $G'$ is the returned group, and $\gamma$ is a *contract*.
A contract $G(\bar{G})\{\gamma\} G'$ binds the group of the object this and the group of the arguments of the method invocation in the sequence $\gamma$. The returned group $G'$ may belong to $G, \bar{G}$ or not, that is it may be a new group created by the method. For example, let $\gamma = C.m:G(); D.n^9:G'; E.p^a:G''();$ in (i) $G(G', G'')\{\gamma\} G''$ and (ii) $G(G')\{\gamma\} G''$. In case (i) every group name in $\gamma$ is bound by names in the header. This means that method invocations are bound to either the group name of the caller or to group names of the arguments. This is not the case for (ii), where the third method invocation in its body and the returned group address a group name that is unbound by the header. This means that the method with contract (ii) is creating an object of class E belonging to a new group – called $G''$ in the body – and is performing the third invocation to a method of this object.

Method contracts are quotiented by the least equivalence $=^\alpha$ identifying two contracts that are equivalent after an injective renaming of (free and bound) group names. For example $G(G')\{C.m:G(); D.n^9:G'; E.p^a:G''();\} G' =^\alpha G_1(G_2)\{C.m:G_1(); D.n^9:G_2(); E.p^a:G''();\} G_2$. Additionally, since the occurrence of $G''$ represents an unbound group, writing $G''$ or any other free group name is the same. That is $G(G')\{C.m:G(); D.n^9:G'; E.p^a:G''();\} G' =^\alpha G_1(G_2)\{C.m:G_1(); D.n^9:G_2(); E.p^a:G_3();\} G_2$.

Let $\Gamma$, called environment, be a map from either names to pairs $(T, G)$ or class and method names, i.e. $C.m$, to terms $G(\bar{G}) \to G'$, called group types, where $G, \bar{G}, G'$ are all different from $\emptyset$. The contract judgement for expressions has the following form and meaning: $\Gamma \vdash e : (T, G)$, $\gamma$ means that the expression $e$ has type $T$ and group $G$ and has contract $\gamma$ in the environment $\Gamma$.

Contract rules for expressions are presented in Tables 4 where,

- in rule (T-INVK) we use the operator fresh($\bar{G}, G$) that returns $G$ if $G \in \bar{G}$ or a fresh group name otherwise;

- in rules (T-GET) and (T-AWAIT), we use the operator $\emptyset$ defined as follows:

$$ 
\begin{array}{l@{\qquad}l}
\varepsilon \emptyset \text{ await} = \varepsilon & \\
(\gamma; C.m G(\bar{G})) \emptyset \text{ await} = \gamma; C.m^a G(\bar{G}) & (\gamma; C.m^a G(\bar{G})) \emptyset \text{ await} = \gamma; C.m^a G(\bar{G}) \\
(\gamma; C.m G(\bar{G})) \emptyset \text{ get} = \gamma; C.m^9 G(\bar{G}) & (\gamma; C.m^a G(\bar{G})) \emptyset \text{ get} = \gamma; C.m^a G(\bar{G})
\end{array}
$$

(the other combinations of get and await are forbidden by the contract system).

The rule (T-FIELD) associates the group $\emptyset$ to the expression this.f, provided the field f exists. This judgment, together with the premises of (T-INVK) and the assumption that $\emptyset$ does not appear in $\Gamma(C.m)$, imply that subjects and objects of method invocations cannot be expressions as this.f. Apart these constraint, the contract of $e!m(\bar{e})$ is as expected, i.e. the sequence of the contract of $e$, plus the one of $\bar{e}$, with a tailing item $C.m G(\bar{G})$. Rules (T-NEW) and (T-NEWG) are almost the same, except the fact that the latter one returns a fresh group name while the former one return the group of this. The other rules are standard.

Let $G(\bar{G}) \to G' =^\alpha H(\bar{H}) \to H'$ if and only if $G(\bar{G})\{\varepsilon\}G' =^\alpha H(\bar{H})\{\varepsilon\}H'$. The contract judgements for method declarations, class declarations and programs have the following forms and meanings:

- $\Gamma; C \vdash D' m (\bar{D} \bar{x})\{\text{return } e;\} : G(\bar{G})\{\gamma\} G'$ means that the method $D' m (\bar{D} \bar{x})\{\text{return } e;\}$ has method contract $G(\bar{G})\{\gamma\} G'$ in the class C and in the environment $\Gamma$;

- $\Gamma \vdash \text{class C extends D} \{\bar{C} \bar{f}; \bar{M}\} : \{\bar{m} \mapsto \bar{G}\}$ means that the class declaration C has contract $\{\bar{m} \mapsto \bar{G}\}$ in the environment $\Gamma$;
$$
\begin{array}{l@{\qquad}l}
\text{(T-VAR)} & \Gamma \vdash \mathbf{x} : \Gamma(\mathbf{x}), \varepsilon \qquad \frac{\Gamma \vdash \mathbf{this} : (\mathbf{C}, \mathbf{G}), \varepsilon \quad \mathbf{D} \mathbf{f} \in \mathit{fields}(\mathbf{C})}{\Gamma \vdash \mathbf{this} . \mathbf{f} : (\mathbf{D}, \mathbf{D})}, \varepsilon} \\
\text{(T-INVK)} &
\end{array}
$$

$$
\begin{array}{r@{\quad}l}
\Gamma \vdash e : (C, G), \gamma & \Gamma \vdash \bar{e} : (\bar{D}, \bar{G}), \bar{\gamma} \quad \bar{D} \notin \bar{G} \\
& mtype(\mathfrak{m}, C) = \bar{C} \rightarrow C' \quad \bar{D} < : \bar{C} \\
\multicolumn{2}{c}{\Gamma(C.m) = G'(\bar{G}') \rightarrow G'' \quad G''' = fresh(\bar{G}\bar{G}, G''[\bar{G}\bar{G}/G'\bar{G}'])} \\
\multicolumn{2}{c}{\Gamma \vdash e!\mathfrak{m}(\bar{e}) : (\mathfrak{F}ut(C'), G'''), \gamma; (\mathit{seq}(\bar{\gamma})); C.m : G(\bar{G})}
\end{array}
$$

$$
\begin{array}{l}
\text{(T-NEW)} \\
\Gamma \vdash \mathbf{this} : (C, G), \varepsilon \quad \Gamma \vdash \bar{e} : (\bar{C}, \bar{G}), \bar{\gamma} \\
\qquad \mathit{fields}(C') = \bar{C}' \quad \bar{F}' \quad \bar{C}' < : \bar{C}' \\
\hline
\Gamma \vdash \mathbf{new} \ C'(\bar{e}) : (C', G), (\mathit{seq}(\bar{\gamma}))
\end{array}
$$

$$
\begin{array}{l}
\text{(T-NEWG)} \\
\Gamma \vdash \bar{e} : (\bar{C}, \bar{G}), \bar{\gamma} \quad \mathbf{G} \mathit{fresh} \\
\qquad \mathit{fields}(\mathbf{C}) = \bar{C}' \quad \bar{F}' \quad \bar{C}' < : \bar{C}' \\
\hline
\Gamma \vdash \mathbf{newg} \ C(\bar{e}) : (\mathbf{C}, G), (\mathit{seq}(\bar{\gamma}))
\end{array}
$$

$$
\begin{array}{l}
\text{(T-GET)} \\
\frac{\Gamma \vdash e : (\mathit{F}ut(C), G), \gamma}{\Gamma \vdash e . \mathit{get} : (C, G), \gamma \emptyset \mathit{get}}
\end{array}
$$

$$
\begin{array}{l}
\text{(T-AWAIT)} \\
\frac{\Gamma \vdash e : (\mathit{F}ut(C), G), \gamma}{\Gamma \vdash e . \mathit{await} : (\mathit{F}ut(C), G), \gamma \emptyset \mathit{await}}
\end{array}
$$

$$
\begin{array}{l}
\text{(T-UPDATE)} \\
\frac{\Gamma \vdash \mathbf{this} : (C, G), \varepsilon \quad \mathbf{D} \mathbf{f} \in \mathit{fields}(C)}{\Gamma \vdash e : (D', G'), \gamma \quad \mathbf{D}' < : \mathbf{D}} \\
\hline
\frac{\Gamma \vdash \mathbf{this} . \mathbf{f} = e : (D', G'), \gamma}{\Gamma \vdash \mathbf{this} . \mathbf{f} = e : (D, G'), \gamma}
\end{array}
$$

$$
\frac{\text{(T-SEQ)} \quad \Gamma \vdash e : (T, G), \gamma \quad \Gamma \vdash e' : (T', G'), \gamma'}{\Gamma \vdash e ; e' : (T', G'), \gamma ; \gamma'}
$$

<caption>Table 4. Contract rules of FJg expressions</caption>

$\vdash$ (ct, e) : cct, (T, G), $\gamma$ means that the program (ct, e) has contract class table cct and type/group/contract (T, G), $\gamma$, where a contract class table maps class names to terms {$\bar{m} : \bar{G}$}.

Table 5 reports the typing judgments for method and class declarations and for pro-
grams. We use the auxiliary function mname(M) that returns the sequence of method
names in M. We also write m ∈ ct(C) if ct(C) = class C extends D {C f; M} and
m ∈ mname(M). Rule (T-PROGRAM) requires that if a subclass overrides a method of a
superclass then the two methods must have equal contract. This constraint is expressed
by the predicate cct is ct consistent defined as follows:

$$
\textit{for every } \mathrm{ct}(C) = \mathrm{class } C \ \mathrm{ extends } \ \mathbf{D} \{\dots\} : \\
m \in \mathrm{ct}(C) \ \textit{ and } m \in \mathrm{ct}(\mathbf{D}) \ \textit{ implies } \mathrm{cct}(C)(m) = \alpha \ \mathrm{cct}(\mathbf{D})(m)
$$

This consistency requirement may be definitely weakened: we defer to future works the
issue of studying a sub-contract relation that is correct with respect to class inheritance.

The proof of correctness of the contract system in Tables 4 and 5 requires additional
rules that define the contract correctness of (runtime) configurations. These rules are:

$$
\frac{\text{(T-TASK)} \quad \Gamma \vdash \mathbf{this} : (C, G), \varepsilon \quad \Gamma \vdash t : (\mathit{F}ut(C), G'), \varepsilon}{\Gamma \vdash t . \mathit{get} : (C, G'), (G, G')}
$$

$$
\frac{(\text{T-GETR}) \quad \Gamma \vdash e : (\mathit{F}ut(C), G), \varepsilon \quad e \neq t}{\Gamma \vdash e . \mathit{get} : (C, G), \varepsilon}
$$
Contractually correct method declaration and class declaration:

$$
\begin{array}{l}
\text{(T-METHOD)} \\
\bar{G}, G \text{ fresh } \Gamma + \bar{x} : (\bar{C}', \bar{G}) + \text{this} : (C, G) \vdash e : (T', G'), \gamma \quad T' \prec C' \\
\phantom{\bar{G}, G \text{ fresh }} \Gamma(C,m) = \alpha G(\bar{G}) \to G' \\
\hline
\Gamma; C \vdash C' m (\bar{C} \bar{x})\{\text{return e;}\} : G(\bar{G})\{\gamma\} G'
\end{array}
$$

Contractually correct class and program:

$$
\begin{array}{l}
\text{(T-CLASS)} \\
\quad \Gamma; C \vdash \bar{M} : \bar{G} \\
\hline
\Gamma \vdash \text{class C extends D } \{\bar{C} \bar{f}; \bar{M}\} : \{mname(\bar{M}) \mapsto \bar{G}\} \\
\text{(T-PROGRAM)} \\
\quad C \in \text{dom}(\text{CT}) \text{ implies } \Gamma \vdash \text{ct}(C) : \text{cct}(C) \\
\phantom{\quad C \in \text{dom}(\text{CT}) \text{ implies }} \text{cct is ct consistent} \\
\text{G fresh } \Gamma + \text{this} : (\text{Object}, G) \vdash e : (T, G), \gamma \\
\quad \vdash (\text{ct}, e) : \text{cct}, (T, G), \gamma
\end{array}
$$

<caption>**Table 5.** Contract rules for method declarations and class declarations</caption>

$$
\begin{array}{l}
\text{(T-CONFIGURATION)} \\
\quad \mathit{fields}(C) = \bar{C} \bar{f} \\
\quad \mathbf{H}(o) = (C, G, [\bar{f} : \bar{v}]) \quad \text{implies} \quad \Gamma \vdash o : (C, G), \varepsilon \text{ and } \Gamma \vdash \bar{v} : \bar{C}' \text{ and } \bar{C}' \prec \bar{C} \\
\quad t \coloneqq o \in S \quad \text{implies} \quad \Gamma \vdash t : (\mathbf{Fut}(D), G'), \varepsilon \text{ and } \Gamma \vdash e : (D, G'), \gamma \text{ and } o \in \mathit{dom}(\mathbf{H}) \\
\hline
\Gamma \vdash (\mathbf{H} \dashv S)
\end{array}
$$

Rule (T-TASK) define contract correctness of runtime expressions as t.get. The rule uses contracts extended with terms (G, G'). γ. While rule (T-GETR) deals with the expression t awaits.get. It is worth to notice the absence of rules for the runtime expression t awaits. In fact, the judgment of this expression follows by (T-AWAIT) and the definition of ε ∖ await.

**Theorem 1 (Subject reduction).**

1. If $\Gamma \vdash (ct, e) : (cct, \gamma)$ then the initial configuration of $(ct, e)$ is contractually correct. Namely, there is $\Gamma$ such that $\Gamma \vdash (H \dashv t \coloneqq_o^\top e[^0/this])$, where $\Gamma = o \mapsto (Object, G)$, $t \mapsto (Fut(C), G)$ and $H = o \mapsto (Object, G, [])$, $G \mapsto \top$.

2. Let $\Gamma \vdash (H \dashv S)$ and $H \dashv S \longrightarrow H' \dashv S'$. Then there is $\Gamma'$ such that $\Gamma' \vdash (H' \dashv S')$.

**5 Deadlock analysis in FJg**

The contract system in Tables 4 and 5 does not convey any information about dead-
locks: it only associates contracts to expressions (and methods). The point is that con-
tracts retain the necessary informations about deadlocks and the analysis may be safely
reduced to them, overlooking all the other details. We begin with the formal definition
of a deadlock.
**Definition 1.** A configuration $H \Vdash S$ is deadlocked if there are $t_i, o_i, E_i$, and $e_i$, with $1 \le i \le n+k$, such that $n \ge 1$ and

- every $1 \le i \le n$ is $t_i :_{o_i}^{\top} E_i[t_{t_i}.get]$ with $l_i \in 1..n+k$ and

- every $n+1 \le j \le n+k$ is $t_j :_{o_j}^{\perp} e_j$ with $group(H, o_j) \in \{group(H, o_1), \dots, group(H, o_n)\}$.

A configuration $H \Vdash S$ is deadlock-free if, for every $H \Vdash S \rightarrow_S^* H' \Vdash S'$, $H' \Vdash S'$ is not deadlocked. A program $(ct, e)$ is deadlock-free if its initial configuration is deadlock-free.

It is easy to verify that the programs discussed in Section 3 are not deadlock-free. We observe that a configuration may have a blocked task without retaining any deadlock. This is the case of the process $C.m^g G()$, where $C.m: G() \{C.m^g(G')\} G$, that produces an infinite chain of tasks $t_i :_{o_i}^{\top} t_{i+1}.get$. (The following dla algorithm will reject this contract.)

We say that a configuration $H \Vdash S$ has a *group-dependency* $(G, G')$ if $S$ contains either the tasks $t :_{o_0}^{\top} E[t'.get]$, $t' :_{o'} e$, with $t'$ retaining or not its group lock, or the tasks $t :_{o_0}^{\perp} e$, $t' :_{o'}^{\top} E[t''.get]$ (in both cases $e$ is not a value) and $G = group(H, o)$ and $G' = group(H, o')$. A configuration contains a *group-circularity* if the transitive closure of its group-dependencies has a pair $(G, G)$. The following statement asserts that a group-circularity signals the presence of a sequence of tasks mutually waiting for the release of the group lock of the other.

**Proposition 1.** *A configuration is deadlocked if and only if it has a group-circularity.*

In the following, sets of dependencies will be noted $G, G', \dots$. Sequences $G_1; \dots; G_n$ are also used and shortened into $\bar{G}$. Let $G \cup (G_1; \dots; G_n)$ be $G \cup G_1; \dots; G \cup G_n$. A set $G$ is *not circular*, written $G: \text{not-circular}$, if the transitive closure of $G$ does not contain any pair $(G, G)$. The definition of being not circular is extended to sequences $G_1; \dots; G_n$, written $G_1; \dots; G_n: \text{not-circular}$, by constraining every $G_i$ to be not circular.

Dependencies between group names are extracted from contracts by the algorithm dla defined in Table 6. This algorithm takes an abstract class contract table $\Delta_{CCT}$, a group name $G$ and a contract $\gamma$ and returns a sequence $\bar{G}$. The abstract class contract table $\Delta_{CCT}$ takes a pair class name $C$/method name $m$, written $C.m$, and returns an abstract method contract $(G, \bar{G})G$. The map $\Delta_{CCT}$ is the least one such that

$$ \Delta_{CCT}(C.m) = (G, \bar{G}) \bigcup_{i \in 1..n} G_i \quad \text{if and only if} \quad \begin{array}{l} \text{cct}(C)(m) = G(\bar{G})\{\gamma\} G' \\ \text{dla}(\Delta_{CCT}, G, \gamma) = G_1; \dots; G_n \end{array} $$

We notice that $\Delta_{CCT}$ is well-defined because: (i) group names in cct are finitely many; (ii) dla never introduces new group names; (iii) for every $C.m$, the element $\Delta_{CCT}(C.m)$ is a finite lattice where elements have shape $(G, \bar{G})G$ and where the greatest set $G$ is the cartesian product of group names in cct. Additionally, in order to augment the precision of $\Delta_{CCT}$, we assume that cct satisfies the constraint that, for every $C.m$ and $D.n$ such that $C.m \neq D.n$, $cct(C)(m)$ and $cct(D)(n)$ have no group name in common (both bound and free). (When this is not the case, sets in the codomain of $\Delta_{CCT}$ are smaller, thus manifesting more circularities.)
$$ \text{dla}(\Delta_{\text{CCT}}, G, \varepsilon) = \emptyset \qquad \frac{\Delta_{\text{CCT}}(C.m) = (G''; \bar{G}'')G \quad \text{dla}(\Delta_{\text{CCT}}, G, \gamma') = \bar{G}}{\text{dla}(\Delta_{\text{CCT}}, G, C.m \ G'(\bar{G}'); \gamma') = G[G'; \bar{G}'/G''; \bar{G}''] \cup \bar{G}} $$

$$ \frac{\Delta_{\text{CCT}}(C.m) = (G''; \bar{G}'')G \quad \text{dla}(\Delta_{\text{CCT}}, G, \gamma') = \bar{G}}{\text{dla}(\Delta_{\text{CCT}}, G, C.m^g G'(\bar{G}'); \gamma') = (\{(G, G')\} \cup G[G'; \bar{G}'/G''; \bar{G}'']); \bar{G}} $$

$$ \frac{\Delta_{\text{CCT}}(C.m) = (G''; \bar{G}'')G \quad \text{dla}(\Delta_{\text{CCT}}, G, \gamma') = \bar{G}}{\text{dla}(\Delta_{\text{CCT}}, G, C.m^a G'(\bar{G}'); \gamma') = G[G'; \bar{G}'/G''; \bar{G}'']; \bar{G}} $$

<caption>**Table 6.** The algorithm `dla`</caption>

Let us comment the rules of Table 6. The second rule of `dla` accounts for method invocations `C.m G'(G''); \gamma'`. Since the code of `C.m` will run asynchronously with respect to the continuation `\gamma'`, i.e. it may be executed at any stage of `\gamma'`, the rule adds the pairs of `C.m` (stored in `\Delta_{CCT}(C.m)`)) to every set of the sequence corresponding to `\gamma'`. The third rule of `dla` accounts for method invocations followed by `get C.m^g G'(G'')`; `\gamma'`. Since the code of `C.m` will run before the continuation `\gamma'`, the rule prefixes the sequence corresponding to `\gamma'` with the pairs of `C.m` extended with `(G, G')`, where `G` is the group of the caller and `G'` is the group of the called method. The rule for method invocations followed by `await` is similar to the previous one, except that no pair is added because the `await` operation releases the group lock of the caller.

A program `(ct, e)` is deadlock free if `ct` (ct, e) : `CCT`, `(T, G)`, `\gamma` and `dla(\Delta_{CCT}, G, \gamma)` : not-circular, where `G` is a fresh group name, that is `G` does not clash with group names in `cct` (group names in `\gamma` are either `G` or fresh as well – see Table 4).

**Example 2.** Let `C` and `D` be the classes of Table 1 and `D'` be the class in Section 3. We derive the following contract class table `cct` and abstract contract class table `\Delta_{CCT}:`

```
C.m    ↦ G() { ε } G'
D.n    ↦ E(E') {D.m^g:E'()} E''
D.m    ↦ F() { ε } F'
D'.n   ↦ H(H', H'') {D'.p:H'(H''); D'.p:H''(H')} H
D'.p   ↦ I(I') { D'.m^g: I'() } I''
D'.m   ↦ L() { ε } L'

C.m    ↦ (G)Ø
D.n    ↦ (E, E') { (E, E') }
D.m    ↦ (F)Ø
D'.n   ↦ (H, H', H'') {(H', H'), (H'', H')}
D'.p   ↦ (I, I') { (I, I') }
D'.m   ↦ (L)Ø
```

Now consider the expressions `(newg D())!n(newg D()).get` and `(newg D())!n(new D()).get` of Section 2, which have contracts `D.n^g:L_2(L_3)` and `D.n^g:L_2(L_1)`, respectively, with `L_1` being the group of this. We obtain `dla(\Delta_{CCT}, L_1, D.n^g : L_2(L_3)) = \{(L_2, L_3), (L_1, L_2)\}` and `dla(\Delta_{CCT}, L_1, D.n^g : L_2(L')) = \{(L_2, L_1), (L_1, L_2)\}` where the first set of dependencies has no group-circularity – therefore `(newg D())!n(newg D()).get` is deadlock-free – while the second has a group-circularity – `(newg D())!n(new D()).get` – may manifest a deadlock, and indeed it does.

Next consider the expression `(newg D')!n(newg D', new D').get` of Section 3, which has contract `D'.n^g:L''(L'''', L')`, being `L'` the group of this. We obtain

`dla(\Delta_{CCT}, L', (newg D')!n(newg D', new D').get) = \{(L'''', L'), (L', L''''), (L', L'')\}`
where the set of dependencies manifests circularities. In fact, in Section 3, we observed
that the above expression may manifest a deadlock.

The d1a algorithm is correct, that is, if its result contains a group-circularity, then
the evaluation of the analyzed expression may manifest a deadlock (vice versa, if there
is no group-circularity then no deadlock will be ever manifested).

**Theorem 2.** If $\vdash$ (cT, e) : (cCT, y) and d1a($\Delta_{CCT}$, G, y) is not circular then (cT, e) is deadlock-free.

The algorithm d1a may be strengthened in several ways. Let us discuss this issue
with a couple of examples. Let C' be the class

class C' { C' m(C' b, C' c){ return b!n(c).get ; c!n(b).get ;}
C' n(D' c){ return (c!p).get ;}
C' p() { return new C'() ;} }

and let cct be its contract class table:

C'.m ↦→ G(G', G''){C'.n⁹:G'(G'') ; C'.n⁹:G''(G')} G'
C'.n ↦→ F(F'){C'.p⁹:F'(F')} F'
C'.p ↦→ E() {ε} E

The reader may verify that the expression (new C'())!m1(newg C'(), newg C'()) never deadlocks. However, since ΔCCT(C'.m) = (G, G', G''){(G, G'), (G', G''), (G, G''), (G', G')}, the algorithm d1a wrongly returns a circular set of dependencies. This problem is due to the fact that ΔCCT melds the group dependencies of different time points into a single set. Had we preserved the temporal separation, that is {(G, G'), (G', G'')}; {(G, G''), (G'', G')}, no group-circularity should have been manifested.

The second problem is due to the fact that free group names in method contracts
should be renamed each time the method is invoked (with fresh group names) be-
cause two invocations of a same method create different group names. On the con-
trary, the algorithm d1a always uses the same (free) name. This oversimplification
gives a wrong result in this case. Let C'' be class C'' { C'' m() { return (newg
C''())!m().get ;} } (with cct(C''.m) = G() {C'.m⁹ : G'()}G') and consider the ex-
pression (newg C''())!m().get. The evaluation of this expression never manifests
a deadlock, however its contract is C''.m⁹ : F() and the algorithm d1a will return the
set {(G, F), (F, G'), (G', G')}, which has a group-circularity. In the conclusions we will
discuss the techniques for reducing these errors.

# 6 Related works

The notion of grouping objects dates back at least to the mid 80’s with the works of Yonezawa on the language ABCL/1 [8, 21]. Since then, several languages have a notion of group for structuring systems, such as Eiffel// [3], Hybrid [17], and ASP [4]. A library for object groups has also been defined for CORBA [7]. In these proposals, a single task is responsible for executing the code inside a group. Therefore it is difficult to model behaviours such as waiting for messages without blocking the group for other activities.
Our FJg calculus is inspired to the language Creol that proposes object groups, called *JCoBoxes*, with multiple cooperatively scheduled tasks [10]. In particular FJg is a subcalculus of JCoBox<sup>c</sup> in [19], where the emphasis was the definition of the semantics and the type system of the calculus and the implementation in Java.

The proposals for static analyses of deadlocks are largely based on types (see for instance [11, 20] and, for object-oriented programs [1]). In these papers, a type system is defined that computes a partial order of the locks in a program and a subject reduction theorem demonstrates that tasks follow this order. On the contrary, our technique does not computes any ordering of locks, thus being more flexible: a computation may acquire two locks in different order at different stages, thus being correct in our case, but incorrect with the other techniques. A further difference with the above works is that we use contracts that are terms in simple (= with finite states) process algebras [12]. The use of simple process algebras to describe (communication or synchronization) protocols is not new. This is the case of the exchange patterns in sSDL [18], which are based on CSP [2] and the pi-calculus [14], or of the behavioral types in [16] and [5], which use CCS [13]. We expect that finite state abstract descriptions of behaviors can support techniques that are more powerful than the one used in this contribution.

# 7 Conclusions

We have developed a technique for the deadlock analysis of object groups that is based on abstract descriptions of methods behaviours.

This study can be extended in several directions. One direction is the total coverage of the full language FJg. This is possible by using group records $\Theta, \Theta' = G[\mathfrak{f}_1 : \Theta_1, \dots, \mathfrak{f}_k : \Theta_k]$ instead of simple group names. Then contracts such as $C.m : G(\bar{G})$ become $C.m : \Theta(\Theta_1, \dots, \Theta_n)$ and the rule (T-FIELD) is refined into

$$ \frac{\Gamma \vdash \mathit{this} : (C, G[\bar{\mathfrak{f}} : \bar{\Theta}]), \varepsilon \quad D f \in \mathit{fields}(C) \quad f : \Theta' \in \bar{\mathfrak{f}} : \bar{\Theta}}{\Gamma \vdash \mathit{this.f} : (D, \Theta'), \varepsilon} $$

The overall effect of this extension is to hinder the notation used in the paper, without conveying any interesting difficulty (for this reason we have restricted our analysis to a sublanguage). We claim that every statement for plain FJg in this paper also hold for full FJg.

A different direction of research is the study of techniques for augmenting the accuracy of the algorithm *dla*, which is imprecise at the moment. The intent is to use finite state automata with name creation, such as those in [15], and modeling method contracts in terms of finite automata and study deadlocks in sets of these automata.

Other directions address extensions of the language FJg. One of these extensions is the removal of the constraint that future types cannot be used by programmers in FJg. Future types augment the expressivity of the language. For example it is possible to synchronize several tasks and define *livelocks*:

```java
class C { f: Fut(C) ; C m() { return this.f = this!n() ; new C() ;}
    C n() { return this.f.get ; new C() ;} }
```
Another extension is about re-entrant method invocations (usually used for tail recursions), which are synchronous invocations. Such extension requires revisions of semantics rules, of the contract rules in Table 4, and of the d1a algorithm.

## References

1. M. Abadi, C. Flanagan, and S. N. Freund. Types for safe locking: Static race detection for java. *ACM Trans. Program. Lang. Syst.*, 28, 2006.

2. S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. *J. ACM*, 31:560–599, 1984.

3. D. Caromel. Towards a method of object-oriented concurrent programming. *Commun. ACM*, 36(9):90–102, 1993.

4. D. Caromel, L. Henrio, and B. P. Serpette. Asynchronous and deterministic objects. In *Proc. POPL'04*, pages 123–134. ACM, 2004.

5. S. Chaki, S. K. Rajamani, and J. Rehof. Types as models: model checking message-passing programs. *SIGPLAN Not.*, 37(1):45–57, 2002.

6. F. de Boer, D. Clarke, and E. Johnsen. A complete guide to the future. In *Progr. Lang. and Systems*, volume 4421 of LNCS, pages 316–330. Springer, 2007.

7. P. Felber and R. Guerraoui. Programming with object groups in corba. *IEEE Concurrency*, 8:48–58, 2000.

8. Y. Honda and A. Yonezawa. Debugging concurrent systems based on object groups. In *Proc. ECOOP'88*, volume 322 of LNCS, pages 267–282. Springer, 1988.

9. A. Igarashi, B. C. Pierce, and P. Wadler. Featherweight Java: a minimal core calculus for Java and GJ. *ACM Trans. Program. Lang. Syst.*, 23:396–450, 2001.

10. E. B. Johnsen and O. Owe. An asynchronous communication model for distributed concurrent objects. *Software and System Modeling*, 6(1):39–58, 2007.

11. N. Kobayashi. A new type system for deadlock-free processes. In *Proc. CONCUR 2006*, volume 4137 of LNCS, pages 233–247. Springer, 2006.

12. C. Laneve and L. Padovani. The *must* preorder revisited. In *Proc. CONCUR 2007*, volume 4703 of LNCS, pages 212–225. Springer, 2007.

13. R. Milner. *A Calculus of Communicating Systems*. Springer, 1982.

14. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, ii. *Inf. and Comput.*, 100:41–77, 1992.

15. U. Montanari and M. Pistore. History-dependent automata: An introduction. In *Formal Methods for the Design of Computer Communication, and Software Systems*, volume 3465 of LNCS, pages 1–28. Springer, 2005.

16. H. R. Nielson and F. Nielson. Higher-order concurrent programs with finite communication topology. In *Proc. POPL '94*, pages 84–97. ACM, 1994.

17. O. Nierstrasz. Active objects in Hybrid. In *Proc. OOPSLA'87*, pages 243–253, 1987.

18. S. Parastatidis and J. Webber. *MEP SSDL Protocol Framework*, Apr. 2005. http://ssdl.org.

19. J. Schäfer and A. Poetzsch-Heffter. JCoBox: Generalizing active objects to concurrent components. In *Proc. ECOOP'10*, volume 6183 of LNCS, pages 275–299. Springer, 2010.

20. V. T. Vasconcelos, F. Martins, and T. Cogumbreiro. Type inference for deadlock detection in a multithreaded polymorphic typed assembly language. In *Proc. PLACES'09*, volume 17 of EPTCS, pages 95–109, 2009.

21. A. Yonezawa, J.-P. Briot, and E. Shibayama. Object-oriented concurrent programming in ABCL/1. In *Proc. OOPSLA'86*, pages 258–268, 1986.