Cosimo Laneve
email: cosimo.laneve@unibo.it.

A lightweight deadlock analysis for programs with threads and reentrant locks

Keywords:

Deadlock analysis of multi-threaded programs with reentrant locks is complex because these programs may have infinitely many states. We define a simple calculus featuring recursion, threads and synchronizations that guarantee exclusive access to objects. We detect deadlocks by associating an abstract model to programs -the extended lam model -and we define an algorithm for verifying that a problematic object dependency (e.g. a circularity) between threads will not be manifested. The analysis is lightweight because the deadlock detection problem is fully reduced to the corresponding one in lams (without using other models). In fact, the technique is intended to be an effective tool for the deadlock analysis of programming languages by defining ad-hoc extraction processes. We demonstrate this effectivity by applying our analysis to a core calculus featuring shared objects, threads and Java-like synchronization primitives. We also discuss a prototype verifier, called JaDA, that covers several features of Java and deliver initial assessments of the tool.

Introduction

Threads and locks are a common model of concurrent programming that is nowadays widely used by the mainstream programming languages (Java, C#. C++, Objective C, etc.). In these languages, deadlocks are flaws that occur when two or more threads are blocked because each one is attempting to acquire an object's lock held by another one. As an example, consider the following method setTable(C x,C y,int n) = (new C z)( if (n=0) then sync(y){ sync(x){ 0 } } else fork{ sync(x){ sync(z){ 0 } } } z.setTable(z,y,n-1) )

where new C z creates a new object of class C, fork{P } Q creates a new thread whose body is P and runs it in parallel with the continuation Q , and sync(x){ P } is the operation locking the object x, performing P , and releasing x when P terminates. The method setTable creates a table of n + 1 threads -the philosophers -each one sharing an objectthe fork -with the nearby philosopher. Every philosopher, except one, grabs the fork on his left -the first argument -and on his right -the second argument -in this order and then releases them. The exceptional case is the then-branch (n=0) where the grabbing strategy is opposite. It is well-known that, when the method is invoked with x.setTable(x,x,n), no deadlock will ever occur because at least one philosopher has a strategy that is different from the other ones. On the contrary, if we change the then-branch into sync(this){ sync(y){ 0 } } a deadlock may occur because philosophers' strategies are all symmetric. It is worth to notice that x.setTable(x,x,0) is deadlock-free because it just locks twice the object x, which is admitted in the model with threads and locks -a thread may acquire a same lock several times (lock-reentrancy).

In order to ensure termination, current analyzers [START_REF] Boyapati | Ownership types for safe programming: preventing data races and deadlocks[END_REF][START_REF] Flanagan | A type and effect system for atomicity[END_REF][START_REF] Abadi | Types for safe locking: static race detection for Java[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Suenaga | Type-based deadlock-freedom verification for non-block-structured lock primitives and mutable references[END_REF][START_REF] Vasco | Type inference for deadlock detection in a multithreaded polymorphic typed assembly language[END_REF] use finite approximate models representing the dependencies between object names. The corresponding algorithms usually return false positives with input x.setTable(x,x,n) because they are not powerful enough to manage structures that are not statically bounded.

In [START_REF] Giachino | Deadlock analysis of unbounded process networks[END_REF][START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF] we solved this problem for value-passing CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF] and pi-calculus [START_REF] Milner | A calculus of mobile processes[END_REF]. In that case, the technique used two formal models: Petri Nets [START_REF] Reisig | Petri Nets: An Introduction[END_REF] and deadLock Analysis Models -lams [START_REF] Giachino | Deadlock detection in linear recursive programs[END_REF]. The former ones are a well-known model of concurrent and distributed systems; the latter ones are basic recursive models that collect dependencies and features recursion and dynamic name creation. In the pi-calculus analyzer, Petri Nets were used to verify the consistency of the communication protocol of every channel, while lams were used for guaranteeing the correctness of the dependencies between different channels. The analysis algorithm of [START_REF] Giachino | Deadlock analysis of unbounded process networks[END_REF][START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF] required a tool for verifying the reachability of Petri Nets that model channels' behaviors (which has exponential computational complexity with respect to the size of the net [START_REF] Neil | Complexity of some problems in Petri nets[END_REF]) and a tool for analyzing lams (which has exponential computational complexity with respect to the number of arguments of functions).

In this paper we demonstrate that it is possible to define a deadlock analyzer for programs with threads and (reentrant) locks by only using an extension of lams. For example, the lam function corresponding to setTable is2 setTable(t, x, y) = (ν s, z) (y, x) t + ((x, z) s & setTable(t, z, y)) .

The term (y, x) t , called dependency, indicates that the thread t, which owns the lock of y, is going to grab the lock of x. The operation "+" and "&" are disjunction and conjunctions of dependencies, respectively. The index t of (y, x) t was missing in [START_REF] Giachino | Deadlock detection in linear recursive programs[END_REF][START_REF] Giachino | Deadlock analysis of unbounded process networks[END_REF][START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF]; it has been necessary for modeling reentrant locks. In particular, (x, x) is a circularity in the standard lam model, whilst (x, x) t is not a circularity in the extended lam model because t can acquire x twice. Therefore, setTable(t, x, x) manifests a circularity in the model of [START_REF] Giachino | Deadlock detection in linear recursive programs[END_REF][START_REF] Giachino | Deadlock analysis of unbounded process networks[END_REF][START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF] and it does not in the extended model. A circularity in the extended model is (y, x) t &(x, y) s , which denotes that two different threads are attempting to acquire two objects in different order. This lam gives (x, x) , which represents a circularity.

Because of the foregoing extension, the algorithm for detecting circularities in extended lams is different than the one in [START_REF] Giachino | Deadlock analysis of unbounded process networks[END_REF][START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF]. In particular, while there is a decision algorithm for the presence/absence of circularities in standard lams, in Section 2 we define an algorithm that verifies the absence and is imprecise in some cases (it may return that a lam will manifest a circularity while it will not be the case -a false positive).

We also define a simple language of concurrent programs featuring recursion, threads, shared objects and synchronization primitives inspired to those of Java. (The foregoing method setTable is a term of our calculus.) The syntax, semantics, and examples of the calculus are in Section 3. Section 4 reports a type system that associates lams to processes. For example, the type system returns the lam function setTable for the method setTable. As a byproduct of the type system and the algorithm for detecting circularities in lams, our technique can detect deadlocks of programs like setTable.

In order to deliver initial assessments of our technique, we have extended the basic language in Section 3 to cover several features of Java. In Section 5 we focus on inheritance that allows classes to be defined as sub-classes of other ones by deriving the corresponding method (and field) definitions and eventually redefine them (method overriding). In a language with inheritance, locating a method definition is performed at run-time through a mechanism called dynamic dispatch that uses the actual value of the called object. Since our technique extracts lams from programs at static time, the precise modeling of dynamic dispatch is not feasible. We therefore over-approximate the type by returning the lam functions of every possible overridden method in the subclasses. In Section 6 we also analyze assignments and recursive data-types.

The analysis of other features of Java can be found in Garcia's PhD thesis [START_REF] Garcia | Static Analysis of Concurrent Programs Based on Behavioral Type Systems[END_REF]. This analysis does not address coordination primitives (methods wait, notify and notifyAll) and Java concurrent libraries, such as java.util.concurrent, -see Section 9 for a discussion.

Our theoretical developments are complemented by an analyzer prototype called JaDA [START_REF] Garcia | JaDA -the Java deadlock analyser[END_REF][START_REF] Laneve | Deadlock detection of Java bytecode[END_REF]. While the type system in this paper simply checks static information, JaDA infers the behavioral types from the code. Inference is important in practice because it lightens the analysis but checking is crucial for type safety. Section 7 reports on initial assessments of the tool.

We discuss a few weaknesses of the techniques in Section 8 and we point to related works and give some concluding remarks in Section 9. The paper also includes an appendix that contains the demonstration of type safety for the language of Section 3 and the type system of Section 4. This paper collects two conference contributions about deadlock analysis of Java-like languages: [START_REF] Laneve | A lightweight deadlock analysis for programs with threads and reentrant locks[END_REF] and [START_REF] Laneve | Deadlock detection of Java bytecode[END_REF]. Here we extend [START_REF] Laneve | A lightweight deadlock analysis for programs with threads and reentrant locks[END_REF] with the proof of type soundness and with the discussion on the extensions of the basic calculus in Section 3.

With respect to [START_REF] Laneve | Deadlock detection of Java bytecode[END_REF], we adopt a different presentation style. We discuss typing rules for the Java language, while in the conference paper the focus was on Java bytecode.

Lams and the algorithm for detecting circularities

This section extends the theory developed in [START_REF] Giachino | Deadlock analysis of unbounded process networks[END_REF][START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF] to cover thread reentrancy. In particular, the new definitions are those of transitive closure and Definition 2.3. Theorem 2.8 is new.

Preliminaries. We use an infinite set A of names, ranged over by x, y, t, s,

• • • . A relation on A , denoted R, R , • • • , is an element of P(A × A × (A ∪ { , •}))
= t then (x, z) ∈ R + ; 2. if (x, y) t , (y, z) t ∈ R + , t ∈ A ∪ { }, then (x, z) t ∈ R + ; 3. if (x, y) • , (y, z) • ∈ R + , (x, y) • = (y, z) • , then (x, z) ∈ R + . -{R 1 , • • • , R m } {R 1 , • • • , R n } if and only if, for all R i , there is R j such that 1. if (x, y) t ∈ R i , t ∈ A , then (x, y) t ∈ R j + 2. if (x, y) ∈ R i then either (x, y) ∈ R j + or there is t ∈ A such that (x, y) t ∈ R j + ; 3. if (x, y) • ∈ R i then either (x, y) • ∈ R j + or there is t ∈ A such that (x, y) t ∈ R j + . -{R 1 , • • • , R m }&{R 1 , • • • , R n } def = {R i ∪ R j | 1 ≤ i ≤ m and 1 ≤ j ≤ n}. We use R, R , • • • to range over {R 1 , • • • , R m }, which are elements of P(P(A × A × (A ∪ { , •}))).
The names and • are managed in an ad-hoc way in the transitive closure R + and in the relation . In particular, if (x, y) t and (y, z) t belong to a relation and t = t , the dependency obtained by transitivity, e.g. (x, z) , records that it has been produced by a contribution of two different threads -this is important for separating circularities, e.g. (x, x) , from lock reentrancy, e.g. (x, x) t . The name • copes with another issue: it allows us to abstract away thread names that are created inside methods. For this reason the transitive dependency of (x, y) • and (y, z) • is (x, z) because the threads producing (x, y) • and (y, z) • might be different. The meaning of R R is that R is "more precise" with respect to pairs (x, y): if this pair is indexed with either or • in some R ∈ R then it may be indexed by a t (t = ) in the corresponding (transitive closure) relation of R . For example { {(x, y) • , (y, z) • , (x, z) } } { {(x, y) t , (y, z) t } } and { {(x, x) • } } { {(x, x) t , (x, x) t } }. Definition 2.1. A relation R has a circularity if (x, x) ∈ R + for some x. A set of relations R has a circularity if there is R ∈ R that has a circularity.

Lams. In our technique, dependencies are expressed by means of lams [START_REF] Giachino | Deadlock detection in linear recursive programs[END_REF], noted , whose syntax is

::= 0 | (x, y) t | (ν x) | & | + | f(x)
The term 0 is the empty type; (x, y) t specifies a dependency between the name x and the name y that has been created by (the thread) t. The operation (ν x) creates a new name x whose scope is the type ; the operations & and + define the conjunction and disjunction of the dependencies in and , respectively. The operators + and & are associative and commutative; the operator & has precedence over +. The term f(x) defines the invocation of f with arguments x.

The argument sequence x has always at least two elements in our case: the first element is the thread that performed the invocation, the second element is the last object whose lock has been acquired by it.

A lam program is a pair L , , where L is a finite set of function definitions f(x) = f with f being the body of f, and is the main lam. We always assume that (i) x is a sequence of pairwise different names and (ii) f = (ν z) f where f has no ν-binder. The constraint (ii) also applies to and, whenever we write L , (ν x)

we always mean that has no ν-binder.

f(x) = (ν z) f ∈ L z are fresh L[f(u)] -→ L[ f { z / z }{ u / x }]
with initial state . We write -→ * for the reflexive and transitive closure of -→.

For example, if f(t, x) = (ν s, z) ((x, z) t &f(s, z)) then f(t, x) -→ (x, z ) t &f(t , z ), where t and z are fresh names. By continuing the evaluation of f(t, x), the reader may observe that (i) every invocation creates new fresh names and (ii) the evaluation does not terminate because f is recursive. These two points imply that a lam model may have infinite states, which makes the analysis nontrivial.

Flattening and circularities. Lams represent elements of the set P(P(A × A × (A ∪ { , •}))). This property is displayed by the following flattening function. Let L be a set of function definitions and let I(•), called flattening, be a function on lams that (1) maps function name f defined in L to elements of P(P(A × A × (A ∪ { , •}))) and ( 2) is defined on lams as follows Let L be the set

I(0) = {∅}, I((x, y) t ) = {{(x, y) t }}, I( & ) = I( )&I( ), I( + ) = I( ) ∪ I( ), I((ν x) ) = I( ){ x / x } with x fresh, I(f(u)) = I(f){ u / x } (
f i (x i ) = (ν z i ) i , with i ∈ 1..n. Let A = i∈1.
.n x i and be a special name that does not occur in L , . We use the domain

P(P((A ∪ { }) × (A ∪ { }) × (A ∪ { , •}))), ⊆ which is a finite lattice [5]. Definition 2.3. Let f i (x i ) = (ν z i ) i , with i ∈ 1.
.n, be the function definitions in L . The family of flattening functions

I (k) L : {f 1 , • • • , f n } → P(P((A ∪ { }) × (A ∪ { }) × (A ∪ { , •}))
) is defined as follows (f i ) and, in particular, the function proj:

I (0) L (f i ) = {∅} I (k+1) L (f i ) = {proj z i x i (R + ) | R ∈ I (k) L ( i )} where proj z x (R) def = {(u, v) t | (u, v) t ∈ R and u, v ∈ x and t ∈ x ∪ { }} ∪ {( , ) | (u, u) ∈ R and u / ∈ x} ∪ {(u, v) • | (u, v) t ∈ R and u, v ∈ x and t ∈ z}
• first of all, notice that proj applies to the transitive closures of relations, which may have names in A, z i , , • and ;

• the transitive closure operation is crucial because a circularity may follow with the key contribution of fresh names. For instance the model of f

(x) = (ν t, t , z) (x, z) t & (z, x) t is {{(x, x) }}; the model of g() = (ν t, t , x, y) (x, y) t & (y, x) t is { {( , )
} } (this is the reason why we use the name );

• every dependency (u, v) t ∈ proj z x (R) is such that u, v ∈ x, except for ( , ) . For example, if f (x, y) = (ν s, z) ((x, y) s & (x, z) s ) then, if we invoke f (u, v) we obtain (u, v) t & (u, z ) t ,
where t and z are fresh object names. This lam may be simplified because, being z fresh and unknown elsewhere, the dependency (u, z ) t will never be involved in a circularity. For example, if we have

= (v, u) t & f (u, v) then we may safely reason on -simplified (u, v) t & (u, v) t .
For this reason we drop the dependencies containing fresh names after their contribution to the transitive closure has been computed;

• the same argument does not apply to names used as threads. For example, in the above -simplified lam we cannot drop (u, v) t because t is fresh. In fact, the context (v, u) t & (u, v) t gives a circularity. Therefore, dependencies whose thread names are fresh must be handled in a different way. We take a simple solution: these dependencies all have • as thread name. That is, we assume that they are all generated by the contribution of different threads. For example,

g (x, y) = (ν t) (x, y) t . Then, I (1) L (g ) = { {(x, y) • } }.
Example 2.4. The flattening functions of setTable are

I (0) L (setTable) = {∅} I (1) L (setTable) = { {(y, x) t } }
As another example, consider the function g(x, y, z) = (ν t, u) (x, y) t & g(y, z, u). Then:

I (0) L (g) = {∅} I (1) L (g) = { {(x, y) • } } I (2) L (g) = { {(x, y) • , (y, z) • , (x, z) } } Proposition 2.5. Let f(x) = (ν z) f ∈ L . 1. For every k, I (k) L (f) ∈ P(P((x ∪ { }) × (x ∪ { }) × (x ∪ { , •}))).

For every k, I

(k)

L (f) I (k+1) L (f).
Proof.

(1) follows by definition. As regards (2), we observe that I( ) is monotonic on I . That is, if I and I are two flattening functions such that, for every f, I(f) I (f) then it is possible to demonstrate by a standard structural induction that I( ) I ( ). An induction on k gives

I (k) L (f) I (k+1) L (f). 2
Since, for every k, I

L (f i ) ranges over a finite lattice, by the fixpoint theory [START_REF] Davey | Introduction to Lattices and Order[END_REF], there exists m such that

I (m) L is a fixpoint, namely I (m) L ≈ I (m+1) L
where ≈ is the equivalence relation induced by . In the following, we let I L , called the interpretation function (of a lam), be the least fixpoint

I (m) L . In Example 2.4, I (1)
L is the fixpoint of setTable and

I (2)
L is the fixpoint of g . Proposition 2.6. Let L be a lam context, be a lam with no ν binder, and I(•) be a flattening. Then we have:

I(L[ ]) has a circularity if and only if I(L[R]) has a circularity for

some R ∈ I( ). 2. Let f(x) = (ν z) f ∈ L and R ∈ I( f { z / z }) with z fresh. If I(L[R{ u / x }]) has a circularity then I(L[(proj z x (R + )){ u / x }]) has a circularity.
Proof. Property 1 follows from the definitions. To see 2, we use a straightforward induction on L. We analyze the basic case L = [ ]: the general case follows by induction. Let R ∈ I( f { z / z }) such that R{ u / x } has a circularity. There are two cases:

• (v, v) ∈ R + . By definition of proj z x (R + ) either (v, v) ∈ proj z x (R + ), when v / ∈ z , or ( , ) ∈ proj z x (R + ), otherwise.
In this case the statement 2 follows immediately.

• (v, v) ∈ R{ u / x } + . By definition of transitive closure R{ u / x } + = (R + ){ u / x }. Then there is a dependency (x 1 , x 2 ) ∈ R + such that (x 1 , x 2 ) { u / x } = (v, v) . By definition of proj, (x 1 , x 2 ) ∈ proj z x (R + ). Therefore proj z x (R + ){ u / x } has also a circularity. 2 Lemma 2.7. Let L = {f 1 (x 1 ) = (ν z 1 ) 1 , • • • , f n (x n ) = (ν z n ) n } and let L[f i 1 (u 1 )] • • • [f i m (u m )] -→ m L[ i 1 { z 1 / z i1 }{ u 1 / x i1 }] • • • [ i m { z m / z im }{ u m / x im }] where L[•] • • • [•] is a multiple context without function invocations. If I (k) L (L[ i 1 { z 1 / z i1 }{ u 1 / x i1 }] • • • [ i m { z m / z im }{ u m / x im }]) has a circularity then I (k+1) L (L[f i 1 (u 1 )] • • • [f i m (u m )]) has also a circularity.
Proof. To show the implication suppose that

I (k) L (L[ i 1 { z 1 / z i1 }{ u 1 / x i1 }] • • • [ i m { z m / z im }{ u m / x im }])
has a circularity. By repeated applications of Proposition 2.6(1), there exists R j ∈ I (k)

L ( i 1 { z j / z i j }{ u j / x i j }) with 1 ≤ j ≤ m such that I (k) L (L[R 1 ] • • • [R m ]
) has a circularity. It is easy to verify that every R j may be written as R j { u j / x i j }, for some R j . By repeated application of Proposition 2.6(2), we have that

I (k) L (L[proj z i 1 x i 1 (R 1 + ){ u 1 / x 1 }] • • • [proj z im x im (R m + ){ u m / x m }])
has a circularity. Since, for every 1 ≤ j ≤ m, proj

z i j x i j (R j + ){ u 1 / x 1 } ∈ I (k+1) L (f i j (u j ))
and since L has no function invocation, we derive that

I (k+1) L (L[f i 1 (u 1 )] • • • [f i m (u m )]
) has also a circularity. 2

Unlike [START_REF] Giachino | Deadlock analysis of unbounded process networks[END_REF][START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF], Lemma 2.7 is strict in our case, for every k. For example, consider

h(x, y, z) = (ν t) (x, y) t & (y, z) t .
Then, when k ≥ 1,

I (k) L (h) = { {(x, y) • , (y, z) • } }. Notice that I (k) L (h(x, y, x)) = { {(x, y) • , (y, x) • } },
I (0)
L ( ) I L ( ). Therefore I L ( ) has also a circularity. Then, by Lemma 2.7, since I L is the fixpoint interpretation function, I L ( ) has also a circularity. 2

Our algorithm for verifying that a lam will never manifest a circularity consists of computing I L (f), for every f, and I L ( ), where is the main lam. As discussed in this section, I L (f) uses a saturation technique on names based on a powerset construction. Hence it has a computational complexity that is exponential on the number of names. We remind that the names we consider are the arguments of lam functions (that corresponds to methods' arguments), which are usually not so many. In fact, this algorithm is quite efficient in practice [START_REF] Garcia | JaDA -the Java deadlock analyser[END_REF].

The language and its semantics

In this section we define a simple programming model of concurrent object-oriented languages featuring threads and object synchronizations (the reader may easily recognize the basic operations of thread creation and synchronization used in Java and C#). We give a description of how deadlock may be identified, and discuss few examples. The following section contains the type system that associates lams to the programs.

Our model has two disjoint countable sets of names: there are integer and object names, ranged over by x, y, z, t, s, • • • , and method names, ranged over by m, n,

• • • . A program is a tuple C 1 D 1 , • • • , C n D n , P
where D i are finite sets of method name definitions m(T x) = P m , with T x being the formal parameters x and their types T and P m being the body of m; we assume that method name definitions have an implicit formal parameter C i this which refers to the carrier. The process P is the main process. Types T are either integers int or C i .

The syntax of processes P and expressions e is defined below

P ::= 0 | (new C x) P | fork{P } P | if e then P else P | x.m(e) | sync(x){ P } e ::= x | v | e op e
A process can be the inert process 0, or a restriction (new C x) P that behaves like P except that the external environment cannot access to the object x of class C, or the spawn fork{Q } P of a new thread Q by a process P , or a conditional if e then P else Q that evaluates e and behaves either like P or like Q depending on whether the value is = 0 (true) or = 0 (false), or an invocation x.m(e) of the method m with carrier x and actual parameters e. The last process is sync(x){ P } that executes P with exclusive access to x.

An expression e can be a name x, an integer value v, or a generic binary operation on integers op , where op ranges over a set including the usual operators like +, ≤, etc. Integer expressions without names (constant expressions) may be evaluated to an integer value (the definition of the evaluation of constant expressions is omitted). Let JeK be the evaluation of an expression e: JeK is undefined when e is an integer expression that contains integer names; JxK = x when x is a non-integer name.

To define the semantics of the above language, we use states, ranged over by P , that are multisets of threads P • σ , where σ is a (possibly empty) sequence of object names representing the locks that the process P has already grabbed (in order, from the left to right). When P terminates, the locks of σ must be all released. The thread P • σ is reentrant on x when σ contains at least two occurrences of x. We usually write states as

P 1 • σ 1 | • • • | P n • σ n
and sometime shorten them into i∈1..n P i • σ i . We write x ∈ P if P contains σ and x occurs in σ . Since states are multiset, we identify those that are equal up-to associativity and commutativity of | . Empty sequences σ are written ε. In order to ease the definitions, we will use few notational conventions

• Object names are partitioned into infinitely countable disjoint sets that are addressed by class names. The notation z = fresh(C) states that z is a fresh name in the set C (e.g. z does not occur in the state). • We make explicit that z is a name in the set C by writing z ∈ C.

= C 1 D 1 , • • • , C n D n , P
is a transition system where the initial state is P • ε, and the transition relation -→ is the least one closed under the rules:

(Zero) 0 • σ -→ (NewO) z = fresh(C) (new C x) P • σ | P -→ P { z / x } • σ | P (NewT) fork{P } Q • σ -→ P • ε | Q • σ (IfT) [[e]] = 0 if e then P else Q • σ -→ P • σ (IfF) [[e]] = 0 if e then P else Q • σ -→ Q • σ (Call) JeK = v x ∈ C C.m(T z) = P ∈ x.m(e) • σ -→ P { x, v / this, z } • σ (Sync) x / ∈ P sync(x){ P } • σ | P -→ P • σ • x | P
We often omit the subscript of -→ when it is clear from the context. We write -→ * for the reflexive and transitive closure of -→.

We discuss the relevant rules. Rule (Zero) models termination: every lock taken by the thread is released and the thread disappears from the state (which is a multiset). This is because, according to the syntax, there is no continuation in this case. Rule (NewO) creates a new object of class C: we simply take a name that does not occur in the state, replace the bound name with the fresh one, and remove the binder. We observe that the renaming only applies to P : being x new, it cannot have been already locked (σ is not in the scope of the renaming). Rule (NewT) spawns a new thread that has an empty sequence of locks (because it has not performed any synchronization so far). Rule (Call) dispatches the invocation to the right method definition and executes the method body once the formal parameters have been replaced by the actual ones. Rule (Sync) models synchronizations. A thread may lock x provided it is not already locked by another thread in the state -premise x / ∈ P . We observe that x may occur in σ , that is a thread may lock x several times (thread reentrancy).

Our basic programming model does not retain the explicit instruction for sequential composition, e.g. P ; Q . However, this operation may be easily encoded using synchronizations:

(new C x) sync(x){ fork{sync(x){ Q }} P }
That is, we sequentialize P and Q by letting P to acquire the lock of a new object x before spawning Q . In turn Q will begin after the termination of P because the lock of x is grabbed by it. According to our rules, we have

(new C x) sync(x){ fork{sync(x){ Q }} P } • σ -→ sync(x ){ fork{sync(x ){ Q }} P } • σ -→ fork{sync(x ){ Q }} P • σ • x -→ P • σ • x | sync(x ){ Q } • ε
and, by rule (Sync), Q cannot start as long as x is locked by P .

Definition 3.2 (Deadlock-freedom). A program C 1 D 1 , • • • , C n D n , P is deadlock-free if the following condition holds:
whenever P • ε -→ * P and P = sync(x){ Q } • σ | P then there exists P such that P -→ P .

Example 3.3. We select three processes and discuss their behaviors, highlighting whether they deadlock or not:

• fork{sync(x){ sync( y){ 0 } }} sync(x){ sync( y){ 0 } }. This process spawns a thread that acquire the locks of x and y in the same order of the main thread: no deadlock will ever occur.

• On the contrary, the process fork{sync(y){ sync(x){ 0 } }} sync(x){ sync( y){ 0 } } spawns a thread acquiring the locks in reverse order. This is a computation giving a deadlock:

fork{sync(y){ sync(x){ 0 } }} sync(x){ sync( y){ 0 } } • ε -→ sync( y){ sync(x){ 0 } } • ε | sync(x){ sync( y){ 0 } } • ε -→ sync(x){ 0 } • y | sync(x){ sync( y){ 0 } } • ε -→ sync(x){ 0 } • y | sync( y){ 0 } • x • The following method m(C x, C y, int n) = if (n = 0) then fork{sync(y){ sync(x){ 0 } }} sync( y){ 0 } else sync(x){ this.m(x, y, n -1) }
performs n-nested synchronizations on this (reentrancy) and then spawns a thread acquiring the locks y and x in this order, while the main thread acquire the lock y. This method deadlocks for every n ≥ 1, however it never deadlocks when n ≤ 0.

Static semantics

Environments, ranged over by , contain the types of objects, e.g. x : C, the type of integer variables e.g. x : int, and the types of method names, e.g. C.m : [T]. Without loss of generality, in method definitions of Fig. 1 we order formal parameters of methods: those of type class are in front of those of type integer. Therefore (C.m) will have shape [C , int].

Let dom( ) be the domain of and let

• , x:T, when x / ∈ dom( ) ( , x:T)( y) def = T if y = x (x) otherwise • + , when x ∈ dom( ) ∩ dom( ) implies (x) = (x): ( + )(x) def = ⎧ ⎨ ⎩ (x) if x ∈ dom( ) (x) if x ∈ dom( )
( e i : T i ) i∈1.
.n e 1 ,. . ., e n : T 1 ,. . ., T n Programs: Let also

(T-Prog) = {C.m : [C , int] | C.m(C x, int y) = P C.m ∈ } , this : C, x : C , y : int, t : Thread, u : Obj; u t P C.m : C.m C.m(C x,int y)=P C.m ∈ L = C.m(C x,int y)=P C.m ∈ {f C.m (t, z, this, x) = C.m } , t : Thread, u : Obj; u t .main : : L ,
(x 1 • • • x n • x n+1 ) t def = ⎧ ⎨ ⎩ 0 i f n = 0 (x 1 • • • x n ) t if x n+1 ∈ {x 1 , • • • , x n } (x 1 • • • x n ) t &(x n , x n+1 ) t otherwise
The static semantics has three judgments:

• e : T -the expression e has type T in ;

• ; σ t P : -the thread P with name t has lam in ; σ . We assume that the class of t is a predefined class Thread and contains the bindings t : Thread; • : L , the program has lam program L , in .

In addition to Thread, the static semantics also uses another predefined class, called Obj. The objects of this class are used for typing new threads (cf. rule (T-Par) in Fig. 1; this expedient allows us to have a simpler rule for typing function invocations.

Few notational conventions are in order. When = C 1 D 1 , • • • , C n D n , P , we let .main = P and we write C i .m(T x) = P C i .m ∈ whenever D i contains m(T x) = P C i .m .

The type system is defined in Fig. 1. A few key rules are discussed. Rule (T-Zero) types the process 0 in a thread t that has locked the objects in σ in (inverse) order. The lam is the conjunction of dependencies in σ with thread t -cf. notation (σ ) t . Rule (T-Sync) types the critical section P with a sequence of locks extended with x. Rule (T-Par) types a parallel composition of processes by collecting the lams of the components. We use a new name t for the spawned thread and a new name u for the object that is already grabbed by t . This object has class Obj. (According to our convention, when we write , t : Thread, u : Obj we assume that t , u / ∈ dom( ).) Rule (T-Call) types a method name invocation in terms of a (lam) function invocation and constrains the types of actual arguments to match with the types of formal parameters in the method declaration. The arguments of the lam function invocation are extended with the thread name of the caller and the name of the last object locked by it (and not yet released). In addition we also conjunct the dependencies (σ • x) t created by the caller because the method invocation run in a thread that holds those locks. This rule must be read in conjunction with (T-Prog). (T-Prog) associates a lam function to every method -c.f. its second and third premises. The body of the lam function is defined by typing the body of the method in the hypothetical context where the thread only owns one lock, which is given as argument of the lam function. Of course, this is not the general case: a method may be invoked by a thread that grabs many locks. To address the general case we record the last object synchronized by the thread and build the dependencies of the invocation starting from it. It turns out that taking these dependencies in conjunction with those of the caller -see rule (T-Call) -does suffice for keeping track of the overall dependencies (see Proposition A.1). Because of this technicality, we require that every thread, even those that are just created, locks at least one object.

P = sync(y){ sync(x){ 0 } } Q = fork{sync(x){ sync(z){ 0 } }} z.setTable(z, y, n -1) Then , z : C; u • y • x t 0 : 1 1 = (u, y) t &( y, x) t , z : C; u • y t sync(x){ 0 } : 1 , z : C; u t P : 1 ( * ) , z : C; u t Q : 2 , z : C; u t if n = 0 then P else Q : 1 + 2 ; u t (new C z) (if n = 0 then P else Q ) : (ν z) ( 1 + 2 )
where ( * ) are the two proof trees which has two additional arguments with respect to the one in the Introduction: u and this. In fact, these arguments, as well as u , do not play any role in the analysis of circularities of setTable(t, u, this, x, y).

The following theorem states the soundness of our type system. The technical details of the proof are reported in the Appendix.

Theorem 4.2. Let C 1 D 1 , • • • , C n D n , P : L , . If L , has no circularity then C 1 D 1 , • • • , C n D n , P is deadlock-free.
I (0) L (setTable) = {∅} I (1) L (setTable) = { {(u, y) t , (y, x) t , (u, x) t } } I (2) L (setTable) = { {(u, y) t , (y, x) t , (u, x) t }, {(u, y) t } } . Since I (2) L = I L , we are reduced to compute I (2) L (setTable(t, u, x, x, x)). That is { {(u, y) t , (y, x) t , (u, x) t }, {(u, y) t } }{ x / y } = { {(u, x) t , (x, x) t }, {(u, x) t } }
which has no circularity, therefore the process x.setTable(x, x, n) is deadlock-free.

It is interesting to verify whether the process x.setTableD(x, x, n) is deadlock-free, where setTableD is the method having philosophers with symmetric strategies:

setTableD(C x,C y,int n) = (new C z)( if (n=0) then sync(x){ sync(y){ 0 } } else fork { sync(x){ sync(z){ 0 } } } z.

setTableD(z,y,n-1) )

In this case I L (setTableD) = { {(u, x) t , (x, y) t , (u, y) t }, {(x, y) , (u, y) t } }. It is easy to verify that I L (setTableD(t, u, x, x, x)) has a circularity, therefore the process x.setTableD(x, x, n) may have (and actually has) a deadlock.

To conclude, we observe that the deadlock freedom property guaranteed by Theorem 4.2 is stronger than the one defined in Definition 3.2 that admits a subset of processes to deadlock provided that some other process progresses. In fact, as usual [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF], our type system guarantees that no subset of processes deadlocks.

The extension of inheritance

The basic language in Section 3 does not admit derivations of classes from other classes. As a consequence, when a method is invoked, it is possible to uniquely locate the method definition. This feature is expressed in the type system in Fig. 1 by the strict correspondence between types of arguments and types of formal parameters (e.g. the constraint u : C in the type rule (T-Call)). On the contrary, object-oriented programming languages admit subclasses, thereby allowing redefinitions of methods in the subclasses. In this context, locating a method definition is performed at run-time through a mechanism called dynamic dispatch that uses the actual value of the called object.

For example, let C be a class with a method foo that is overridden in the subclasses C 1 and C 2 . Then, consider a method with arguments x, y, z of types C, C, and int, respectively. If this snippet if z then x.foo( ) else y.foo( ) is part of its body and the method is invoked with objects of types C 1 and C 2 , the method foo of C 1 or of C 2 will be performed according to the value of z. Clearly, dispatching an invocation to a definition rather than another may change the overall result of the deadlock analysis.

In order to study the impact of inheritance on the deadlock analysis, we extend the language in Section 3 as follows. Let a program be a tuple

D 1 D 1 , • • • , D n D n , P
where every D i is as in Section 3 and D is a term of the following grammar

D ::= C | C extends C
This extension carries a subtyping relation <: that is reflexive, transitive and contains C <: C if C extends C is in the program. Processes are extended with a more flexible object creation operation:

P ::= • • • | (new C 1 , • • • , C m x) P
meaning that the type of x may be one of C 1 , • • • , C m (it is non-deterministic) and it is intended that there is C such that C i <: C for every C i . This apparently exotic operation corresponds to the pattern

C x ; if e 1 x = new C 1 () ; else if e 2 x = new C 2 () ; • • • else x = new C m () ;
that we cannot use because our basic language does not feature assignments (see Section 6).

The static semantics of the foregoing extensions uses (finite) sets of object names {C 1 , • • • , C m } such that there is a C with C i <: C for every C i . Let C , C , • • • range over these sets. Let also environments bind object names to sets C . The typing rules become (+ 0≤i≤n i is an abbreviation for

1 + • • • + n ): (T-Subt) C [extends C ]{• • • , m(C x, int y) = P , • • • } is in the program E <: C E <: C E.m : [E , int] (T-New-Inh)
, x:C ; σ t P :

t (new C x) P : (ν x) (T-Call-Inh) (z) = C u : C C.m : [C, int] C∈C ,C∈C e : int ; σ • x t z.m(u, e) : + C∈C ,C∈C f C.m[C] (t, x, z, u) &(σ • x) t
In the rule (T-Subt), the text in [ • • • ] is optional: the rule applies both to class and to subclass definitions. Our analyzer associates a lam function f C.m[C ] to every method m such that C.m : [C , int]. As in the system of Fig. 1, the body of this function is defined by the judgment (it is assumed that m(C x, int y) = P belongs to a class C):

, x : {C }, y : int, t : {Thread}, u : {Obj}; u t P :

(T-Call-Inh) is the critical rule. Since statically we do not know what method will be actually executed at runtime, we return the disjunctions of the lams of every possible method, in conjunction with the dependencies (σ • x) t created by the caller. We illustrate the point by discussing an example. In this case, the type of u may be either C1 or C2, therefore the method m that will be actually invoked will be either C1.m or C2.m. Therefore we may have a deadlock because the main thread locks x and then y, while the spawned thread C2.m locks y and then x. There is no deadlock if the type of u is C1.

By rule (T-Call-Inh) and (T-Par) we derive the following lam for main:

= ((u, x) t &(x, y) t ) & (ν t ) (((u, x) t &(x, y) t ) + ((u, y) t &( y, x) t ))
It is easy to verify that I ⊥ ( ) has a circularity.

The foregoing management of inheritance is generic. In several cases, it is possible to have a more specific solution using explicit typings. In particular, whenever the run-time types of objects are known, it is possible to attach the right type to method invocations and apply concrete type reasoning. JaDA uses this technique starting the analysis from the main program.

Other extensions

In order to deliver initial assessments of our technique, we have extended the language in Sections 3 and 5 to cover many features of Java. The resulting tool, called JaDA [START_REF] Garcia | JaDA -the Java deadlock analyser[END_REF][START_REF] Laneve | Deadlock detection of Java bytecode[END_REF], has been prototyped. Overall, the attitude we had in the development of JaDA was to stick to solutions that can be easily integrated with the type system of the core language (and possibly simple to implement). In many places, we might have taken more refined solutions (see, for instance, the following paragraph about recursive types), with the danger of further delaying the release of the tool because of issues that are orthogonal to our technique.

In this section we overview two relevant extensions -assignments and recursive data types -and discuss our solutions in JaDA; the details of other extensions (e.g. static members, exceptions, and arrays) can be found in Garcia's PhD thesis [START_REF] Garcia | Static Analysis of Concurrent Programs Based on Behavioral Type Systems[END_REF].

The comparison of JaDA with other deadlock analysis tools is reported in Section 7.

Assignments. In the language of Sections 3 and 5 it is not possible to store and retrieve values. These operations are usually achieved by admitting objects with fields and the operations of read and write of fields. E.g. the syntax of processes and expressions is extended as follows

P ::= • • • | f = e. P e ::= • • • | x.m(e)
(method invocations may return values). Assignments impact the type system in a significative way because field values change during the execution and these changes may be unpredictable because of concurrency. In addition, since fields may store other objects and may be method's arguments, it is possible to create aliases. Overall, tracing the state changes becomes quite hard. The type system of JaDA overcomes these issues by

• checking data races of parallel threads (for example, one thread reading an object and the other one writing on the object). In particular, the environment binds fields to annotations in {-, r, w}, withmeaning no access, r meaning read access, w meaning write (and possible read) access. The set {-, r, w} is a total order (-< r < w) and we use the operation of least upper-bound .

• analyzing aliases created by copying mechanisms. This is implemented by decoupling the connection between object names and values in the environment. E.g. we introduce object pointers, noted a, b, • • • (that include the pointer ) and we let the environment to bind object names to object pointers and object pointer to pairs

([f h 1 1 : a 1 , • • • , f h m m : a m ], C
), where h i are in {-, r, w} and a i may also be . The pointer represents a record with fields that are tagged w and with values .

In order to trace data races, we use a companion type system e P :

that stores in the type of accesses performed by P to fields of objects in (we assume that accesses in are all set to -; when this is not the case, we use the function ↑that rewrites accesses into -). The merge operation on environments, noted , returns an environment where fields have the least upper-bounds of accesses in and while values are set to when accesses are conflictual (e.g. either r-w or w-w). For instance, let

= a → ([f r : b, g -: b ], C ) = a → ([f w : c, g w : d], C ) then = a → ([f w : , g w : d],
C ), that is 1. the field f has access w because this is the least upper bound of the two accesses; additionally the resulting value of f is because we do not know whether the read access in will read b or c;

2. the field g has access w because does not accesses to it while writes it; additionally the resulting value of g is d because this is the value written by .

Updates are recorded by means of judgments that also return environments. Namely, we use ; σ t P : , , where is the environment updated by P . We also use the operation [ ] that returns the environment updated according to what is prescribed in . The typing rule for the spawn of new threads is

(T-Par-Eff)
↑e P : P ↑e P : P [ P P ]; σ t P : ,

[ P P ], u : Obj; u t P : , t fork{P } P : & (ν t ,u ) ,
We notice that P and P are verified in an environment that already record the possible data races (a priori, P might start after P or conversely). We also notice that the returned environment in the conclusion is the merge of the returned environments in the premises. The presence of assignments also impacts on lams. First of all, in order to model object values, arguments of lam functions may also be records. This extension is not problematic with respect to Theorem 2.8 because our records are finite trees with fixed structures (this is also the case when object have recursive types, see below). In addition, the special name influences the definition of R + in Section 2. In fact, this name, being a place holder for possible object names, may be replaced by every name when transitive closure is computed, thereby overapproximating the set R + with more dependencies (and circularities). For example, ( , a) t &(a, b) t is a circularity (because may be replaced by b), while ( , a) t &(a, b) t is not a circularity (because, in case, this may be a reentrant thread).

Recursive types. In JaDA, the analysis of objects with recursive types is over-approximated by using finite representations.

In particular, a record of a recursive type is built by unfolding the type (exactly) up to those nodes containing a name of a class already present in the tree. Nodes inside the tree have values that are object names, nodes in the leaves whose type Lists like the foregoing one are therefore abstracted by a single node. The analyzer replaces names indexed by $ with and uses the same approximation described in previous paragraph. In particular, if the types of r $ and of r $ are the same, a term like (r $ , a) t &(b, r $ ) t is a circularity because it corresponds to ( , a) t &(b, ) t .

JaDA and its assessment

Since JaDA covers many features of Java, it has been possible to deliver an initial assessment of it with respect to existing deadlock analysis tools. In particular, we have considered tools using different techniques: Chord for static analysis [START_REF] Naik | Effective static deadlock detection[END_REF], Sherlock for dynamic analysis [START_REF] Eslamimehr | Sherlock: scalable deadlock detection for concurrent programs[END_REF], and GoodLock for hybrid analysis [START_REF] Bensalem | Dynamic deadlock analysis of multi-threaded programs[END_REF]. We have also considered a commercial tool, ThreadSafe3 [START_REF] Atkey | Threadsafe: static analysis for Java concurrency[END_REF]. Out of these tools, we were able to install and effectively test only two of them -Chord and ThreadSafe -because the other twos have been discontinued; the results corresponding to GoodLock and Sherlock come from [START_REF] Eslamimehr | Sherlock: scalable deadlock detection for concurrent programs[END_REF]. We also had problems in testing Chord with some of the examples in the benchmarks, perhaps due to some misconfigurations, that we were not able to solve because Chord has been also discontinued.

The analyzed programs exhibit a variety of sharing patterns. The source of all benchmarks in Table 1 is available either at [START_REF] Eslamimehr | Sherlock: scalable deadlock detection for concurrent programs[END_REF][START_REF] Naik | Effective static deadlock detection[END_REF] or in the JaDA-deadlocks repository. 4 Since the current release of JaDA does not completely cover Java, in order to gain preliminary experience, we modified the Java libraries and the multithreaded server programs of RayTracer, MolDyn and MonteCarlo (labeled with "(*)" in the Table 1) and implemented them in our system. This required little programming overhead; in particular, we removed volatile variables, avoided the use of Runnable interfaces for creating threads, and reduced the invocations of native methods involved in I/O operations. For every program, we give the lines of code (LOC), the number #Threads of threads explicitly created (in the second and third block this number depends on the argument N). We also state whether the program under examination has a deadlock or not and the time in seconds (tm) each tool took to perform the analysis. The times for GoodLock and Sherlock were taken from the literature [START_REF] Eslamimehr | Sherlock: scalable deadlock detection for concurrent programs[END_REF].

Here are our remarks. The first block of programs belongs to a well known group used as benchmarks for several Java analysis tools; the second block corresponds to examples designed to test JaDA against complex deadlock scenarios. First of all, at least for the benchmark codes in Table 1, JaDA is the unique tool that never returns false negatives (in general, JaDA may return false positives). Chord and ThreadSafe are unsound because they return false negatives (see the second block). The execution time of the tools are similar (JaDA appears more efficient), except for GoodLock and Sherlock, which appear however much less precise (they return a lot of false positives). As regards the second block, we observe that JaDA returns few deadlocks, which do not depend from N. This is because our analysis is symbolic and does not consider numeric values (most of the deadlock are considered "to be similar").

We retain that the results of Table 1 are encouraging and solicit further programming efforts for covering Java features that have not been considered so far, as well as more elaborate comparisons. This is left for future work.

It is also worth to observe that JaDA actually addresses the Java bytecode (we compile Java programs into bytecode and analyze it). This means that JaDA also analyzes every programming language that is compiled into Java bytecode, such as Scala [START_REF] Odersky | An Overview of the Scala Programming Language[END_REF]. As regards Scala, to the best of our knowledge, JaDA is the first static deadlock analysis tool.

Remarks about the analysis technique

The deadlock analysis technique presented in this paper is lightweight because it is compact, intelligible and theoretically manageable. The technique is also very powerful because we can successfully verify processes like buildTable and its variant where every philosopher has a symmetric strategy. However, there are processes for which our technique of collecting dependencies is too rough (and we get false positives).

One example is

fork{sync(x){ sync(z){ sync( y){ 0 } } }} sync(x){ sync( y){ sync(z){ 0 } } } .
This process has two threads: the first one locks x and then z and y in order; the second one locks x and then grabs y and z in order. Since the two threads initially compete on the object x, they will be executed in sequence and no deadlock will ever occur. However, if we compute the dependencies, we obtain

(x • z • y) t & (x • y • z) s that is equal to ((x, z) t &(z, y) t ) & ((x, y) s &( y, z) s )
where the reader may easily recognize the circularity (z, y) t &( y, z) s . This inaccuracy follows by the fact that our technique does not record the dependencies between threads and their state (of locks) when the spawns occur: this is the price we pay to simplicity. In [START_REF] Garcia | JaDA -the Java deadlock analyser[END_REF] we overcome this issue by associating line codes to symbolic names and dependencies. Then, when a circularity is found, we can exhibit an abstract witness computation that, at least in the simple cases as the above one, can be used to manually verify whether the circularity is a false positive or not.

Another problematic process is m(C x, C y, int n) in Example 3.3. This process never deadlocks when n ≤ 0. However, since our technique drops integer values, it always return a circularity (this is a correct result when n > 0 and it is a false positive otherwise). To cope with these cases, it suffices to complement our analysis with standard techniques of data-flow analysis and abstract evaluation of expressions.

Related works and conclusions

We have defined a simple technique for detecting deadlocks in object-oriented programs. This technique uses an extension of the lam model in order to cope with reentrant locks, a standard feature of object-oriented programs. We have specified an algorithm for verifying the absence of circularities in extended lams and we have applied this model to a simple concurrent object-oriented calculus that is intended to be a minimal concurrent subset of Java. We demonstrate the effectivity of our analysis by applying it to Java. In particular, we discuss a prototype verifier, called JaDA, and deliver initial assessments that seem quite encouraging.

The lam model has been introduced and studied in [START_REF] Giachino | Deadlock detection in linear recursive programs[END_REF] for detecting deadlocks of an object-oriented language with futures (and no lock and lock reentrancy) [START_REF] Giachino | A framework for deadlock detection in core ABS[END_REF], but the extension discussed in this paper is new as well as the algorithm for the circularity of lams. We have prototyped this algorithm in JaDA, where we use it for the deadlock analysis of Java [START_REF] Garcia | JaDA -the Java deadlock analyser[END_REF].

As we discussed in the Introduction, the model has been also applied to process calculi [START_REF] Giachino | Deadlock analysis of unbounded process networks[END_REF][START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF].

Several techniques have been developed for the deadlock detection of concurrent object-oriented languages. The technique [START_REF] Atkey | Threadsafe: static analysis for Java concurrency[END_REF] uses a data-flow analysis that constructs an execution flow graph and searches for cycles within this graph. Some heuristics are used to remove likely false positives. No alias analysis to resolve object identity across method calls is attempted. This analysis is performed in [START_REF] Eslamimehr | Sherlock: scalable deadlock detection for concurrent programs[END_REF][START_REF] Naik | Effective static deadlock detection[END_REF], which can detect reentrance on restricted cases, such as when lock expressions concern local variables (the reentrance of formal parameters, as in buildTable(x,x,0) is not detected).

The technique in [START_REF] Bensalem | Dynamic deadlock analysis of multi-threaded programs[END_REF] and its refinement [START_REF] Eslamimehr | Sherlock: scalable deadlock detection for concurrent programs[END_REF] use a theory that is based on monitors. Therefore the technique is a runtime technique that tags each segment of the program reached by the execution flow and specifies the exact order of lock acquisitions. Thereafter, these segments are analyzed for detecting potential deadlocks that might occur because of different scheduler choices (than the current one). This kind of technique is partial because one might overlook sensible patterns of methods' arguments (cf. buildTable, for instance). A powerful static techniques that is based on abstract interpretation is SACO [START_REF] Flores-Montoya | May-happen-in-parallel based deadlock analysis for concurrent objects[END_REF]. SACO has been developed for ABS [START_REF] Broch Johnsen | ABS: a core language for abstract behavioral specification[END_REF], an object-oriented language with a concurrent model different from Java. A comparison between SACO and a tool using a technique similar to the one in this paper can be found in [START_REF] Giachino | A framework for deadlock detection in core ABS[END_REF].

Our future work includes the analysis of concurrent features of object-oriented calculi that have not been studied yet.

A relevant one is thread coordination, which is usually expressed by the methods wait and notify (and notifyAll). These methods modify the scheduling of processes: the thread executing wait(x) is suspended, and the corresponding lock on x is released; the thread executing notify(x) wakes up one thread suspended on x, which will attempt again to grab x. A simple deadlock in programs with wait and notify is when the wait operation is either mismatched or happens-after the matching notification. Initial steps toward the deadlock analysis of coordination primitives can be found in [START_REF] Laneve | Deadlock analysis of wait-notify coordination[END_REF], where we design a behavioral type system for coordination primitives. This system resorts to simple object protocols -called usages -to determine whether objects are used reliably, so as to guarantee deadlock freedom. In turn, this reliability is reduced to a reachability problem in a Petri net that, in the case of coordination primitives, have also inhibitor arcs. While the technique in [START_REF] Laneve | Deadlock analysis of wait-notify coordination[END_REF] seems complementary to our extended lam model, the actual integration must still be studied.

A research direction that is close to the above one is the analysis of concurrent libraries, such as java.util.concurrent. This issue has several cases, we discuss the most relevant ones. One case is when a library function can be implemented in Java (bytecode) using features that are already covered [START_REF] Garcia | Static Analysis of Concurrent Programs Based on Behavioral Type Systems[END_REF] or that can be covered by our analysis (e.g. coordination primitives). In this case, we derive the corresponding lam either in an automatic way or in a semi-automatic way, by providing the missing judgments, and use explicit typing in every place where the function is used. A second case is when a function is written in native code. In this case, we compute all the dependencies by parsing the code manually and type the function with the resulting lam (and again use explicit typing). Another case is when the function uses synchronization primitives that rely on conditional expressions, such as conditional await. In this case, a reasonable solution is integrating our technique with some axiomatic formalism using pre-and post-conditions. These axiomatic formalisms are also very powerful for tackling assignments and pointers (see Section 6), cf. separation logic [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF]. The study of this integration and the possible definition of an hybrid solution for the deadlock analysis of Java-like languages is matter of future research.

Further work will be also necessary for the development of JaDA: while the results of Table 1 are encouraging, they also solicit further programming efforts for covering Java features that have not been considered so far. This should allow us to address the benchmarks labeled (*) without any programming overhead and possibly other benchmarks as in [START_REF] Naik | Effective static deadlock detection[END_REF].

L

  is the function I ⊥ . Let us analyze the definition of I (k+1) L

•Definition 3 . 1 .

 31 If a program has a pair C D such that D contains a method m(T x) = P then we write C.m(T x) = P ∈ . The operational semantics of a program

Fig. 1 .

 1 Fig. 1. The type system (we assume a function name f C.m for every method name m of class C).

Example 4 . 1 .

 41 Let us show the typing of the method setTable in the Introduction. Let = C.setTable : [C, C, int], this : C, x : C, y : C, n : int, t : Thread, u : Obj

Example 4 . 3 .

 43 Let us verify whether the process x.setTable(x, x, n) is deadlock-free. The lam function associated by the type system is detailed in Example 4.1. The interpretation function I L (setTable) is computed as follows:

Example 5 . 1 .

 51 Consider the following program: C1 { m(C x, C y) = sync(x){ sync(y){ 0 } } } ; C2 extends C1 { m(C x, Cy) = sync(y){ sync(x){ 0 } } } ; new C x, C y, {C1,C2} u. fork{ u.m(x,y) } sync(x){ sync(y){ 0 } }

  , where P(•) is the standard powerset operator, • × • is the cartesian product, and , • / ∈ A are two special names. The elements of R, called dependencies, are denoted by (x, y) t , where t is called thread. The name indicates that the dependency is due to the contributions of two or more threads; • indicates that the dependency is due to a thread whose name is unknown. Let -R + be the least relation containing R and closed under the operations: 1. if (x, y) t , (y, z) t ∈ R + and t

  The function setTable in the Introduction is an example of a lam function.As usual L[ ] is the lam where the hole of L[ ] is replaced by . We remark that, according to the syntax, lam contexts have Since relations R are collections of dependencies, with an abuse of notation, we often use R and & (x,y) t ∈R (x, y) t interchangeably, allowing the context to disambiguate whether we mean a relation or a lam. For example, we will often writeL[R] meaning the lam L[& (x,y) t ∈R (x, y) t ].Similarly, when we write R{ y / x }, we may mean either the relation R where the occurrences of x in the dependencies have been replaced by y or the lam (& (x,y) t ∈R (x, y) t ){ y / x }.The operational semantics of a lam program L , (ν x) is a transition system where states are lams, the transition relation is the smallest transition relation induced by the following rule

	(Red)
	Let a lam context, noted L[ ], be a term derived by the following syntax:
	L[ ] ::= [ ]	|	&L[ ]	|	+ L[ ]

no ν-binder.

  where x are the formal parameters of f). I ⊥ be the map such that, for every f defined in L , I ⊥ (f) = {∅}. For example, let setTable be the function in the

	Let Introduction and let
	I(setTable) = {{(y, x) t }}	= setTable(t, x, y)&(x, y) s + (x, y) s .
	Then I( ) = {(y, x) t , (x, y) s }, {(x, y) s } , I ⊥ ( ) = {(x, y) s } .
	Definition 2.2. A lam has a circularity if I ⊥ ( ) has a circularity. A lam program L , (ν x) -→ * and has a circularity.	has a circularity if there is
	For example the above lam has a circularity because
	setTable(t, x, y)&(x, y) s + (x, y) s
	-→ ((y, x) t + (x, z) s &setTable(t, z, y))&(x, y) s + (x, y) s
	=
	and I ⊥ ( ) has a circularity.
	Fixpoint definition of the interpretation function. Our algorithm relies on the computation of lam functions' interpretation,
	which is done by a standard fixpoint technique.

  Obj; w t sync(x){ sync(z){ 0 } } : 2 (as an exercise, the reader may try to complete them). By rule (T-Par), we derive 2 = 2 &(ν t , u ) 2 . After completing the

	proof tree, one obtains the lam function
	setTable(t, u, this, x, y) =
	(ν z, t ,

• • • , z : C; u t z.setTable(z, y, n -1) : 2 and • • • , z : C, t : Thread, u : u ) (u, y) t &( y, x) t + (u , x) t &(x, z) t & setTable(t, u, x, z, y)

Table 1

 1 Comparison with different deadlock detection tools. The inner cells show the number of deadlocks detected by each tool. The output labeled "(*)" are related to modified versions of the original programs: see the text. not recursive are marked int (a primitive type value); leaves of a recursive type have values that are names subscribed by a $; the name corresponds to the nodes of the classes that are already present in the tree.For instance, if C is a class whose type is [val : Thread, next : C] (a list of threads) then, in correspondence of a new C instruction, we produce an environment r $ → [val : (a[ ], Thread), next : r $ ].

	Benchmarks	LOC, #Threads	Deadlock	Static		Hybrid	Dynamic	Commercial
				JaDA[tm]	Chord[tm]	GoodLock[tm]	Sherlock[tm]	ThreadSafe[tm]
	Sor	1274, 5	yes	1 [135s]	1 [210s]	7 [4s]	1 [39s]	4 [435s]
	RayTracer(*)	1292, 5	no	0 [155s]	0 [223s]	8 [2s]	2 [30s]	0 [502s]
	MolDyn (*)	1351, 5	no	0 [110s]	0 [191s]	6 [5s]	1 [49s]	0 [423s]
	MonteCarlo (*)	3619, 4	no	0 [231s]	0 [342s]	23 [5s]	2 [102s]	0 [821s]
	BuildNetworkN	40, N+1	yes	3 [8s]	0 [50s]			0 [50s]
	PhilosophersN	60, N+1	yes	3 [12s]	0 [51s]			0 [51s]
	ThreadArraysN	23, N+1	yes	1 [6s]	1 [40s]			1 [40s]
	ThreadArraysJoinsN	37, N+1	yes	1 [6s]	1 [41s]			0 [41s]

is

Actually, this is a simplified form of setTable. The lam function associated to setTable by the type system in Section 4 has two additional names that record the last name synchronized by the thread t and the carrier of the invocation.

http://www.contemplateltd .com /threadsafe.

https://github .com /abelunibo /Java -Deadlocks.

Acknowledgements

We thank Abel Garcia and Elena Giachino for the fruitful discussions and useful comments. In particular, Abel has been the main developer of JaDA. We also thank the anonymous referees for reading the paper carefully and for their many insightful comments and suggestions.

H2020-MSCA-RISE project ID 778233 "Behavioural Application Program Interfaces (BEHAPI)".

Appendix A. Proof of Theorem 4.2

We first need to extend the typing to states. Therefore we extend the type system in Fig. 1 with the following two rules:

(T-Thread) , t : Thread; σ t P :

Theorem 4.2 is a consequence of the following statements. The first two are obtained by a standard induction on the proof-tree of the judgment in the premise.

Proposition A.1. If ; x t P : and names in σ belong to dom( ) then there is such that ; σ • x t P : and I L ( )

Let { u / x } be defined as follows:

In the above definition, the topmost alternative applies before the other one. Therefore, for example, { x / x } = and { u, v / v, u } simply swaps the mappings of u and v, e.g.

Lemma A.2 (Substitution lemma). Let ; σ t P :

Similarly for e : T.

Lemma A.3 (Type preservation).

Let Proof. This follows by induction on the derivation of P • ε -→ * P , with case analysis on the last rule used, let it be P -→ P . The only non-trivial cases are (Sync) and (Call).

• Case (Sync): In this case, we have

where P = i∈1..n P i • σ i .

By the condition + P : and rules (T-State) and (T-Thread) we have + , t 0 : Thread; σ t 0 sync(x){ P } : 0 (A.1)

By using (T-Sync), from (A.1) we derive + , t 0 : Thread; σ • x t 0 P : 0 By (T-Thread) applied to the foregoing judgment we derive

Then, by applying (T-State) to this last judgment and (A.2), we have the required result (with = ).

We notice that m ≥ 1, otherwise rule (Sync) is possible. We also assume that, for every j, there is i j = j such that x j ∈ σ i j , otherwise (Sync) is also possible. We demonstrate a contradiction: I L ( ) must have a circularity.

By Lemma A. Consider the thread sync(x 0 ){ P 0 } • σ 0 and let x 0 ∈ σ 1 . For simplicity, assume that x 1 ∈ σ 0 .

By (T-Sync) and Proposition A.1, we have

. Since, according to the assumptions, (x 1 , x 0 ) t 0 ∈ I L ((σ 0 • x 0 ) t 0 ) and (x 0 , x 1 ) t 1 ∈ I L ((σ 1 • x 1 ) t 1 ), by definition of and of I L , we derive {(x 1 , x 0 ) t 0 , (x 0 , x 1 ) t 1 } I L ( ) (without loss of generality, we assuming t 0 and t 1 are replaced by identical names). Therefore I L ( ) contains a circularity and, by Theorem 2.8, I L ( ) must also have a circularity. This contradicts the hypothesis.

The general case, when the chain x 0 ∈ σ 1 , x 1 ∈ σ 2 , • • • , x h ∈ σ 0 , is similar. 2


To re ect on these ET-related subjects, a workshop is being organized for 7-9 October 2019 in Sydney, Australia, hosted by the University of New South Wales. It is intended to bring together specialists from di erent disciplines

Quarter 1 2019 the coupling to runo and the improved treatment of terrain heterogeneity are amongst the main challenges that SVAT modeling faces currently.

ET determination in numerical models is now facing the transitioning of weather models into convection permitting models that experience far more fast uctuations near the land surface than models in which convection is parameterized. A thorough review is needed of whether conventional concepts, such as the Monin-Obukhov Similarity eory (MOST), need to be improved for the next-generation models. Furthermore, models have to continuously improve their performances related to forecasting, data assimilation, trend analysis and climate projections.

Fourth Challenge: Estimating ET Remotely and at the Catchment Scale Satellite remote sensing ET estimates normally use the approaches of PM, Priestley-Taylor or the residual method and make a number of further assumptions to obtain H, G or R n , usually imposing the closure of the SEB. As mentioned above, parameterizing ET essentially as a function of solar radiation is also an option. e resulting values are compared with in situ ET estimates and calibrated accordingly.

To obtain the actual ET, normally a function is derived that varies between wet conditions-corresponding to ETp-and dry conditions when sensible heat ux prevails. Quantities like albedo, land surface temperature, surface roughness, soil moisture or some vegetation index are used. For heterogeneous vegetated surfaces, two-source energy balance (TSEB) approaches are common. ere exist also purely empirical algorithms trained by data, using, for example, neural networks.

Satellite estimates of ET are given at the scale of the pixel, and some applications require information at much higher resolutions, such as the hectometer and subdaily scale. is is leading to the development of downscaling methods for most satellites.

e scale issue has a speci c hydrological side, since hydrologists have traditionally analyzed the water budget at the catchment level, looking for closure at relatively large time scales (typically annual) and using the water balance as the basic methodology, with ET=precipitation-runo , assuming that storage changes might be neglected at annual time scales. However, hydrological numerical models require estimations of ET at a higher time-space resolution. Annual catchment water budgets may be used as a calibration or validation method for other approaches.

Introduction

One of the largest challenges facing environmental science is understanding future changes in the terrestrial water cycle and the subsequent impact on water resources. It has also been recognized by international organizations such as the World Climate Research Programme (WCRP) that human activities are playing a key role in modifying the continental water cycle, and therefore must be accounted for in projections. As highlighted by the WCRP Grand Challenge on "Water for the Food Baskets of the World," this issue is especially critical in bread basket regions where water resources are already limited, such as the Mediterranean basin. Understanding the processes that drive the hydrological cycle in this region is a key aim of the international HYdrological cycle in the Mediterranean Experiment (HyMeX). Climate projections from the Coupled Model Intercomparison Project phase 5 (CMIP5) predict that the Mediterranean region will be a so-called climate change "hot spot" during the twenty-rst century (Di enbaugh and Giorgi, 2012). However, semi-arid regions are also hot spots for biases in climate model variables, in particular land surface temperature (LST) and components of the surface energy balance. e Mediterranean basin is also characterized by highly heterogeneous land cover in terms of both natural and anthropized surfaces, largely driven by the limited availability of soil moisture and the nature of the precipitation. Since rainfall is essentially limited to winter and mountainous areas, human management of the natural river systems is required to provide water for crops and an ever-increasing population. Dams and extraction for irrigation modify the amount and timing of the water owing into the ocean. Irrigation is also known to signi cantly impact local atmospheric boundary layer (ABL) growth and structure, in addition to modifying near surface atmospheric conditions and increasing convective activity and clouds downwind of irrigated areas (e.g., [START_REF] Lawston | Impact of irrigation methods on land surface model spinup and initialization of WRF forecasts[END_REF]. It also greatly enhances the aforementioned land surface ( ux) heterogeneity. e current representation of anthropization in land surface models (LSMs) and therefore within global climate models (GCMs) is in a relatively nascent stage and urgently needs attention if we are to make accurate future projections of water resources and modi cations to the global water cycle

Land Surface Interactions with the Atmosphere over the Iberian Semi-Arid Environment (LIAISE)

Aaron Boone1 , Martin Best2 , Joan Cuxart3 , Jan Polcher4 , Pere Quintana5 , Joaquim Bellvert6 , Jennifer Brooke 2 , Guylaine Canut-Rocafort 1 and Jeremy Price 2

Quarter 1 2019 [START_REF] Harding | Anthropogenic In uences on the Global Water Cycle -Challenges for the GEWEX Community[END_REF]. e understanding of the impact of anthropization and its representation in models have been inhibited due to a lack of consistent and extensive observations. Here we present the plans for a project which will bring together ground-based and airborne measurements with modeling studies to improve our understanding of key natural and anthropogenic land processes and the subsequent feedbacks with the Mediterranean boundary layer and basin-scale hydrological cycle. ese observations will provide the opportunity for a number of community modeling experiments to move forward within GEWEX, helping to highlight gaps in our knowledge and identify current model de ciencies within land surface processes and land/atmosphere interactions.

Objectives and Science Questions e overall objective of this new activity, the Land surface Interactions with the Atmosphere over the Iberian Semi-arid Environment (LIAISE) project, is to improve our understanding of the impact of anthropization on the water cycle in terms of land-atmosphere-hydrology interactions, and the limitations of models to represent all aspects of the terrestrial water cycle in a semi-arid environment on the Iberian peninsula. ese include: i) the in uence of heterogeneity in land cover, including large irrigated areas, on area-averaged surface uxes of momentum, heat and moisture; ii) the consequence of land/ atmosphere interactions on local initiation of precipitation and boundary layer evolution; iii) the interactions between soil moisture, reservoirs and groundwater in both natural and irrigated regions; iv) the impact of changes in runo generation owing to anthropogenic e ects and its in uence on stream ow and reservoir storage; and v) the rami cations of human in uences on the future evolution of the water cycle. e main science questions can be summarized as:

