Elena Giachino
email: giachino@cs.unibo.it

Cosimo Laneve
email: laneve@cs.unibo.it

A beginner's guide to the deadLock Analysis M odel

Keywords: Static deadlock analyzers, object-oriented languages, circular dependencies, lam, livelocks

. We present a basic Java-like language and the deadlock analysis model in an accessible way. We also overview the algorithm for deciding deadlockfreeness by discussing a number of paradigmatic examples. We finally explore the techniques for coping with extensions of the object-oriented language.

Introduction

Modern systems are designed to support a high degree of parallelism by ensuring that as many system components as possible are operating concurrently. Deadlock represents an insidious and recurring threat when such systems also exhibit a high degree of resource and data sharing. In these systems, deadlocks arise as a consequence of exclusive resource access and circular wait for accessing resources. A standard example is when two processes are exclusively holding a different resource and are requesting access to the resource held by the other. An alternative description is that the correct termination of each of the two process activities depends on the termination of the other. Since there is a circular dependency, termination is not possible.

Deadlocks may be particularly insidious to detect in systems where the basic communication operation is asynchronous and the synchronization explicitly occurs when the value is strictly needed. Speaking a Java idiom, methods are synchronized, that is each method of the same object is executed in mutual exclusion, and method invocations are asynchronous, that is the caller thread continues its execution without waiting for the result of the called method. Additionally, an operation of join explicitly synchronizes caller and called methods (possibly returning the value of the called method). In this context, when a thread running on an object x performs a join operation on a thread on y then it blocks every other thread that is competing for the lock on x. This blocking situation corresponds to a dependency pair (x, y), meaning that the progress on x is possible provided the progress of threads on y. A deadlock then corresponds to a circular dependency in some configuration.

Further difficulties arise in the presence of infinite (mutual) recursion: consider, for instance, systems that create an unbounded number of processes such as server applications. In such systems, process interaction becomes complex and really hard to predict. In addition, deadlocks may not be detected during testing, and even if they are it can be difficult to reproduce them and find their causes.

