Alex Klinkhamer

Ali Ebnenasir
email: aebnenas@mtu.edu

On the Complexity of Adding Convergence

Keywords: Self-Stabilization, Convergence, NP-Completeness

This paper investigates the complexity of designing Self-Stabilizing (SS) distributed programs, where an SS program meets two properties, namely closure and convergence. Convergence requires that, from any state, the computations of an SS program reach a set of legitimate states (a.k.a. invariant). Upon reaching a legitimate state, the computations of an SS program remain in the set of legitimate states as long as no faults occur; i.e., Closure. We illustrate that, in general, the problem of augmenting a distributed program with convergence, i.e., adding convergence, is NP-complete (in the size of its state space). An implication of our NP-completeness result is the hardness of adding nonmasking fault tolerance to distributed programs, which has been an open problem for the past decade.

Introduction

Today's distributed programs are subject to a variety of transient faults due to their inherent complexity, human errors and environmental factors, where transient faults perturb program state without causing any permanent damage (e.g., bad initialization, loss of coordination, soft errors). Distributed applications should guarantee service availability even in the presence of faults. However, providing global recovery in distributed programs is difficult in part due to [START_REF] Dijkstra | Self-stabilizing systems in spite of distributed control[END_REF] no central point of control/administration; (2) lack of knowledge about the global state of the program by program processes/components, and (3) the need for global recovery using only the local actions of processes. To design programs that recover from any arbitrary configuration/state without human intervention, Dijkstra [START_REF] Dijkstra | Self-stabilizing systems in spite of distributed control[END_REF] proposed self-stabilization as a property of distributed programs. A Self-Stabilizing (SS) program meets two requirements, namely closure and convergence. Convergence requires that, from any state, the computations of an SS program reach a set of legitimate states (a.k.a. program invariant). Upon reaching an invariant state, the computations of an SS program remain in its invariant as long as no faults occur; i.e., Closure. Indeed, self-stabilization is a special case of nonmasking fault tolerance [START_REF] Arora | A foundation of fault-tolerant computing[END_REF][START_REF] Arora | Closure and convergence: A foundation of faulttolerant computing[END_REF], where instead of providing recovery from any state, designers identify a subset of the state space from where recovery to invariant can be provided. While there are several approaches in the literature for the design of SS algorithms for specific problems, we are not aware of a general case complexity analysis of designing SS programs.

Several researchers have investigated the problem of adding nonmasking fault tolerance to programs [START_REF] Dijkstra | Self-stabilizing systems in spite of distributed control[END_REF][START_REF] Arora | A foundation of fault-tolerant computing[END_REF][START_REF] Liu | Transformation of programs for fault-tolerance[END_REF][START_REF] Arora | Closure and convergence: A foundation of faulttolerant computing[END_REF][START_REF] Arora | Constraint satisfaction as a basis for designing nonmasking fault-tolerant systems[END_REF][START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF]. For instance, Liu and Joseph [START_REF] Liu | Transformation of programs for fault-tolerance[END_REF] present a method for the transformation of an intolerant program to a fault-tolerant version thereof by going through a set of refinement steps. Arora and Gouda [START_REF] Arora | A foundation of fault-tolerant computing[END_REF][START_REF] Arora | Closure and convergence: A foundation of faulttolerant computing[END_REF] use the notions of closure and convergence to define three levels of fault tolerance based on the extent to which safety and liveness specifications [START_REF] Alpern | Defining liveness[END_REF] are satisfied in the presence of faults. In their setting, a failsafe fault-tolerant program ensures its safety at all times even if faults occur, whereas, in the presence of faults, a nonmasking program provides recovery to its invariant; no guarantees on meeting safety during recovery. A masking fault-tolerant program is both failsafe and nonmasking. Arora et al. [START_REF] Arora | Constraint satisfaction as a basis for designing nonmasking fault-tolerant systems[END_REF] design nonmasking fault tolerance by creating a dependency graph of the local constraints of program processes, and by illustrating how these constraints should be satisfied so global recovery is achieved. Kulkarni and Arora [START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF] demonstrate that adding failsafe/nonmasking/masking fault tolerance to high atomicity programs can be done in polynomial-time in program's state space, where a high atomicity program can read/write all program variables in an atomic step. Nonetheless, they illustrate that adding masking fault tolerance to low atomicity programs -where processes have read/write restrictions with respect to variables of other processes -is NP-complete (in the size of the state space). 1 Moreover, Kulkarni and Ebnenasir [START_REF] Sandeep | Complexity issues in automated synthesis of failsafe fault-tolerance[END_REF] show that adding failsafe fault tolerance to low atomicity programs is also an NP-complete problem. Nonetheless, while adding nonmasking fault tolerance is known to be in NP, no polynomial-time algorithms are known for efficient design of nonmasking fault tolerance for low atomicity programs; neither has there been a proof of NP-hardness!

In this paper, we illustrate that adding nonmasking fault tolerance to low atomicity programs is NP-complete (in the size of the state space). Our hardness proof is based on a reduction from the 3-SAT problem [START_REF] Gary | Computers and Intractability: A Guide to the Theory of NP-Completeness[END_REF] to the problem of adding convergence to non-stabilizing programs. Since adding convergence is a special case of adding nonmasking fault tolerance, it follows that, in general, it is unlikely that adding nonmasking fault tolerance to low atomicity programs can be done efficiently (unless P = N P ). The significance of our NP-hardness proof is multi-fold. First, our proof provides a solution for a problem that has been open for more than a decade. Second, illustrating the NP-completeness of adding convergence is particularly important since the proof requires the construction of the entire state space of the instance of the problem of adding convergence, yet such a mapping should be polynomial in the size of the instance of the source NP-complete problem (in our case 3-SAT). Devising such a reduction has been 1 Low atomicity programs enable the modeling of distributed programs.

another open problem in the literature. Third, our proof illustrates that even if we have a process in a program that can atomically read the global state of the program and can update its own local state, the addition of recovery still remains a hard problem. Fourth, the presented hardness proof lays the foundation for the design of a new family of synthesis algorithms inspired by the DPLL algorithm [START_REF] Davis | A computing procedure for quantification theory[END_REF], which we are currently investigating. We conjecture that such synthesis algorithms will be more efficient than existing methods for SAT-based synthesis of fault tolerance [START_REF] Ebnenasir | SAT-based synthesis of fault-tolerance[END_REF] where one formulates the sub-problems of adding fault tolerance in terms of CNF formulas and invokes off-the-shelf SAT solvers. Organization. Section 2 presents the basic concepts of programs, faults and fault tolerance. Section 3 formally states the problem of adding nonmasking fault tolerance and convergence. Section 4 illustrates that adding convergence in particular and adding nonmasking fault tolerance in general are NP-complete. Section 5 discusses related work. Finally, Section 6 makes concluding remarks and discusses future work.

Preliminaries

In this section, we present the formal definitions of programs, faults, fault tolerance and self-stabilization, and our distribution model (adapted from [START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF]). Programs are defined in terms of their set of variables, their transitions and their processes. The definitions of fault tolerance and self-stabilization is adapted from [START_REF] Dijkstra | Self-stabilizing systems in spite of distributed control[END_REF][START_REF] Arora | Closure and convergence: A foundation of faulttolerant computing[END_REF][START_REF] Gouda | The triumph and tribulation of system stabilization[END_REF][START_REF] Gouda | The theory of weak stabilization[END_REF]. For ease of presentation, we use a simplified version of Dijkstra's token ring protocol [START_REF] Dijkstra | Self-stabilizing systems in spite of distributed control[END_REF] as a running example. Programs as (non-deterministic) finite-state machines. A program in our setting is a representation of any system that can be captured by a (finite-state) non-deterministic state machine (e.g., network protocols). Formally, a program p is a tuple V p , δ p , Π p , T p of a finite set V p of variables, a set δ p of transitions, a finite set Π p of k processes, where k ≥ 1, and a topology T p . Each variable

v i ∈ V p , for i ∈ N m where N m = {0, 1, • • • , m -1} and m > 0, has a finite non- empty domain D i . A state s of p is a valuation d 0 , d 1 , • • • , d m-1 of variables v 0 , v 1 , • • • , v m-1
, where d i ∈ D i . A transition t is an ordered pair of states, denoted (s 0 , s 1 ), where s 0 is the source and s 1 is the target/destination state of t. A deadlock state is a state with no outgoing transitions. For a variable v and a state s, v(s) denotes the value of v in s. The state space of p, denoted S p , is the set of all possible states of p, and |S p | denotes the size of S p . A state predicate is any subset of S p specified as a Boolean expression over V p . We say a state predicate X holds in a state s (respectively, s ∈ X) if and only if (iff ) X evaluates to true at s. Read/Write model. We adopt a shared memory model [START_REF] Lamport | Handbook of Theoretical Computer Science: Chapter 18, Distributed Computing: Models and Methods[END_REF] since reasoning in a shared memory setting is easier, and several (correctness-preserving) transformations [START_REF] Nesterenko | Stabilization-preserving atomicity refinement[END_REF][START_REF] Demirbas | Convergence refinement[END_REF] exist for the refinement of shared memory fault-tolerant programs to their message-passing versions. We model the topological constraints (denoted T p ) of a program p by a set of read and write restrictions imposed on variables that identify the locality of each process. Specifically, we consider a subset of variables in V p that a process P j (j ∈ N k ) can write, denoted w j , and a subset of variables that P j is allowed to read, denoted r j . We assume that for each process P j , w j ⊆ r j ; i.e., if a process can write a variable, then it can also read that variable. Impact of read/write restrictions. Every transition of a process P j belongs to a group of transitions due to the inability of P j in reading variables that are not in r j . Consider two processes P 0 and P 1 each having a Boolean variable that is not readable for the other process. That is, P 0 (respectively, P 1 ) can read and write x 0 (respectively, x 1 ), but cannot read x 1 (respectively, x 0 ). Let x 0 , x 1 denote a state of this program. Now, if P 0 writes x 0 in a transition ( 0, 0 , 1, 0 ), then P 0 has to consider the possibility of x 1 being 1 when it updates x 0 from 0 to 1. As such, executing an action in which the value of x 0 is changed from 0 to 1 is captured by the fact that a group of two transitions ( 0, 0 , 1, 0 ) and ( 0, 1 , 1, 1 ) is included in P 0 . In general, a transition is included in the set of transitions of a process iff its associated group of transitions is included. Formally, any two transitions (s 0 , s 1 ) and (s 0 , s 1 ) in a group of transitions formed due to the read restrictions of a process P j , denoted r j , meet the following constraints:

∀v : v ∈ r j : (v(s 0 ) = v(s 0 )) ∧ (v(s 1 ) = v(s 1 )) and ∀v : v / ∈ r j : (v(s 0 ) = v(s 1 )) ∧ (v(s 0 ) = v(s 1 )).
Due to read/write restrictions, a process P j (j ∈ N k ) includes a set of transition groups P j = {g j0 , g j1 , • • • , g j(max-1) } created due to read restrictions r j , where max ≥ 1. Due to write restrictions w j , no transition group g ji (i ∈ N max ) can have a transition (s 0 , s 1 ) that updates a variable v / ∈ w j . Thus, the set of transitions δ p of a program p is equal to the union of the transition groups of its processes; i.e., δ p = ∪ k-1 j=0 P j . (It is known that the total number of groups is polynomial in |S p | [START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF]). We use p and δ p interchangeably.