1. What are the key natural and anthropogenic semi-arid surface processes that modulate or control in ltration and runo and govern turbulent uxes and their spatial heterogeneity?

2. How does anthropization impact boundary layer development, mesoscale circulations and potentially precipitation recycling over this region via feedbacks with the atmosphere?

3. What is the sustainability of ground water and reservoirs in the face of expanding agricultural and farming activities, especially in light of projected future warming and drying over this region?

e study domain for LIAISE is the Ebro basin in northeastern Spain, which is bound to the north by the Pyrenees and to the south by the Iberian System. Surface heterogeneity has grown due to the presence of human society, which has been altering the hydrological cycle and the landscape mainly through intense agricultural activity. e bulk of the basin runo is generated in the Pyrenees region, therefore infrastructure has been built to store and transport water from the mountainous areas to the agricultural elds. Most of the water used for agriculture, approximately 75%, is stored in reservoirs while the rest is maintained by the snow pack in the mountains.

is infrastructure has increased agricultural production and dramatically enlarged irrigated areas. In addition, agricultural elds in the headwater region have been abandoned, which leads to the expansion of forests, increasing evapotranspiration and decreasing river ow. erefore, the human component of the Ebro system cannot be avoided in any study that aims to understand the water cycle of a basin driven by meteorological and hydrological processes.