Deadlock detection has been largely investigated both with static and runtime techniques [START_REF] Boyapati | Ownership types for safe program.: preventing data races and deadlocks[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Agarwal | Detection of deadlock potentials in multithreaded programs[END_REF] (just to cite few references). Static analysis guarantees that all executions of a program are deadlock-free, at the cost of being not precise because it may discard safe programs (false positives). Run-time checking cannot be exhaustive. However, whenever applicable, it produces fewer false positives than static analysis.

We adopt a static approach, while retaining the precision of a run-time checker in a large number of cases. Our deadlock detection framework consists of an inference algorithm that extracts abstract behavioral descriptions out of the concrete program. These abstract descriptions, called lam programs, an acronym for deadLock Analysis Model, retain necessary informations for the deadlock analysis (typically all the synchronization informations are extracted, while data values are ignored). Then a decision algorithm evaluates the abstract program for verifying its circularity-freeness (every state has no circular dependency). In turn, this property implies the deadlock-freeness of the original program. Our approach is then both flexible (since only the inference algorithm has to be adapted to the language, while the analyzer is language-independent) and precise (since the analyzer is a decision algorithm on a large class of lam programs -see below). The major benefits of our technique are that (i) it does not use any pre-defined partial order of resources and that (ii) it accounts for dynamic resource creation.

To overview our analyzer, we observe that, in presence of recursion in the code, the evaluation of the abstract description may end up into an infinite sequence of states, without giving back any answer. Instead, our analysis always terminates. The theoretical framework we have designed allow us to determine when to stop the evaluation. Informally, when the abstract program is linear -it has (mutual) recursions of the kind of the factorial function -, then states reached after some point are going to be equivalent to past states. That point, called saturated state, may be determined in a similar way as the orbit of a permutation [START_REF] Comtet | Advanced Combinatorics: The Art of Finite and Infinite Expansions[END_REF] (actually, our theory builds on a generalization of the theory of permutations [START_REF] Giachino | Mutations, flashbacks and deadlocks[END_REF]). A saturated state represents the end of a pattern that is going to repeat indefinitely. Therefore it is useless to analyze it again and, if a deadlock has not been encountered up to that point, then it cannot be produced afterwords. Analogously, if a deadlock has been encountered, then a similar deadlock must be present each time the same pattern recurs. When the abstract program is nonlinear -it has (mutual) recursions of the kind of the fibonacci function -our technique is not precise because it introduce fake dependency pairs. However, it is sound.

The aim of this paper is to present our deadlock technique informally, by means of examples and without going into the (many) theoretical details. The interested reader may find the theoretical developments in [START_REF] Giachino | Mutations, flashbacks and deadlocks[END_REF] and the application of our abstract descriptions to a programming language in [START_REF] Giachino | Deadlock and livelock analysis in concurrent objects with futures[END_REF][START_REF] Giachino | Deadlock analysis in practice[END_REF].

The structure of the paper is as follows. In Section 2, we introduce the programming language and the analysis model. In Section 3, we overview the algorithm for detecting circularities in the analysis model. In Section 4, we discuss a number of programs and their associated abstract models. In Section 5, we explore two relevant extensions of the programming language: field assignment and an operation for releasing the lock. We conclude in Section 6.

2 Languages and models

The language FJf

The programs that are analyzed in this paper will be written in a Java-like language. Instead of using Java, which is quite verbose, we stick to a dialect of the abs language [START_REF] Johnsen | ABS: A core language for abstract behavioral specification[END_REF], called FJf. To enhance readability, the semantics of FJf will be given in an indirect way by discussing the compilation patterns of the main constructs of FJf into Java (the reader is referred to [START_REF] Giachino | Deadlock analysis in practice[END_REF] for a direct operational semantics). where sequences of field declarations T f, method declarations M, and parameter declarations T 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, called main expression.

According to the syntax, every class has a superclass declared with extends. To avoid circularities, we assume a distinguished class name Object with no field and method declarations and whose definition does not appear in the class table. We always omit the declaration "extends Object".

The main features of FJf are:

futures -Fut(T) these terms are called futures of type T and represent pointers to values of type T that may be not available yet. Fut(T) are the types of method invocations that have T as return type.

asynchronous method invocationx!m(y): the caller continues its execution when a method m of x is invoked without waiting for the result. The called method is evaluated in parallel (on a new spawned thread). The invocation x!m(y) has the same behavior as the following code written in Java new Thread ( new Runnable() { public void run() { x.m(y); } }).start();

where, for the sake of conciseness, the code for exception handling is omitted. In particular, in Java, every join() statement and every synchronized method invocation should handle an InterruptedException. mutual exclusion: in FJf every method invocation spawns a new thread. However at most one thread per object is executed at the same time. This is translated in Java by declaring every method to be synchronized. thread synchronization for value retrieval : in FJf the caller retrieves the result of an invocation by the operation t.get, where t is a reference of the invocation. The get operation is blocking until the returned value is produced. The FJf code:

x!m(y).get;

corresponds to the synchronization behavior of the following code in Java (without exception handling management)

Thread t = new Thread ( new Runnable() { public void run() { x.m(y); } }); t.start(); t.

join();

The operations get in FJf and join in Java have not the exact same meaning: while get synchronizes the two threads and retrieves the value, join is just a synchronization between the callee's and the caller's threads. However, from the point of view of deadlock analysis, the behaviors of the two operations are equivalent.

We omit examples at this stage: several FJf codes will be discussed in Section 4.

Analysis models for detecting circularities

In [START_REF] Giachino | Mutations, flashbacks and deadlocks[END_REF], we have developed a theoretical framework for defining relations on names (every pair of a relation defines a dependency between two tasks, the first one is waiting for the result of the second) and for determining whether a definition may produce a circular dependency -a deadlock -or not. The language for defining relation is called lam -an acronym for deadLock Analysis Model. Lams are defined by terms that use a set of names, ranged over by x, y, z, • • •, and a disjoint set of function names, ranged over m, m

′ , n, n ′ , • • •. A lam program is a tuple m 1 ( x 1 ) = L 1 , • • • , m ℓ ( x ℓ ) = L ℓ , L where m i ( x i ) = L i are function definitions and L is the main lam. The syntax of L i and L is L ::= 0 | (x, y) | m( x) | L L | L; L
such that (i) all function names occurring in L i and L are defined, and (ii) the arity of function invocations matches that of the corresponding function definition.

It is possible to associate a lam function to each method of a FJf program. The purpose of the association is to abstract the object dependencies that a method will generate out of its definition. For instance, the FJf method declaration

C m1( C y, C z ) { return ( y!m2( z ) ).get ; } has the associated function declaration in a lam program m1(x, y, z) = (x, y) m2(y, z)
where the first argument is the name of the object this, which is x for m1 and y in the invocation of m2. The association method-definition/lam-function is defined by an inference system in [START_REF] Giachino | Deadlock and livelock analysis in concurrent objects with futures[END_REF]. In this paper, in order to be as simple as possible, we keep this association informal.

The semantics of a lam program requires a couple of preliminary notions. Let V, V ′ , I, • • • be partial orders on names (relations that are reflexive, antisymmetric, and transitive) and let V ⊕ x< z, with x ∈ V and z / ∈ V, be the least partial order V ′ that satisfies the following rules

V ⊆ V ′ x ∈ x (x, y) ∈ V ′ z ∈ z (y, z) ∈ V ′
That is, z become maximal names of V ⊕ x< z. Let lam contexts, noted L[ ], be terms derived by the following syntax:

L[ ] ::= [ ] | L L[ ] | L; L[ ] As usual L[L]
is the lam where the hole of L[ ] is replaced by L. Finally, let var (L) be the set of names occurring in L.

The operational semantics of a program m 1 (

x 1 ) = L 1 , • • • , m ℓ ( x ℓ ) = L ℓ , L ℓ+1
is defined by a transition relation between states that are pairs V, L and satisfying the rule:

(Red) m( x) = L var (L) \ x = z w are fresh L[ w / z ][ u / x ] = L ′ V, L[m( u)] -→ V ⊕ u< w, L[L ′ ]
By (red), a lam is evaluated by successively replacing function invocations with the corresponding lam instances. At every evaluation step, free names in a lam definition m( u) = L, namely var (L) \ x, are replaced by fresh names. This replacement models name creation and correspond to the new operation in FJf. For example, if m(x) = (x, y) m(y) and m(u) occurs in the main lam, then m(u) is replaced by (u, v) m(v), where v is a fresh maximal name in some partial order. The initial state of a program with main lam L is I x , L , where

x = x 1 , • • • , x n = var (L) and I x = {(x, x) | x ∈ x} (we are abusing of the set-notation).
Lams record sets of relations on names. To make explicit these relations, let ♭(•), called flattening, be the function inductively defined as follows

♭(0) = 0, ♭((x, y)) = (x, y), ♭(m( x)) = 0, ♭(L L ′ ) = ♭(L) ♭(L ′ ), ♭(L; L ′ ) = ♭(L); ♭(L ′ ).
For example

♭(m(x, y, z); (x, y) n(y, z) m(u, y, z); n(u, v) (u, v); (v, u)) = (x, y); (u, v); (v, u)
that is, the argument of ♭(•) defines three relations: {(x, y)} and {(u, v)} and {(v, u)}. It is easy to verify that, up-to the axioms

(x, y) (x, y) = (x, y) (L; L ′ ) (x, y) = L (x, y); L ′ (x, y) L = (x 1 , y 1 ) • • • (x n , y n ) L; L = L ♭(L)
♭(L) = (x 1 , x 2 ) (x 2 , x 3 ) • • • (x m , x 1 ) L ′ ; L ′′ for some x 1 , • • • , x m . A state V, L has a circularity if L has a circularity. A program m 1 ( x 1 ) = L 1 , • • • , m ℓ ( x ℓ ) = L ℓ ,
L is circularity-free if no state yielded by evaluating I var (L) , L has a circularity.

The algorithm for deciding circularity-freeness

In case of non-recursive lam programs, since the evaluations always terminate, the circularity-freeness problem is (easily) decidable. Otherwise -when functions are (mutually) recursive -the evaluation would not terminate and would produce infinite relations due to the creation of names. Nevertheless, the problem of circularity-freeness is decidable for a large set of mutual recursive lam programs -the linear ones.

Definition 2. A lam program m 1 ( x 1 ) = L 1 , • • • , m ℓ ( x ℓ ) = L ℓ , L is linear if, for every function m i0
, there is at most one sequence m i0 • • • m im such that, for every 0 ≤ j ≤ m, L ij contains exactly one invocation of m i j+1%m (the operation % is the remainder of the natural division).

For example, a factorial-like programs, such as fact(x) = (x, y) fact(y), fact(x) , are linear, while fibonacci-like ones, such as fib(x) = (x, y) (x, z) fib(y) fib(z), fib(x) , are not. The idea of our technique is to recognize the pattern of the recursion in order to be able to determine the states when the evaluation flow is going to repeat the same pattern (with different names) and only produce pattern of dependencies that were already discovered in the past of the evaluation. Once our algorithm recognizes these states, called saturated states, it just interrupts avoiding non-terminating evaluations.

Theorem 1 ( [START_REF] Giachino | Mutations, flashbacks and deadlocks[END_REF]). The problem of circularity-freeness in linear lam programs is decidable.

The theoretical details of this theorem are out of the scope of this paper.

Here we illustrate the algorithm on the following sample program: fact(x) = (x, y) fact(y), fact(x) . In this case, our theory affirms that the saturated state is reached in two steps of evaluation. That is

I x , fact(x) -→ I x ⊕ (x<y), (x, y) fact(y) -→ I x ⊕ (x<y) ⊕ (y<z), (x, y) (y, z) fact(z) .
We observe that, if we perform a further step of evaluation, we get

I x ⊕ (x<y) ⊕ (y<z) ⊕ (z<u), (x, y) (y, z) (z, u) fact(u)
and there is an injective partial map ρ on

I x ⊕ (x<y) ⊕ (y<z) ⊕ (z<u), namely ρ = [z → x, u → y], such that
1. fact(u) is mapped to an invocation that is already evaluated -that is fact(x); 2. dependencies produced by fact(z), namely (z, u) are mapped to dependencies that have been already produced, namely (x, y).

These properties allow us to decide that the evaluation is repeating the same pattern (on new names) and conclude that no circularity will be ever manifested since the saturated state is circularity-free.

When the lam program is nonlinear, our technique is imprecise but sound: the nonlinear lam program is transformed into a linear one by contracting multiple method invocations to one. This contraction introduces fake dependencies (i.e. false positives in terms of circularities). Once the linear transformed program is obtained, then the analysis is run on it. It turns out that these additional dependencies cannot be eliminated because of a cardinality argument. More precisely, the evaluation of a method invocation m( u) in a linear program may produce at most one invocation of m, while an invocation of m( u) in a nonlinear program may produce two or more invocations of m. When the invocations of m create names, contracting different invocations into one means reducing an exponential number of new names to a linear number. This, in terms of the analysis means losing precision. Nevertheless, we prove the soundness of our technique: if the transformed linear program is circularity-free then the original nonlinear one is also circularity-free. For example, consider the fibonacci-like program fib(x) = (x, y) (x, z) fib(y) fib(z), fib(x)

The transformed program is

fib aux (x, x ′ ) = (x, y) (x, z) (x ′ , y) (x ′ , z) fib aux (y, z) , fib aux (x, x)
which is linear but adds dependencies. In this transformation, the two invocations of fib have been contracted into one -the fib aux invocation -that carries two arguments, one for every invocation -notice that the invocation fib aux (y, z) corresponds to the two invocations fib(y) and fib(z). In the body of fib aux , the creation of the two names in fib is simulated by creating two names as well. However, these two names are the same both for the first argument and for the second one (that correspond to the two recursive invocations of fib). This results into fake dependencies between names originally belonging to two different and independent invocations. In particular, after two steps of evaluation, fib aux (x, x) gives, (x, y)

(x, z) (y, y ′ ) (y, z ′ ) (z, y ′ ) (z, z ′ ) fib aux (y ′ , z ′ )
whilst the corresponding lam of the original nonlinear program is

(x, y) (x, z) (y, y ′ ) (y, y ′′ ) (z, z ′ ) (z, z ′′ ) fib(y ′ ) fib(y ′′ ) fib(z ′ ) fib(z ′′ ) .
We demonstrate that, if no circularity is manifested by the saturated state of fib aux then the original fibonacci program is circularity-free. Since the circularityfreeness of fib aux is decidable, by Theorem 1, then, in case of circularity-freeness, we are able to state the same property for fib.

The technique by examples

We illustrate our analysis technique by discussing a number of programs written in FJf. Every example is discussed as follows:

1. we first present the FJf description; 2. then we give the associated lam, by keeping informal the association technique (see [START_REF] Giachino | Deadlock and livelock analysis in concurrent objects with futures[END_REF] for on a inference system defining the formal association); 3. we finally inspect and evaluate lams looking for circularities. An invocation x!m1(y,z) spawns a thread (in the thread pool of x) that will invoke y!m2(z) and immediately blocks because of the get (hence it will not release the lock on x), waiting for the value that is returned by m2. The invocation y!m2(z), in turn, causes a new thread to be spawned (in the thread pool of y) that invokes z!m3() and blocks waiting for its result. The lam functions associated to the above methods are m1(x, y, z) = (x, y) m2(y, z) m2(x, y) = (x, y) m3(y) m3(x) = 0 That is, to every method declaration we associate a lam declaration with an additional first argument representing the object this (which is always x). The body of the lam declaration ignores every local computation and translates FJf method invocations into lam function invocations and get operations into dependency pairs.

If the code of the main is

new C()!m1( new C(), new C() )
then the evaluation of the program will lock objects as depicted below and no deadlock will appear. Since in this case the lam program is not recursive, our analysis technique is straightforward: just evaluate completely the lam program and verify whether the final lam is circularity-free. In fact, we get:

Ix,y,z, m1(x, y, z) -→ Ix,y,z, (x, y) m2(y, z) -→ Ix,y,z, (x, y) (y, z) m3(z)

-→ Ix,y,z, (x, y) (y, z) 0 which has no circularity. On the contrary, if the code of main is

C x = new C(); x!m1( new C(), x )
then a deadlock will occur. In fact, in this case x = z and the thread executing y!m2(x) will block waiting for the result of x!m3(). In turn, this method will never be executed since the object x is locked by the initial invocation, as depicted below

object x method m1 object y method m2 method m3
This circularity is exactly what our analysis is able to catch. In this case, the main lam is m1(x, y, x) and the computation is Ix,y, m1(x, y, x) -→ Ix,y, (x, y) m2(y, x) -→ Ix,y, (x, y) (y, x) m3(x)

-→ Ix,y, (x, y) (y, x) 0 which has a final state with a circularity. and evaluate (new D)!m1(new D, new D). This evaluation is nondeterministic: it may yield a deadlock or not according to the scheduling of the threads. In particular, the execution terminates successfully if the lock of the object z is grabbed by z!m3() (inside m2) before the invocation of z!m2(y) (inside m1) obtains the lock. If, on the contrary, the lock on z is taken by the invocation of z!m2(y) inside m1, then a deadlock occurs. Let us analyze the program with our technique. The lam functions associated to the above methods are: m1(x, y, z) = (x, u) m4(u, y, z) ; m2(z, y) m2(y, z) , m2(x, y) = (x, y) m3(y) , m3(x) = 0 , m4(x, y, z) = m2(y, z) , In this case, the lam of m1 has shape T 1 ; T 2 because the corresponding code spawns two threads in sequence: the invocation of m2 after the termination of the invocation of m4. In turn, since the invocation of m4 spawns an asynchronous behavior (the asynchronous invocation of m2), then T 2 also contains an invocation of m2 caused by m4. That is, the leftmost invocation of m2 in T 2 is due to the code of m1, the rightmost one is due to the invocation of m4.

As before, this lam program is not recursive and, in order to analyze it, we have to compute the final state, assuming m1(x, y, z) as the main function:

Ix,y,z, m1(x, y, z) -→ Ix,y,z ⊕ (x, y, z < u), (x, u) m4(u, y, z) ; m2(z, y) m2(y, z) -→ Ix,y,z ⊕ (x, y, z < u), (x, u) m2(y, z) ; m2(z, y) m2(y, z) -→ ... -→ Ix,y,z ⊕ (x, y, z < u), (x, u) (y, z) ; (z, y) (y, z)
thus manifesting a circularity.

The cooperative factorial function. Let us extend the language of Section 2.1 with the primitive type int, the arithmetic operations and the conditional expression. The meanings of these features are standard. Then consider the following class Maths where the method fact(n) computes the factorial of the of the argument (when positive) by performing a recursive invocation on a newly created object. The evaluation produces a finite chain of newly created threads waiting for the termination of the next thread on a new object.

class Maths { int fact(int n) { return if (n==0) then 1 ; else n*((new Maths)!fact(n-1).get) ; } }

The evaluations of fact(n) never yield a deadlock, since no circular dependency can be constructed. This may be verified by translating the program into the lam formalism fact(x) = (x, y) fact(y), fact(

(the integer parameter is abstracted away, and the method shows only the parameter x representing the object this) and evaluating fact(x) till the saturated state, as discussed in Section 3. We notice that the conditional expression is translated into a lam by gathering the dependencies of the two branches, a standard technique in static analysis (in this case, the dependencies of the then-branch are empty).

A complex recursive pattern. As an example of recursive program, consider the following FJf class:

class R { R m1(R y, R z){ return y!m1(z,new R()).get ; z } }
The method m1 is a recursive method (of the same kind of the foregoing factorial function) that invokes m1 on its first argument with the second argument that is a new object. It does not generate any circularity when invoked with different arguments. However, several concurrent instances of its may produce a circular dependency. For instance, consider the main expression containg two invocations of m1 with the swapped arguments: R x = new R() ; R y = new R() ; R z = new R() ; x!m1(y,z); x!m1(z,y) (we are using local variables; these may be easily encoded in our calculus as arguments of additional auxiliary methods). The associated lam program is m1(x, y, z) = (x, y) m1(y, z, w) , m1(x, y, z) m1(x, z, y) which is linear. Our theory guarantees that, unfolding six times the two invocations of m1, it is possible to establish the circularity-freeness of the program. This means that, in order to get the saturated state we have a computation of length twelve. In particular, after four steps of the computation, we get Ix,y,z, m1(x, y, z) m1(x, z, y) -→ 2 V1, (x, y) (x, z) m1(y, z, u) m1(z, y, v)

-→ 2 V2, (x, y) (x, z) (y, z) (z, y) m1(z, u, u ′ ) m1(y, v, v ′ )
where V 1 = I x,y,z ⊕ (x, y, z < u) ⊕ (x, y, z < v) and

V 2 = V 1 ⊕ (y, z, u < u ′ ) ⊕ (y, z, v < v ′ ).
Since the last state has a circular dependency, we can stop the analysis here and deduce that the corresponding program deadlocks.

Another complex recursive pattern. and let new Rec()!m1(new Rec(), new Rec(), new Rec()) be the main expression. The lam function associated to the above methods are m1(x, y, z, w) = m2(z, y) m2(x, z) m2(w, z) m1(y, x, w, w ′ ) , m2(x, y) = (x, y) m3(y) , m3(x) = 0 , and our theory guarantees that the saturated state is obtained after four unfoldings of m1 (and completely unfolding the auxiliary method invocations m2 and m3). However, we notice that it is possible to obtain a state with a circularity after two unfoldings of m1(x, y, z) (which we assume as the main function):

Ix,y,z, m1(x, y, z) -→ * V, (z, y) (x, z) (w, z) m1(y, x, w) -→ * V ′ , (z, y) (x, z) (w, z) (w, x) (y, w) (w ′ , w) m1(x, y, w ′ ) where V = I x,y,z ⊕ (x, y, z < w) and V ′ = V ⊕ (y, x, w < w ′ ). In particular, the last state has circularity (z, y) (y, w) (w, z). However, if we perform a further unfolding of m1(x, y, w ′ ) we get the relation (z, y) (x, z) (w, z) (w, x) (y, w) (w ′ , w) (w ′ , y) (x, w ′ ) (w ′′ , w ′ ) that manifests the additional circularity (w, x) (x, w ′ ) (w ′ , w), which has no counterpart in the previous states (it cannot be mapped to a past circularity). That is, in order to have a complete account of circular dependencies, it is necessary to compute the lam till the saturated state.

The cooperative fibonacci function. A paradigmatic program that yields a nonlinear lam is the one computing fibonacci numbers. Consider to augment the above class Maths with the following method fib int fib(int n) { return if n==0 then 1 ; else if n==1 then 1 ; else new Maths()!fib(n-1).get + new Maths()!fib(n-2).get ; } } that implements the standard recursive algorithm of fibonacci. As in the factorial example, the above code is a cooperative solution: the recursive invocations are performed on new objects every time, so that the result is computed in parallel threads. The values of the spawned threads are retrieved by get operations, which corresponds to synchronization points. To analyze this program, we consider the associated lam: fib(x) = (x, y) (x, z) fib(y) fib(z), fib(x) (as before, the integer parameter is abstracted away and the method only carries the parameter x representing the object this). This lam program is not linear and, as discussed in Section 3, it is circularity-free.

Additional issues

Two relevant extensions of the language FJf are field assignment and the operation await. In this section we indicate the techniques we are developing for coping with them.

Fields and assignments. The update operation increases the difficulties of the deadlock analysis. In particular, a field of an object that is modified by concurrent threads has a nondeterminate final value. This, in turn, may cause unpredictable behaviors due to the scheduling of the threads (see also Section 4). In [START_REF] Giachino | Lock analysis for an asynchronous object calculus[END_REF] there is a preliminary study of this issue. For instance, consider the two classes E and F below (as before, we are using local variables). The evaluation of this expression yields a thread (spawned inside m1) that modifies the field f of x (because of the invocation x!n1). This thread is concurrent with the invocation x!n2(). If the execution flow is such that the invocation f.m2() (inside x!n2()) is evaluated before the assignment, then the execution will terminate (with a new object stored in f), otherwise f will contain a reference to this and the computation deadlocks.

In order to take into account the updates, we extend lams with the possibility of specifying sets of objects, which model the possible values that may be stored in fields. In particular, the lam program associated to the above code is

m1(x, y, Y) = n1(y, Y), m2(x) = 0, n1(z, Z) = 0, n2(z, Z) = m2(Z) (z, Z), m1(x, y, {x, y}) n2(y, {y, z})
where Y is the set of possible values the fields of the object y may be assigned. Analogously for Z with respect to z. Notice that the first arguments of m1 and m2 are of class E, therefore they do not have any fields. This is why they do not have any associated set. The body of n2 has the pair (z, Z), which represent the set of pairs {(z, z ′ ) | z ′ ∈ Z}. The execution of the lam program will be the following:

Ix,y,z, m1(x, y, {x, y}) n2(y, {y, z}) -→ Ix,y,z, n1(y, {x, y}) n2(y, {y, z}) -→ Ix,y,z, n2(y, {y, z}) -→ Ix,y,z, (y, {y, z}) m2({y, z}) -→ Ix,y,z, (y, {y, z}) -→ Ix,y,z, (y, y) (y, z)

The final state has a circular dependency, i.e. (y, y).

Await and livelocks.

A further synchronization operator of ABS is await (see [START_REF] Johnsen | ABS: A core language for abstract behavioral specification[END_REF][START_REF] Giachino | Deadlock and livelock analysis in concurrent objects with futures[END_REF] for its formal semantics and examples). The operation await suspends the current thread, by releasing the lock on its own object, while waiting for a thread termination. Later on, the thread competes again for grabbing the lock and, when acquired, it tries again for the result. If it is available, the computation proceeds, otherwise the lock is released again and so on. With this semantics, a circular dependency does not correspond to a blocking situation, but to a situation where one or more threads are caught in an infinite loop of getting and releasing the lock. This phenomenon is usually called a livelock.

In the presence of livelocks, a circular dependency may not necessarily be a bad situation. Let us discuss this issue. A dependency pair (x, y) in a livelock analysis means that some thread on x is waiting -not busy-waiting -for the result of some thread on y. Under this meaning, the term (x, y) (y, x), which is signaled as an incorrect state by our technique, may be safe because the involved threads can be different. In fact, in this case, since the threads do not busy-wait on the objects x and y, the computation terminates successfully.

In order to distinguish between the two types of circularities, we extend the names used in lams with thread names. In this extension -lams with two sorts of names, thread names have a "type", which is the (object) name -, the livelocks are those manifested by terms such as (t, t ′ ) (t ′ , t); while terms as (t, t ′ ) (t ′ , t ′′ ), even if t and t ′′ have the same object type, are painless.

Conclusion

This paper surveys a technique for the static analysis of deadlocks. This technique associates abstract descriptions, called lams, to programs and then evalu-ates such descriptions to catch circular dependencies. The technique does not use any pre-defined partial order of resources and does account for dynamic resource creation. We stuck to a popularizing exposition; therefore the technical details have been omitted and several examples should help in clarifying the difficult points.

We are currently experiencing our technique in the hats European project (www.hats-project.eu) on large programs written in an object-oriented language with futures [START_REF] Giachino | Deadlock analysis in practice[END_REF]. An inference systems for deriving lams [START_REF] Giachino | Deadlock and livelock analysis in concurrent objects with futures[END_REF], for a subset of this language, has been defined and additional annotations allow us to instruct the inference system when structured data types and iterations occur.

Lams have been used in the first place for detecting the so-called resource allocation deadlocks, as encountered in e.g. operating systems. However, our technique seems also adequate for deadlocks due to process synchronizations, as those in process calculi [START_REF] Milner | A calculus of mobile processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Kobayashi | Type systems for concurrent programs[END_REF]. A thorough comparison with these works is scheduled for the next future.

An interesting direction of research is the application of our algorithm for static analysis to verify properties different than deadlocks. This might boil down to devise languages different than lams and to different definitions of saturated states.

  FJf syntax uses four disjoint infinite sets of names: class names, ranged over by A, B, C, • • •, field names, ranged over by f, g, • • •, method names, ranged over by m, n, • • •, and variables, ranged over by x, y, • • •. The special name this is assumed to belong to the set of variables. The notation C is a shorthand for C 1 ; • • • ;C n and similarly for the other names. Sequences of pairs are abbreviated as C 1 f 1 ; • • • ;C n f n with C f. The syntactic categories of class declarations CL, method declarations M, expressions e, and types T are defined as follows CL ::= class C extends C { T f ; M} M ::= T m ( T x){ return e ; } e ::= x | e.f | e!m( e) | new C( e) | e; e | e.get T ::= C | Fut(T)

  always returns sequences of pairwise different parallels of pairs (i.e. sets of pairwise different relations). Definition 1. A lam L has a circularity if

  Getting started: a simple deadlocked program. Consider the following class C with three synchronized methods m1, m2, and m3: class C { C m1( C y, C z ) { return y!m2(z).get ; } C m2( C z ){ return z!m3( ).get ; } C m3( ) { return new C( ) ; } }

Scheduler's choices

  and deadlocks. Deadlocks that are usually difficult to detect are those caused by scheduler's choices. Consider the following class D class D { D m1( D y, D z ) { return new D()!m4(y,z).get ; z!m2(y) ; new D() ; } D m2( D y ){ return y!m3( ).get ; } D m3( ) { return new D( ) ; } D m4( D y, D z ) { return y!m2(z) ; new D() ; } }

  F y ) { return y!n1 ; new E() ; } E m2( ) { return new E( ); } } class F { E f; E n1( ) { return f = this ; } E n2( ) { return f!m2().get ; } } and the main expression F x = new F( new E() ) ; new E()!m1(x) ; x!n2() ;

  The following FJf class manifest another issue about saturation. Let

	class Rec {
	Rec m1(Rec y, Rec z, Rec w){
	return z!m2(y) ; this!m2(z) ; w!m2(z) ; y!m1(this,w,new Rec()) ; z ;
	}
	Rec m2(Rec y){ return y!m3().get; }
	Rec m3() { new Rec(); }
	}