To simplify the specification of δ p for designers, we use Dijkstra's guarded commands language [START_REF] Dijkstra | A Discipline of Programming[END_REF] as a shorthand for representing the set of program transitions. A guarded command (action) is of the form grd → stmt, and includes a set of transitions (s 0 , s 1 ) such that the predicate grd holds in s 0 and the atomic execution of the statement stmt results in state s 1 . An action grd → stmt is enabled in a state s iff grd holds at s. A process P j ∈ Π p is enabled in s iff there exists an action of P j that is enabled at s. Example: Token Ring (TR). The Token Ring (TR) program (adapted from [START_REF] Dijkstra | Self-stabilizing systems in spite of distributed control[END_REF]) includes three processes {P 0 , P 1 , P 2 } each with an integer variable x j , where j ∈ N 3 , with a domain {0, 1, 2}. The process P 0 has the following action (addition and subtraction are in modulo 3):

A 0 : (x 0 = x 2 ) -→ x 0 := x 2 + 1
When the values of x 0 and x 2 are equal, P 0 increments x 0 by one. We use the following parametric action to represent the actions of processes P j , for 1 ≤ j ≤ 2:

A j : (x j = x (j-1) ) -→ x j := x (j-1)
Each process P j copies x j-1 only if x j = x j-1 , where j = 1, 2. By definition, process P j has a token iff x j = x j-1 . Process P 0 has a token iff x 0 = x 2 . We define a state predicate I T R that captures the set of states in which only one token exists, where

I T R is ((x 0 = x 1 ) ∧ (x 1 = x 2 )) ∨ ((x 1 = x 0 ) ∧ (x 1 = x 2 )) ∨ ((x 0 = x 1 ) ∧ (x 1 = x 2 ))
Each process P j (1 ≤ j ≤ 2) is allowed to read variables x j-1 and x j , but can write only x j . Process P 0 is permitted to read x 2 and x 0 and can write only x 0 . Thus, since a process P j is unable to read one variable (with a domain of three values), each group associated with an action A j includes three transitions. For a TR protocol with n processes and with n values in the domain of each variable x j , each group includes n n-2 transitions. Computations. Intuitively, a computation of a program p = V p , δ p , Π p , T p is an interleaving of its actions. Formally, a computation of p is a sequence σ = s 0 , s 1 , • • • of states that satisfies the following conditions: (1) for each transition (s i , s i+1 ) in σ, where i ≥ 0, there exists an action grd → stmt in some process P j ∈ Π p such that grd holds at s i and the execution of stmt at s i yields s i+1 , and (2) σ is maximal in that either σ is infinite or if it is finite, then σ reaches a state s f where no action is enabled. A computation prefix of a program p is a finite sequence σ = s 0 , s 1 , • • • , s z of states, where z > 0, such that each transition (s i , s i+1 ) in σ (i ∈ N z ) belongs to some action grd → stmt in some process P j ∈ Π p . The projection of a program p on a non-empty state predicate X, denoted as

δ p |X, is the program V p , {(s 0 , s 1 ) : (s 0 , s 1 ) ∈ δ p ∧ s 0 , s 1 ∈ X}, Π p , T p .
In other words, δ p |X consists of transitions of p that start in X and end in X. Closure and invariant. A state predicate X is closed in an action grd → stmt iff executing stmt from any state s ∈ (X ∧ grd) results in a state in X. We say a state predicate X is closed in a program p iff X is closed in every action of p. In other words, closure [START_REF] Gouda | The theory of weak stabilization[END_REF] requires that every computation of p starting in X remains in X. We say a state predicate I is an invariant of p iff I is closed in p. TR Example. Starting from a state in the predicate I T R , the TR protocol generates an infinite sequence of states, where all reached states belong to I T R . Faults. Intuitively, we capture the impact of faults on a program as state perturbations. Formally, a class of faults f for a program p = V p , δ p , Π p , T p is a subset of S p × S p . We use p[]f to denote the transitions obtained by taking the union of the transitions in δ p and the transitions in f . We say that a state predicate T is an f -span (read as fault-span) of p from a state predicate I iff the following two conditions are satisfied: (1) I ⊆ T , and (2) T is closed in p[]f . Observe that for all computations of p that start in I, the state predicate T is a superset of I in S p up to which the state of p may be perturbed by the occurrence of f transitions. We say that a sequence of states, σ = s 0 , s 1 , ... is a computation of p in the presence of f iff the following conditions are satisfied: (1) ∀j : j > 0 : (s j-1 , s j ) ∈ (p[]f );

(2) if σ is finite and terminates in state s l , then there is no state s such that (s l , s) ∈ δ p , and (3) ∃n : n ≥ 0 : (∀j : j > n : (s j-1 , s j ) ∈ δ p ). The first requirement captures that in each step, either a program transition or a fault transition is executed. The second requirement captures that faults do not have to execute. That is, if the only transition that starts from s l is a fault transition (s l , s f ) then as far as the program is concerned, s l is still a deadlock state because the program does not have control over the execution of (s l , s f ); i.e., (s l , s f ) may or may not be executed. Finally, the third requirement captures that the number of fault occurrences in a computation is finite. This requirement is the same as that made in previous work (e.g., [START_REF] Dijkstra | Self-stabilizing systems in spite of distributed control[END_REF][START_REF] Arora | Designing masking fault-tolerance via nonmasking fault-tolerance[END_REF][START_REF] Arora | Closure and convergence: A foundation of faulttolerant computing[END_REF][START_REF] Varghese | Self-stabilization by local checking and correction[END_REF]) to ensure that eventually recovery can occur. The same way we use guarded commands to represent program transitions, we use them to specify fault transitions. That is, the impact of faults can be captured as a set of actions that update program variables. TR Example. The TR protocol is subject to transient faults that can perturb its state to an arbitrary state. For instance, the following action captures the impact of faults on x 0 , where | denotes non-deterministic assignment of values to x 0 :

F 0 : true -→ x 0 := 0|1|2;
The impact of faults on x 1 and x 2 are captured with two actions F 1 and F 2 symmetric to F 0 . Nonmasking fault-tolerance and self-stabilization. Let I be a state predicate closed in a program p and f be a class of faults. We say that p is nonmasking f -tolerant from I iff there exists an f -span of p from I, denoted T , such that T converges to I in p. That is, from any state s 0 ∈ T , every computation of p that starts in s 0 reaches a state where I holds. We say that p is self-stabilizing from I iff p is nonmasking f -tolerant from I, where T = true. That is, the f -span of p is equal to S p , and convergence to I is guaranteed from any state in S p . Notice that, to design recovery, one has to ensure that no deadlock states exist in T -I, and no non-progress cycles exist in Note. In this paper, we analyze the complexity of adding convergence under the assumption of no fairness.

δ p | (T -I). A non-progress cycle (a.k.a. livelock) in δ p | (T -I) is a sequence of states σ = s 0 , s 1 , • • • , s m , s 0 , where m ≥ 0, (s i , s i⊕1 ) ∈ δ p and s i ∈ (T -I), for i ∈ N

Problem Statement

In this section, we represent the problem of adding nonmasking fault-tolerance from [START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF]. Consider a fault-intolerant program p = V p , δ p , Π p , T p , a class of faults f , and a state predicate I, where I is closed in p. Our objective is to generate a revised version of p, denoted p , such that p is nonmasking f -tolerant from an invariant I . To separate fault tolerance from functional concerns, we would like to preserve the behaviors of p in the absence of f during the addition of fault tolerance. For this reason, during the synthesis of p from p, no states (respectively, transitions) are added to I (respectively, δ p |I). Thus, we have I ⊆ I and p |I ⊆ p|I . This way, if p starts in I in the absence of faults, then p will preserve the correctness of p; i.e., the added recovery does not interfere with normal functionalities of p in the absence of faults. Moreover, if p starts in a state outside I , then only recovery to I will be provided by p . Thus, we formally state the problem as follows:

Hardness Results

In this section, we illustrate that adding convergence to low atomicity programs is NP-complete (in the size of the state space). This hardness result implies the hardness of general case addition of nonmasking fault tolerance to low atomicity programs (i.e., Problem 2). Specifically, we demonstrate that, for a given intolerant program p with an invariant I, adding convergence from S p to I is an NP-hard problem. Section 4.1 presents a polynomial-time mapping from 3-SAT to an instance of Problem 3. Section 4.2 shows that the instance of 3-SAT is satisfiable iff a self-stabilizing version of the instance of Problem 3 exists.

Problem 4. The 3-SAT decision problem.

-INSTANCE: A set V of n propositional variables (v 0 , • • • , v n-1 ) and k clauses (C 0 , • • • , C k-1
) over V such that each clause is of the form (l q ∨l r ∨l s ), where q, r, s ∈ N k and

N k = {0, 1, • • • , k -1}.
Each l r denotes a literal, where a literal is either ¬v r or v r for v r ∈ V. We assume that ¬(q = r = s) holds for all clauses; otherwise, the 3-SAT instance can efficiently be transformed to a formula that meets this constraint.

-QUESTION: Is there a satisfying truth-value assignment for the variables in V such that each C i evaluates to true, for all i ∈ N k ?

Notation. We say l r is a negative (respectively, positive) literal iff it has the form ¬v r (respectively, v r ), where v r ∈ V. Consider a clause C i = (l q ∨ l r ∨ l s ). We use a binary variable b i j , where i ∈ N k and j ∈ N 3 , to denote the sign of the first, second and the third literal in C i . For example, if l q = ¬v q , l r = v r and l s = ¬v s , then we have b i 0 = 0, b i 1 = 1 and b i 2 = 0. Accordingly, for each clause C i , we define a tuple

B i = b i 0 , b i 1 , b i 2 .
Notice that, the binary variable b i j is independent from the indices of the literals in clause C i and represents only the positive/negative form of the three literals in C i .

Polynomial Mapping

In this section, we present a polynomial-time mapping from an instance of 3-SAT to the instance of Problem 3, denoted p = V p , δ p , Π p , T p . That is, corresponding to each propositional variable and clause, we illustrate how we construct a program p, its processes Π p , its variables V p , its read/write restrictions and its invariant I. We shall use this mapping in Section 4.2 to demonstrate that the instance of 3-SAT is satisfiable iff convergence from S p can be added to p.

Processes, variables and read/write restrictions. We consider three processes, P 0 , P 1 , and P 2 in p. Each process P j (j ∈ N 3 ) has two variables x j and y j , where the domain of x j is equal to N n = {0, 1, • • • , n -1} and y j is a binary variable. (Notice that n denotes the number of propositional variables in the 3-SAT instance.) The process P j can read both x j and y j , but can write only y j . We also consider a fourth process P 3 that can read all variables and write a binary variable sat ∈ N 2 . The variable sat can be read by processes P 0 , P 1 and P 2 , but not written. That is, we have r j = {x j , y j , sat}, w j = {y j } for j ∈ N 3 , and r 3 = {x 0 , y 0 , x 1 , y 1 , x 2 , y 2 , sat} and w 3 = {sat} (see Figure 1). We also have V p = {x 0 , y 0 , x 1 , y 1 , x 2 , y 2 , sat}, Π p = {P 0 , P 1 , P 2 , P 3 }.