Strategy

e overall strategy for LIAISE is to take a multidisciplinary approach consisting of utilizing a suite of LSMs and hydrological and meteorological models that will employ remotely-sensed data or data assimilation strategies to prescribe input parameters and conduct evaluations. It can be summarized as follows:

1. A network of surface energy budget (SEB) observing stations will be installed within an approximately 10 km radius centered over the Urgell and Plà d'Urgell (Lleida) region of the Ebro basin. is area is selected since it encompasses several representative Mediterranean land cover types: irrigated cereal crops (corn, alfalfa), non-irrigated crops (wheat and other cereals), irrigated fruit trees (pear, apple), irrigated poplar plantations, natural grasses and baresoil, non-irrigated fruit trees (olives, almonds) and a lake used for irrigation. e land sites will also include soil moisture, temperature and vegetation monitoring data. is location will also allow us to bene t from the dense local meteorological station and radar data from the Spanish State Meteorological Agency (AEMET) and the Meteorological Service of Catalonia (SMC), along with an existing extensive observation site run by the Institute of Agrifood Research and Technology (IRTA), which includes weighing lysimeters in apple orchards. is network will enable us to evaluate the ability of LSMs to simulate uxes, especially evapotranspiration, over irrigated sites and to contrast the uxes with those from natural surfaces. ese sites will be maintained at least through entire growing season as part of the Intensive Observation Period (IOP) from early April through September 2020.

