Cosimo Laneve

Luca Padovani

Deadlock Analysis of Wait-Notify Coordination

Deadlock analysis of concurrent programs that contain coordination primitives (wait, notify and notifyAll) is notoriously challenging. Not only these primitives affect the scheduling of processes, but also notifications unmatched by a corresponding wait are silently lost. We design a behavioral type system for a core calculus featuring shared objects and Java-like coordination primitives. The type system is based on a simple language of object protocols -called usages -to determine whether objects are used reliably, so as to guarantee deadlock freedom.

Introduction

Locks and condition variables [START_REF] Hoare | Monitors: An operating system structuring concept[END_REF] are established mechanisms for process coordination that are found, in one form or another, in most programming languages. Java provides synchronized blocks for enforcing exclusive access to shared objects and wait, notify and notifyAll primitives to coordinate the threads using them: a thread performing a wait operation on an object releases the lock on that object and is suspended; a notify operation performed on an object awakens a thread suspended on it, if there is one; notifyAll is similar to notify, except that it awakens all suspended threads. Writing correct concurrent programs using these primitives is notoriously difficult. For example, a thread may block indefinitely if it attempts to lock an object that is permanently owned by a different thread or if it suspends waiting for a notification that is never sent.

We see an instance of non-trivial concurrent Java program in Figure 1, which models a coordination problem whereby a single consumer retrieves items from two producers. Each producer repeatedly generates and stores a new item into a buffer (line 5), notifies the consumer that the item is available (line 6) and waits until the consumer has received the item (line 7). At each iteration, the consumer waits for an item from each buffer (lines 12 and 15) and notifies the corresponding producer that the item has been processed (lines 14 and 17). The main thread of the program forks the producers (lines 25-26) and then runs as the consumer (line 27). In this example, the fact that producers and consumer use the two buffers in mutual exclusion is guaranteed by the syntactic structure of the code, since all accesses to x and y occur within synchronized blocks. However, understanding whether the three threads coordinate correctly so as to realize the desired continuous flow of information is not as obvious. This difficulty is largely due to the ephemeral nature of notifications: a notification sent to a shared object has an effect only if there is another thread waiting to be notified on that object. Otherwise, the notification is lost, with likely undesired implications. For example, suppose to change the program in Figure 1 so that the synchronized blocks now in the main method (lines 23-24) are moved into the consumer method, each protecting accesses to the corresponding buffer. This change would give producer and consumer a visually appealing symmetric structure, but the correctness of the program would be fatally compromised. Now a producer could lock x before the consumer and notify x at a time when the consumer is not yet waiting for a notification. Eventually, the consumer would block waiting for a notification on x that will never arrive, leading to a deadlock. The contribution of this paper is a behavioral type system ensuring that welltyped programs using shared objects and coordination primitives are deadlock free. The type system combines two features inspired by previous works on the static analysis of concurrent programs. First, we use a formulation of the typing rule for parallel compositions akin to that found in linear logic interpretations of session types [START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Caires | Linear logic propositions as session types[END_REF]. Unlike these works, where session endpoints are linear resources, here we apply the typing rule in a setting with shared (hence, nonlinear) objects. Second, we rely on behavioral types -called usages -to make sure that objects are used reliably, ruling out deadlocks due to missing notifications. Kobayashi [START_REF] Kobayashi | Type-based information flow analysis for the pi-calculus[END_REF] has already studied a type system based on usages for the deadlock analysis of pi-calculus processes. He shows how to reduce usage reliability to a reachability problem in a Petri net. As is, this reduction does not apply to our setting because the encoding of usages with coordination primitives requires the use of Petri nets with inhibitor arcs [START_REF] Busi | Analysis issues in petri nets with inhibitor arcs[END_REF].

The rest of the paper is structured as follows. Section 2 presents a core calculus of concurrent programs featuring threads, shared objects and coordination primitives. Section 3 defines types, usages and the key notion of reliability. Typing rules and properties of well-typed programs are given in Section 4. Section 5 discusses related work in more detail and Section 6 concludes. Because of space limitations, proofs and the handling of the notifyAll primitive are found in the appendix, which is not formally part of the submission.

Language Syntax and Semantics

We define a core language of concurrent programs featuring threads, shared objects and a minimal set of coordination primitives inspired to those of Java. We formalize our language as a process calculus comprising standard constructs (termination, conditional behavior, object creation, parallel composition, recursion) in which actions represent coordination primitives on objects. Instead of providing a synchronized construct to enforce mutually exclusive access to a shared object, we use explicit acquire and release operations on the object.

Formally, our calculus makes use of a countable set of variables and object names, ranged over by x, y, z, and a set of procedure names, ranged over by A. A program is a pair D, P , where D is a finite set of procedure definitions of the form A(x) = P A , with x and P A respectively being the formal parameters and the body of A. In a program D, P we say that P is the main process. Hereafter we write α for possibly empty, finite sequences α 1 , . . . , α n of various entities. The syntax of processes, expressions and actions is given in Table 1.

Expressions comprise integer literals, variables and object names, and an unspecified set of operators op such as +, ≤, and so forth. Expressions are evaluated by means of a total function • such that x = x.

The process done performs no action. The process π.P performs the action π and continues as P . The conditional process if e then P else Q behaves as P if e = 0 or else as Q. The process new x in P creates a new object x with scope P . The process fork{P }Q forks P and continues as Q. Finally, A(e) denotes the invocation of the process corresponding to A with actual parameters e.

An action is either acq(x), which acquires the lock on x, or rel(x), which releases the lock on x, or wait(x), meaning that the process unlocks x and suspends waiting for a notification, or notify(x) that notifies a process waiting on x, if there

Action π ::= acq(x) (acquire) | rel(x) (release) | wait(x) (wait) | wait(x, n) (waiting) † | notify(x) (notify)
is any. Objects are reentrant and can be locked multiple times by the same process. The prefix wait(x, n) is a runtime version of wait(x) that keeps track of the number of times (n) x has been locked before wait(x) was performed. User programs are not supposed to contain wait(x, n) prefixes. We write acq(x) n .P in place of acq(x) • • • acq(x).P where there are n subsequent acquisitions of x.

To define the operational semantics of a program we make use of an infinite set of process identifiers, ranged over by t and s, and states, which are pairs of the form H P made of a heap H and a process pool P. Heaps are finite maps from object names to pairs of the form t, n where t identifies the process that has locked x and n is the number of times x has been acquired. We allow t to be the distinguished name • and n to be 0 when x is unlocked. Process pools are finite maps from process identifiers to processes and represent the set of processes running at a given time. In the following we occasionally write H as {x i : t i , n i } i∈I and P as {t i : P i } i∈I . We also write H, H for the union of H and H when dom(H) ∩ dom(H ) = ∅. Similarly for P, P .

The operational semantics of a program D, P is determined by the transition relation -→ D defined in Table 2 applied to the initial state ∅ main : P . To reduce clutter, for each rule we only show those parts of the heap and of the process pool that are affected by the rule. For example, the verbose version of [r-done] is H t : done, P -→ D H P. Rules [r-acq-*] and [r-rel-*] model the acquisition and release of a lock. There are two versions of each rule to account for the fact that locks are reentrant and can be acquired multiple times. Rule [r-wait] models a process that unlocks an object x and suspends waiting for a notification on it. The number n of acquisitions is stored in the runtime prefix wait(x, n) so that, by the time the process is awoken by a notification, it re-acquires x the appropriate number of times. Rules [r-nfy-*] model notifications. The two rules differ depending on whether or not there exists a process that is waiting for such x : •, 0 t : acq(x).P -→D x : t, 1 t : P [r-acq -2] x : t, n t : acq(x).P -→D x : t, n + 1 t : P x : t, 1 t : rel(x).P -→D x : •, 0 t :

P [r-rel-2]
x : t, n + 2 t : rel(x).P -→D x : t, n + 1 t : P x : t, n t : wait(x).P -→D x : •, 0 t : wait(x, n).P [r-nfy-1] t : wait(x, n).P, s : notify(x).Q -→D t : acq(x) n .P, s : notification. In [r-nfy-1], one waiting process is awoken and guarded by the appropriate number of acquisitions. In [r-nfy-2], the side condition wait(x) / ∈ P means that P does not contain a process of the form t : wait(x, n).P , implying that no process is currently suspended waiting for a notification on x. In this case, the notification is simply lost. Rules [r-done], [r-if-*], [r-fork], [r-new] and [r-call] model terminated processes, conditional processes, forks, object creation and procedure calls as expected. Notice that [r-fork] has an implicit assumption stating that the name s of the process being created is fresh. This is because the composition P, P is well defined only provided that dom(P) ∩ dom(P ) = ∅. Similarly, rule [r-new] implicitly assumes that the object x being created is fresh.

Q [r-
We write =⇒ D for the reflexive, transitive closure of -→ D and H P -→ D if there exist no H and P such that H P -→ D H P . With this notation in place, we formalize the property that we aim to ensure with the type system: Definition 1 (deadlock-free program). We say that D, P is deadlock free if ∅ main : P =⇒ D H P -→ D implies H = {x i : •, 0} i∈I and P = ∅.

In words, a program is deadlock free if every maximal, finite computation starting from the initial state -in which the heap is empty and there is only one running process main : P -ends in a state in which all the objects in the heap are unlocked and all processes have terminated.

We conclude the section showing how to model the producer-consumer coordination program of Figure 1 in our calculus.

Example 1 (multiple-producers/single-consumer coordination). We model the program in Figure 1 by means of the following procedure definitions, which make use of two objects x and y to coordinate producer and consumer: Main = new x in new y in acq(x).acq(y).fork{P(x)} fork{P(y)} C(x, y) P(x) = acq(x).notify(x).wait(x).rel(x).P(x) C(x, y) = wait(x).notify(x).wait(y).notify(y).C(x, y) Table 3. Syntax of types and usages.

Type

T ::

= int | n • U Usage U ::= 0 | κ.U | U | V | U + V | α | µα.U Usage prefix κ ::= acq | rel | wait | waiting | notify
The overall structure of these procedures matches quite closely that of the correspondings methods in Figure 1. Let us discuss the differences. First of all, in the calculus we focus on coordination primitives. All other operations performed on objects -notably, Put and Get in Figure 1 -that do not affect coordination are not modeled explicitly. Second, we model while loops using recursion. Third, we model synchronized blocks in Figure 1 as (matching) pairs of acquire-release operations on objects. Notice that the consumer never performs explicit releases, for x and y are always released by wait(x) and wait(y). This corresponds to the fact that, in Figure 1, the whole code of the consumer runs within a block that synchronizes on x and y.

It is worth noting that, even after all the background noise that is present in Figure 1 has been removed, understanding whether the program deadlocks is not trivial. As anticipated in the introduction, the most critical aspect is determining whether x and y are always notified at a time when there is a process waiting to be awoken.

Types and Usages

Our type system rules out deadlocks using two orthogonal mechanisms. The first one makes sure that well-typed programs do not contain cycles of parallel processes linked by shared objects. This mechanism suffices to avoid circular waits, but does not guarantee that each process suspended on a wait operation is awoken by a notification. To rule out these situations, we also associate each shared object with a simple protocol description, called usage, that specifies the operations performed by processes on it. Then, we make sure that usages are reliable, namely that each wait operation is matched by (at least) one notification. The rest of this section is devoted to the formal definition of types, usages and related notions, leading to the formalization of reliability. The description of the actual typing rules is deferred to Section 4.

The syntax of types and usages is shown in Table 3. A type is either int, denoting an integer value, or an object type n•U where n is a natural number called counter and U is a usage. The counter indicates the number of times the object has been acquired. The usage describes the combined operations performed by processes on the object. The usage 0 describes an object on which no operations are performed. The usage κ.U describes an object that is used to perform the operation κ and then according to U . Usage prefixes acq, rel , wait, waiting and notify are in direct correspondence with the actions in Table 1. In particular, waiting is a "runtime version" of wait and describes an object on which the wait operation has been performed and is waiting to be notified. Usages of user programs are not supposed to contain the waiting prefix. The usage U | V describes an object that is used by concurrent processes according to U and V , whereas the usage U + V describes an object that is used either according to U or to V . Terms of the form µα.U and α are used to describe recursive usages.

We adopt standard conventions concerning (recursive) usages: we assume contractiveness, namely that, in a usage µα.U , the variable α occurring in U is always guarded by a usage prefix; we identify usages modulo (un)folding of recursions; we omit trailing 0's.

To illustrate usages before describing the typing rules, consider the process fork{acq(x).rel(x)} acq(y).acq(x).rel(x).rel(y) which uses two objects x and y. Notice that x is acquired by two concurrent subprocesses and that, in one case, this acquisition is nested within the acquisition and release of y. The operations performed on x are described by the usage acq.rel | acq.rel whereas those performed on y are described by the usage acq.rel .

In the following, we restrict our attention to well-formed usages in which every release corresponds to a former acquire and there can only be wait and notify operations in between them. In particular, we forbid usages that nest acquire operations. To accommodate reentrance, namely the possibility that the same object is aquired more than once, we use the information given by the counter. We keep the notion of well-formed usage informal since it is not essential in the following.

We now proceed to define a series of auxiliary notions related to types and usages and that play key roles in the type system and the proofs of its soundness. To begin with, we formalize a predicate on usages that allows us to identify those objects on which there is no process waiting for a notification: Definition 2 (wait-free usage). Let wf(•) be the least predicate on usages defined by the axioms and rules below:

wf(0) wf(acq.U ) wf(U ) wf(V ) wf(U | V ) wf(U + V )
Note that wf(U + V ) holds regardless of U and V because the usage U + V describes an object on which a process behaves according to either U or V , but the process has not committed to any such behavior yet. Hence, the process cannot be waiting for a notification on the object.

Next, we define a reduction relation describing the evolution of the type of an object as the object is used by processes. As we have anticipated earlier, the effect of operations depends on whether and how many times the object has been locked. For this reason, the reduction relation we are about to define concerns types and not just usages.

Definition 3 (type reduction).

Let ≡ be the least congruence on usages containing commutativity and associativity of | with identity 0, commutativity, associativity, and idempotency of +. The reduction relation T T is the least

0 • acq.U | V 1 • U | V [u-acq-2] n + 1 • U n + 2 • U [u-rel-1] 1 • rel .U | V 0 • U | V [u-rel-2] n + 2 • U n + 1 • U [u-wait] n + 1 • wait.U | V 0 • waiting.U | V [u-choice] n • (U + U ) | V n • U | V [u-nfy-1] n + 1 • waiting.U | notify.U | V n + 1 • acq.U | U | V [u-nfy-2] wf(V ) n + 1 • notify.U | V n + 1 • U | V [u-cong] U ≡ U n • U n • V V ≡ V n • U n • V
relation defined by the axioms and rules in Table 4. As usual, we write * for the reflexive and transitive closure of .

Rules [u-acq-1] and [u-rel-1] model the acquisition and the release of an object; in the first case, the object must be unlocked (the counter is 0) whereas, in the second case, the object must have been locked exactly once. Rules [u-acq-2] and [u-rel-2] model nested acquisitions and releases on an object. These rules simply change the counter to reflect the actual number of (nested) acquisitions and do not correspond to an actual prefix in the usage. Rule [u-wait] models a wait operation performed on an object: the counter is set to 0 and the wait prefix is replaced by waiting, indicating that the object has been unlocked waiting for a notification. This makes it possible for another process to acquire the object and eventually notify the one who waits. Rules [u-nfy-1] and [u-nfy-2] model notifications. In [u-nfy-1], the notification occurs at a time when there is indeed another process that is waiting to be notified. In this case, the waiting process attempts to acquire the object. In [u-nfy-2], the notification occurs at a time when no other process is waiting to be notified. In this case, the notification has no effect whatsoever and is lost. Finally, rule [u-choice] (in conjunction with commutativity of +) models the nondeterministic choice between two possible usages of an object and [u-cong] closes reductions under usage congruence.

Not all types are acceptable for our type system. More specifically, there are two properties that we wish to be guaranteed:

whenever there is a pending acquisition operation on a locked object, the object is eventually unlocked; whenever there is a pending wait operation on an object, the object is eventually notified.

A type that satisfies these two properties is said to be reliable:

Definition 4 (type reliability). We say that T is reliable, written rel (T), if the following conditions hold for all n, U and V :

1. T * n • acq.U | V implies n • V * 0 • V for some V , and 2. T * 0 • waiting.U | V implies 0 • V * n • notify.U | V for some U , V .
For example, it is easy to verify that 0 • acq.(wait.rel | acq.notify.rel ) is reliable whereas 0 • acq.wait.rel | acq.notify.rel is not. In the latter usage, the object may be acquired by a process that notifies the object at a time when there is no other process waiting to be notified. Eventually, the object is acquired again but the awaited notification is lost.

(U | V ) is reliable, we derive 0 • acq.(U | V ) 1 • U | V 0 • U | waiting.notify.V ( ) 1 • notify.wait.rel .U | waiting.notify.V 1 • wait.rel .U | acq.notify.V 0 • waiting.rel .U | acq.notify.V 1 • waiting.rel .U | notify.V 1 • acq.rel .U | V 0 • acq.rel .U | waiting.notify.V 1 • rel .U | waiting.notify.V 0 • U | waiting.notify.V ( )
and observe that no other reductions are possible apart from those shown above, that the two types labelled ( ) are equal, and that both conditions of Definition 4 are satisfied for each reachable state. As we shall see in Example 3, the type 0 • acq.(U | V ) describes the behavior of the main thread of Example 1 with respect to each buffer.

Static Semantics

Type environments

The type system uses type environments, ranged over by Γ , which are finite sets of associations on variables and procedure names defined by the grammar below:

Type environment Γ ::= ∅ | x : T, Γ | A : [T], Γ
An association x : T indicates that x has type T, whereas an association A : [T] indicates that A is a procedure accepting parameters of type T.

We write dom(Γ ) for the set of variable/procedure names for which there is an association in Γ and Γ (x) for the type associated with x ∈ dom(Γ ). With an abuse of notation, we write Γ , Γ for the union of Γ and Γ when dom(Γ ) ∩ dom(Γ ) = ∅. In addition: we write live(Γ ) for the subset of dom(Γ ) of live object references on which there are pending operations, that is live(Γ

) def = {x ∈ dom(Γ ) | Γ (x) = n • U ∧ (n > 0 ∨ U ≡ 0)}; we write iszero(Γ ) if Γ (x) = 0 • U for every x ∈ dom(Γ ); we write noAct(Γ ) if live(Γ ) = ∅.
The same object may be used in different ways in different parts of a program. In order to track the combined usage of the object we inductively define two operators | and + on type environments with the same domain. Intuitively, (Γ | Γ )(x) is the type of an object that is used both as specified in Γ and also as specified in Γ whereas (Γ + Γ )(x) is the type of an object that is used either as specified in Γ or as specified in Γ . The former case happens if x is shared by two concurrent processes respectively typed by Γ and Γ . The latter case happens if x is used in different branches of a conditional process. Formally:

∅ | ∅ = ∅ x : int, Γ | x : int, Γ = x : int, (Γ | Γ ) A : [T], Γ | A : [T], Γ = A : [T], (Γ | Γ ) n • U, Γ | m • V, Γ = n + m • U | V, (Γ | Γ ) n = 0 ∨ m = 0 ∅ + ∅ = ∅ x : int, Γ + x : int, Γ = x : int, (Γ + Γ ) A : [T], Γ + A : [T], Γ = A : [T], (Γ + Γ ) n • U, Γ | n • V, Γ = n • U + V, (Γ + Γ )
Note that both | and + for environments are partial operators and that the former enforces the property that the same object cannot be owned by more than one process at any given time (at least one of the counters must be 0). It is easy to see that | on environments is commutative and associative (modulo ≡ on usages). In the following we write i=1..n Γ i in place of

Γ 1 | • • • | Γ n .
As usual for behavioral type systems, the type environment used for typing a process is an abstraction of the behavior of the process projected on the objects it uses. In particular, a live object association x : n•U in the type environment of a process means that the process uses x as specified by U , whereas an association such as x : 0 • 0 means that the process does not use x at all. To prevent circular waits between parallel processes, we forbid the existence of cycles in the corresponding type environments: Definition 5 (acyclic type environments). We say that a family {Γ } of type environments has a cycle x 1 , . . . , x n of n ≥ 2 pairwise distinct names if there exist Γ 1 , . . . ,

Γ n ∈ {Γ } such that x i ∈ live(Γ i ) ∩ live(Γ (i mod n)+1 ) for all 1 ≤ i ≤ n.
We say that {Γ } is acyclic if it has no cycle.

Typing rules for user syntax

The typing rules for the language in Section 2 are defined in Table 5 and derive three kinds of judgments. A judgment Γ e : T means that the expression e is well typed in Γ and has type T. A judgment Γ P means that the process P is well typed in Γ . In particular, P uses each object x ∈ dom(Γ ) according to the Table 5. Typing rules for user syntax.

Typing rules for (sequences of ) expressions Γ e :

T Γ = Ai : [Ti] (i=1..n) Γ , xi : Ti Pi (i=1..n) Γ P Γ ({Ai(xi) = Pi}i=1..n, P )
usage in Γ (x). Finally, a judgment Γ D, P means that the program D, P is well typed in Γ . We now describe the typing rules.

The typing rules for (sequences of) expressions are unremarkable except for the fact that, as common in substructural type systems, the unused part of the type environment cannot contain live associations, hence the premise noAct(Γ ) in [t-const] and [t-var].

Rule [t-done] states that the terminated process is well typed in an environment without live associations, because done does not perform any operation.

Rules [t-acq-1] and [t-acq-2] concern a process acq(x).P that acquires the lock on x and then continues as P . The difference between the two rules is that in [t-acq-1] the process is attempting to acquire the lock for the first time (the counter of the object is 0), whereas in [t-acq-2] the process is performing a reentrant acquisition, having already acquired the lock n + 1 times. The continuation P is typed in an environment that reflects the (possibly reentrant) acquision of x. Note that the acq action occurs in the usage of x only in the case of [t-acq-1]. As we have anticipated in Section 3, in usages we only keep track of non-reentrant acquisitions and releases.

Rules [t-rel-1] and [t-rel-2] concern a process rel(x).P . As in the case of [t-acq-*] rules, they differ depending on whether the lock is actually released ([t-rel-1]) or not ([t-rel-2]). Only in the first case the release action is noted in the usage of x. Besides that, the rules update the environment for typing the continuation P .

Rules [t-wait] and [t-notify] concern the coordination primitives. In both cases, the object must have been previously acquired (the counter is strictly positive) and the number of acquisitions does not change.

Rule [t-if] is essentially standard. Since only one of the two continuations P 1 and P 2 executes, the respective type environments Γ 1 and Γ 2 are composed using the appropriate disjunctive operator.

Rule [t-fork] types a parallel composition of two processes P 1 and P 2 . The objects used by the parallel composition are used both by P 1 and also by P 2 . For this reason, the respective type environments are combined using |. The iszero(Γ 1 ) premise enforces the property that the process P 1 being forked off does not own any lock. The last premise requires that the family {Γ 1 , Γ 2 } be acyclic, which is equivalent to checking that live(Γ 1 ) ∩ live(Γ 2 ) contains at most one element. This prevents circular waits between P 1 and P 2 as discussed earlier.

Rule [t-new] concerns the creation of a new object. The object is initially unlocked (its counter is 0) and its type must be reliable (Definition 4).

Rule [t-call] is unremarkable and types a process invocation. The only standard requirement is for the types of the arguments to match those expected in the corresponding process declaration.

The typing rule [t-program] ensures that all process names have a corresponding definition and verifies that the main process is itself well typed.

Example 3. Let us show that the Main process in Example 1 is well typed. To do that, consider the type environment

Γ = P : [0 • U ], C : [1 • V, 1 • V ]
where U and V are the usages defined in Example 2 and observe that noAct(Γ ) holds.

For the two invocations P(x) and P(y) we easily derive

(1) Γ , x : 0 • U, y : 0 • 0 x : 0 • U Γ , x : 0 • U, y : 0 • 0 P(x)
(2) Γ , x : 0 • 0, y : 0 • U y : 0 • U Γ , x : 0 • 0, y : 0 • U P(y)

using [t-var] and [t-call]. Then we have (1)
(2)

Γ , x : 1 • V, y : 1 • V x, y : 1 • V, 1 • V Γ , x : 1 • V, y : 1 • V C(x, y) Γ , x : 1 • V, y : 1 • U | V fork{P(y)} C(x, y) Γ , x : 1 • U | V, y : 1 • U | V fork{P(x)} fork{P(y)} C(x, y) Γ , x : 1 • U | V, y : 0 • acq.(U | V ) acq(y).fork{P(x)} fork{P(y)} C(x, y) Γ , x : 0 • acq.(U | V ), y : 0 • acq.(U | V ) acq(x) • • • rel (0 • acq.(U | V )) Γ , x : 0 • acq.(U | V ) new y in • • • rel (0 • acq.(U | V ))
Γ new x in new y in acq(x).acq(y).fork{P(x)} fork{P(y)} C(x, y)

where the reliability of 0 • acq.(U | V ) has already been proved in Example 2.

In the two applications of [t-fork], the acyclicity of the involved environments is easily established since in each conclusion of ( 1) and ( 2) there is only one live association, for x and y respectively.

Typing rules for runtime syntax and states

The soundness proof of our type system follows a standard structure and includes a subject reduction result stating that typing (but not necessarily types) are preserved by reductions. Since the operational semantics of a program makes use of constructs that occur at runtime only (notably, waiting processes and states) we must extend the typing rules to these constructs before we can formulate the properties of the type system. The additional typing rules are given in Table 6.

Table 6. Typing rules for runtime syntax.

[t-waiting]

Γ , x : n • U P Γ , x : 0 • waiting.U wait(x, n).P [t-state] Γ = i∈I Γi Γi Pi (i∈I) rel (Γ (xj)) (j∈J) {Γi}i∈I acyclic Γi(xj) = n + 1, U ⇐⇒ ti = sj (i∈I,j∈J) Γ (xj) = 0 • U ⇐⇒ sj = • (j∈J)
Γ {xj : sj, nj}j∈J i∈I ti : Pi Rule [t-waiting] accounts for a process waiting for a notification, after which it will attempt to acquire the lock on x. Once x is notified and the process awakened, the process will acquire the lock n times, reflecting the state of acquisitions at the time the process performed the wait(x) operation (see [r-wait]).

The rule [t-state] for states looks more complex than it actually is. For the most part, this rule is a generalization of [t-fork] and [t-new] to an arbitrary number of concurrent processes (indexed by i ∈ I) and of objects (indexed by j ∈ J). From left to right, the premises of the rule ensure that:

each process P i is well typed in its corresponding environment Γ i ; the type of each object x j , which describes the overall usage of x j by all the processes, is reliable; the family {Γ i } i∈I of type environments is acyclic; the process t i owns the object x j if and only if the counter for x j in the type environment Γ i of P i is strictly positive. Because of the definition of | for type environments, this implies that no other process owns x j ; no process owns the object x j if and only if the counter for x j in the overall environment is zero. T T Γ , x : T Γ , x : T As usual, * denotes the reflexive, transitive closure of .

The first rule accounts for the possibility that a new object x is created. We can now formally state subject reduction, which shows that typing is preserved for any reduction of a well-typed program: Lemma 1 (subject reduction). Let Γ D, P and ∅ main : P -→ * D H P . Then Γ H P for some Γ such that Γ * Γ .

The soundness theorem states that well-typed programs are deadlock free:

Theorem 1 (soundness). If Γ (D, P ), then (D, P ) is deadlock free.

Related work

Despite the number of works on deadlock analysis of concurrent programs, only a few address coordination primitives. Below we discuss the most relevant ones. Static techniques typically employ control-flow analysis to build a dependency graph between objects and enforce its acyclicity. These techniques may adopt some heuristics to remove likely false positives, but they are necessarily conservatives. For instance, Deshmukh et al. [START_REF] Deshmukh | Symbolic modular deadlock analysis[END_REF] analyze libraries of concurrent objects looking for deadlocks that may manifest for some clients of such objects, by considering all possible aliasing between the locks involved in the objects. The technique of von Praun [START_REF] Von Praun | Detecting synchronization defects in multi-threaded object-oriented programs[END_REF] is based on the detection of particular patterns in the code, such as two threads that perform wait(x) and wait(y) in different orders, which does not necessarily lead to a deadlock. Naik et al. [START_REF] Naik | Effective static deadlock detection[END_REF] combine different static analyses that correspond to different conditions that are necessary to yield a deadlock. Their technique concerns lock acquisition and release, but not coordination primitives. Williams et al. [START_REF] Williams | Static deadlock detection for java libraries[END_REF] build a lock-order graph that describes the sequences of lock acquisitions in a library of Java classes. In particular, they consider implicit acquisitions due to wait operations, but not deadlocks caused by missed notifications. Hamin and Jacobs [START_REF] Hamin | Deadlock-free monitors[END_REF] present a refinement of separation logic to reason on locks and wait/notify coordination primitives. Their technique ensures deadlock freedom by imposing an ordering on the use of locks and by checking that each wait is matched by at least one notification. The logic allows them to address single wait operations within loops, which is something our type system is unable to handle. On the other hand, the use of a lock ordering limits the technique in presence of loops and recursion whereby blocking operations on several locks are interleaved, as in our running example (Figure 1).

Dynamic techniques perform deadlock detection by analyzing the log or scheduling of a program execution [START_REF] Agarwal | Run-time detection of potential deadlocks for programs with locks, semaphores, and condition variables[END_REF][START_REF] Joshi | An effective dynamic analysis for detecting generalized deadlocks[END_REF][START_REF] Eslamimehr | Sherlock: scalable deadlock detection for concurrent programs[END_REF]. By considering actual program runs, these techniques potentially offer better precision, at the cost of delayed deadlock detection. Agarwal and Stoller [START_REF] Agarwal | Run-time detection of potential deadlocks for programs with locks, semaphores, and condition variables[END_REF] define feasible sequences, called traces, that are consistent with the original order of events from each thread and with constraints imposed by synchronization events. By analyzing all the possible traces, they verify that a wait operation always happens before a notify operation. Joshi et al. [START_REF] Joshi | An effective dynamic analysis for detecting generalized deadlocks[END_REF] extract a simple multi-threaded program from the source code that records relevant operations for finding deadlocks. Then, they consider any possible interleavings of the simple program by means of a model checker in search of deadlocks. The technique returns both false positives (the simple program manifests a deadlock that never occurs in the source program) and false negatives (the simple program is defined by observing a single execution and the deadlock may occur in another execution). Deadlocks due to coordination primitives are not covered by the technique of Eslamimehr and Palsberg [START_REF] Eslamimehr | Sherlock: scalable deadlock detection for concurrent programs[END_REF].

Demartini et al. [START_REF] Demartini | A deadlock detection tool for concurrent java programs[END_REF] translate Java into the Promela language, for which the SPIN model checker verifies deadlock freedom. Their analysis reports all deadlock possibilities so long as the program does not exceed the maximum number of modeled objects or threads. Java Pathfinder, a well-known tool that is used to analyze execution traces, also performs model checking by translating Java to Promela [9]. When checking matches between wait and notify operations, this technique may suffer from the state-space explosion due to the number of traces to analyse.

Kobayashi and Laneve [START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF] present a deadlock analysis for the pi-calculus which provided the initial inspiration for this work. In fact, attempts were made to encode the language of Section 2 in the pi-calculus so as to exploit the technique of Kobayashi and Laneve. The encoding approach proved to be unsatisfactory because of the many false positives it triggered. Notably, Kobayashi and Laneve [START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF], following [START_REF] Kobayashi | Type-based information flow analysis for the pi-calculus[END_REF], define a notion of usage reliability which can be reduced to a reachability problem in Petri nets. However, the encoding of usages with wait-notify primitives requires the use of Petri nets with inhibitor arcs [START_REF] Busi | Analysis issues in petri nets with inhibitor arcs[END_REF], which are more expressive than standard Petri nets.

Our type system does not impose an order on the usage of locks. Rather, it adopts a typing rule for parallel threads ([t-fork]) inspired by session type systems based on linear logic [START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Caires | Linear logic propositions as session types[END_REF]. The key idea is to require that, whenever two threads are combined together in a parallel composition, they can only interact through at most one object, as suggested by the structure of the cut and tensor rules in (classical) linear logic [START_REF] Girard | Linear logic[END_REF]. This approach results in a simple and expressive type system which can deal with recursive processes interleaving blocking actions on different objects (Figure 1). The downside is that [t-fork] imposes well-typed programs to exhibit a forest-like topology, ruling out some interesting programs which are in the scope of other techniques, such as those based on lams [START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF].

Concluding Remarks

We have described a deadlock analysis technique for concurrent programs using Java-like coordination primitives wait and notify. The technique extends also to notifyAll (Appendix D). Our technique is based on behavioral types, called usages, that may be encoded as Petri nets with inhibitor arcs [START_REF] Busi | Analysis issues in petri nets with inhibitor arcs[END_REF]. Thereby, we reduce deadlock freedom to the reachability problem in this class of Petri nets.

Our technique is unable to address programs where two threads share more than one object because of the acyclicity constraint in rule [t-fork]. A more finegrained approach for tracking object dependencies has been developed by Laneve [START_REF] Laneve | A lightweight deadlock analysis for programs with threads and reentrant locks[END_REF] and is based on lams [START_REF] Kobayashi | Deadlock analysis of unbounded process networks[END_REF]. However, this approach does not consider coordination primitives. We initially tried to combine lams and usages with coordination primitives, but the resulting type system proved to be overly restrictive with respect to recursive processes: the amount of dependencies prevented the typing of any recursive process interleaving blocking operations on two or more objects (such as the consumer in Figure 1). Whether lams and usages with coordination primitives can be reconciled is still to be determined.

Another limitation of the type system is that it assumes precise knowledge of the number of acquisitions for each shared object, to the point that types contain a counter for this purpose. However, this information is not always statically available. It may be interesting to investigate whether this limitation can be lifted by allowing a form of counter polymorphism.

Γ , x : 1 • rel .U, y : 0 • 0 rel(x).P(x) Γ , x : 1 • wait.rel .U, y : 0 • 0 wait(x).rel(x).P(x) Γ , x : 1 • notify.wait.rel .U, y : 0 • 0 notify(x).wait(x).rel(x).P(x) Γ , x : 0 • U, y : 0 • 0 acq(x).notify(x).wait(x).rel(x).P(x) for the producer, recalling that we identify recursive usages with their unfolding.

B Soundness Proofs

B.1 Subject Reduction

Given that the syntax and semantics of expressions is only partially specified, in the following we make the assumption that well-typed expressions satisfy the basic principle of type preservation under evaluation, namely that Γ e : T and e = v imply Γ v : T. Lemma 2 (substitution). The following properties hold: Proof. The first property is assumed, since syntax and semantics of expressions are only partially specified. The second property follows by a simple induction on the typing derivation and a standard weakening result whereby a type environment can be augmented by associations for integer numbers and objects with type 0 • 0.

Proposition 1. If both {Γ 1 | Γ 2 , Γ } and {Γ 1 , Γ 2 } are acylic, then so is {Γ 1 , Γ 2 , Γ }.
Proof. We prove the contrapositive of the statement, namely that if {Γ 1 , Γ 2 , Γ } has a cycle, then either {Γ 1 | Γ 2 , Γ } or {Γ 1 , Γ 2 } have one too. If the cycle is entirely within {Γ } or entirely within {Γ 1 , Γ 2 } the result is trivial. Otherwise, observe that live(Γ 1 | Γ 2 ) = live(Γ 1 )∪live(Γ 2 ) and that the length of a cycle in a family of type environments is the same as the number of environments in the family involved in the cycle. So, if the cycle goes through Γ 1 or Γ 2 , but not both, the same cycle is also found in We discuss only a few interesting cases assuming, without loss of generality, that H = {x j : s j , n j } j∈J and P = {t i : P i } i∈I . Then, from [t-state], we deduce the following facts:

{Γ 1 | Γ 2 , Γ }.
1. Γ = i∈I Γ i ; 2. Γ i P i for every i ∈ I; 3. rel (Γ (x j )) for every j ∈ J; 4. {Γ i } i∈I is acyclic; 5. Γ i (x j ) = n + 1, U iff t i = s j and Γ (x j ) = 0, U iff s j = • for all i ∈ I, j ∈ J;

[r-acq-1] Then P = t i : acq(x j ).Q, P and H = H , x j : •, 0 and P = Q, P and H = H , x j : t i , 1 for some i ∈ I and j ∈ J. From [t-state] and [t-acq-1] we deduce that there exist Γ i and U such that Γ i = Γ i , x j : 0 • acq.U and Γ i , x j : 1

• U Q. Let Γ i def = Γ i , x j : 1 • U and Γ k def = Γ k for every k ∈ I \ {i}. Let Γ def = i∈I Γ i .
Note that Γ is well defined because the fact 5 ensures that no other process owns x j . We conclude by observing that Γ Γ . [r-acq-2] Similar to the previous case, except that H = H , x j : t i , n + 1 and H = H , x j : t i , n + 2. We use fact 5 to deduce that n j = n + 1 and we use the reentrant reduction of types to increment this counter.

[r-rel-1] Then P = t i : rel(x j ).Q, P and H = H , x j : t i , 1 and P = t i : Q, P and H = H , x j : •, 0 for some i ∈ I and j ∈ J. From [t-rel-1] and the fact 5 we deduce that there exist Γ i and U such that

Γ i = Γ i , x j : 1 • rel .U and Γ i , x j : 0 • U Q. Let Γ i def = Γ i , x j : 0 • U and Γ k def = Γ k for every k ∈ I \ {i}. Let Γ def = i∈I Γ i .
We conclude by observing that Γ Γ .

[r-fork] Then P = t i : fork{P 1 }P 2 , P and P = t i : P 1 , s : P 2 , P and H = H. From [t-fork] we deduce that Γ i = Γ i1 | Γ i2 and Γ ik P ik for k = 1, 2 and iszero(Γ i1 ) and {Γ i1 , Γ i2 } is acyclic. From iszero(Γ i1 ) and the fact that s is a new thread identifier we deduce that all objects owned by t i before the reduction are still owned by t i after the reduction and that all objects not owned by t i before the reduction are not owned by s after the reduction. This suffices to deduce that the last two premises of [t-state] hold. We conclude by taking Γ def = Γ and observing that {Γ i1 , Γ i2 } ∪ {Γ k } k∈I\{i} is acyclic by Proposition 1.

[r-new] Then P = t i : new x in Q, P and P = t i : Q, P and H = H, x : •, 0 for some i ∈ I. From [t-new] we deduce that there exists U such that Γ i , x : 0 • U P and rel (0

• U ). Take Γ i def = Γ i , x : 0 • U and Γ k def = Γ i , x : 0 • 0 for every k ∈ I \ {i} and Γ def = i∈I Γ i .
We conclude by observing that Γ Γ and that {Γ k } k∈I is acyclic. Proof. Let H = {y j : s j , n j } j∈J and P = {t i : Q i } i∈I . From [t-state] we deduce that Γ = i∈I Γ i and Γ i Q i for all i ∈ I and there exist U j such that Γ (y j ) = n j • U j for all j ∈ J. Also, {Γ i } i∈I is acyclic. Using the hypotheses Γ H P : and H P -→ D and the assumption that every process name has a corresponding declaration in D we deduce that Q i = π i .P i for every i ∈ I, where π i is a synchronization primitive concerning some lock x i .

From the hypothesis that H P is well typed we deduce that all the processes in P are closed, hence for every i ∈ I there exists j ∈ J such that y j = x i . Let η : I → J be the map such that y η(i) = x i for every i ∈ I.

Using once again the hypothesis that H P -→ D we can make the following deductions:

1. if π i = acq(x i ), then s η(i) ∈ {•, t i } or else H P would reduce using either

[r-acq-1] or [r-acq-2]; 2. if π i = wait(x i ), then s η(i) = t i or else H P would reduce using [r-wait]; 3. if π i = rel(x i ), then s η(i) = t i or else H P would reduce using either [r-rel-1] or [r-rel-2]; 4. if π i = notify(x i ), then s η(i) = t i or else H P would reduce using [r-nfy-2].
From these deductions and the hypothesis that H P is well typed we can further rule out the possibility that any prefix is wait(x i ) or rel(x i ) or notify(x i ), because the type system allows these operations only when the thread performing them owns the corresponding lock x i . In summary, each π i has either the form acq(x i ) or the form wait(x i , n). Also, we may deduce x i ∈ live(Γ i ) because the process t i is performing an action on x i . Now we show that, by starting from the assumption that I = ∅, it is possible to find a cycle in {Γ i } i∈I . This, of course, contradicts the hypothesis that {Γ i } i∈I is acyclic and therefore the assumption I = ∅. To build the cycle, it suffices to show that for every i ∈ I there exists k ∈ I \ {i} such that x i ∈ live(Γ i ) ∩ live(Γ k ) and x k = x i , bearing in mind that I is finite.

We discuss three sub-cases, in which j def = η(i):

-If π i = acq(x i ), then x i is owned by a process s j = t i . Take k ∈ I such that t k = s j and observe that k = i. From rel (Γ (x i )) we know that t k must eventually perform an action rel(x i ) or wait(x i ), hence x i ∈ live(Γ k ). Furthermore, the process t k must be blocked on a prefix π k concerning an object x k different from x i , hence x i = x k . -If π i = wait(x i ) and x i is owned by a process s j = t i , then we can reason as in the previous case to find the x k with the desired properties. -If π i = wait(x i ) and x i is not owned by any process, then from [t-waiting] and rel (Γ (x i )) we deduce that Γ (

x i ) = n j • U and U ≡ wait.U 1 | U 2 and n j • U 2 * m • notify.U 3 | U 4 .
Hence there is (at least) another thread t k = t i owning a reference to x i such that Γ k (x i ) contains the subterm notify.U 3 not guarded by a wait, therefore x i ∈ live(Γ k ). We conclude observing that the process t k must be blocked on a prefix π k concerning an object x k different from x i , because x i is free.

The above arguments suffice to establish that P = ∅. All that remains to prove is that all the objects in H are unlocked. From [t-state] we deduce Γ (y j ) = n j • 0 for all j ∈ J. Then, from rel (n j • 0), we deduce n j = 0. From [t-state] we conclude s j = •.

C Partial Decidability of Reliability

In this appendix we demonstrate that the predicate rel (n, U ) is partially decidable. To this aim, we encode usages in a variant of Petri nets using inhibitor arcs and we reduce reliability to the reachability predicate in this class of nets [START_REF] Busi | Analysis issues in petri nets with inhibitor arcs[END_REF]. Below we briefly recall the definition of Petri nets with inhibitor arcs and the definition of execution of a transition. Busi [START_REF] Busi | Analysis issues in petri nets with inhibitor arcs[END_REF] gives all the details. Definition 7. A Petri net with inhibitor arcs is a tuple N = (S, T, F, I), where -S and T are finite sets of places and transitions such that S ∩ T = ∅; places and transitions are denoted by circles and boxes, respectively, in Figure 2; -F : (S × T ) ∪ (T × S) → N is the flow function (N is the set of natural numbers); -I ⊆ S × T is the inhibiting relation; inhibitor arcs are drawn in red in Figure 2.

A multiset over the set S of places is called a marking and noted by m, m , . . . . That is, markings are maps S → N. Given a marking m and a place s, we say that the place s contains m(s) tokens. The preset of a transition t, noted • t, is the marking such that • t(s) = F (s, t) and represents the tokens to be "consumed"; the postset of t, noted t • , is the marking such that t • (s) = F (t, s) and represents the tokens to be "produced". The inhibitor set of a transition t is the set •t = {s ∈ S | (s, t) ∈ I} and represents the places to be "tested for absence" of tokens.

A transition t is enabled at m if • t ⊆ m and dom(m) ∩ •t = ∅. The execution of a transition t enabled at m produces the marking m = (m \ • t) t • . This is written as m[t m .

In order to verify the reliability predicate for types n • U we will encode these pairs into Petri nets (with inhibitor arcs) and define a correspondence between the reduction and the transitions of Petri nets. Actually, we may simplify our arguments. First, we notice that the rules [u-acq-2] and [u-rel-2] of Table 4 are not relevant for reliability. This follows by the following proposition. Then, we also notice that, in the typing rules for user syntax, reliability is always checked for pairs 0 • U where U never contains the waiting prefix (this prefix is produced by the relation -rule [u-wait] -and will have a counterpart in the Petri net).

Because of the foregoing remarks, we encode a usage U (without any counter) in a Petri net with inhibitor arcs. The definition of the function PN(U ) is reported in Figure 2. We use three special places, that are called x, w x and n x . These places are dotted in the figure. Their meaning is as follows:

if m(x) ≥ 0 then the object x is unlocked, otherwise (m(x) = 0) it is locked; m(w x ) specifies the number of usages waiting to be notified; m(n x ) specifies the number of notifications that will awake waiting usages.

The map PN(U ) returns a net with an "initial place", which is the topmost one in every net. We compose nets by connecting these initial places. Below we discuss the interesting encodings:

-PN(acq.U ) is encoded by a net where a token is put into the initial place of PN(U ) if x is unlocked, e.g. the place x contains a token; no one else can lock x if PN(U ) does not release the lock (the place x always contains at most one token); -PN(rel .U ) is encoded by a net where a token is put into the x place -e.g. x is unlocked -that PN(U ) is triggered; -PN(wait.U ) is encoded by a net whose first transition releases the lock of x, puts a token into the place w x and puts a token into a place expressing that the thread is waiting to be notified -this place models the waiting prefix. When the notification arrives -e.g. n x contains a token -then the net transits into a place waiting for acquiring the lock of x -that corresponds to the acq prefix. When the lock has been acquired then PN(U ) can start; -PN(notify.U ) is encoded by a net using an inhibitor arc. This arc is used for separating the two cases of notifications awaking a waiting thread and of notifications that are skipped because there is no waiting thread. Therefore, if the place w x is empty then (inhibitor arc) PN(U ) starts and the notification is lost; otherwise a token in n x is put and PN(U ) starts; -PN(µα.U ) is defined by taking PN(U ) and adding a transition from any place labelled α to a place that triggers the initial place of PN(U ).

The initial marking of PN(U ) has a token in the initial place of the net and a token in the place labelled x. With this setup, the proof that rel (n • U ) is partially decidable is analogous to the corresponding one in [START_REF] Kobayashi | Type-based information flow analysis for the pi-calculus[END_REF].

D Extension

Below we discuss the extension of our system to an additional coordination primitive that is present in Java. The primitive is notifyAll() that awakes all the waiting threads. The formal account of this primitive consists of extending prefixes π in Section 2 with the action notifyAll() and the operational semantics with the rules (I is finite, possibly empty):

[R-NfyAll]

x : t, n + 1 i∈I t i : wait(x, n i ).P i , t : notifyAll(x).Q, P -→ D x : t, n + 1 i∈I t i : acq(x) ni .P i , t : Q, P if wait(x) / ∈ P Notice that, since I may be empty, notifyAll(x) is ephemeral, similarly to notify(x).

Correspondingly, usage prefixes are extended with notifyAll whose reductions are

[U-NfyAll] wf(V ) n + 1, i∈I waiting.U i | notifyAll .U | V n + 1, i∈I acq.U i | U | V
To account for the new notifyAll prefix, Definition 4 of reliability is extended as follows: T is reliable, written rel (T), whenever the following two conditions hold:

1. if T * n • acq.U | V then n • V * 0 • V , for some V , and 2. if T * 0 • waiting.U | V , 0 • V * n • κ.V | V for some n, V , V and κ ∈ {notify, notifyAll }.

Finally, we extend PN() to notifyAll so that PN(notifyALL(x). U )= PN(U ) wx nx and it is now possible to demonstrate that the predicate rel (T) is partially decidable as in the basic case without notifyAll().

Fig. 1 .

 1 Fig. 1. Multiple-producers/single-consumer coordination in Java.

Example 2 .

 2 Consider the type 0•acq.(U | V ) where U def = µα.acq.notify.wait.rel .α and V def = µα.wait.notify.α. To prove that 0 • acq.

1 .

 1 If Γ , x : T e : T and Γ v : T, then Γ e{v/x} : T ; 2. If Γ , x : T P and Γ v : T, then Γ P {v/x}.

  [r-call] Then P = t i : A(e), P and P = t i : Q{v/x}, P , where e = v and H = H and A(x) = Q ∈ D. From [t-state] and [t-call] we deduce that Γ i = Γ i , A : [T] and Γ i e : T. From the assumed type preservation property of well-typed expressions we deduce Γ i v : T. From the hypothesis that the program is well typed we dedice that Γ = Γ 0 | Γ 1 and Γ 0 , x : T Q. From Lemma 2 we deduce Γ 0 | Γ i Q{v/x}. We conclude by taking Γ def = Γ .B.2 SoundnessTheorem 2 (soundness). If Γ H P and H P -→ D , then P = ∅ and all the objects in H are unlocked.

Proposition 2 .

 2 Let [n] be 0 if n = 0 and be 1 if n > 0. Then n • U * n • U if and only if [n] • U * [n ] • U .

Fig. 2 .

 2 Fig. 2. The encoding of usages in Petri nets with inhibitor arcs.

Table 1 .

 1 Syntax of the language with runtime syntax marked by †.

	Expression	e ::= n	(constant)
		| x	(variable)
		| e op e	(operator)
	Process P, Q ::= done	(termination)
		| π.P	(action prefix)
		| if e then P else Q (conditional)
		| new x in P	(new object)
		| fork{P }Q	(new process)
		| A(e)	(invocation)

Table 2 .

 2 Reduction rules.

	[r-acq-1]

Table 4 .

 4 Reduction of types.

[u-acq

-1]

  The most interesting case is when the only cycles of {Γ 1 , Γ 2 , Γ } go through both Γ 1 and Γ 2 and at least one more environment in Γ . Consider a cycle x 1 , . . . , x n where x 1 ∈ live(Γ 1 ) ∩ live(Γ 2 ). Then n ≥ 3 and we conclude that x 2 , . . . , x n is a cycle of {Γ 1 | Γ 2 , Γ }.

	Lemma 3 (subject reduction). Let Γ P . Then Γ H P for some Γ such that Γ * Γ . D, P and ∅ main : P -→ * D H
	Proof. By induction on the length of ∅	main : P -→ * D H	P . The basic
	case is obvious. For the inductive case, we decompose the computation into
	∅	main : P -→ * D H	P -→ D H	P and we reason by cases on the
	reduction rule being applied to H	P -→ D H	P .

[t-const] noAct(Γ ) Γ n : int [t-var] noAct(Γ ) Γ , x : T x : T [t-op] Γ e : int Γ e : int Γ e op e : int [t-seq]Γi ei :Ti (i=1..n) Γ1 | • • • | Γn e1, .. . , en : T1, . . . , TnTyping rules for processes Γ P[t-done] noAct(Γ ) Γ done [t-acq-1] Γ , x : 1 • U P Γ , x : 0 • acq.U acq(x).P [t-acq-2] Γ , x : n + 2 • U P Γ , x : n + 1 • U acq(x).P [t-rel-1] Γ , x : 0 • U P Γ , x : 1 • rel .U rel(x).P [t-rel-2] Γ , x : n + 1 • U P Γ , x : n + 2 • U rel(x).P [t-wait] Γ , x : n + 1 • U P Γ , x : n + 1 • wait.U wait(x).P [t-notify] Γ , x : n + 1 • U P Γ , x : n + 1 • notify.U notify(x).P [t-if] Γ e : int Γi Pi (i=1,2) Γ | (Γ1 + Γ2) if e then P1 else P2 [t-call] Γ e : T Γ , A : [T] A(e) [t-fork] Γi Pi (i=1,2) iszero(Γ1) {Γ1, Γ2} acyclic Γ1 | Γ2 fork{P1}P2 [t-new]Γ , x : 0 • U P rel (0, U )Γ new x in P Typing rule for programs Γ (D, P )[t-program]

4.4 Properties of well-typed programsAs usual, the key lemma for proving soundness of the type system is subject reduction, stating that a well-typed state reduces to well-typed state. In our case, this result guarantees the preservation of typing, but not necessarily the preservation of types. Indeed, as a program reduces and operations are performed on objects, the type of such objects changes consequently. To account for these changes, we lift reduction of types to type environments, thus: Definition 6 (environment reduction). The reduction relation for environments, noted , is the least relation such that: Γ Γ , x : T

Cosimo Laneve and Luca PadovaniA Typing derivations for producer-consumerIn this section we provide the typing derivations for the producer and consumer processes in Example 1. Using the definitions of U and V in Example 2 and that of Γ in Example 3, we deriveΓ , x : 1 • V, y : 1 • V x, y : 1 • V, 1 • V Γ , x : 1 • V, y : 1 • V C(x, y) Γ , x : 1 • V, y : 1 • notify.V notify(y).C(x, y) Γ , x : 1 • V, y : 1 • V wait(y).notify(y).C(x, y) Γ , x : 1 • notify.V, y : 1 • V notify(x).wait(y).notify(y).C(x, y) Γ , x : 1 • V, y : 1 • V wait(x).notify(x).wait(y).notify(y).C(x, y)for the consumer and Γ , x : 0 • U, y : 0 • 0 x : 0 • U Γ , x : 0 • U, y : 0 • 0 P(x)


J Fondard

A Billard

G Bertrand

S Fourcade

P Batocchi

F Mauvy

P Briois

Effect of total pressure on La 2 NiO 4 coatings deposited by reactive magnetron sputtering using plasma emission monitoring

Keywords:

This work focuses on the structural, microstructural, electrical and electrochemical characterization of La Ni O coatings deposited by reactive magnetron sputtering under different argon partial pressures. Deposition was driven by Plasma Emission Monitoring system (PEM) which allows high deposition rate. For each pressure, the optimal regulation setpoint for lanthanum oxide deposition is determined and then the current dissipated on the nickel target is adjusted to obtain the convenient La/Ni ratio to achieve the K 2 NiF 4 structure. After an appropriate annealing treatment, coatings crystallize in the desired structure with more or less impurities. In creasing the device's pressure from 0.4 to 4.8 Pa produces more porous samples with different microstructures. Then, a coating with porosity gradient was built by using these four different total pressures. Its electrical perfor mances were tested and allowed its utilization as cathode layer in intermediate temperature solid oxide fuel cell (IT SOFC). This modified architecture cathode allows better performances (71 mW•cm -2 ) than dense cathode produced by the same technique (51 mW•cm -2 ).

Introduction

Since solid oxide fuel cells (SOFC) are designed to operate at inter mediate temperature (873 1073 K), research works try to face with the drop of the cell performances. Solutions have to be found on each ac tive layer to reduce losses. Reducing layer's thicknesses and using new materials remain the most effective ways to solve this problem. At the cathode side, where high overpotentials cause high resistances, mixed ionic and electronic conductors (MIECs) are dedicated to be new mate rials. It is believed that the improvements are induced by the extended area reaction from triple phase boundary to the whole surface, reducing electrode polarization. Most studies concerning MIECs are talking about perovskite type oxides [1 5]. These compounds become the reference for cathode materials at these lower temperatures. More recently, Ln 2 NiO 4+δ compounds (Ln = La, Pr, Nd) with K 2 NiF 4 structure have been investigated as cathode material [6 10]. These structures present very good catalytic properties towards the oxygen, a predominant elec tronic conductivity in the whole p(O 2 ) range and they are chemically compatible with the electrolyte and the interconnector materials. Because of these properties, those materials have been studied in half cells with different electrolytes with promising results [START_REF] Philippeau | Comparative study of electrochemical properties of mixed conducting Ln 2 NiO 4+δ (Ln = La, Pr and Nd) and La 0.6 Sr 0.4 Fe 0.8 Co 0.2 O 3 δ as SOFC cathodes associated to Ce 0.9 Gd 0.1 O 2 δ , La 0.8 Sr 0.2 Ga 0.8 Mg 0.2 O 3 δ and La 9 Sr 1 Si 6 O 26.5 electrolytes[END_REF] and they begin to be used as cathode material in single cells [START_REF] Zhao | Electrochemical evaluation of La 2 NiO 4+δ as a cathode material for intermediate temperature solid oxide fuel cells[END_REF].

Whereas thick layers deposited by wet techniques are commonly used as cathodes in IT SOFCs, recent studies deal with the deposition of MIEC coatings by physical surface deposition processes [ 13 15]. Re active magnetron sputtering (RMS) technique allows the deposition of thin and dense layers able to be used as electrolyte [START_REF] Briois | A comparison of electrical properties of sputter-deposited electrolyte coatings dedicated to intermediate temperature solid oxide fuel cells[END_REF] or diffusion barrier layers [START_REF] Jordan | Ce 0.8 Gd 0.2 O 2 δ protecting layers manufactured by physical vapor deposition for IT-SOFC[END_REF] in fuel cells. Recently, half cells were completely pro duced by this process with promising results [START_REF] Solovyev | Application of PVD methods to solid oxide fuel cells[END_REF]. Previous studies per formed in our laboratory proved that this technique may also deposit a cathode layer by co sputtering of several metallic targets [ 19 20]. Thin and dense La 2 NiO 4+δ layers were hence synthesized and electrically tested, revealing interesting results compared to literature [START_REF] Fondard | Synthesis and characterization of La 2 NiO 4 + δ coatings deposited by reactive magnetron sputtering using plasma emission monitoring[END_REF]. Never theless, electrochemical characterizations and complete cell tests of this material disclose low results (i.e 50 mW/cm 2 at 973 K on Ni YSZ/YSZ/ GDC/La 2 NiO 4+δ ). The gas tightness of the dense cathode layer avoids a fast adsorption and diffusion of oxygen, resulting as low electrochemical characteristics as demonstrated in literature with other MIECs [ 21 22]. Therefore, the porosity of this layer has to be increased to improve its performances.

In this study, we investigate the feasibility of producing a thin La 2 NiO 4+δ coatings with a porosity gradient by RMS under unstable conditions using Plasma Emission Monitoring (PEM) [23 24]. This tech nique allows the deposition of oxide coatings with high sputtering rate. Four point probe electrical analyses were performed on annealed lanthanum nickelate films in static air in the temperature range from 293 to 1273 K with temperature steps and stabilization time of about 25 K and 20 min, respectively. A Ni YSZ/YSZ/GDC/La 2 NiO 4+δ complete cell was then synthesized from a commercial NiO YSZ anode support using RMS technique. Manufacture of this cell has been described in a previous study [START_REF] Fondard | Synthesis of half fuel cell Ni-YSZ/YSZ on porous metallic support by dry surface deposition processes[END_REF]. The overall cell performance and detailed imped ance analyses of this cell are presented and compared to this cell presenting a dense La 2 NiO 4+δ layer to elucidate the gain of this special configuration.

Experimental details

Deposition device

An Alcatel SCM 650 setup was used in this study. Fig. 1 shows a scheme of the complete setup. The desired vacuum of this 100 L volume sputtering chamber is obtained via a system using ALCATEL RSV 301B/ 2063 primary pump and a 5401CP turbo molecular pump. The chamber is composed by three magnetron targets (diameter = 200 mm), a rotat ing substrate holder (Ø = 620 mm) and an optical fiber placed near the erosion area of the target. The distance of 110 mm between the sub strate holder, parallel to the targets, was used for these experiments. A pulsed DC dual generator (Advanced Energy Pinnacle +) managed the discharge current of the targets. For each deposition with the lantha num metallic targets, the discharge current was fixed at 2.5 A while it was varied with the nickel target to obtain a La/Ni metallic ratio of 2, and consequently the wished K 2 NiF 4 structure. Different glass, alumina (Ø = 16 mm), YSZ (Ø = 20 mm) samples and Ni YSZ/YSZ/GDC sputtered half cells with commercial anode support (Ø = 23 mm), were used as substrates for the various analyses made during this work. Before to realize the cathode deposition (Ø = 21 mm), a circular mask was placed on the half cell to allow the single measurements. Prior to each deposition, substrates were cleaned by cold soaped water, rinsed and then dried with paper. The anode supports were additionally dried at 353 K for 3 h to remove the water. Electrolyte and GDC protective films were coated in the same setup with Zr Y (84 16 at.%) and Ce Gd (80 20 at.%) metallic targets followed by a thermal treatment at 773 K for 2 h after each deposition process to densify the coatings. Substrates were placed at 170 mm of substrate holder's center, where the coatings present the best homogeneity. Argon and oxygen gases were used to obtain a plasma and deposit ceramic coatings. Flow meters (Brooks) managed the gas flow rates and Baratron gauge (MKS) measured the total pressure of the chamber. A closed loop control PEM system allowed to control the oxygen flow rate by the measurement of the optical intensity of the 391.91 nm lanthanum emission line (I La ⁎ ) col lected through an optical fiber. The signal is sent to a spectrometer (Ropper Scientific SpectraPro 500i), with a 1200 groove mm -2 grating and a photomultiplier tube (Hamamatsu R 636). A homemade software developed with Labview® managed the information and control the ox ygen flow rate to keep the intensity of the optical signal I La ⁎ at the desired value.

Structural, morphological

Samples were analyzed by Scanning Electron Microscopy (SEM) using a JEOL JSM 7800 F to determine their microstructure. Metallic ra tios were measured by Energy Dispersive Spectroscopy (EDS). Samples were coated with carbon by evaporation under vacuum before EDS analyses. These analyses were performed at Working Distance equal 10 mm with 15 kV acceleration voltage and 2 nA probe current. 5 mea surements were made on different parts of the sample and an average value was calculated. A BRUKER D8 focus diffractometer was used to check the structural features of the samples. This device, equipped with the LynxEye linear detector, use the K α1 + α2 of cobalt radiations to XRD collect patterns. Analyses were performed at room temperature from 20°to 80°scattering angle by steps of 0.019°. The thickness of coatings was measured on glass slides with an Altisurf profilometer (Altimet) allowing an accuracy of 20 nm. This device was calibrated before each measurement following the CETIM accreditation (reference sample number 787569). Measurements were performed using the "step" method in which a small surface tape is stuck prior to deposition process, then removed leaving a step revealing the thickness of films.

Electrical measurements

The electrical resistivity measurements were performed with a HP 3458 A multimeter on La Ni O films deposited on alumina substrates. With regard to its high insulating character, it is assumed in the follow ing that the substrate has no significant contribution to the electrical conductivity. The four point probe technique with four Pt aligned elec trodes was used. Two outer probes behaved as the current carrying electrodes (I1, I2) and the two inner ones were used to measure the voltage (E1, E2). Two cell configurations were used for the measure ments: cell 1 was used to define the resistivity at room temperature (Jandel, Linslade, UK). It is a standard and certified cell allowing the ac curate determination of the geometric factor. The second cell developed by the LEPMI laboratory (Grenoble, France) allows measurements at various temperatures. This latter cell is placed inside an alumina tube and positioned into a furnace (Pekly, Thions Gardais, France). The comparison of the resistance measured at room temperature with cell 1 (R 1 ) and cell 2 (R 2 ) was used to determine the geometric factor of cell 2 thanks to the relationship (Eq. ( 1)):

σ 1 ρ 1 4:381 Ã R 2 R 1 Ã t ð1Þ
where 4.381 is the correction factor calculated from the diameter of the sample (Ø = 16 mm) and t, the thickness of the film.

Complete cell tests

The samples were inserted into a homemade cell designed at the ICMCB laboratory (Bordeaux, France). A nickel/gold grid was main tained on the cathode side with springs. Before cell tests, the cathode layer of the stack was first crystallized at 1073 K during 10 h. Anode layer was then reduced at 973 K during 6 h. Measurements were per formed at 973 K with 120 mL/min of H 2 3 vol.% H 2 O on the anode side and 240 mL/min air on the cathode side. Electrochemical measure ments are realized by the use of an Autolab PGSTAT30 potentiostat driven by GPES and FRA software for voltammetry and impedance mea surements. In cyclic voltammetry, the output current is measured from different potentials. The parameters for the Voltammetry measure ments were 2 s equilibrium time, start potential at OCV, end potential 0.2 V and 5 mV/s speed. Electrochemical Impedance Spectroscopy (EIS) was then performed on the Open Circuit Voltage (OCV) from 100 mHz to 10 MHz with 10 points per decade with 50 mV amplitude.

Result and discussion

3.1. Deposition of the cathode layer 3.1.1. Determination of the optimal regulation setpoint for each pressure Fig. 2 shows the discharge voltage versus oxygen flow rate curves of La and Ni targets during their sputtering at discharge current values re spectively 2.5 and 0.7 A applied to metallic targets. For the nickel mate rial, the target voltage oxygen flow rate curve is reversible which corresponds to so called stable sputtering conditions. For the lanthanum metallic target, an hysteresis loop characteristic of the instability of the La O system is observed, depending on whether oxygen flow rate in creases or decreases. With magnetron sputtering technique, the use of metallic targets in presence of oxygen can lead to the deposition of ce ramic or metallic coatings depending on the oxygen content. Low oxy gen flow rates are associated with high sputtering rate but the coating is often oxygen deficient (metallic mode). Conversely, high oxygen flow rates induce a contamination of the target's surface (i.e. formation of oxide compounds). When the surface of the target is entirely oxidized (poisoned mode), the sputtering rate decreases and stoichiometric oxides are deposited. The physicochemical state that conditions the av erage sputtering yield of the target, is usually a monotonic and quite proportional function of the optical signal I M ⁎ measured by Optical Emission Spectroscopy [26 27]. The PEM system allows the deposition of coatings in the unstable domain of the hysteresis loop by fixing the intensity of the plasma emission line of the target using a closed loop control of the oxygen flow rate as explained in a previous work [START_REF] Billard | Attempted modelling of thickness and chemical heterogeneity in coatings prepared by d.c. reactive magnetron sputtering[END_REF]. In deed, PEM is a very suitable technique to allow high rate growth of oxide coatings [START_REF] Fondard | Synthesis and characterization of La 2 NiO 4 + δ coatings deposited by reactive magnetron sputtering using plasma emission monitoring[END_REF][START_REF] Coddet | Reactive co-sputter deposition of YSZ coatings using plasma emission monitoring[END_REF] under unstable sputtering conditions (transition mode). The PEM control was then performed on the La target with a fixed discharge current of 2.5 A. A drop of the optical emission until about 5%, occurs at critical oxy gen flow rate. This critical oxygen flow rate evolves from about 6.4 to 2.6 sccm O 2 with increasing argon pressure from 0.4 to 4.8 Pa which is consistent with a decrease of the pumping speed and a stronger diffu sion of sputtered metal atoms. Whatever the total pressure, using PEM allows the deposition with an optical intensity set point (S) located in the unstable domain inside the hysteresis loop and allows the deposi tion of oxide coatings with higher deposition rates. The setpoint I La ⁎ is fixed by the operator, allowing the control of the oxygen flow rate by the software. The S value was varied from 95 to 10% to obtain the plot ted open symbols (Fig. 3) in the unstable domain. The Table 1 summa rizes the evolution of the hysteresis domain as function of the total pressure. In a previous work [START_REF] Fondard | Synthesis and characterization of La 2 NiO 4 + δ coatings deposited by reactive magnetron sputtering using plasma emission monitoring[END_REF], the methodology for determining the regulation set point had been already described on the La O system. In this study, the regulation set point is respectively 55%, 65%, 70% and 80% for 0.4, 1.9, 3.2 and 4.8 Pa.

Deposition of La Ni O coatings: influence of total pressure

The coatings are deposited by co sputtering of La and Ni metallic targets in Ar O 2 mixtures for which the oxygen flow rate is controlled by the PEM system. Fig. 4 presents the metallic La/Ni atomic ratio determined by EDS analyses versus the discharge current applied to the Ni target while the La target current is fixed at 2.5 A. For each pressure, the metallic ratio La/Ni decreases linearly with increasing the discharge current on the Ni target. The current on the Ni target necessary to obtain the targeted composition for La 2 NiO 4 also increases with increasing the total pressure. This should be ascribed to a stronger diffusion of Ni than La in the gas phase due to its lower mass. Optimal discharge current of 0.38 A, 0.44 A, 0.57 A and 0.68 A with PEM set points fixed at 55%, 65%, 70% and 80% for 0.4, 1.9, 3.2 and 4.8 Pa respectively were deter mined to obtain the La 2 NiO 4 composition. In fact, as EDS analyses do not allow a reliable determination of the oxygen content into the coatings, it was only used to estimate the metallic composition.

As expected for each pressure, XRD measurements performed on as deposited samples show the presence of an amorphous structure what ever the composition of the coating. In order to crystallize the La 2 NiO 4 phase, annealing at 1173 K for 2 h were applied according to a previous study [START_REF] Fondard | Synthesis and characterization of La 2 NiO 4 + δ coatings deposited by reactive magnetron sputtering using plasma emission monitoring[END_REF] with samples presenting a La/Ni ratio of about 2. Fig. 5 pre sents the XRD patterns of annealed coatings deposited on alumina sub strates at 1173 K for 2 h for the different total pressures with a La/Ni ratio close to 2. The increase of the partial pressure changes the phase content of the coating according to the slight drift of the coating compo sition. For these experimental conditions, high pressure favors the for mation of La Ni O perovskite phases (La 4 Ni 3 O 10 and/or La 3 Ni 2 O 7 ) and lanthanum oxide in addition to La 2 NiO 4 desired structure for a La/Ni ratio close to 2. These perovskite phases are normally formed when the La/Ni ratio is lower, but the La 2 O 3 compound, which should be formed at higher ratio, is present. The occurrence of La 4 Ni 3 O 10 together with La 2 NiO 4 and La 2 O 3 was already observed with high oxygen partial pressures by others [START_REF] Zinkevich | Thermodynamic analysis of the ternary La-Ni-O[END_REF] and could explain our results at 1.9 and 4.8 Pa. The intensity of lanthanum oxide peak after deposition at 3.2 and 4.8 Pa is consistent with the slight excess of La (La/Ni = 2.12 ± 0.10 and 2.16 ± 0.04 at 3.2 and 4.8 Pa respectively). Intensity of La 2 O 3 peak is higher at 4.8 Pa because high amount of nickel is present in La 4 Ni 3 O 10 and/or La 3 Ni 2 O 7 structures. It also could be ascribed either to a gradient of composition in the thickness of the coating or more probably to a gradient in the width of the columns, the external surface of the col umns being probably depleted in Ni, which should also explain the quite large amount of La 2 O 3 in the coatings deposited at high pressure which also develop the higher specific surface area.

Deposition of cathode layer with porosity gradient

Previous studies have shown that dense coatings deposited at low pressure (0.4 Pa) reproduce the morphology of alumina and YSZ sub strates [START_REF] Fondard | Synthesis and characterization of La 2 NiO 4 + δ coatings deposited by reactive magnetron sputtering using plasma emission monitoring[END_REF]. According to the Thornton's diagram revised by Anders [START_REF] Anders | A structure zone diagram including plasma-based deposition and ion etching[END_REF], the morphology becomes less and less dense with decreasing the average energy of impinging species, e.g. by increasing the deposition pressure (Fig. 6a,b). Porous morphology is then expected to increase the exchange surface between the cathode and the gas phase. Neverthe less, the adhesion of porous coatings seems to be low. From the literature, the use of a thin and dense interfacial cathode layer is sup posed to improve the adhesion of the cathode by increasing the contact between the porous cathode and electrolyte layer [START_REF] Hildenbrand | Influence of configuration and microstructure on performance of La 2 NiO 4+δ intermediate-temperature solid oxide fuel cells cathodes[END_REF]. For all these rea sons, it was decided to deposit a cathode with porosity gradient with a general La/Ni ratio of about 2 by increasing the pressure during the de position stage according to the results presented earlier. YSZ pellets and Ni YSZ/YSZ/GDC commercial anode supported half cells were then cov ered by a gradient cathode coating. Table 2 summarizes the deposition parameters of those coatings. EDS measurements performed on the top of these as deposited and annealed samples confirmed a La/Ni ratio close to 2 (1.87 ± 0.04 and 1.95 ± 0.05 for as deposited and annealed coatings respectively).

Fig. 6c andd present the morphology of the coating deposited on YSZ pellet after annealing at 1173 K during 2 h from top view and cross section respectively. The desired morphology is obtained on this sample. The top view shows an island like growth of the gradient coating with cracks like separations of the islands corresponding coarsely to the size of the YSZ grains and expected to contribute to the increase of surface exchange between the gas phase and the cathode material.

Electrical and electrochemical tests

Electrical analyses

In order to assess the characteristics of the well crystallized films, electrical measurements were performed implementing a four point probe method on annealed samples. It is compared with the litera ture data [START_REF] Boehm | Oxygen diffusion and transport properties in non-stoichiometric Ln 2 x NiO 4+δ oxides[END_REF][START_REF] Dailly | Perovskite and A 2 MO 4 -type oxides as new cathode materials for protonic solid oxide fuel cells[END_REF][START_REF] Coddet | Planar Solid Oxide Fuel Cell: Electrolyte Deposited by Reactive Magnetron Sputtering and Cell Test[END_REF] and with dense cathode layers presented in a pre vious paper [START_REF] Fondard | Synthesis and characterization of La 2 NiO 4 + δ coatings deposited by reactive magnetron sputtering using plasma emission monitoring[END_REF]. Fig. 7 highlights that, despite a lower conductivity at room temperature of the gradient cathode, its conductivity around 973 1073 K (30 60 S•cm) is closed to that of bulk cathodes of the literature.

Complete cell tests

Previous studies proved that either air or nitrogen conditions gas crystallization treatments were not suitable for this last step of the com plete cell elaboration. Indeed, air conditions treatment at 1173 K deteri orated the anodic side of the cell and nitrogen conditions did not allow the targeted lanthanum nickelate phase. Thus, cathode materials were crystallized prior to the test in the single cell test setup to obtain the convenient La 2 NiO 4 structure. It was performed by increasing the cell temperature up to 1073 K for 6.5 h by introducing on the cathode side 120 sccm O 2 and on the anode side a 6 sccm humidified H 2 114 sccm N 2 gas mixture. Fig. 8 presents structure comparison of Ni/YSZ/YSZ/ GDC cells covered with the porosity gradient LNO layer (p LNO) and with a dense LNO layer produced at 0.4 Pa (d LNO). Due to a thin cath ode layer, GDC substrate's structure is identified. As deposited samples are amorphous. XRD measurements of the crystallized coatings identify the same structure of these samples. The same tetragonal lanthanum nickelate phase is identified with a very low amount of lanthanum oxide impurities. These analyses prove that the crystallization method is suitable in these conditions to crystallize the targeted phase without major impurities.

The anode reduction was then performed at 973 K with a gas flow evolving linearly from 6 to 120 sccm of humidified H 2 on the anode side while 120 sccm O 2 was injected on the cathode side. The Open Circuit Voltage (OCV) was measured during the reduction stage (Fig. 9). The shape of the reduction curves is quite similar for p LNO and d LNO cells. Maximal OCV values were measured at 0.9 V for both cells. This value is quite lower to the theoretical value of 1.05 V at this temperature and proves that it depends mostly on the electrolyte tightness. Increasing oxygen flow rate has no significant effect on the cell's OCV.

When, the OCV is stable, complete cells tests begin. Fig. 10 presents voltammetry tests of these complete cells at 973 K to target the IT SOFC's application domain. These measurements indicate a maximum power density of 71 and 51 mW/cm 2 for porous and dense cathodes, re spectively. It increases up to about 140 mW/cm 2 for the porous cathode when the test is performed at 1073 K. In the literature, anode supported cells with electrolyte manufactured by reactive magnetron sputtering process (RMS) reach a power density of 410 mW/cm 2 at 973 K [START_REF] Wang | Preparation of YSZ films by magnetron sputtering for anode-supported SOFC[END_REF] and 600 mW/cm 2 at 1073 K [START_REF] Coddet | Planar Solid Oxide Fuel Cell: Electrolyte Deposited by Reactive Magnetron Sputtering and Cell Test[END_REF]. Nevertheless, no complete cells pre senting cathode manufactured by RMS were analyzed in complete cell tests. Some improvements of the cell microstructure and reduction of the thickness have to be performed in order to obtain higher perfor mances. These results prove that the porosity gradient is an efficient way to improve the performances of the cell. Indeed, despite the perfor mances are in the same order of magnitude, power densities are improved to 28% by replacing dense cathode by a more porous one. Cathode microstructure should also play an important role in the performances of the cells. This may increase the oxygen reactive area.

To explain the rather low performances of the cells (71 and 51 mW/cm 2 for porous and dense cathodes), Electrochemical Imped ance Spectroscopy (EIS) characterizations were performed on these samples. Impedance of a circuit presents real (Z') and imaginary (Z") parts as shown in (Eq. ( 2)).

Z ω ð Þ Re Z ð Þ þ jIm Z ð Þ Z 0 þ jZ ″ ð2Þ
Impedance is usually represented in complex plan of Nyquist from the relation (Eq. ( 3)).

-Z 0 f Z ″ ð3Þ
Fig. 11 presents Nyquist plots of the complete cells under OCV. These diagrams were fitted using Z View software. Modeled data are repre sented by lines in the figures while experimental measurements are represented by points. Four contributions characteristic of different phenomena appearing were identified in high, medium and low frequency ranges. Each contribution can be modeled by a sum of ele mentary circuits (resistance, capacitance, and inductance). Constant Phase Element function (CPE) can be used to better fit the experiments values. This function can act as a resistance, capacitance or inductance and is more and more used with electrochemical phenomena. Resis tance and associated capacitance values were extracted from these fits. Nyquist curves were fitted by the same equivalent circuits. Their shapes are similar, only the different resistances varying. Total resis tance of the "p LNO" sample is lower than that of the "d LNO" sample, explaining performances measured on the different samples (Fig. 9). These resistances remain very high and explain the lower output power densities of the cells compared to literature data (71 mW/cm 2 and 600 mW/cm 2 respectively). The resistance at high frequencies (serial resistance), usually depending on the electrolyte resistance, re mains identical for both since the electrolyte coatings were deposited during a same run. The characteristics attributed for medium or low fre quencies underline the different electrochemical phenomena occur rence on these samples. Using the Schouler method [START_REF] Schouler | Electrocatalysis and inductive effects at the gas, Pt/stabilized zirconia interface[END_REF], resistance and CPE are each assigned to the resistance and capacitance that can be correlated to a specific electrochemical process. On the basis of the fitted data, the equivalent capacitance and the frequency relaxation of each contribution were calculated using relations (Eqs. ( 4) and ( 5)).

C eq Re

1 n ð Þ n à C 1 n ð4Þ
f n 1 2π C eq n R n À Á 1 n : ð5Þ
Table 3 presents the parameters of the different phenomena for each sample. High, Medium and Low frequency phenomenon are named by 1 (R 1 , Ceq 1 , f 1 ) and 2 (R 2 , Ceq 2 , f 2 ) and 3 (R 3 , Ceq 3 , f 3 ) respectively. Polarization Resistance (R p ) is calculated by the sum of R 2 and R 3 . ASR represents the complete cell resistance. Complete cell resistance ASR are much higher than requirements for IT SOFCs (i.e. 0.8 Ω•cm 2 ). These high values explain the poor performances obtained with these cells at 973 K. Numerous limitations should be induced by the use of several layers. The compatibility of these materials and structures has to be optimized in order to improve the performances by decreasing re sistances. The low frequency range (LF) is characterized by high capac itance values, Ceq ≈ 1 10 F•cm -2 [START_REF] Philippeau | Comparative study of electrochemical properties of mixed conducting Ln 2 NiO 4+δ (Ln = La, Pr and Nd) and La 0.6 Sr 0.4 Fe 0.8 Co 0.2 O 3 δ as SOFC cathodes associated to Ce 0.9 Gd 0.1 O 2 δ , La 0.8 Sr 0.2 Ga 0.8 Mg 0.2 O 3 δ and La 9 Sr 1 Si 6 O 26.5 electrolytes[END_REF][START_REF] Mogni | Oxygen reduction reaction on ruddlesden-popper phases studied by impedance spectroscopy[END_REF], and it was identified as the result of gaseous diffusion through the electrode. The capacitance of the medium frequency contribution (MF) is found to be larger, Ceq ≈ 10 -3 10 -1 F•cm -2 . The source of this contribution is more com plicated to identify; it has been assigned as Oxygen Reduction Reaction (ORR) occurring at the electrode/gas interface in literature [START_REF] Philippeau | Comparative study of electrochemical properties of mixed conducting Ln 2 NiO 4+δ (Ln = La, Pr and Nd) and La 0.6 Sr 0.4 Fe 0.8 Co 0.2 O 3 δ as SOFC cathodes associated to Ce 0.9 Gd 0.1 O 2 δ , La 0.8 Sr 0.2 Ga 0.8 Mg 0.2 O 3 δ and La 9 Sr 1 Si 6 O 26.5 electrolytes[END_REF][START_REF] Hansen | A-site deficient (La 0.6 Sr 0.4 ) 1 s Fe 0[END_REF] or ionic transfers at the electrode/electrolyte interface [START_REF] Dailly | Perovskite and A 2 MO 4 -type oxides as new cathode materials for protonic solid oxide fuel cells[END_REF].

Because cathode material is the only variable parameter, polariza tion resistance should be due to the cathode layer. Equivalent capaci tances and relaxation frequencies are close (10 -3 F•cm -2 , 10 4 Hz and 0.1 F•cm -2 , 1 Hz for the MF and LF phenomena respectively). These values indicate that same electrochemical processes happen. Resistance values of the MF and LF phenomena are significantly improved by this new cathode architecture (20% and 30% gain for MF and LF phenomena respectively). The most important gain happens at LF, corresponding to gaseous diffusion through cathode layer. This indicates the realization of coating with higher porosity. From these two contributions at MF and LF, an electrode polarization resistance of 3.75 and 2.78 Ω/cm 2 was determined for "d LNO" and "p LNO" respectively. Nevertheless, the specifications of fuel cell electrodes have to be lower than 0.5 Ω/cm 2 . The high resistances obtained on samples are too high because of not optimized morphology even if making a porosity gradient thin cathode seems to be a promising option. Analyses of structures and microstruc tures of cathode and electrolyte/cathode interface were then performed to point differences between samples and to explain results. Fig. 12 shows SEM observations of surface (a) and the brittle cross section (b, c, d) of the complete cell after electrical tests. Surface condition of every sample is not completely smooth because of the anode substrate morphology and the high pressure during the last step of the cathode deposition. Interface between the GDC interlayer and the cathode layer is improved in the "p LNO" sample (Fig. 12c) in comparison with the "d LNO" cathode (Fig. 12d). This can explain the best resistance at medium frequencies (20%) noticed with EIS characterization. It is then obvious that the p LNO coating is less tight than the d LNO coating. It fa cilitates the oxygen permeation through the cathode layer and should explain the lower resistance (30%) at low frequencies. No differences can be pointed between d LNO and p LNO samples at low magnification in spite of predicted microstructures. Indeed, "island shape" areas are in minority on the surface. Most of the surface is not modified. This fact should explain the poor performances obtain because active surface is smaller than wished. A combination of lower temperatures with pres sure could explain the different microstructures. Higher magnification permits to underline differences between the two cathodes (Fig. 12c andd). Interface between the GDC layer and the cathode layer is improved in the "p LNO" sample.

Conclusion

A porosity gradient La Ni O coating was deposited by co sputtering of La and Ni metallic targets in the presence of reactive argon oxygen gas mixtures using Plasma Emission Monitoring by gradually increasing the pressure during the deposition stage. Increasing the pressure in duces the decrease of the unstable domain width and change the opti mal sputtering conditions to obtain La 2 NiO 4 structure (regulation setpoint and current on nickel target). Moreover, higher total pressure change the phase occurrence and allows the presence of both La 2 O 3 and La 3 Ni 2 O 7 and La 2 NiO 4 phases, resulted by a possible increase of re sistance. Increasing the pressure also leads to an increase of the porosity of the coatings until obtaining "island shape" of crystallized coatings. Four point probe measurements show the interesting electrical behav ior in IT SOFCs utilization domain of porosity gradient cathode coatings. Ni YSZ/YSZ/GDC/LNO complete cells were then built using dense LNO and gradient cathode LNO and were tested in a cell bench. In order to avoid the deterioration of the cell's component, the crystallization of the cathode and the reduction of the anode were performed during the complete cell tests, allowing to obtain the convenient La 2 NiO 4 struc ture. Nevertheless, the performances are lower than expected with those materials. Impedance measurements allow to point the reasons of these low performances (71 mW/cm 2 ), each layer of the cell presents high resistance but the most important remains the cathode where po larization resistance is three times higher than that of the electrolyte. Nevertheless, it is also shown that the use of a porosity gradient cathode is the convenient way to improve the cell performance. The low perfor mances are certainly induced by the cathode thickness, in future work, it should be developed cathode architected with thickness greater than 2.5 μm.

Fig. 1 .

 1 Fig. 1. Scheme of the deposition setup.

Fig. 3

 3 presents the evolution of the 394.91 nm emission line intensity vs. oxygen flow rate at total pressures varying from 0.4 to 4.8 Pa. Work ing pressures of 0.4 and 1.9 Pa are obtained by increasing the argon flow rate from 50 to 200 sccm with the highest pumping speed. Working pressures of 3.2 and 4.8 Pa are obtained by throttling the suction pipe and also by increasing the argon flow rate from 50 to 200 sccm. Stable sputtering conditions, represented by full symbols, are obtained by fix ing different oxygen flow rates while unstable sputtering conditions, pointed by open symbols, are collected by using the PEM system to maintain the optical intensity at different values. With pure argon, the optical intensity is maximal and fixed at 100%. When increasing oxygen flow rate, optical emission slightly decreases due to the target poison ing.

Fig. 2 .

 2 Fig. 2. Stability of the La-O and Ni-O systems at a pressure of 1.9 Pa.

Fig. 3 .

 3 Fig. 3. Influence of the pressure on the instability of sputtering conditions. Hysteresis loop oxygen flow rate vs. 395 nm La emission line intensity. Stable sputtering conditions (full symbols) and unstable sputtering conditions by PEM (open symbols).

Fig. 4 .

 4 Fig. 4. Evolution of atomic composition ratio La/Ni measured by EDS as a function of current dissipated on the Ni target (I La = 2.5 A) at different total pressures.

Fig. 5 .

 5 Fig. 5. XRD spectra as a function of total pressure after annealing at 1173 K for 2 h.

Fig. 6 .Fig. 7 .

 67 Fig. 6. SEM micrographs of LNO coatings deposited on YSZ substrates after annealing at 1173 K for 2 h. Brittle fracture cross section of samples deposited at 0.4 Pa (a), and at 4.8 Pa (b). Top view (c) and brittle cross section (d) of the porosity gradient coatings.

Fig. 8 .

 8 Fig. 8. XRD measurements of p-LNO and d-LNO complete cells as-deposited and after tests.

Fig. 9 .

 9 Fig. 9. Evolution of p-LNO and d-LNO complete cells' Open circuit Voltage (OCV) during reduction of anode layer at 973 K.

Fig. 10 .

 10 Fig. 10. Voltametry tests of p-LNO and d-LNO complete cells at different temperatures.

Fig. 11 .

 11 Fig. 11. Nyquist plots of p-LNO and d-LNO complete cells. Models are represented by lines. Experimental results are represented by symbols. Logarithm of frequency are indicated in the figure.

  with R: electrical resistance, n: decentering angle of the Constant Phase Element function, C: capacitance of the phenomenon.

Fig. 12 .

 12 Fig. 12. SEM view of surface (a) and brittle fracture cross section complete cells with p-LNO (b, c) and d-LNO (d) cathode after electrical tests with different magnifications.

Table 1

 1 Evolution of the hysteresis domain with the total pressure.

	Total pressure (Pa)	Oxygen flow rate to ESM → RSM (sccm)	Oxygen flow rate to RSM → ESM (sccm)	Width hysteresis (sccm)
	0.4	6.4	2.5	3.9
	1.9	4.7	1.8	2.9
	3.2	4.1	1.3	2.8
	4.8	3.8	1.2	2.6

Table 3

 3 Parameters determined by electrochemical impedance spectroscopy.

	Domain	Phenomena	p-LNO	d-LNO
	HF	R 1 (Ω•cm 2 )	1.01	1.08
		R 2 (Ω•cm 2 )	0.63	0.79
	MF	Ceq 2 (F•cm 2 )	8.1 10 4	6.9 10 4
		f 2 (Hz)	2.3 10 4	3.2 10 4
		R 3 (Ω•cm 2 )	2.12	2.99
	LF	Ceq 3 (F•cm 2 )	4.0 10 1	3.0 10 1
		f 3 (Hz)	1.2 10 0	8.8 10 1
	MF + LF	R p (Ω•cm 2 )	2.75	3.78
	HF + MF + LF	ASR (Ω•cm 2 )	3.76	4.86

Acknowledgments

The authors thank the Pays de Montbéliard Agglomeration (n°13/ 083) for their financial support during this study.