P0 P1 P2

P3

For all i ∈ N3: Invariant/legitimate states. Inspired by the form of the 3-SAT instance and its requirements, we define a state predicate I ss that denotes the invariant of p.

Pi :      xi ∈ Nn (read-only) yi ∈ N2 (read & write) sat (read from P3) P3 : sat ∈ N2 (read & write) xi, yi (
-Corresponding to each clause C i = (l q ∨l r ∨l s ), we construct a state predicate

P redC i ≡ (x 0 = q =⇒ y 0 = b i 0 ) ∨ (x 1 = r =⇒ y 1 = b i 1 ) ∨ (x 2 = s =⇒ y 2 = b i 2 )
. In other words, we have

P redC i ≡ ((x 0 = q) ∧ (x 1 = r) ∧ (x 2 = s)) =⇒ ((y 0 = b i 0 ) ∨ (y 1 = b i 1 ) ∨ (y 2 = b i 2 )
). This way, we construct a state predicate Clauses ≡ (∀i ∈ N k : P redC i ). Notice that, we check the value of each x j with respect to the index of the literal appearing in position j in C i , where j ∈ N 3 . This is due to the fact that the domain of x j is equal to the range of the indices of propositional variables (i.e., N n ).

-A literal l r may appear in positions i and j in distinct clauses of 3-SAT, where i, j ∈ N 3 and i = j. Since each propositional variable v r ∈ V gets a unique truth-value in 3-SAT, the truth-value of l r is independent from its position in the 3-SAT formula. Given the way we construct the state predicate Clauses, it follows that, in the instance of Problem 3, whenever x i = x j we should have y i = y j . Thus, we construct the state predicate Iden ≡ (∀i, j ∈ N 3 : (x i = x j =⇒ y i = y j )), which is conjoined with the predicate Clauses. -In the instance of Problem 3, we require that (sat = 1) holds in all invariant states.

Thus, the invariant of p is equal to the state predicate I ss , where

I ss ≡ Iden ∧ Clauses ∧ (sat = 1)
Notice that, the size of the state space of p is equal to 2 (2n) 3 ; i.e., |S p | is polynomial in the size of the 3-SAT instance.

Example 1. Example Construction

Let us consider the 3-SAT formula φ

≡ (v 0 ∨ v 1 ∨ v 2 ) ∧ (¬v 1 ∨ ¬v 1 ∨ ¬v 2 ) ∧ (¬v 1 ∨ ¬v 1 ∨ v 2 ) ∧ (v 1 ∨ ¬v 2 ∨
¬v 0 ). Since there are three propositional variables and four clauses, we have n = 3 and k = 4. Moreover, based on the mapping described before, we have

C 0 ≡ (v 0 ∨ v 1 ∨ v 2 ), C 1 ≡ (¬v 1 ∨ ¬v 1 ∨ ¬v 2 ), C 2 ≡
(¬v 1 ∨¬v 1 ∨v 2 ) and C 3 ≡ (v 1 ∨¬v 2 ∨¬v 0 ). We have B 0 = 1, 1, 1 , B 1 = 0, 0, 0 , B 2 = 0, 0, 1 and B 3 = 1, 0, 0 . The state predicate Iden is defined as before and Clauses is the conjunction of each PredC i (i ∈ N 4 ) defined as follows:

PredC 0 ≡ (x 0 = 0 ∧ x 1 = 1 ∧ x 2 = 2) =⇒ (y 0 = 1 ∨ y 1 = 1 ∨ y 2 = 1) PredC 1 ≡ (x 0 = 1 ∧ x 1 = 1 ∧ x 2 = 2) =⇒ (y 0 = 0 ∨ y 1 = 0 ∨ y 2 = 0) PredC 2 ≡ (x 0 = 1 ∧ x 1 = 1 ∧ x 2 = 2) =⇒ (y 0 = 0 ∨ y 1 = 0 ∨ y 2 = 1) PredC 3 ≡ (x 0 = 1 ∧ x 1 = 2 ∧ x 2 = 0) =⇒ (y 0 = 1 ∨ y 1 = 0 ∨ y 2 = 0)

Correctness of Reduction

In this section, we illustrate that Problem 3 is NP-complete. Specifically, we show that the instance of 3-SAT is satisfiable iff convergence from S p to I ss can be added to the instance of Problem 3, denoted p. Lemma 1. If the instance of 3-SAT has a satisfying valuation, then convergence from S p can be added to the instance of Problem 3; i.e., there is a self-stabilizing version of p, denoted p ss .

Let there be a truth-value assignment to the propositional variables in V such that every clause evaluates to true; i.e., ∀i : i ∈ N k : C i . Initially, δ p = ∅ and δ p = δ pss . Based on the value assignments to propositional variables, we include a set of transitions (represented as convergence actions) in p ss . Then, we illustrate that the following three properties hold: the invariant I ss ≡ Clauses ∧Iden ∧(sat = 1) remains closed in p ss , deadlock-freedom in ¬I ss and livelock-freedom in p ss |¬I ss .

-If a propositional variable v r (where r ∈ N n ) is assigned true, then we include the following action in each process P j , where j ∈ N 3 : x j = r ∧y j = 0∧sat = 0 → y j := 1.

-If a propositional variable v r (where r ∈ N n ) is assigned false, then we include the following action in each process P j , where j ∈ N 3 : x j = r ∧y j = 1∧sat = 0 → y j := 0. -We include the following actions in P 3 : (Iden ∧ Clauses)∧sat = 0 → sat := 1 and ¬ (Iden ∧ Clauses) ∧ sat = 1 → sat := 0. Now we illustrate that closure, deadlock-freedom and livelock-freedom hold. That is, the resulting program is self-stabilizing to I ss . Closure. Since the first three processes can execute an action only in states where sat = 0, their actions are disabled where sat = 1. Thus, the first three processes exclude any transition that starts in I ss ; i.e., preserving the closure of I ss and ensuring p ss |I ss ⊆ p|I ss . Moreover, P 3 takes an action only when its guards are enabled; i.e., in illegitimate states. Therefore, none of the included actions violates the closure of I ss , and the second constraint of the output of Problem 1 holds. Livelock Freedom. To show livelock-freedom, we illustrate that the included actions have no circular dependencies. That is, no set of actions can enable each other in a cyclic fashion. Due to read/write restrictions, none of the three processes P 0 , P 1 and P 2 executes based on the local variables of another process. Moreover, each process can update only its own y value. Once any one of the processes P 0 , P 1 and P 2 updates its y value, it disables itself. Thus, the actions of one process cannot enable/disable another process. Moreover, since each action disables itself, there are no self-loops either. The guards of the actions of P 3 cannot be simultaneously true. Moreover, once one of them is enabled, the other one is certainly disabled, and the execution of one cannot enable another (because they only update the value of sat). Only processes P 0 , P 1 and P 2 can make the predicate (Iden ∧ Clauses) true when sat = 0. Once P 3 sets sat to 1 from states (Iden ∧ Clauses) ∧ (sat = 0), a state in I ss is reached. Therefore, there are no cycles that start in ¬I ss and exclude any state in I ss . Deadlock Freedom. We illustrate that, in every state in ¬I ss ≡ (¬(Iden ∧ Clauses) ∨ (sat = 0)), there is at least one action that is enabled.

-Case 1: ((Iden ∧ Clauses) ∧ (sat = 0)) holds. In these states, the first action of P 3 is enabled. Thus, there are no deadlocks in this case.

-Case 2: (¬(Iden ∧Clauses)∧(sat = 1)) holds. In this case, the second action of P 3 is enabled. Thus, there are no deadlocks in this case. -Case 3: (¬(Iden ∧ Clauses) ∧ (sat = 0)) holds. None of the actions of P 3 are enabled in this case. Nonetheless, since ¬(Iden ∧Clauses) holds, either ¬Iden or ¬Clauses, or both are true. When ¬Clauses holds, there must be some state predicate PredC i (i ∈ N k ) that is false. (Recall that, the invariant

I ss includes a state predicate PredC i ≡ (x 0 = q =⇒ y 0 = b i 0 ) ∨ (x 1 = r =⇒ y 1 = b i 1 ) ∨ (x 2 = s =⇒ y 2 = b i 2 ) corresponding to each clause C i ≡ (l q ∨ l r ∨ l s ) in the instance of 3-SAT.
) This means that the following three state predicates are false:

(x 0 = q =⇒ y 0 = b i 0 ), (x 1 = r =⇒ y 1 = b i 1 ) and (x 2 = s =⇒ y 2 = b i 2 )
. Since the instance of 3-SAT is satisfiable, at least one of the literals l q , l r or l s must be true. As a result, based on the way we have included the actions depending on the truth-values of the propositional variables, at least one of the following actions must have been included in

p ss : (x 0 = q ∧ y 0 = b i 0 ∧ sat = 0) → y 0 := b i 0 , (x 1 = r ∧ y 1 = b i 1 ∧ sat = 0) → y 1 := b i 1 , and (x 2 = s ∧ y 2 = b i 2 ∧ sat = 0) → y 2 := b i 2 .
Thus, there is some action that is enabled when ¬Clauses holds. A similar reasoning implies that there exists some action that is enabled when ¬Iden holds. Thus, there are no deadlocks in Case 3.

Based on the closure of the invariant I ss in all actions, deadlock-freedom in ¬I ss and lack of non-progress cycles in p ss |¬I ss , it follows that the resulting program p ss is self-stabilizing to I ss .

Example 2. Example Construction

In the example discussed in this section, the formula φ has a satisfying assignment for v 0 = 1, v 1 = 0, v 2 = 0. Using this value assignment, we include the following actions in the first three processes P r where r ∈ N 3 :

x r = 0 ∧ y r = 0 ∧ sat = 0 → y r := 1 x r = 1 ∧ y r = 1 ∧ sat = 0 → y r := 0 x r = 2 ∧ y r = 1 ∧ sat = 0 → y r := 0
The actions of P 3 are as follows:

(Iden ∧ Clauses) ∧ sat = 0 → sat := 1 ¬(Iden ∧ Clauses) ∧ sat = 1 → sat := 0
1 o o 1 o o 1 o o 2 k k 2 k k 2 k k 2 k k 3 p p 3 3 3 3 Ö Ö 3 Ö Ö 3 Ö Ö 3 Ö Ö Fig. 2: Transitions originating in the state predicate x 0 = 0 ∧ x 1 = 1 ∧ x 2 = 2
By assumption, we consider a program p ss to be a self-stabilizing version of p from I ss . That is, p ss satisfies the requirements of Problem 3. Only P 3 can correct (sat = 0). Clearly, p ss must preserve the closure of I ss , and should not have any deadlocks or livelocks in the states in ¬I ss ≡ (¬(Iden ∧ Clauses) ∨ (sat = 0)). Thus, p ss must include actions that correct ¬(Iden ∧ Clauses) and (sat = 0). Since p ss must adhere to the read/write restrictions of p, only P 3 can correct (sat = 0) to (sat = 1). For the same reason, P 3 cannot contribute to correcting ¬(Iden ∧ Clauses); only P 0 , P 1 and P 2 have the write permissions to do so by updating their own y values.

The rest of the reasoning is as follows: We first illustrate that P 0 , P 1 and P 2 in p ss must not execute in states where (sat = 1). Then, we draw a correspondence between actions included in p ss and how propositional variables get unique truthvalues in 3-SAT and how the clauses are satisfied. P 0 , P 1 and P 2 can be enabled only when (sat = 0). We observe that no process P j (j ∈ N 3 ) can have a transition that starts in the invariant I ss ; otherwise, the constraint δ pss |I ss ⊆ δ p |I ss would be violated. We also show that no recovery action of P 0 , P 1 and P 2 can include a transition that starts in a state where sat = 1. By contradiction, assume that some P j (j ∈ N 3 ) includes a transition (s 0 , s 1 ) where s 0 ∈ ¬I ss and sat(s 0 ) = 1 for some fixed values of x j and y j . Since P j cannot read x i and y i of other processes P i , where (i ∈ N 3 )∧(i = j), the transition (s 0 , s 1 ) has a groupmate (s 0 , s 1 ), where x i (s 0 ) = x j (s 0 ) and y i (s 0 ) = y j (s 0 ) for all i ∈ N 3 where (i = j). Thus, Iden is true at s 0 . Moreover, due to the form of the 3-SAT instance, no clause (l q ∨ l r ∨ l s ) exists such that (q = r = s). Thus, Clauses holds at s 0 as well, thereby making s 0 an invariant state. As a result, (s 0 , s 1 ) is grouped with a transition that starts in I ss , which again violates the constraint δ pss |I ss ⊆ δ p |I ss . Hence, P 0 , P 1 and P 2 can be enabled only when (sat = 0).

Actions of P 3 . We show that P 3 must set sat to 0 when ¬(Iden∧Clauses)∧sat = 1 and may only assign sat to 1 when (Iden ∧ Clauses) ∧ sat = 0. As shown above, P 0 , P 1 , and P 2 cannot act when sat = 1, forcing P 3 to execute from ¬(Iden ∧ Clauses) ∧ (sat = 1). P 3 must therefore have the action ¬(Iden ∧ Clauses) ∧ sat = 1 → sat := 0. Consequently, P 3 cannot assign sat to 1 when ¬(Iden ∧ Clauses) ∧ sat = 0; otherwise, it would create a livelock with the previous action. From states where (Iden ∧ Clauses) ∧ sat = 0 holds, P 3 is the only process which can change sat to 1, thereby reaching an invariant state. Thus, P 3 must include the actions ¬(Iden ∧ Clauses) ∧ sat = 1 → sat := 0 and (Iden ∧ Clauses) ∧ sat = 0 → sat := 1. Each P j , for j ∈ N 3 must have exactly one action for each unique value of x j . When sat = 0, fixing the value of x j to some a ∈ N n reduces the possible local states for process P j to 2, where y j = 0 or y j = 1 for j ∈ N 3 . (Notice that, both of these states are illegitimate since sat = 0.) Thus, when (x j = a∧sat = 0) holds, process P j has 4 possible actions: y j = 0 → y j := 0, y j = 0 → y j := 1, y j = 1 → y j := 0, and y j = 1 → y j := 1. It is clear that the first and last of those actions are self-loops and cannot be included. Thus, P j can have either action y j = 0 → y j := 1 or y j = 1 → y j := 0, but not both without creating a livelock. That is, P j cannot have more than 1 action. Additionally, to make Iden true, P j must include some action. By contradiction, assume that P j has no actions. Another process P i (i ∈ N 3 , i = j) can be in the state where x i = x j . There are two possibilities for the y values in this non-invariant state, y j = 0 ∧ y i = 1 or y j = 1 ∧ y i = 0. P i can resolve either scenario with an action but cannot resolve both as this would require 2 actions. That is, to resolve both cases P i needs the cooperation of P j . Thus, P j must have some action. Since P j cannot have more than one action, it follows that P j has exactly one action. Truth-value assignment to propositional variables. Based on the above reasoning, for each value a ∈ N n , if a process P j includes the action x j = a∧y j = 0 ∧ sat = 0 → y j := 1, then we assign true to the propositional variable v a . If P j includes the action x j = a ∧ y j = 1 ∧ sat = 0 → y j := 0, then we assign false to v a . Let P j include the action x j = a ∧ y j = 0 ∧ sat = 0 → y j := 1. By contradiction, if another process P i , where i ∈ N 3 ∧ i = j, includes the action x i = a ∧ y i = 1 ∧ sat = 0 → y i := 0, then Iden would be violated and p ss would never recover from the state x j = a ∧ x i = a ∧ y j = 1 ∧ y i = 0 ∧ sat = 0; i.e., a deadlock state, which is a contradiction with p ss being self-stabilizing. Thus, each propositional variable gets a unique truth-value assignment and these value assignments are logically consistent. Satisfying the clauses. Since p ss is self-stabilizing from I ss , eventually I ss becomes true. This means that every PredC i in the Clauses predicate becomes true. The one-to-one correspondence created by the mapping between each state predicate PredC i and each clause C i implies that PredC i holds iff at least one literal in C i holds. Therefore, all clauses are satisfied with the truth-value assignment based on the actions of p ss .

Theorem 1. Adding convergence to low atomicity programs is NP-complete.

Proof. The NP-hardness of adding convergence follows from Lemmas 1 and 2. The NP membership of adding convergence has already been established in [START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF]; hence the NP-completeness.

Corollary 1. Adding nonmasking fault tolerance to low atomicity programs is NP-complete.

Corollary 1 follows from Theorem 1 and the fact that Problem 3 is a special case of Problem 2.

Discussion

This section discusses extant work in three most related categories: algorithmic design of fault tolerance in general, algorithmic design of self-stabilization in particular, and complexity of algorithmic design. Several researchers have investigated the problem of algorithmic design of fault-tolerant systems [START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF][START_REF] Ebnenasir | Automatic Synthesis of Fault-Tolerance[END_REF][START_REF] Jhumka | Automated design of efficient fail-safe fault tolerance[END_REF][START_REF] Jhumka | An approach to synthesise safe systems[END_REF][START_REF] Bonakdarpour | Exploiting symbolic techniques in automated synthesis of distributed programs with large state space[END_REF], where a specific level of fault tolerance (e.g., failsafe, nonmasking or masking) is systematically incorporated in an existing program. Kulkarni and Arora [START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF] present a family of polynomial-time algorithms for the addition of different levels of fault tolerance to high atomicity programs, while demonstrating that adding masking fault tolerance to low atomicity programs is NP-complete. In our previous work [START_REF] Ebnenasir | Automatic Synthesis of Fault-Tolerance[END_REF], we establish a foundation for the addition of fault tolerance to low atomicity programs using efficient heuristics and component-based methods. Jhumka et. al [START_REF] Jhumka | Automated design of efficient fail-safe fault tolerance[END_REF][START_REF] Jhumka | An approach to synthesise safe systems[END_REF] investigate the addition of failsafe fault tolerance under efficiency constraints. Bonakdarpour and Kulkarni [START_REF] Bonakdarpour | Exploiting symbolic techniques in automated synthesis of distributed programs with large state space[END_REF] exploit symbolic techniques to increase the scalability of the addition of fault tolerance.

Existing methods for the algorithmic design of convergence include constraintbased methods [START_REF] Abujarad | Automated constraint-based addition of nonmasking and stabilizing fault-tolerance[END_REF] and sound heuristics [START_REF] Farahat | A lightweight method for automated design of convergence in network protocols[END_REF][START_REF] Ebnenasir | Swarm synthesis of convergence for symmetric protocols[END_REF]. Abujarad and Kulkarni [START_REF] Abujarad | Automated constraint-based addition of nonmasking and stabilizing fault-tolerance[END_REF] consider the program invariant as a conjunction of a set of local constraints, each representing the set of local legitimate states of a process. Then, they synthesize convergence actions for correcting the local constraints without corrupting the constraints of neighboring processes. Nonetheless, they do not explicitly address cases where local constraints have cyclic dependencies (e.g., maximal matching on a ring), and their case studies include only acyclic topologies. In our previous work [START_REF] Farahat | A lightweight method for automated design of convergence in network protocols[END_REF][START_REF] Ebnenasir | Swarm synthesis of convergence for symmetric protocols[END_REF], we present a method where we partition the state space to a hierarchy of state predicates based on the length of the shortest computation prefix from each state to some state in the invariant. Then, we systematically explore the space of all candidate recovery transitions that could contribute in recovery to the invariant without creating non-progress cycles outside the invariant.

Most hardness results [START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF][START_REF] Sandeep | Complexity issues in automated synthesis of failsafe fault-tolerance[END_REF][START_REF] Bonakdarpour | Revising distributed UNITY programs is NP-complete[END_REF] presented for the addition of fault tolerance lack the additional constraint of recovery from any state, which we have in the addition of convergence. The proof of NP-hardness of adding failsafe fault tolerance presented in [START_REF] Sandeep | Complexity issues in automated synthesis of failsafe fault-tolerance[END_REF] is based on a reduction from 3-SAT, nonetheless, a failsafe fault-tolerant program does not need to recover to its invariant when faults occur. While a masking fault-tolerant program is required to recover to its invariant in the presence of faults, the problem of adding masking fault tolerance relies on finding a subset of the state space from where such recovery is possible; no need to provide recovery from any state. As such, the hardness proof presented in [START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF] is based on a reduction in which such a subset of state space is identified along with corresponding convergence actions if and only if the instance of 3-SAT is satisfiable. This means that some states are allowed to be excluded from the fault span; this is not an option in the case of adding convergence. The essence of the proof in [START_REF] Bonakdarpour | Revising distributed UNITY programs is NP-complete[END_REF] also relies on the same principle where Bonakdarpour and Kulkarni illustrate the NP-hardness of designing progress from one state predicate to another for low atomicity programs.

Conclusions and Future Work

This paper illustrates that adding convergence to low atomicity programs is an NP-complete problem, where convergence guarantees that from any state program computations recover to a set of legitimate states; i.e., invariant. In other words, we demonstrated that designing self-stabilizing programs from their non-stabilizing versions is NP-complete in the size of the state space. Since self-stabilization is a special case of nonmasking fault tolerance, it follows that adding nonmasking fault tolerance to intolerant distributed programs is also NPcomplete. When faults occur, a nonmasking program guarantees recovery from states reached due to the occurrence of faults to its invariant. In the absence of faults, the computations of a nonmasking program remain in its invariant. Thus, this paper solves a decade-old open problem [START_REF] Kulkarni | Automating the addition of fault-tolerance[END_REF]. As an extension of this work, we will investigate special cases where the addition of convergence/nonmasking can be performed efficiently. That is, for what programs, classes of faults and invariants the addition of convergence/nonmasking can be done in polynomial time? Moreover, while we analyzed the general case complexity of adding convergence/nonmasking tolerance under no fairness assumption, it would be interesting to investigate the impact of different fairness assumptions on the complexity of adding convergence.

  m+1 and ⊕ denotes addition modulo m + 1. Proposition 1. A program p is nonmasking f -tolerant from I with a f -span T iff there are no deadlock states in T-I and no non-progress cycles in δ p | (T-I).

Fig. 1 :

 1 Fig. 1: Instance of Problem 3.

Figure 2 Lemma 2 .

 22 Figure 2 illustrates the transitions of the stabilizing program p ss originating in the state predicate (x 0 = 0 ∧ x 1 = 1 ∧ x 2 = 2). Each state is represented by four bits which signify the respective values of y 0 , y 1 , y 2 , sat. Invariant states are depicted by ovals, and the label on each transition denotes the executing process. Lemma 2. If there is a self-stabilizing version of the instance of Problem 3, then the corresponding 3-SAT instance has a satisfying valuation.

  Problem 1. Adding Nonmasking Fault Tolerance -Input: (1) A program p = V p , δ p , Π p , T p ; (2) A class of faults f ; (3) A state predicate I such that I is closed in p, and (4) topological constraints of p captured by read/write restrictions. -Output: A program p = V p , δ p , Π p , T p and a state predicate I such that the following constraints are met: (1) I is non-empty and I ⊆ I; (2) δ p |I ⊆ δ p |I ; (3) Π p and Π p have the same number of processes and T p = T p , and (4) p is nonmasking f -tolerant from I . We state the corresponding decision problem as follows: Problem 2. Decision Problem of Adding Nonmasking Fault Tolerance -INSTANCE: (1) A program p = V p , δ p , Π p , T p ; (2) A class of faults f ; (3) A state predicate I such that I is closed in p, and (4) topological constraints of p captured by read/write restrictions. -QUESTION: Does there exist a program p = V p , δ p , Π p , T p and a state predicate I such that the constraints of Problem 1 are met? A special case of Problem 2 is where f denotes a class of transient faults, I = I , δ p |I = δ p |I , and p is self-stabilizing from I. Problem 3. Decision Problem of Adding Convergence -INSTANCE: (1) A program p = V p , δ p , Π p , T p ; (2) A state predicate I such that I is closed in p, and (3) topological constraints captured by read/write restrictions. -QUESTION: Does there exist a program p ss with an invariant I ss such that I = I ss , δ pss |I ss = δ p |I ss , and p ss is self-stabilizing from I ss ?

This work was sponsored in part by the NSF grant CCF-1116546 and a grant from Michigan Technological University.


Ka I Pun

Martin Steffen

Volker Stolz

Deadlock Checking by Data Race Detection

Deadlocks are a common problem in programs with lock-based concurrency and are hard to avoid or even to detect. One way for deadlock prevention is to statically analyze the program code to spot sources of potential deadlocks. We reduce the problem of deadlock checking to race checking, another prominent concurrency-related error for which good (static) checking tools exist. The transformation uses a type and effect-based static analysis, which analyzes the data flow in connection with lock handling to find out control-points that are potentially part of a deadlock. These control-points are instrumented appropriately with additional shared variables, i.e., race variables injected for the purpose of the race analysis. To avoid overly many false positives for deadlock cycles of length longer than two, the instrumentation is refined by adding "gate locks". The type and effect system and the transformation are formally given. We prove our analysis sound using a simple, concurrent calculus with re-entrant locks.

Introduction

Concurrent programs are notoriously hard to get right and at least two factors contribute to this fact: Correctness properties of a parallel program are often global in nature, i.e., result from the correct interplay and cooperation of multiple processes. Hence also violations are non-local, i.e., they cannot typically be attributed to a single line of code. Secondly, the non-deterministic nature of concurrent executions makes concurrencyrelated errors hard to detect and to reproduce. Since typically the number of different interleavings is astronomical or infinite, testing will in general not exhaustively cover all behavior and errors may remain undetected until the software is in use.

Arguably the two most important and most investigated classes of concurrency errors are data races [START_REF] Beckman | A survey of methods for preventing race conditions[END_REF] and deadlocks [START_REF] Dijkstra | Cooperating sequential processes[END_REF]. A data race is the simultaneous, unprotected access to mutable shared data with at least one write access. A deadlock occurs when a number of processes are unable to proceed, when waiting cyclically for each other's non-shareable resources without releasing one's own [START_REF] Coffman | System deadlocks[END_REF]. Deadlocks and races constitute equally pernicious, but complementary hazards: locks offer protection against races by ensuring mutually exclusive access, but may lead to deadlocks, especially using fine-grained locking, or are at least detrimental to the performance of the program by decreasing the degree of parallelism. Despite that, both share some commonalities, too: a race, respectively a deadlock, manifests itself in the execution of a concurrent program, when two processes (for a race) resp. two or more processes (for a deadlock) reach respective control-points that when reached simultaneously, constitute an unfortunate interaction: in case of a race, a read-write or write-write conflict on a shared variable, in case of a deadlock, running jointly into a cyclic wait.

In this paper, we define a static analysis for multi-threaded programs which allows reducing the problem of deadlock checking to race condition checking. The analysis is based on a type and effect system [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF] which formalizes the data-flow of lock usages and, in the effects, works with an over-approximation on how often different locks are being held. The information is used to instrument the program with additional variables to signal a race at control points that potentially are involved in a deadlock. Despite the fact that races, in contrast to deadlocks, are a binary global concurrency error in the sense that only two processes are involved, the instrumentation is not restricted to deadlock cycles of length two. To avoid raising too many spurious alarms when dealing with cycles of length > 2, the transformation adds additional locks, to prevent that already parts of a deadlock cycle give raise to a race, thus falsely or prematurely indicating a deadlock by a race.

Our approach widens the applicability of freely available state-of-the-art static race checkers: Goblint [START_REF] Seidl | Region analysis for race detection[END_REF] for the C language, which is not designed to do any deadlock checking, will report appropriate data races from programs instrumented through our transformation, and thus becomes a deadlock checker as well. Chord [START_REF] Naik | Effective static race detection for Java[END_REF] for Java only analyses deadlocks of length two for Java's synchronized construct, but not explicit locks from java.util.concurrent, yet through our instrumentation reports corresponding races for longer cycles and for deadlocks involving explicit locks.

The remainder of the paper is organised as follows. Section 2 presents syntax and operational semantics of the calculus. Afterwards, Section 3 formalizes the data flow analysis in the form of a (constraint-based) effect system. The obtained information is used in Sections 4 and 5 to instrument the program with race variables and additional locks. The sections also prove the soundness of the transformation. We conclude in Section 6 discussing related and future work.

Calculus

In this section we present the syntax and (operational) semantics for our calculus, formalizing a simple, concurrent language with dynamic thread creation and higher-order functions. Locks likewise can be created dynamically, they are re-entrant and support non-lexical use of locking and unlocking. The abstract syntax is given in Table 1. A program P consists of a parallel composition of processes p t , where p identifies the process and t is a thread, i.e., the code being executed. The empty program is denoted as / 0. As usual, we assume to be associative and commutative, with / 0 as neutral element. As for the code we distinguish threads t and expressions e, where t basically is a sequential composition of expressions. Values are denoted by v, and let x:T = e in t represents the sequential composition of e followed by t, where the eventual result of e, i.e., once evaluated to a value, is bound to the local variable x. Expressions, as said, are given by e, and threads are among possible expressions. Further expressions are function application, conditionals, and the spawning of a new thread, written spawn t. The last three expressions deal with lock handling: new L creates a new lock (initially free) and gives a reference to it (the L may be seen as a class for locks), and furthermore v. lock and v. unlock acquires and releases a lock, respectively. Values, i.e., evaluated expressions, are variables, lock references, and function abstractions, where we use fun f :T for recursive function definitions. Note that the grammar insists that, e.g., in an application, both the function and the arguments are values, analogously when acquiring a lock, etc. This form of representation is known as a-normal form [START_REF] Flanagan | The essence of compiling with continuations[END_REF].

Listing 1 shows the paraphrased code for the well-known Dining Philosopher example. The recursive body used for each philosopher is polymorphic in the lock locations.

P ::= / 0 | p t | P P program t ::= v | let x:T = e in t thread e ::= t | v v | if v then e else e | spawn t | new L | v. lock | v. unlock expr. v ::= x | l r | true | false | fn x:T.t | fun f :T.x:T.t values Table 1. Abstract syntax
The grammar for types, effects, and annotations is given Table 2, where π represents labels (used to label program points where locks are created), r represents (finite) sets of πs, where ρ is a corresponding variable. Labels π are an abstraction of concrete lock references which exist at run-time (namely all those references created at that program point) and therefore we refer to labels π as well as lock sets r also as abstract locks. Types include basic types B such as integers, booleans, etc., left unspecified, function types T1 ϕ -→ T2 , and in particular lock types L. To capture the data flow concerning locks, the lock types are annotated with a lock set r, i.e., they are of the form L r . This information will be inferred, and the user, when using types in the program, uses types without annotations (the "underlying" types). We write T, T 1 , T 2 , . . . as meta-variables for the underlying types, and T and its syntactic variants for the annotated types, as given in the grammar. Furthermore, polymorphism for function definition is captured by type schemes Ŝ, i.e., types prefix-quantified over variables ρ and X, under some constraints. We let Y abbreviate either variables ρ or X, where X is a variable for effect which is introduced later. Any specialization of the type scheme ∀ Y :C. T has to satisfy the constraints C. For the deadlock and race analysis we need not only information which locks are used where, but also an estimation about the "value" of the lock, i.e., how often the abstractly represented locks are taken.

Estimation of the lock values, resp. their change is captured in the behavioral effects ϕ in the form of pre-and post-specifications ∆ 1 → ∆ 2 . Abstract states (or lock envi-

::= / 0 | ρ r, C | X ≥ ∆ ,C constraints Table 2.
Types ronments) ∆ are of the form r 0 :n 0 , r 1 :n 1 , . . .. The constraint based type system works on lock environments using variables only, i.e., the ∆ are of the form ρ 0 :n 0 , ρ 1 :n 1 , . . ., maintaining that each variable occurs at most once. Thus, in the type system, the environments ∆ are mappings from variables ρ to lock counter values n, where n ranges from +∞ to -∞. As for the syntactic representation of those mappings: we assume that a variable ρ not mentioned in ∆ corresponds to the binding ρ:0, e.g. in the empty mapping •. Constraints C finally are finite sets of subset inclusions of the forms ρ r and X ≥ ∆ . We assume that the user provides the underlying types, i.e., without location and effect annotation, while our type system in Section 3 derives the smallest possible type in terms of originating locations for each variable of lock-type L in the program.

Semantics

Next we present the operational semantics, given in the form of a small-step semantics, distinguishing between local and global steps (cf. Tables 3 and4). The local semantics deals with reduction steps of one single thread of the form t 1 -→ t 2 . Rule R-RED is the basic evaluation step which replaces the local variable in the continuation thread t by the value v (where [v/x] represents capture-avoiding substitution). The Let-construct generalizes sequential composition and rule R-LET restructures a nested let-construct expressing associativity of that construct. Thus it corresponds to transforming (e 1 ;t 1 );t 2 into e 1 ; (t 1 ;t 2 ). Together with the first rule, it assures a deterministic left-to-right evaluation within each thread. The two R-IF-rules cover the two branches of the conditional and the R-APP-rules deals with function application (of non-recursive, resp. recursive functions).

The global steps are given in Table 4, formalizing transitions of configurations of the form σ P, i.e., the steps are of the form σ P -→ σ P , where P is a program, i.e., the parallel composition of a finite number of threads running in parallel, and σ is a finite mapping from lock identifiers to the status of each lock (which can be either free or taken by a thread where a natural number indicates how often a thread has acquired the lock, modelling re-entrance). Thread-local steps are lifted to the global level by R-LIFT. Rule R-PAR specifies that the steps of a program consist of the steps of the individual threads, sharing σ . Executing the spawn-expression creates a new thread with a fresh identity which runs in parallel with the parent thread (cf. rule R-SPAWN). Globally, the process identifiers are unique. A new lock is created by new L (cf. rule R-NEWL) which allocates a fresh lock reference in the heap. Initially, the lock is free. A lock l is acquired

let x:T = v in t - → t[v/x] R-RED let x 2 :T 2 = (let x 1 :T 1 = e 1 in t 1 ) in t 2 - → let x 1 :T 1 = e 1 in (let x 2 :T 2 = t 1 in t 2 ) R-LET let x:T = if true then e 1 else e 2 in t - → let x:T = e 1 in t R-IF 1 let x:T = if false then e 1 else e 2 in t - → let x:T = e 2 in t R-IF 2 let x:T = (fn x :T .t ) v in t - →let x:T = t [v/x ] in t R-APP 1 let x:T = (fun f :T 1 .x :T 2 .t ) v in t - → let x:T = t [v/x ][fun f :T 1 .x :T 2 .t / f ] in t R-APP 2
: If σ (l) = free, then σ + p l = σ [l → p(1)] and if σ (l) = p(n), then σ + p l = σ [l → p(n + 1)]. Dually σ -p l is defined as follows: if σ (l) = p(n + 1), then σ -p l = σ [l → p(n)], and if σ (l) = p(1), then σ -p l = σ [l → free].
Unlocking works correspondingly, i.e., it sets the lock as being free resp. decreases the lock count by one (cf. rule R-UNLOCK). In the premise of the rules it is checked that the thread performing the unlocking actually holds the lock.

t 1 - → t 2 R-LIFT σ p t 1 - → σ p t 2 σ P 1 - → σ P 1 R-PAR σ P 1 P 2 - → σ P 1 P 2 σ p 1 let x:T = spawn t 2 in t 1 - → σ p 1 let x:T = p 2 in t 1 p 2 t 2 R-SPAWN σ = σ [l → free] l is fresh R-NEWL σ p let x:T =new L in t - → σ p let x:T = l in t σ (l) = free ∨ σ (l) = p(n) σ = σ + p l R-LOCK σ p let x:T = l. lock in t - → σ p let x:T = l in t σ (l) = p(n) σ = σ -p l R-UNLOCK σ p let x:T = l. unlock in t - → σ p let x:T = l in t Table 4. Global steps
To analyze deadlocks and races, we specify which locks are meant statically by labelling the program points of lock creations with π, i.e., lock creation statements new L are augmented to new π L where the annotations π are assumed unique for a given program. We assume further that the lock references l are also labelled l ρ ; the labelling is done by the type system presented next.

Type and effect system

Next we present a constraint-based type and effect system for information which locks are being held at various points in the code. The analysis works thread-locally, i.e., it analyzes the code of one thread. In Section 4, we will use this information to determine points in a program, that globally may lead to deadlocks and which are then instrumented appropriately by additional race variables. The judgments of the system are of the form Γ e : T ::

ϕ;C , (1)
where ϕ is of the form ∆ 1 → ∆ 2 . Equivalently, we write also Γ ; ∆ 1 e : T :: ∆ 2 ;C for the judgment. The judgment expresses that e is of type T , where for annotated lock types of the form L r the r expresses the potential points of creation of the lock. The effect ϕ = ∆ 1 → ∆ 2 expresses the change in the lock counters, where ∆ 1 is the pre-condition and ∆ 2 the post-condition (in a partial correctness manner). The types and the effects contain variables ρ and X; hence the judgement is interpreted relative to the solutions of the set of constraints C. Given Γ and e, the constraint set C is generated during the derivation. Furthermore, the pre-condition ∆ 1 is considered as given, whereas ∆ 2 is derived.

The rules for the type system are given in Table 5. The rule TA-VAR combines looking up the variable from the context with instantiation, choosing fresh variables to assure that the constraints θC, where C is taken from the variable's type scheme, are most general. As a general observation and as usual, values have no effect, i.e., its preand post-condition are identical. Also lock creation in rule TA-NEWL does not have an effect. As for the flow: π labels the point of creation of the lock; hence a new constraint is generated, requiring ρ {π} for the ρ-annotation in the lock type. The case for lock references l ρ in rule TA-LREF works analogously, where the generated constraint uses the lock variable ρ instead of the concrete point of creation.

For function abstraction in rule TA-ABS 1 , the premise checks the body e of the function with the typing context extended by x: T A , where the operation T A turns all occurrences of lock types L in T into their annotated counter-parts using fresh variables, as well as introducing state variables for the latent effects of higher-order functions. Also for the pre-condition of the function body, a fresh variable is used. The recursive function is also formulated similarly. It uses in addition a fresh variable for the post-condition of the function body, and constraints requiring X 2 ≥ ∆ 2 and T2 ≥ T 2 are generated. For function application (cf. rule TA-APP), the subtyping requirement between the type T2 of the argument and the function's input type T 2 is used to generate additional constraints. Furthermore, the precondition ∆ of the application is connected with the precondition of the latent effect ∆ 1 and the post-condition of the latent effect with the post-condition of the application, the latter one using again a fresh variable. The corresponding two constraints ∆ ≤ ∆ 1 and ∆ 2 ≤ X represent the control flow when calling, resp. when returning to the call site. The treatment of conditionals is standard (cf. rule TA-COND). To assure that the resulting type is an upper bound for the types of the two branches, two additional constraints C and C are generated.

The let-construct (cf. rule TA-LET) is combined with the rule for generalization, such that for checking the body e 2 , the typing context is extended by a type scheme Ŝ1 which generalizes the type T1 of expression e 1 . The close-operation is defined as close(Γ ,C, T ) = ∀ Y :C. T where the quantifier binds all variables occurring free in C and T but not in Γ . Spawning a thread in rule TA-SPAWN has no effect, where the premise of the rule checks well-typedness of the thread being spawned. The last two rules deal with locking and unlocking, simply counting up, resp. down the lock counter, setting the post-condition to over-approximate ∆ ⊕ ρ, resp. ∆ ρ.

Γ (x) = ∀ Y :C. T Y fresh θ = [ Y / Y ] TA-VAR Γ x : θ T :: ∆ → ∆ ; θC Γ t : T :: • → ∆ 2 ;C TA-SPAWN Γ spawn t : Thread:: ∆ 1 → ∆ 1 ;C ρ fresh TA-NEWL Γ new π L : L ρ :: ∆ → ∆ ; ρ {π} ρ fresh TA-LREF Γ l ρ : L ρ :: ∆ → ∆ ; ρ ρ T1 = T 1 A Γ , x: T1 e : T2 :: X → ∆ 2 ;C X fresh TA-ABS 1 Γ fn x:T 1 .e : T1 X→∆ 2 ---→ :: ∆ 1 - → ∆ 1 ;C T1 = T 1 A T2 = T 2 A X 1 , X 2 fresh Γ , f : T1 X 1 →X 2 ----→ T2 , x: T1 e : T 2 :: X 1 → ∆ 2 ;C 1 T 2 ≤ T2 C 2 C 3 = ∆ 2 ≤ X 2 TA-ABS 2 Γ fun f :T 1 → T 2 , x:T 1 .e : T1 X 1 →X 2 ----→ T2 :: ∆ 1 - → ∆ 1 ;C 1 ,C 2 ,C 3 Γ v 1 : T2 ∆ 1 →∆ 2 ----→ T1 :: ∆ - → ∆ ;C 1 Γ v 2 : T Γ v : L ρ :: ∆ → ∆ ;C 1 X fresh C 2 = X ≥ ∆ (ρ:1) TA-UNLOCK Γ v. unlock: L ρ :: ∆ → X;C 1 ,C 2

Table 5. Constraint based type and effect system

The type system is basically a single-threaded analysis. For subject reduction later and soundness of the analysis, we also need to analyse processes running in parallel. The definition is straightforward, since a global program is well-typed simply if all its threads are. For one thread, p t : p ϕ;C , if t : T :: ϕ;C for some type T . We will abbreviate p 1 ϕ 1 ;C 1 . . . p k ϕ k ;C k by Φ.

Constraints C come in two forms: r ρ and X 1 ≤ X 2 ⊕ (ρ:n) resp. X 1 ≤ X 2 (ρ:n). We consider both kinds of constraints as independent, in particular a constraint of the form X 1 ≤ X 2 ⊕ (ρ:n) is considered as a constraint between the two variables X 1 and X 2 and not as a constraint between X 1 , X 2 , and ρ. Given C, we write C ρ for the ρconstraints in C and C X for the constraints concerning X-variables. Solutions to the constraints are ground substitutions; we use θ to denote substitutions. analogous to the distinction for the constraints, we write θ ρ for substitutions concerning the ρ-variables and θ X for substitutions concerning the X-variables. A ground θ ρ -substitution maps ρ's to finite sets {π 1 , . . . , π n } of labels and a ground θ X -substitution maps X's to ∆ 's (which are of the form ρ 1 :n 1 , . . . , ρ k :n k ); note that the range of the ground θ X -substitution still contains ρ-variables. We write

θ ρ |= C if θ ρ solves C ρ and analogously θ X |= C if θ X solves C X . For a θ = θ X θ ρ , we write θ |= C if θ ρ |= C and θ X |= C. Further- more we write C 1 |= C 2 if θ |= C 1 implies θ |= C 2 ,
for all ground substitutions θ . For the simple super-set constraints of the form ρ r, constraints always have a unique minimal solution. Analogously for the C X -constraints. A heap σ satisfies an abstract state ∆ , if ∆ over-approximates the lock counter for all locks in σ : Assuming that ∆ does not contain any ρ-variables and that the lock references in σ are labelled by π's, σ |= ∆ if ∑ π∈r σ (l π ) ≤ ∆ (r) (for all r in dom(∆ )). Given a constraint set C, an abstract state ∆ (with lock references l ρ labelled by variables) and a heap σ , we write σ

|= C ∆ ("σ satisfies ∆ under the constraints C"), iff θ |= C implies θ σ |= θ ∆ , for all θ . A heap σ satisfies a global effect Φ (written σ |= Φ), if σ |= C i ∆ i for all i ≤ k where Φ = p 1 ϕ 1 ;C 1 . . . p k ϕ k ;C k and ϕ i = ∆ i - → ∆ i .

Soundness

Next we prove soundness of the analysis wrt. the semantics. The core of the proof is the preservation of well-typedness under reduction ("subject reduction"). The static analysis does not only give back types (as an abstraction of resulting values) but also effects (in the form of pre-and post-specification). While types are preserved, we cannot expect that the effect of an expression remains unchanged under reduction. As the preand post-conditions specify (upper bounds on) the allowed lock values, the only steps which change are locking and unlocking steps. To relate the change of pre-condition with the steps of the system we assume the transitions to be labelled. Relevant is only the lock set variable ρ; the identity p of the thread, the label π and the actual identity of the lock are not relevant for the formulation of subject reduction, hence we do not include that information in the labels here. The steps for lock-taking are of the form

σ 1 p t 1 p ρ.lock
----→ σ 2 p t 2 ; unlocking steps analogously are labelled by ρ. unlock and all other steps are labelled by τ, denoting internal steps. The formulation of subject reduction can be seen as a form of simulation (cf. Figure 1): The concrete steps of the system -for one process in the formulation of subject reduction-are (weakly) simulated by changes on the abstract level; weakly, because τ-steps are ignored in the simulation. To make the parallel between simulation and subject reduction more visible, we write ∆ 1 ρ.lock ---→ ∆ 2 for ∆ 2 = ∆ 1 ⊕ ρ (and analogously for unlocking).

Lemma 1 (Subject reduction). Assume Γ P p t 1 :: Φ p ∆ 1 → ∆ 2 ;C 1 , and furthermore θ |= C 1 for some ground substitution and σ 1 |= θ ∆ 1 and σ 1 |= Φ.

1. σ 1 P p t 1 p τ --→ σ 2 P p t 2 , then Γ P p t 2 :: Φ p ∆ 1 - → ∆ 2 ,C 2 where C 1 ∆ 1 ≤ ∆ 1 and C 1 ∆ 2 ≤ ∆ 2 . Furthermore, C 1 |= C 2 and σ 2 |= θ ∆ 1 and σ 2 |= Φ. 2. σ 1 P p t 1 p ρ.lock ----→ σ 2 P p t 2 , then Γ P p t 2 :: Φ p ∆ 1 - → ∆ 2 ,C 2 where C 1 ∆ 1 ⊕ ρ ≤ ∆ 1 and C 1 ∆ 2 ≤ ∆ 2 . Furthermore C 1 |= C 2 and σ 2 |= θ ∆ 1 and σ 2 |= Φ. 3. σ 1 P p t 1 p ρ.unlock ------→ σ 2 P p t 2 , then Γ P p t 2 :: Φ p ∆ 1 - → ∆ 2 ,C 2 where C 1 ∆ 1 ρ ≤ ∆ 1 and C 1 ∆ 2 ≤ ∆ 2 . Furthermore C 1 |= C 2 and σ 2 |= θ ∆ 1 and σ 2 |= Φ.
The property of the lemma is shown pictorially in Figure 1.

As an immediate consequence, all configurations reachable from a well-typed initial configuration are well-typed itself. In particular, for all those reachable configurations, the corresponding pre-condition (together with the constraints) is a sound overapproximation of the actual lock counters in the heap.

Corollary 1 (Soundness of the approximation). Let σ 0 p t 0 be an initial configuration. Assume further Γ p t 0 :: p ∆ 0 → ∆ 2 ;C and θ |= C and where ∆ 0 is the empty context. If σ 0 p t 0 -→ * σ P, then Γ P :: Φ, where

Φ = p 1 ∆ 1 → ∆ 1 ;C 1 . . . p k ∆ k → ∆ k ;C k
and where σ |= θ ∆ i (for all i).

Race variables for deadlock detection

Next we use the information inferred by the type system in the previous section to locate control points in a program which potentially give rise to a deadlock. As we transform the given program after analyzing it, for improved precision, we assume that in the following all non-recursive function applications are instantiated/ inlined: a unique callsite per function ensures the most precise type-and effect information for that function, and correspondingly the best suitable instrumentation. The polymorphic type system gives a context-sensitive representation, which can then be instantiated per call-site. Note that this way, we need to analyze only the original program, and each function in there once, although for the next step, we duplicate methods. Recursive functions are instantiated once with (minimal) effects capturing all call-sites.

Those points are instrumented appropriately with assignments to additional shared variables, intended to flag a race. To be able to do so, we slightly need to extend our calculus. The current formulation does not have shared variables, as they are irrelevant for the analysis of the program, which concentrates on the locks. In the following we assume that we have appropriate syntax for accessing shared variables; we use z, z , z 1 , . . .

∆ ∆ σ 1 p t 1 σ 2 p t 2 = p τ |= θ |= θ ∆ 1 ∆ 1 σ 1 p t 1 σ 2 p t 2 ρ. lock p ρ. lock |= θ |= θ
Fig. 1. Subject reduction (case of unlocking analogous)

to denote shared variables, to distinguish them from the let-bound thread-local variables x and their syntactic variants. For simplicity, we assume that they are statically and globally given, i.e., we do not introduce syntax to declare them. Together with the lock references, their values are stored in σ . To reason about changes to those shared variables, we introduce steps of the form p !z --→ and p ?z --→, representing write resp. read access of process p to z. Alternatives to using a statically given set of shared variables, for instance using dynamically created pointers to the heaps are equally straightforward to introduce syntactically and semantically, without changing the overall story.

Deadlocks and races

We start by formally defining the notion of deadlock used here, which is fairly standard (see also [START_REF] Pun | Deadlock checking by a behavioral effect system for lock handling[END_REF]): a program is deadlocked, if a number of processes are cyclically waiting for each other's locks.

Definition 1 (Waiting for a lock). Given a configuration σ P, a process p waits for a lock l in σ P, written as waits(σ P, p, l), if (1) it is not the case that σ P p l.lock ----→, and furthermore (2) there exists σ s.t. σ P p l.lock ----→ σ P . In a situation without (1), we say that in configuration σ P, process p tries for lock l (written tries(σ P, p, l)).

Definition 2 (Deadlock).

A configuration σ P is deadlocked if σ (l i ) = p i (n i ) and furthermore waits(σ P, p i , l i+ k 1 ) (where k ≥ 2 and for all 0 ≤ i ≤ k -1). The + k is meant as addition modulo k. A configuration σ P contains a deadlock, if, starting from σ P, a deadlocked configuration is reachable; otherwise it is deadlock free.

Thus, a process can only be deadlocked, i.e., being part of a deadlocked configuration, if p holds at least one lock already, and is waiting for another one. With re-entrant locks, these two locks must be different. Independent from whether it leads to a deadlock or not, we call such a situation -holding a lock and attempting to acquire another one-a second lock point. More concretely, given a configuration, where we abbreviate the situation where process p holds lock l 1 and tries l 2 by slp(σ P) l 1 →l 2 p . The abstraction in the analysis uses program points π to represent concrete locks, and the goal thus is to detect in an approximate manner cycles using those abstractions π. As stated, a concrete deadlock involves a cycle of processes and locks. We call an abstract cycle ∆ C a sequence of pairs p: π with the interpretation that p i is holding π i and wants π i+1 (modulo the length of the cycle). Next we fix the definition for being a second lock point. At run-time a process is at a second lock point simply if it holds a lock and tries to acquire a another, different one.

Definition 3 (Second lock point (runtime)).

A local configuration σ p t is at a second point (holding l 1 and attempting l 2 , when specific), written slp(σ p t ) l 1 →l 2 , if σ (l 1 ) = p(n) and tries(σ p t , l 2 ). Analogously for abstract locks and heaps over those: slp(σ p t ) π 1 →π 2 , if σ (π 1 ) = p(n) and tries(σ p t , π 2 ). Given an abstract cycle ∆ C a local configuration is at a second lock point of ∆ C , if slp(σ p t ) π 1 →π 2 where, as specified by ∆ C , p holds π 1 and wants π 2 . Analogously we write for global configurations e.g., slp(σ P) π 1 →π 2 p , where p is the identity of a thread in P.

Ultimately, the purpose of the static analysis is to derive (an over-approximation of the) second lock points as a basis to instrument with race variables. The type system works thread-locally, i.e., it derives potential second lock points per thread. Given a static thread, i.e., an expression t without run-time syntax, second lock points are control points where the static analysis derives the danger of attempting a second lock. A control-point in a thread t corresponds to the occurrence of a sub-expression; we write t[t ] to denote the occurrence of t in t. As usual, occurrences are assumed to be unique. Definition 4 (Second lock point (static)). Given a static thread t 0 [t], a process identifier p and ∆ 0 p t 0 : ∆ , where ∆ 0 = •. The occurrence of t in t 0 is a static slp if:

1. t = let x:L {...,π,...} = v. lock in t . 2. ∆ 1 p t :: ∆ 2 , for some ∆ 1 and ∆ 2 , occurs in a sub-derivation of ∆ 0 t 0 :: ∆ . 3. there exists π ∈ ∆ 1 s.t. ∆ C p has π , and ∆ C p wants π .

Assume further σ 0 p t 0 -→ * σ p t . We say σ p t is at a static second lock point if t occurs as static second lock point in t 0 .

Lemma 2 (Static overapproximation of slp's). Given ∆ C and σ P be a reachable configuration where P = P p t and where furthermore the initial state of p is p t 0 . If σ p t is at a dynamic slp (wrt. ∆ C ), then t is a static slp (wrt. ∆ C ).

Proof. A direct consequence of soundness of the type system (cf. Corollary 1).

Next we define the notion of race. A race manifests itself, if at least two processes in a configuration attempt to access a shared variables at the same time, where at least one access is a write-access.

Definition 5 (Race).

A configuration σ P has a (manifest) race, if σ P p 1 !x ---→, and σ P p 2 !x ---→ or σ P p 2 ?x ---→, for two different p 1 and p 2 . A configuration σ P has a race if a configuration is reachable where a race manifests itself. A program has a race, if its initial configuration has a race; it is race-free else.

Race variables will be added to a program to assure that, if there is a deadlock, also a race occurs. More concretely, being based on the result of the static analysis, appropriate race variables are introduced for each static second lock points, namely immediately preceding them. Since static lock points over-approximate the dynamic ones and since being at a dynamic slp is a necessary condition for being involved in a deadlock, that assures that no deadlock remains undetected when checking for races. In that way, that the additional variables "protect" the second lock points.

Definition 6 (Protection).

A property ψ is protected by a variable z starting from configuration σ p t , if σ p t -→ * a -→ σ p t and ψ(p t ) implies that a =!z. We say, ψ is protected by z, if it is protected by z starting from an arbitrary configuration.

Protection, as just defined, refers to a property and the execution of a single thread. For race checking, it must be assured that the local properties are protected by the same, i.e., shared variable are necessarily and commonly reached. That this is the case is formulated in the following lemma: Lemma 3 (Lifting). Assume two processes p 1 t 1 and p 2 t 2 and two thread-local properties ϕ 1 and ϕ 2 (for p 1 and p 2 , respectively). If ψ 1 is protected by x for p 1 t 1 and ψ 2 for p 2 t 2 by the same variable, and a configuration σ P with P = p 1 t 1 p 2 t 2 P is reachable from σ P such that ψ 1 ∧ ψ 2 holds, then σ P has a race.

Instrumentation

Next we specify how to transform the program by adding race variables. The idea is simple: each static second lock point, as determined statically by the type system, is instrumented by an appropriate race variable, adding it in front of the second lock point. In general, to try to detect different potential deadlocks at the same time, different race variables may be added simultaneously (at different points in the program). The following definition defines where to add a race variable representing one particular cycle of locks ∆ C . Since the instrumentation is determined by the static type system, one may combine the derivation of the corresponding lock information by the rules of Table 5 such that the result of the derivation not only derives type and effect information, but also transforms the program at the same time, with judgments of the form Γ t t : T :: ϕ, where t is transformed to t . Note that we assume that a solution to the constraint set has been determined and applied to the type and the effects. Since the only control points in need of instrumentation are where a lock is taken, the transformation for all syntactic constructs is trivial, leaving the expression unchanged, except for v. lock-expressions, where the additional assignment is added if the condition for static slp is satisfied (cf. equation ( 7) from Definition 4). Definition 7 (Transformation). Given an abstract cycle ∆ C . For a process p from that cycle, the control points instrumented by a !z are defined as follows:

Γ v : L r :: ∆ 1 - → ∆ 1 ∆ = ∆ 1 ⊕ r π ∈ r π ∈ ∆ 1 ∆ C p wants π ∆ C p has π Γ v. lock : L r :: ∆ 1 - → ∆ 2 Γ , x:L r t t : T :: ∆ 2 → ∆ 3 Γ let x:T = v. lock in t let x:T = (!z; v. lock) in t : T :: ∆ 1 - → ∆ 3
By construction, the added race variable protects the corresponding static slp, and thus, ultimately the corresponding dynamic slp's, as the static ones over-approximate the dynamic ones.

Lemma 4 (Race variables protect slp's). Given a cycle ∆ C and a corresponding transformed program. Then all static second lock points in the program are protected by the race variable (starting from the initial configuration).

The next lemma shows that there is a race "right in front of" a deadlocked configuration for a transformed program.

Lemma 5. Given an abstract cycle ∆ C , and let P 0 be a transformed program according to Definition 7. If the initial configuration σ 0 P 0 has a deadlock wrt. ∆ C , then σ 0 P 0 has a race.

Proof. By the definition of deadlock (cf. Definition 2), some deadlocked configuration σ P is reachable from the initial configuration: σ 0 P 0 -→ * σ P where P = . . . p i t i . . . p j t j . . . ,

where by assumption, the processes p i and the locks they are holding, resp. on which they are blocked are given by ∆ C , i.e., σ (l i ) = p i (n i ) and waits(σ P , p i , l i+ k 1 ). Clearly, each participating process σ p i t i is at a dynamic slp (cf. Definition 3). Since those are over-approximated by their static analogues (cf. Lemma 2), the occurrence of t i in t 0 i resp. of t j in t 0 j is a static slp. By Lemma 4, all static slp (wrt. the given cycle) are protected, starting from the initial configuration, by the corresponding race variable. This together with the fact that σ p i t i is reachable from σ 0 p i t 0 i implies that the static slp in each process p i is protected by the same variable x. Hence, by Lemma 3, σ 0 P 0 has a race between p i and p j .

The previous lemma showed that the race variables are added at the "right places" to detect deadlocks. Note, however, that the property of the lemma was formulated for the transformed program while, of course, we intend to detect deadlocks in the original program. So to use the result of Lemma 5 on the original program, we need to convince ourselves that the transformation does not change (in a relevant way) the behavior of the program, in particular that it neither introduces nor removes deadlocks. Since the instrumentation only adds variables which do not influence the behavior, this preservation behavior is obvious. The following lemma shows that transforming programs by instrumenting race variables preserves behavior.

Lemma 6 (Transformation preserves behavior). P is deadlock-free iff P T is deadlockfree, for arbitrary programs.

Next, we state that with the absence of data race in a transformed program, the corresponding original one is deadlock-free: Lemma 7 (Data races and deadlocks). P is deadlock-free if P T is race-free, for arbitrary programs.

Gate locks

Next we refine the transformation to improve its precision. By definition, races are inherently binary, whereas deadlocks in general are not, i.e., there may be more than two processes participating in a cyclic wait. In a transformed program, all the processes involved in a specific abstract cycle ∆ C share a common race variable. While sound, this would lead to unnecessarily many false alarms, because already if two processes as part of a cycle of length n > 2 reach simultaneously their race-variable-instrumented control-points, a race occurs, even if the cycle may never be closed by the remaining processes. In the following, we add not only race variables, but also additional locks, assuring that parts of a cycle do not already lead to a race; we call these locks gate locks. Adding new locks, however, needs to be done carefully so as not to change the behavior of the program, in particular, not to break Lemma 6.

We first define another (conceptual) use of locks, denoted short-lived locks. A process which is holding a short-lived lock has to first release it before trying any other lock. It is obvious to see that transforming a program by adding short-lived locks does not lead to more deadlocks.

A gate lock is a short-lived lock which is specially used to protect the access to race variables in a program. Since gate locks are short-lived, no new deadlocks will be introduced. Similar to the transformation in Definition 7, we still instrument with race variables at the static second lock points, but also wrap the access with locking/unlocking of the corresponding gate lock (there is one gate lock per ∆ C ). However, we pick one of the processes in ∆ C which only accesses the race variable without the gate lock held. This transformation ensures that the picked process and exactly one of the other processes involved in a deadlock cycle may reach the static second lock points at the same time, and thus a race occurs. That is, only the race between the process which could close the deadlock cycle and any one of the other processes involved in the deadlock will be triggered.

Observe that depending on the chosen process, the race checker may or may not report a race-due to the soundness of our approach, we are obviously interested in the best result, which is "no race detected". Therefore, we suggest to run the analysis with all processes to find the optimal result. Note that checks for different cycles and with different "special" processes for the gate lock-based instrumentation can easily be run in parallel or distributed. It is also possible to instrument a single program for the detection of multiple cycles: even though a lock statement can be a second lock point for multiple abstract locks, the transformations for each of them do not interfere with each other, and can be analyzed in a single race checker-run.

Theorem 1. Given a program P, P T is a transformed program of P instrumenting with race variables and gate locks, P is deadlock-free if P T is race-free.

Conclusion

We presented an approach to statically analyze multi-threaded programs by reducing the problem of deadlock checking to data race checking. The type and effect system statically over-approximates program points, where deadlocks may manifest themselves and instruments programs with additional variables to signal a race. Additional locks are added to avoid too many spurious false alarms. We show soundness of the approach, i.e., the program is deadlock free, if the corresponding transformed program is race free.

Numerous approaches have been investigated and implemented over the years to analyze concurrent and multi-threaded programs (cf. e.g. [START_REF] Rinard | Analysis of multithreaded programs[END_REF] for a survey of various static analyses). Not surprisingly, in particular approaches to prevent races [START_REF] Beckman | A survey of methods for preventing race conditions[END_REF] and/or deadlocks [START_REF] Corbett | Evaluating deadlock detection methods for concurrent software[END_REF] have been extensively studied for various languages and are based on different techniques. (Type-based) analyses for race detection include [START_REF] Abadi | Types for safe locking: Static race detection for Java[END_REF] [10] [START_REF] Boyapati | A parameterized type system for race-free Java programs[END_REF] [19] [START_REF] Grossman | Type-safe multithreading in Cyclone[END_REF] to name a few. Partly based on similar techniques, likewise for the prevention of deadlocks are [21] [14]. Static detection of potential deadlocks is a recurring topic: traditionally, a lock-analysis is carried out to discover whether the locks can be ordered, such that subsequent locks can only be acquired following that order [START_REF] Birrell | An introduction to programming with threads[END_REF]. Then, a deadlock is immediately ruled out as this construction precludes any "deadly embrace". The lock order may be specified by the user, or inferred [START_REF] Boyapati | Ownership types for safe programming: Preventing data races and deadlocks[END_REF]. To the best of our knowledge, our contribution is the first formulation of (potential) deadlocks in terms of data races. Due to the number of race variables introduced in the transformation, and assuming that race checking scales linearly in their number, we expect an efficiency comparable to explicit-state model checking.

In general, races are prevented not just by protecting shared data via locks; a good strategy is to avoid also shared data in the first place. The biggest challenge for static analysis, especially when insisting on soundness of the analysis, is to achieve better approximations as far as the danger of shared, concurrent access is concerned. Indeed, the difference between an overly approximate analysis and one that is usable in practice lies not so much in obtaining more refined conditions for races as such, but to get a grip on the imprecision caused by aliasing, and the same applies to static deadlock prevention.

Future work A natural extension of our work would be an implementation of our type and effect system to transform concurrent programs written in e.g. C and Java. Complications in those languages like aliasing need to be taken into account, although results from a may-alias analysis could directly be consumed by our analysis. The potential blowup of source code-size through instantiation of function applications can be avoided by directly making use of context in the race-checker, instead of working on a source-based transformed program. As a first step, we intend to make our approach more applicable, to directly integrate the transformation-phase into Goblint, so that no explicit transformation of C programs needs to take place.

For practical applications, our restriction on a fixed number of processes will not fit every program, as will the required static enumeration of abstract cycle information. We presume that our approach will work best on code found e.g. in the realm of embedded system, where generally a more resource-aware programming style means that threads and other resources are statically allocated.

For lack of space, most of the proofs have been omitted here. Further details can be found in the accompanying technical report [START_REF] Pun | Deadlock checking by data race detection[END_REF].

r

  ::= ρ | {π} | r r lock/label sets T ::= B | L r | T ϕ -→ T types Ŝ ::= ∀ Y :C. T type schemes ϕ ::= ∆ → ∆ effects/pre-and post specification ∆ ::= • | X | ∆ , r:n lock env./abstract state C

  1 .x:T 2 .t ,l 2 )); . . . ; spawn ( phil ( l n ,l 1 ))

	Listing 1. Dining Philosophers
	let l 1 = new L ; . . .; l n = new L	/* create all locks */
	phil = fun F (x , y ) . ( x . lock ; y . lock ;	/* eat */
	y . unlock ; x . unlock ; /* think */
	F (x , y ) )
	in spawn ( phil ( l 1

Table 3 .

 3 Local

steps by executing l. lock. There are two situations where that command does not block, namely the lock is free or it is already held by the requesting process p. The heap update σ + p l is defined as follows

:: ∆ -→ ∆ ;C 2 T 2 ≤ T2 C X fresh TA-APP Γ v 1 v 2 : T1 :: ∆ -→ X;C 1 ,C 2 ,C, ∆ ≤ ∆ 1 , ∆ 2 ≤ X T = T1 = T2 T ;C = T1 ∨ T2 ∆ ;C = ∆ 1 ∨ ∆ 2 Γ v : Bool:: ∆ 0 -→ ∆ 0 ;C 0 Γe 1 : T1 :: ∆ 0 -→ ∆ 1 ;C 1 Γ e 2 : T2 :: ∆ 0 -→ ∆ 2 ;C 2 TA-COND Γ if v then e 1 else e 2 : T :: ∆ 0 → ∆ ;C 0 ,C 1 ,C 2 ,C,C Γ e 1 : T1 :: ∆ 1 → ∆ 2 ;C 1 T1 = T 1 Ŝ1 = close(Γ ,C 1 , T1 ) Γ , x: Ŝ1 e 2 : T2 :: ∆ 2

→ ∆ 3 ;C 2 TA-LET Γ let x:T 1 = e 1 in e 2 : T2 ::∆ 1 → ∆ 3 ;C 2 Γ v : L ρ :: ∆ → ∆ ;C 1 X fresh C 2 = X ≥ ∆ ⊕ (ρ:1) TA-LOCK Γ v. lock: L ρ :: ∆ → X;C 1 ,C 2

Acknowledgements We are grateful for detailed discussion of Goblint to Kalmer Apinis, and Axel Simon, from TU München, Germany.