2. A 15-day Special Observation Period (SOP) is planned for mid July 2020, when contrasts between irrigated and natural surfaces are at their maximum. During the SOP, the SEB network will be complemented by extensive measurements of the lowest 4 km of the atmosphere using captive balloons, frequent radio-sounding releases, a UHF wind pro ler, lidars and up to ve ights by the French O ce of Aircraft Instrumented for Environmental Research (SAFIRE)/ATR42 aircraft. Measured atmospheric uxes and state variables will be used in conjunction with fully coupled, non-hydrostatic mesoscale models to study the impact of irrigation on the spatial variability of the ABL, the basin scale circulation and water budget and interactions between the irrigated and natural surfaces.

3. During the observational campaign, a 5-day period will be identi ed during the dry down of soil moisture in the spring. roughout this period, radiosondes will be launched at regular periods to add to atmospheric and ux pro les along a 50 m mast. ese data will be used to study the Quarter 1 2019 impact on interactions with the lower part of the boundary layer and the contrast in the surface uxes between the sites with natural dry down and the irrigated sites. A number of LSMs will be confronted with the data to help understand the limitations identi ed by [START_REF] Ukkola | Land surface models systematically overestimate the intensity, duration and magnitude of seasonal-scale droughts[END_REF].

4. Several LSM-hydrological modeling platforms will be tested over this region. e improved understanding and representation of evaporation from irrigated surfaces and their high resolution mapping by satellite data will be incorporated into models, which include new parameterizations for dams, rivers and canals, groundwater and reservoirs. Extensive discharge and dam release data will be obtained from the basin authority, the Hydrographic Confederation of the Ebro, through its real-time data portal, Sistema Automático de Información Hidrológica (SAIH). e focus will be on better understanding the exchanges between the di erent components of the water cycle.

5. Two measurements from the ATR42, high resolution land surface temperature and soil moisture estimates from the GLObal navigation satellite system Re ectometry Instrument (GLORI), will be used alongside state-of-the-art soil moisture products based on downscaled data such as that from the Soil Moisture and Ocean Salinity (SMOS) and Soil Moisture Active Passive (SMAP) missions. is data will be used for assimilation into LSMs and/or evaluation alongside in situ soil moisture observations from an existing Ebro Observatory network and measurements from irrigation-monitoring companies. e use of high-resolution remotely-sensed data from both satellites and aircraft along transects crossing swaths of irrigated and nonirrigated land with concomitant surface observations will permit a multi-scale modeling approach going from the parcel to the regional scale. An example of the detection of irrigated zones over this region using remote sensing is shown in Figure 1 (see cover).

6. e improved coupled LSM-hydrological model systems that include anthropogenic e ects will be used in conjunction with statistically downscaled new high-resolution regional climate data as part of the European-Mediterranean Coordinated Regional Climate Downscaling Experiment (EuroMed-CORDEX) project in order to provide estimates of the evolution of water resources over this region.

7. Field-scale actual and potential evapotranspiration will be evaluated using two-source energy balance (TSEB) models, which combine thermal observations from Sentinel-3 satellites and optical observations from Sentinel-2 satellites. e methodology for combining Sentinel-3 and Sentinel-2 data to obtain high-resolution ET is currently being researched in the Sentinels for Evapotranspiration (SEN-ET) project (http://esa-sen4et.org/).

Summary and Outcomes

To the authors' knowledge, this is the rst international project which will focus on the human impact on the water and energy cycle in a semi-arid environment for which the models are advanced enough to explicitly account for dams, irrigation methodologies, river ow, ground water interactions, vegetation phenology and atmospheric feedbacks. ese models are sophisticated enough to exploit remotely-sensed data as input or to use data assimilation strategies, but despite recent advances, water management is either quite simple or nonexistent in most LSMs. is was evident during the GEWEX Hydroclimatology Panel (GHP)-Global Land/Atmosphere System Study (GLASS) Workshop on Including Water Management in Large Scale Models [START_REF] Harding | Anthropogenic In uences on the Global Water Cycle -Challenges for the GEWEX Community[END_REF]. So we seek to improve the representation of anthropization in the LSM component of Earth system models. LIAISE addresses the GEWEX Science Questions and contributes to WCRP's Grand Challenges, notably how a warming world will a ect available fresh water resources globally, speci cally in the food basket regions, and how it will change human interactions with these resources and their value to society. Another key GEWEX Science Question addressed by LIAISE pertains to improving our understanding of the e ects and uncertainties of water and energy exchanges in the current and changing climate and how to convey this information to society. e improvement of the representation of anthropogenic e ects in models will form the foundation for water resource impact studies under future climate change. ese results will be communicated to water management services within the Ebro basin. A comprehensive database, consisting of surfacebased and aircraft measurements of surface and hydrological uxes and states and properties of the ABL, will be integrated into the Mediterranean Integrated STudies at Regional And Local Scales (MISTRALS)/HyMeX database, which can accessed upon request by interested researchers. is database of observations will form the basis for a number of international modeling experiments that will cut across many areas of interest to GEWEX, ranging from the ability of LSMs to capture soil moisture dry down, the representation of heterogeneity and how this interacts with the atmospheric boundary layer, the impacts of human in uence on land surface uxes and land/atmosphere interactions and the impact of human in uence of the terrestrial water cycle of semi-arid environments.

CNRM-Université de Toulouse, Météo-France/CNRS, France;

UKMO, Exeter, UK;

University of the Balearic Islands, Palma, Mallorca, Spain

; 4 Laboratoire de Météorologie Dynamique, CNRS/IPSL, Ecole Polytechnique,

France; 5 Observatori de l'

Ebre, Spain; 6 Efficient Use of Water in Agriculture Program, IRTA, Lleida, Spain


Quarter 1 2019 e kicko workshop for the "Impact of initialized land temperature and snowpack on sub-seasonal to seasonal prediction" (LS4P) Initiative and " ird Pole Experiment Multi-Model Intercomparison" (TPEMIP) Project was held just prior to 2018's annual American Geophysical Union meeting. Subseasonal to seasonal (S2S) prediction, especially the prediction of extreme climate events such as droughts and oods, is scienti cally challenging and has substantial societal impacts and economic consequences. Despite the substantial progress that has been achieved in recent decades, the prediction skill for precipitation anomalies in spring and summer months has remained stubbornly low.

e GEWEX/Global Atmospheric System Study (GASS) LS4P initiative put forward a new approach that complements sea surface temperature (SST), snow and soil moisture research by suggesting the e ect of land memory in terms of the land surface/subsurface temperature (LST/SUBT) on S2S prediction. Most land-atmosphere interaction studies have focused on the local e ect, while the possible remote effects of large-scale LST/SUBT anomalies in geographical areas upstream on S2S prediction have largely been ignored. e LS4P project intends to address the question of the impact of the initialization of large scale LST/SUBT and snow pack, including aerosols in snow, in climate models on the S2S prediction over di erent regions. East Asia has been selected as the focus area in the rst phase because of the presence of the high elevation Tibetan Plateau (TP) and largescale snow cover there, in addition to a signi cant amount of available observational data from the ird Pole Experiment (TPE). is provides an ideal geographical location for the rst phase experiment. Regional Earth system (multi-sphere) modeling for the ird Pole region and its impact on the adjacent regions at di erent scales is also one of TPEMIP's main focuses. Studies on the LST/SUBT e ect as well as aerosols in snow were presented and discussed in the workshop. After preliminary studies explored the relationship between spring LST/SUBT anomalies and the summer precipitation anomaly in downstream regions in North America and East Asia [START_REF] Xue | Spring land temperature anomalies in northwestern US and the summer drought over Southern Plains and adjacent areas[END_REF][START_REF] Xue | Spring land surface and subsurface temperature anomalies and subsequent downstream late spring-summer droughts/ oods in North America and East Asia[END_REF][START_REF] Diallo | Dynamical downscaling the impact of spring Western U.S. land surface temperature on the 2015 ood extremes at the Southern Great Plains: E ect of domain choice, dynamic cores and land surface parameterization[END_REF] e TPE and the ird Tibetan Plateau Atmospheric Scienti c Experiment (TIPEX-III) have conducted extensive and comprehensive measurements over the TP for decades and their activities were reported by Dr. Xin Li of the Institute of Tibetan Plateau Research and Dr. Ping Zhao of the Chinese Academy of Meteorological Sciences, respectively. TPE has four data centers and their four websites provide about 2,000 data sets covering glacier, permafrost, snow aerosol and near surface ux information, include data from a soil moisture and temperature network in the TP. TIPEX-III has established multiscale land-surface and planetary boundary layer (PBL) observation networks over the TP and a tropospheric radiosonde network over the western TP. Drs. Li and Zhao indicated that they will provide data services for LS4P and TPEMIP. Data availability and the TPE database for the storage of our projects' model outputs are two of the main reasons why we selected East Asia as the focus of the rst phase. In addition, satellite data applications for the TP area have been reported by Dr. Shunlin Liang of UMD. e workshop attendees decided to change the project acronym name from the initial designation of "ILSTSS2S" to the more concise "LS4P." e workshop participants also discussed future prospects of the LS4P plan. One major task is to demonstrate the potential of using LST/SUBT for S2S prediction, which will include the following: i) Earth system model (ESM) experiments for selected regions and seasons to test the LST/ SUBT e ect (the rst phase focuses on the TP LST/SUBT anomaly impact on surrounding Asian regions; in the second and third phase, ESMs will be used to identify Rocky Mountain and Andes Mountain LST/SUBT e ects, respectively); ii) Data analyses to show the relationship between T2m/LST and precipitation for di erent major mountains and to identify hot spots over the globe where LST has signi cant impacts [a Ti- Quarter 1 2019 betan Plateau Oscillation Index (TPO) will be proposed]; iii) e demonstration of regional climate model (RCM) dynamic downscaling e ects on S2S prediction; iv) e improvement of land model physics and the re ning of the land model LST/SUBT initialization strategy; v) e identi cation of the source of LST/SUBT anomalies and other mechanisms. Moreover, we will explore the role of snow and aerosols in snow with LST/SUBT in S2S prediction.

Remote Effects of High

Major activities for 2019 were also discussed.

1. A paper will be submitted to Geoscienti c Model Development to present the LS4P project early in the year.

2. We will accept model results for May T2m and June precipitation until May 31, 2019. e results will be for the year 2003 and for model climatology, if model climatology is available.

3. Most model results for the rst stage sensitivity experiment are expected to be done by about August 31, 2019.

A paper with multi-model results will be submitted to a journal early in 2020, and a special issue relevant research from each group will be prepared by that time.

4. An LS4P and TPEMIP regional modeling group workshop will be held in summer 2019 in Nanjing, China. Nanjing University will host this workshop and limited travel support will be available. e announcement will be distributed soon.

5. A Tibetan Plateau Oscillation Index (TPO) that suggests a global impact of TP LST/SUBT will be proposed and a paper will be submitted in summer 2019.

6. A session in the next American Geophysical Union (AGU) Fall Meeting or American Meteorological Society (AMS) Annual Meeting will be proposed.

e LS4P workshop information and relevant materials can be found at the UCLA website, https://ls4p.geog.ucla.edu, and on the GEWEX website at https://www.gewexevents.org/events/ ilstss2s-kicko -workshop-by-invitation-only/. e working group brings together scientists from several communities: satellite observations, radiative transfer and transport modeling, as well as small-scale process and climate modeling. 30 participants were hosted by the Sorbonne University in Paris for the 2018 UTCC PROES Workshop last October. During the two-day event, participants discussed observational analyses of mesoscale convective systems, water vapor and convective transport, process studies, climate variation and feedbacks, as well as parameterizations and model diagnostic studies.

On the rst day, results from complementary observations were presented, which gave an interesting perspective on synergetic studies. Transport studies and the possibility of diagnosing convective transport were also examined. Vertical velocity is an important variable in process and climate modeling and it requires observations to be evaluated. e proposed National Aeronautics and Space Administration (NASA) D-Train mission will provide valuable insight, if the project is selected. e second day featured exciting observational studies coupled with modeling on cloud feedbacks to di erent climate modes, and on the role of convection in the maintenance of tropical margins. e last part of the meeting was dedicated to climate model sensitivity studies. Presentations are available at the UTCC PROES website (https:// gewex-utcc-proes.aeris-data.fr/) and at the GEWEX website (https://www.gewexevents.org/events/utcc-proes-workshop/).

  California, Los Angeles, USA; 2 Centre National de Recherches Météorologiques, Météo-France/CNRS, France; 3 Institute of Tibetan Plateau Research, Chinese Academy of Sciences, China e workshop, held in Washington, D.C., USA with 36 participants from di erent institutions around the world and U.S. government agencies, was very productive with ve sessions and many inspiring presentations. GEWEX, GASS, TPE and the University of California, Los Angeles (UCLA) sponsored the event. TPE and the National Science Foundation (NSF) provided nancial support. Dr. Peter van Oevelen of the International GEWEX Project O ce, GASS Co-Chair Dr. Xubin Zeng, Dr. Ailikun of the TPE Project O ce and World Weather Research Programme (WWRP)/WCRP Subseasonal to Seasonal Prediction Project co-Chair Dr. Andrew Robinson expressed their support for the respective projects that they are leading for this workshop, and they also presented summaries of related research. Dr. Jennifer Saleem Arrigo of the U.S. Global Change Research Program presented a multi-federal agency e ort, the Climate, Water, and Energy Exchanges (CWEX) program. CWEX facilitates U.S. inter-agency research seeking to enhance predictive understanding of the water cycle and energy uxes of the changing Earth and global climate system, and to coordinate interactions with relevant e orts of WCRP, such as GEWEX. Dr. Vijay Tallapragada of the National Centers for Environmental Prediction (NCEP)/the National Oceanic and Atmospheric Administration (NOAA), Constantin Ardilouze of Meteo France, and Dr. Qi Tang of the Lawrence Livermore National Laboratory (LLNL)/U.S. Department of Energy (DOE) provided presentations or gave introductions on their respective institutions' relevant S2S research. Dr. Randy Koster of the Goddard Space Flight Center (GSFC)/National Aeronautics and Space Administration (NASA) introduced current soil moisture research and suggestions to the LS4P experimental design.

  Participants of the First Workshop on LS4P and TPEMIPMeeting/Workshop ReportsQuarter 1 2019 Agency (JMA), KIAPS/the Korea Meteorological Administration (KMA) and UCLA have provided preliminary LS4P results, which were presented at the workshop. ese models' results show a consistent relationship between their May 2003 2 meter temperature (T2m) bias over the TP and June 2003 precipitation bias in many parts of the world. For instance, the models with warm bias in May T2m in the TP also have a wet bias in June precipitation over the region to the south of the Yangtze River. e workshop also reported on the observed global June precipitation di erence between warm and cold TP spring T2m years. e results between these two (observation and model bias) are very consistent, as shown in Figure1for the eastern part of Asia, with similar results for many other parts of the world, suggesting a possible global remote e ect of TP spring LST/SUBT on summer precipitation in many areas. Dr. Hailan Wang of GSFC/NASA reported that their model bias over the TP a ects their model's simulation of the North American droughts.Some presentations explored the source of the spring LST/ SUBT anomalies. Dr. William Lau of the University of Maryland (UMD) showed that aerosols in TP snow may trigger large spring LST anomalies there, and Dr. Mike Burke of the University of Arizona also demonstrated the e ect of snow on T2m. Dr. Yang Zhang of Nanjing University suggested that the linkage between TP spring snow and LST anomaly may be related to the Arctic Oscillation.

Figure 1 .

 1 Figure 1. Comparisons of relationship between May T2m temperature in Tibetan Plateau and June precipitation from observed anomalies and model biases. Figure 1(a): Observed June precipitation difference between warm and cold years in May 2m Temperature (T2m) over the Tibetan Plateau. The anomaly year's selection is based on whether the year's May absolute T2m anomaly is larger than 0.5 standard deviation of May climatology. (b) Multi-model ensemble mean June precipitation bias when models have a warm bias over TP. Every model has a large T2m bias over the Tibetan Plateau area. For the model with negative T2m bias, the precipitation bias is multiplied by -1 to be included in the composite. The red circles highlight hot spots.

  , a number of studies have been carried out on this issue. Dr.

	Yuhei Takaya
	of the Meteorological Research Institute
	(MRI), Dr. Zhaohui Lin of the Institute
	of Atmospheric Physics (IAP) and Dr.
	Myung-Seo Koo of the Korea Institute of Atmospheric Predic-
	tion Systems (KIAPS) reported their initial tests on the LST/
	SUBT e ect on East Asian S2S prediction. Since the LS4P ini-
	tiative was approved by GEWEX in spring 2018, eight institu-
	tions including the Australian Bureau of Meteorology (BOM),
	Environment and Climate Change Canada, National Meteo-
	rological Center/the China Meteorological Administration,
	IAP/Chinese Academy of Sciences (CAS), the Indian Institute
	of Tropical Meteorology (IITM), MRI/Japan Meteorological

Process Evaluation Study on Upper Tropospheric Clouds and Convection: 2018 Highlights Paris, France 22-23 October 2018 Claudia Stubenrauch 1 and the GEWEX UTCC PROES Working Group

  1 Laboratoire de Météorologie Dynamique/Institut Pierre-Simon Laplace, Sorbonne University, Paris, France e GEWEX Upper Tropospheric Clouds and Convection Process Evaluation Study (UTCC PROES) working group was created in 2015 to ultimately advance our knowledge of the climate feedbacks of Upper Tropospheric (UT) clouds (GEWEX News, May 2017). As large-scale modeling is necessary to identify the most in uential feedback mechanisms, it is important that the relevant cloud processes are well represented in climate models. erefore, the UTCC PROES goals are to: • Understand the relation between convection, cirrus anvils and radiative heating, and • Develop observational diagnostic methods to probe processes that detrain UT clouds from convection.