Henri Casanova
email: henric@hawaii.edu

Fanny Dufossé

Yves Robert

Frédéric Vivien

Mapping Tightly-Coupled Applications on Volatile Resources

Platforms that comprise volatile processors, such as desktop grids, have been traditionally used for executing independent-task applications. In this work we study the scheduling of tightly-coupled iterative masterworker applications onto volatile processors. The main challenge is that workers must be simultaneously available for the application to make progress. We consider two additional complications: one should take into account that workers can become temporarily reclaimed and, for dataintensive applications, one should account for the limited bandwidth between the master and the workers.

In this context, our first contribution is a theoretical study of the scheduling problem in its off-line version, i.e., when processor availability is known in advance. Even in this case the problem is NP-hard. Our second contribution is an analytical approximation of the expectation of the time needed by a set of workers to complete a set of tasks and of the probability of success of this computation. This approximation relies on a Markovian assumption for the temporal availability of processors. Our third contribution is a set of heuristics, some of which use the above approximation to favor reliable processors in a sensible manner. We evaluate these heuristics in simulation. We identify some heuristics that significantly outperform their competitors and derive heuristic design guidelines.

I. INTRODUCTION

In this paper we study the problem of scheduling parallel applications onto volatile processors. We target typical scientific iterative applications in which a master process parallelizes the execution of each iteration across worker processes. Each iteration requires the execution of a fixed number of tasks, with a global synchronization at the end of each iteration.

We consider a platform that consists of processors that alternate between periods of availability and periods of unavailability. When available each processor runs a worker process, and a master process can choose to enroll a subset of these workers to participate in the application execution. Worker unavailability can be due to software faults, in which case unavailability may last only the time of a reboot. A hardware failure can lead to a longer unavailability period, until a repair is completed and followed by a reboot. We consider a third source of processor unavailability, which comes from cyclestealing scenarios: when a processor is contributed to the platform by an individual owner, this owner can reclaim it at any time without notice for some unknown length of time. A difference here is that the processor is merely preempted (as opposed to being terminated) until the processor is no longer reclaimed. A worker process on this processor can later resume its computation. Accordingly, we use a 3-state availability model: UP (available), DOWN (crashed, computation is lost) and RECLAIMED (preempted, but computation can resume later). Our platform model also accounts for the fact that, due to bandwidth limitation, the master is only able to communicate simultaneously with a limited number of workers (to send them the application program as well as task data). This limitation corresponds to the bounded multi-port model [START_REF] Hong | Adaptive allocation of independent tasks to maximize throughput[END_REF]. It turns out that limiting the communication capacity of the master dramatically complicates the design of scheduling strategies. But without this limitation, it would be in principle possible to enroll thousands of new processors at each iteration, which is simply not feasible in practice even if these many processors are available.

Given the above application and platform models, and given a deadline (typically expressed in hours or days), the scheduling problem under study is that of maximizing the expected number of application iterations successfully completed before the deadline. Informally, during each iteration, one must use the "best" processors among those that are simultaneously UP ; these could be the fastest ones, or those expected to remain UP for the longest time. In addition, with processors failing, becoming reclaimed, and becoming UP again later, one has to decide when and how to change the set of currently enrolled processors. Each such change comes at a price: first, the application program needs to be sent to newly enrolled processors, thereby consuming some of the master's bandwidth; second, and more importantly, iteration computation that was only partially completed is lost due to the tight coupling of tasks.

Our contribution in this work is threefold. First, we determine the complexity of the off-line scheduling problem, i.e., when processor availability is known in advance. Even with such knowledge the problem is NP-hard. Second, we compute approximations of the expectation of the time needed by a set of processors to complete a set of tasks and of the probability that this computation succeeds. These approximations provide a sound basis for making sensible scheduling decisions. Third, we design several on-line heuristics that we evaluate in simulation. Some of these contributions assume Markovian processor availability, which is not representative of real-world platforms but provides a tractable framework for obtaining theoretical and experimental results in laboratory conditions. Due to lack of space we refer the reader to the companion research report [START_REF] Casanova | Mapping Tightly-Coupled Applications on Volatile Resources[END_REF] for a worked-out example, related work, statements and proofs of all NP-completeness results, and complete experimental results.

II. MODELS AND ASSUMPTIONS

A. Application model

We consider an application that performs a sequence of iterations. Each iteration consists of executing m tasks and ends with a global synchronization. All m tasks are identical (in terms of computational cost) and communicate throughout the iteration execution. Therefore, all tasks must make progress at the same rate. If a task is terminated prematurely (due to a worker failure), all computation performed so far for the current iteration is lost, and the entire iteration has to be restarted. If a task is suspended (due to a worker becoming temporarily reclaimed), then the entire execution of the iteration is also suspended. Due to the global synchronization, there is no overlap between communication of task data and computation, but only between communication between tasks and computation. We thus consider that an iteration proceeds in two phases: a communication phase and a computation phase. Finally, before being able to compute, a worker must acquire the application code once (e.g., binary executable, byte code), of constant size V prog in bytes, and the input data for each task and iteration, of constant size V data in bytes. Data messages depend on tasks but have identical size.

B. Platform model

The platform comprises p processors, or workers. Worker P q , q = 1, . . . , p, can be in one of three states (UP , RECLAIMED or DOWN ), and transitions between these states occur for each processor at each time-slot independently of the other processors. More precisely:

• Any UP processor can become DOWN or RECLAIMED.

• Any UP or RECLAIMED processor can become DOWN . It then loses the application program and all the data for its current tasks. If it was computing some of these tasks, these computations are lost. • Any UP processor can become RECLAIMED.

The processor does not lose any state. If it was receiving the application program or data for a task, the communication is temporarily suspended.

If it was computing a task, the computation on all processors is temporarily suspended. We denote by S q the vector that gives the state of P q at each time-slot starting with time-slot 0.

P q can compute a task in w q time-slots if it remains UP . If w q = w for each processor P q , then the processors are homogeneous. The master has network bandwidth BW and communicates with a worker with bandwidth bw, meaning that we assume same capacity links from the master to each worker. Here we equate bandwidth with data transfer rate, acknowledging that in practice the data transfer rate is a fraction of the physical bandwidth. Let n prog be the number of workers receiving the program at time t, and let n data be the number of workers receiving the input data of a task at time t. The constraint on the master's bandwidth writes n prog + n data ≤ n com = BW /bw , where n com is the maximum number of. processors that the master can communicate with (sending either program or input data) at each time-slot. Indeed, consider a worker on processor P q that is communicating at time t. Either P q is receiving the program, or it is receiving data for a task. In both cases, it does this at data transfer rate bw. Overall, the master can execute only a limited number n com of such communications simultaneously. The time for a worker to receive the program is T prog = V prog /bw, and the time to receive the data is T data = V data /bw. For simplicity we assume that T prog and T data consist of integral numbers of time-slots. We also assume that the master is always UP , which can be enforced by using, for instance, two dedicated servers with a primary backup mechanism.

C. Application execution model

Let config(t) denote the set of workers enrolled by the master, or configuration, at time t. The configuration is determined by an application scheduler, and in this work we propose algorithms to be used by this scheduler. To complete an iteration, enrolled workers must progress concurrently throughout the computations. One worker may be assigned several tasks and execute them concurrently if it has enough memory to do so. Formally, we define for each worker P q a bound µ q on the maximum number of tasks that it can execute concurrently. We assume that p q=1 µ q ≥ m, otherwise the configuration cannot execute the application. The m tasks are mapped onto k ≤ m workers. Each enrolled worker P q is assigned x q tasks, where k q=1 x q = m. To be able to compute their tasks, the k enrolled workers must have received the application program and all necessary data. More precisely: (i) each enrolled worker P q must receive the program, unless it has received it at some previous time and has not be DOWN since then; (ii) in addition, each worker P q must receive a number x q of data messages (one per task) from the master. Suppose that since the begin of the current iteration P q has received x q data messages. At least (x q -x q )T data time-slots are needed for this communication, and likely more since the master can be engaged in at most n com concurrent communications.

Overall, the computation can start at a time t only if each of the k enrolled workers is in the UP state, has the program, has the data of all its allocated tasks, and has never been in the DOWN state since receiving these messages. Because tasks must proceed in locked steps, the execution goes at the pace of the slowest worker. Hence the computation of an iteration requires max q (x q w q ) time-slots of concurrent computations (not necessarily consecutive, due to workers possibly being reclaimed). Consider the interval of time between time t 1 and time t 2 = t 1 + max q (x q w q ) + t -1 for some t . For the iteration to be successfully completed by time t 2 , between t 1 and t 2 there must be max q (x q w q ) timeslots for which all enrolled workers are simultaneously UP , and there may be t time-slots during which one or more workers are RECLAIMED.

The scheduler may choose a new configuration at each time t. If at least one worker in config(t) becomes DOWN , the scheduler must select another configuration and restart the iteration from scratch. Even if all workers in config(t) are UP , the scheduler may decide to change the configuration because more desirable (i.e., faster, more reliable) workers have become available. Let P q be a newly enrolled worker at that point, i.e., P q ∈ config(t + 1) \ config(t). P q needs to receive the program unless it already has a copy of it and has not been DOWN since receiving it. In all cases, P q needs to receive task data, i.e., x q messages of V data bytes. This holds true even if P q had been enrolled at time t < t but was un-enrolled since then. In other words, any interrupted communication must be resumed from scratch if the worker became DOWN or was removed from the configuration.

III. OFF-LINE COMPLEXITY

The scheduling problem is to maximize the expected number of completed application iterations before time N , where N is a specified deadline. In the off-line version of this problem, one assumes full knowledge of future worker states. In other words, S q [j] is known for 1 ≤ q ≤ p and 1 ≤ j ≤ N . It is shown in [START_REF] Casanova | Mapping Tightly-Coupled Applications on Volatile Resources[END_REF] that the simplest off-line and deterministic versions of the problem are NP-hard.

IV. ANALYTICAL APPROXIMATIONS

In this section, we compute the expectation of the time needed by a configuration to compute a given workload conditioned on this computation being successful (i.e., with no worker becoming DOWN ), as well as the probability of success. Intuitively, these quantities seem relevant for developing scheduling heuristics that account for the need for workers to be UP simultaneously, and for workers that can become temporarily RECLAIMED. To compute the above expectation and probability, we introduce a Markov model of processor availability. The availability of processor P q is described by a 3-state recurrent aperiodic Markov chain, defined by 9 probabilities: P (q) i,j , with i, j ∈ {u, r, d}, is the probability for P q to move from state i at time t to state j at time t + 1, which does not depend on t.

A. Probability of success and expected duration of a computation

Consider a set S of workers all in the UP state at time 0. This set is assigned a workload that requires W time-slots of simultaneous computation. To complete this workload successfully, all the workers in S must be simultaneously UP during another W -1 time-slots. They can possibly become RECLAIMED (thereby temporarily suspending the execution) but must never become DOWN in between. What is the probability of the workload being completed? And, if it is successfully completed, what is the expectation of the number of time-slots until completion?

Definition 1: Knowing that all processors in a set S are UP at time-slot t 1 , let P (S) + be the conditional probability that they will all be UP simultaneously at a later time-slot, without any of them going to the DOWN state in between. Formally, knowing that ∀P q ∈ S, S q [t 1 ] = u, P (S) + is the conditional probability that there exists a time t 2 > t 1 such that ∀P q ∈ S, S q [t 2 ] = u and S q [t] = d for t 1 < t < t 2 .

Definition 2: Let E (S) (W) be the conditional expectation of the number of time-slots required by a set of processors S to complete a workload of size W knowing that all processors in S are UP at the current time-slot t 1 and none will become DOWN before completing this workload. Formally, knowing that S q [t 1 ] = u, and that there exist

W -1 time-slots t 2 < t 3 < • • • < t W , with t 1 < t 2 , S q [t i ] = u for i ∈ [2, W ], and S q [t] = d for t ∈ [t 1 , t W ], E (S) (W ) is the expectation of t W -t 1 + 1 conditioned on success.
Theorem 4.1: It is possible to approximate the values of P (S) + and E (S) (W ) numerically up to an arbitrary precision ε in fully polynomial time.

B. Probability of success and expected duration of a communication

Similar approximations cannot be obtained for communications due to complexity added by the n com constraint. Instead, we resort to a coarser approximation as explained hereafter. Let S be a set of enrolled workers. For worker P q ∈ S, let n q be the number of time-slots of communication needed to receive the application program and all the data of its allocated tasks. Suppose first that |S| ≤ n com . In this case, the expected communication time on worker P q , E q , can be estimated precisely reusing the result in the previous section: E q = E (Pq) (n q ). We then estimate the expected communication time of the current configuration as E (S) comm = max Pq∈S {E (Pq) (n q )} . In the case |S| ≥ n com , obtaining an estimate close to the actual expected communication time seems out of reach. Instead, we use a coarser estimation:

E (S) comm = max max Pq∈S E (Pq) (n q ) , Pq ∈S nq ncom . Let P (Pq)
N D (t) denote the probability that worker P q that was UP at time t does not become DOWN between time t and time t + t. The probability of success is then estimated as P (S)

comm = Pq∈S P (Pq) N D (E (S)
comm ) . The expression for P (S) comm does not take into account the time needed after the end of all communications for all workers to be UP simultaneously. The probability of success of an iteration is estimated by multiplying the probability of success of the communications and the probability of success of the computations.

V. ON-LINE HEURISTICS

We propose heuristics for solving the on-line version of the scheduling problem, i.e., assuming no knowledge of future processor states. Conceptually, we distinguish between two classes of heuristics. Passive heuristics conservatively keep current processors active as long as possible: the current configuration is changed only when one of the enrolled processors becomes DOWN . In this case, all previously executed work is lost. However, a worker that has not become DOWN but has already received task data, can reuse that data if the scheduler reassigns tasks to it. Proactive heuristics allow for a complete reconfiguration even if no worker fails, possibly aborting ongoing computation if a better configuration is found. This makes it possible for an iteration to never complete. A criterion must thus be derived to decide whether and when such an aggressive reconfiguration is worthwhile. Our proactive heuristics are defined by a pair (criterion, passive heuristic). When a new configuration is computed using the heuristic, it is compared to the current configuration according to the criterion. If the new configuration is better than the current one, then it is launched, leading to new communications and task allocations. Otherwise, the execution continues with the current configuration for an additional time slot.

A. Passive heuristics

Passive heuristics assign tasks to workers, which must be in the UP state, one by one until m tasks are assigned. Each task is assigned to a worker according to a criterion that defines the heuristic. As described hereafter, we consider four different criteria: probability of success, expected completion time, estimated yield, and estimated apparent yield.

• IP (Incremental: Probability of success) -This heuristic attempts to find configurations with high probability of success. The next task is assigned to the worker such that the probability of success of all currently assigned tasks (including the new one) is maximized. More precisely, consider the set S of workers with at least one task already assigned. For each worker P q , either in S or not, we compute the probability P (S) (q) of success of the communication and the computation if the additional task is assigned to P q , using the results of Section IV: P (S) (q) = P (S∪{Pq}) (W q ) × P (S∪{Pq}) comm with W q the maximal load in S∪{P q } with an additional task on P q . We assign the next task to worker P q0 , with q 0 = ArgMax P (S) (q) . This natural idea of the most reliable workers has been used for scheduling independent tasks in [START_REF] Estrada | The Effectiveness of Threshold-Based Scheduling Policies in BOINC Projects[END_REF], [START_REF] Anglano | Fault-aware scheduling for Bag-of-Tasks applications on Desktop Grids[END_REF], [START_REF] Wingstrom | Probabilistic Allocation of Tasks on Desktop Grids[END_REF].

• IE (Incremental: Expected completion time) -This heuristic attempts to find fast configurations, without considering reliability. The next task is assigned to the worker that minimizes the expected execution time of the iteration. More precisely, consider the set S of workers with at least one task already assigned. For each worker P q , either in S or not, we compute the expected communication time E (S∪{Pq}) comm and the expected computation time E (S∪{Pq}) (W q ) with an additional task on P q . We obtain the expected duration of the iteration E (S) (q) = E (S∪{Pq}) comm + E (S∪{Pq}) (W q ). We assign the next task to worker P q0 , with q 0 = ArgMin E (S) (q) . This idea of picking the fatest workers has been used for scheduling independent tasks in [START_REF] Kondo | Resource Management for Rapid Application Turnaround on Enterprise Desktop Grids[END_REF].

• IY (Incremental: Expected yield) -This heuristic assigns the next task to the worker that maximizes the yield of the configuration. The yield is the expected value of the inverse of the execution time of the current iteration, which we estimate as follows. For a given configuration with probability of success P and expected completion time E for an iteration that has already been running for t time slots, the yield is estimated as Y = P E+t . Intuitively, we expect the yield to achieve a trade-off between reliability (probability of success) and execution speed. Consider the set S of workers with at least one task already assigned. For each processor P q , either in S or not, we compute the expected yield with an additional task on P q : let P (S) (q) be the probability computed for heuristic IP, E (S) (q) be the expected completion time computed for heuristic IE, and t be the time spent since the beginning of the current iteration. We assign the next task to worker P q0 , with q 0 = ArgMax P (S) (q) t+E (S) (q) . This general idea of trading off reliability for speed has been used in the context of independent tasks in many previous works [START_REF] Kondo | Resource Management for Rapid Application Turnaround on Enterprise Desktop Grids[END_REF], [START_REF] Anglano | Fault-aware scheduling for Bag-of-Tasks applications on Desktop Grids[END_REF], [START_REF] Byun | MJSA: Markov job scheduler based on availability in desktop grid computing environment[END_REF], [START_REF] Heien | Computing Low Latency Batches with Unreliable Workers in Volunteer Computing Environments[END_REF].

• IAY (Incremental: Expected apparent yield) -The yield takes into account the time already spent in the current iteration. It could be worthwhile to consider only future work, i.e., the remaining time until iteration completion. To this end we define the apparent yield as AY = P E . Using the same notations as for heuristic IY, we assign the next task to processor P q0 with q 0 = ArgMax P (S) (q) E (S) (q) . B. Proactive heuristics Consider an application executing on a platform using a passive heuristic H and criterion C at some time t. The configuration config(t -1) was selected by H at time t ≤ t -1 because of a configuration change due to a proactive decision, due to a worker becoming DOWN , or due to the beginning of a new iteration. Let config 1 = config(t ) = config(t -1). At time t , the configuration was measured by criterion C value c . Suppose that by time t no worker in this configuration has failed. Between t and t, some work may have been done: some communications may be in process or completed, and computations may have started. Consequently, the measure of this configuration given by C should be updated to account for the progress between t and t. Let c be the updated value of criterion C for the current configuration. At step t, a new configuration is computed from scratch using heuristic H, as if no task were allocated to any worker. Let config 2 be this new configuration and c 2 its measure by C. If c ≥ c 2 , then the current configuration at time t -1 is kept for another time-slot: config(t) = config 1 . Otherwise, the current configuration is interrupted, and the new configuration is config(t) = config 2 .

For certain criterion choices, a heuristic could diverge and continually change the configuration, even with workers that are reliably UP . To avoid this divergence, proactive criteria have to respect the following constraint: a given configuration that has been running for t + 1 time-slots must be better for the proactive criterion than the same configuration running for t time slots. With this constraint, all possible configurations are ordered by their value for the selected criterion at the beginning of the iteration, and a lower-ranked configuration in this order cannot be chosen to replace the current configuration. As the number of possible configurations is finite, no proactive heuristic can diverge. The four criteria used to define passive heuristics in the previous section meet this constraint. However, AY (Apparent Yield) leads to many (unnecessary) configuration changes before converging, while the other criteria should be stable. Hence, for the proactive criterion C, we only retain P (Probability of success), E (Expected completion time) and Y (Expected yield). Any passive heuristic H can be used as the building block for a proactive heuristic. We thus obtain 3 × 4 proactive heuristics named C-H where C ∈ {P, E, Y} and H ∈ {IP, IE, IY, IAY}. VI. CONCLUSION Unlike previous work that has considered looselycoupled master-worker applications, in this study a single processor failure can have a dramatic effect on application execution. The requirement that the application can progress only when all enrolled processors are simultaneously available, dramatically complicates all scheduling decisions. By assuming a Markov model of processor availability, we have proposed polynomial time approximation schemes to compute the expected completion time of a computation, and its probability of success. We have then proposed many heuristics that are easily defined as combinations of two among four sensible metrics: probability of success, expected completion time, expected yield and expected apparent yield. All these heuristics have been extensively evaluated in simulations, see [START_REF] Casanova | Mapping Tightly-Coupled Applications on Volatile Resources[END_REF]. The main conclusion is that a proactive heuristic that selects processors to maximize expected execution time and changes configuration based on yield or probability of success is very promising.

Acknowledgments. This work was supported in part by the ANR RESCUE project.


Frédéric Yves Robert

Dounia Zaidouni

On the complexity of scheduling checkpoints for computational workflows

On the complexity of scheduling checkpoints for computational workflows

Yves Robert 1,2 , Frédéric Vivien 1 and Dounia Zaidouni 1 1. Ecole Normale Supérieure de Lyon & INRIA, France {Yves.Robert|Frederic.Vivien|Dounia.Zaidouni}@ens-lyon.fr 2. University of Tennessee Knoxville, USA

Abstract-This paper deals with the complexity of scheduling computational workflows in the presence of Exponentially distributed failures. When such a failure occurs, rollback and recovery is used so that the execution can resume from the last checkpointed state. The goal is to minimize the expected execution time, and we have to decide in which order to execute the tasks, and whether to checkpoint or not after the completion of each given task. We show that this scheduling problem is strongly NP-complete, and propose a (polynomialtime) dynamic programming algorithm for the case where the application graph is a linear chain. These results lay the theoretical foundations of the problem, and constitute a prerequisite before discussing scheduling strategies for arbitrary DAGS of moldable tasks subject to general failure distributions.

I. Introduction

In this paper, we provide preliminary results on the complexity of scheduling workflows in the presence of Exponentially distributed failures. More precisely, there is an application graph to be executed, whose tasks are executed sequentially on some (parallel) platform. When a failure occurs, rollback and recovery is used so that the execution can resume from the last checkpointed state. In a nutshell, the goal is to decide (i) in which order to execute the tasks (always enforcing all dependences); and (ii) whether to checkpoint or not after the completion of each given task. The objective is to minimize the expectation of the total execution time. We show that this scheduling problem is quite difficult: we establish the strong NP-completeness of the instance with independent tasks (Section IV). We also propose a (polynomial-time) dynamic programming algorithm for the case where the application graph is a linear chain (Section V). Both results rely on an exact formula for the expected time needed to successfully execute a task and checkpoint right after it (Section III). To the best of our knowledge, this formula, together with its recursive proof, is original. Before detailing these results, we outline the framework in full details in Section II. In the last sections of the paper, we discuss some possible extensions of this work (Section VI), and we briefly survey related work (Section VII). Finally, we provide concluding remarks in Section VIII.

II. Framework

We are given an application task graph G = (V, E), i.e., a Directed Acylic Graph (DAG) where nodes represent tasks and edges correspond to dependences between them. We let V = {T 1 , T 2 , . . . , T n }, and each task T i is weighted by its computational weight w i . The application DAG is executed on a platform of p identical processors. We use the term processor to indicate any individually scheduled compute resource (a core, a multi-core processor, a cluster node) so that our work is agnostic to the granularity of the platform. These processors are subject to failures, and we assume that a standard coordinated checkpointing and roll-back recovery is performed at the system level. At the end of the execution of each task T i , we can decide either to perform a checkpoint, or to proceed with the computation of another task. The former option (checkpoint) induces overhead to the total execution time, but allows to recover from the current state if a failure happens further on, thereby reducing the time wasted due to that failure. The latter option (no checkpoint) saves time in a failure-free execution but is more risky, since a subsequent failure would cause a longer rollback from an older execution state. The objective is to minimize the expected total execution time (also called makespan).

The overhead due to checkpointing is modeled as follows: a checkpoint taken after executing task T i requires an arbitrary time C i . For recoveries, we assume that if the most recent available checkpoint was taken after task T i , then the recovery takes an arbitrary time R i . Finally, we add an additional overhead D for downtime. The downtime accounts for software rejuvenation (i.e., rebooting [START_REF] Kolettis | Software rejuvenation: Analysis, module and applications[END_REF]) or for the replacement of the failed processor by a spare. Note that failures can take place during recovery, but not during downtime (otherwise simply combine downtime with recovery). For the sake of simplicity, we make two important restrictive assumptions: Full parallelism: Each task is executed by all the p processors;

Poisson process: Processor failure inter-arrival times follow an Exponential distribution of parameter λ proc (hence platform failure inter-arrival times follow an Exponential distribution of parameter λ = pλ proc ).

Section VI discusses several extensions to this model, and hints to alleviate these limitations. The first assumption (full parallelism) amounts to linearize the task graph and to execute all tasks sequentially. This is the only possibility when the original DAG is a linear chain, a situation very frequent in scientific applications [START_REF]DataCutter Project: Middleware for Filtering Large Archival Scientific Datasets in a Grid Environment[END_REF], [START_REF] Taura | A heuristic algorithm for mapping communicating tasks on heterogeneous resources[END_REF], [START_REF] Wu | Supporting distributed application workflows in heterogeneous computing environments[END_REF], but it may prove a severe restriction when several tasks could be executed concurrently. However, full parallelism allows to avoid any resource allocation problem. Instead, we search for the best ordering of the tasks so as to minimize the expectation of the total execution time. As shown in Section IV, this simpler problem instance already is NPhard in the strong sense, even with constant checkpoint costs. This negative result shows the intrinsic combinatorial difficulty to deciding which tasks to execute first, and which ones to checkpoint. On a more constructive basis, Section V presents a polynomial solution when the DAG is a linear chain, with arbitrary checkpoint costs. These important results provide theoretical foundations for the problem, and constitute a prerequisite before tackling even more challenging instances.

The second assumption (Poisson process) is standard in theoretical analyses [START_REF] Duda | The effects of checkpointing on program execution time[END_REF], [START_REF] Daly | A higher order estimate of the optimum checkpoint interval for restart dumps[END_REF] because the memoryless property of Exponential distributions allows for deriving scheduling strategies that do not depend upon the history of previous failures. However, we do acknowledge that Weibull and/or log-normal distributions are considered more relevant in practice [START_REF] Heath | Improving cluster availability using workstation validation[END_REF], [START_REF] Schroeder | A large-scale study of failures in high-performance computing systems[END_REF], [START_REF] Liu | An optimal checkpoint/restart model for a large scale high performance computing system[END_REF], [START_REF] Heien | Modeling and tolerating heterogeneous failures in large parallel systems[END_REF].

III. Expectation of the time needed to execute a work and to checkpoint it

In this section, we provide an exact formula to compute the expected time E(T (W, C, D, R, λ)) to execute a work of duration W followed by a checkpoint of duration C. If a failure interrupts a given attempt, there is a downtime of duration D followed by a recovery of length R. Recall that failures follow an Exponential distribution (of parameter λ) and can take place during recovery, but not during downtime. To the best of our knowledge, this important result is original. Daly only provides first and second order approximations [START_REF] Daly | A higher order estimate of the optimum checkpoint interval for restart dumps[END_REF], and the formula in Bouguerra et al. [START_REF] Bouguerra | A flexible checkpoint/restart model in distributed systems[END_REF] is inaccurate (in their approach, a recovery always takes place before execution, which is false for the first attempt). In addition, the proof is original too: we use an elegant recursive approach, while in the literature, the standard approach is to consider consecutive execution attempts iteratively, until success.

Proposition 1. E(T (W, C, D, R, λ)) = e λR 1 λ + D (e λ(W +C) -1).
Proof: Let T be the time needed for successfully executing a work of duration W . There are two cases: (i) if there is no failure during execution and checkpointing, then the time needed is exactly W + C; (ii) if there is one failure before successfully completing the work and its checkpoint, then some additional delays are incurred. These delays come from two sources: the time spent computing by the processors before the failure (accounted for by variable T lost ), and the time spent for downtime and recovery (accounted for by variable T rec ). Regardless, once a successful recovery has been completed, there still remain W units of work to execute. Thus we can write the following recursion:

T = W + C if no failure happens T lost + T rec + T otherwise (1)
Here, T lost denotes the amount of time spent by the processors before the first failure, knowing that this failure occurs within the next W +C units of time. In other terms, it is the time that is wasted because computation and checkpoint were not both completed. The other variable T rec represents the amount of time needed by the system to recover from the failure. Weighting the two cases in Equation ( 1) by the probability of their occurrence, and taking expectations, we obtain the following equation:

E(T ) = e -λ(W +C) (W + C) + (1 -e -λ(W +C) ) [E(T lost ) + E(T rec ) + E(T )] (2)
This simplifies to:

E(T ) = W + C + (e λ(W +C) -1)(E(T lost ) + E(T rec )) (3)
We have

E(T lost ) = ∞ 0 xP(X = x|X < W + C)dx = 1 P(X < W + C) W +C 0 e -λx dx,
and P(X < W + C) = 1 -e -λ(W +C) . Integrating by parts, we derive that

E(T lost ) = 1 λ - W + C e λ(W +C) -1 (4)
Next, to compute E(T rec ), we have a recursive equation quite similar to Equation ( 2):

E(T rec ) = e -λR (D + R) + (1 -e -λR )(D + R lost + E(T rec ))
Here, R lost is the expected amount of time lost to executing the recovery before a failure happens, knowing that this failure occurs within the next R units of time. Replacing W + C by R in Equation (4), we obtain

R lost = 1 λ - R e λR -1 .
The expression for E(T rec ) simplifies to

E(T rec ) = De λR + 1 λ (e λR -1) (5)
Plugging the values of E(T lost ) and E(T rec ) into Equation (3) leads to the desired value:

E(T (W, C, D, R, λ)) = e λR 1 λ + D (e λ(W +C) -1) (6)
Equation ( 6) is fully general, in the sense that the values of W , C, D, and R may arbitrarily depend upon the number p of processors in the platform (recall that λ = pλ proc linearly depends on p for Exponential laws). Let us write W (p), C(p), R(p) and D(p) to make the dependence on p explicit. In [START_REF] Bougeret | Checkpointing strategies for parallel jobs[END_REF]

W total = O(N 3
). In the algorithm in [START_REF] Blackford | ScaLAPACK Users' Guide[END_REF], q = r 2 and each processor receives 2r blocks of size N 2 /r 2 during the execution. Here γ is the communicationto-computation ratio of the platform.

Checkpoint overhead. Assuming that the application's memory footprint is V bytes, with each processor holding V /p bytes, we can have: Finally, there is a technical difficulty hidden in Equation [START_REF] Daly | A higher order estimate of the optimum checkpoint interval for restart dumps[END_REF]: with a single processor (p = 1), the downtime has constant value D, but with several processors, the duration of the downtime is difficult to compute: a processor can fail while another one is down, thereby leading to cascading downtimes. Hence in Equation ( 6), D should be taken as the expectation of the variable D(p), whose exact value is unknown, but for which an upper bound can be provided (see [START_REF] Bougeret | Using group replication for resilience on exascale systems[END_REF] for details). In most practical cases, the lower bound D(p) = D(1) = D is expected to be very accurate.

IV. Complexity

In this section we prove that the general scheduling problem is NP-complete in the strong sense. This result holds true for independent tasks and the simplest checkpoint cost model where all costs are equal. Intuitively, this shows that deciding for an ordering to execute several independent tasks, and after which task completions to checkpoint, is a difficult combinatorial problem. Note that this holds true independently of the value of the number of processors p. In particular, the result holds when using a single-processor platform. Proposition 2. Consider n independent tasks, T 1 , ..., T n , with task T i of duration w i for 1 ≤ i ≤ n. All checkpoint and recovery times are equal to C, and there is no downtime (D = 0). The problem to schedule these tasks, and to decide after which tasks to checkpoint, so as to minimize the expected execution time, is NP-complete in the strong sense.

Proof: The decision problem is the following: given a time bound K, can we find an ordering for the execution, and decide after which tasks to checkpoint, so that the expected execution time E does not exceed K? The problem clearly belongs to NP, with the ordered list of tasks and checkpoints being a linear-size certificate. To establish the completeness, we use a reduction from 3-PARTITION, which is NP-complete in the strong sense [START_REF] Garey | Computers and Intractability, a Guide to the Theory of NP-Completeness[END_REF]. Consider the following general instance I 1 of 3-PARTITION: given 3n integers a 1 , . . . , a 3n and a number T such that 1≤j≤3n a j = nT , and T 4 < a i < T 2 for 1 ≤ i ≤ 3n, does there exist a partition in n subsets B 1 , . . . , B n of {a 1 , . . . , a 3n } such that for all 1 ≤ i ≤ n, aj ∈Bi a j = T ? Note that necessarily in any solution, each B i has cardinal 3.

We build the following instance I 2 of our problem with 3n independent tasks, T 1 , ..., T 3n , task T i being of size w i = a i . We let

λ = 1 2T , C = R = 1 λ (ln(2) - 1 2
), D = 0, K = n e λC λ (e λ(T +C) -1).

The size of I 2 is polynomial (even linear) in the size of I 1 . We show that I 1 has a solution if and only if I 2 has a solution. Suppose first that I 1 has a solution B 1 , . . . , B n . We propose the following solution for I 2 : we execute the subsets in any order; for each subset B i , we schedule its three tasks in any order, and we checkpoint after the third one. From Proposition 1, the expected execution time for each subset is e λC λ (e λ(T +C) -1). The expected total execution time is E = n e λC λ (e λ(T +C) -1) = K, hence a solution to I 2 .

Suppose now that I 2 has a solution, which includes m checkpoints. Let B 1 be the set of tasks executed before the first checkpoint, and for 2 ≤ i ≤ m, let B i be the set of tasks executed between checkpoints i -1 and i. For 1 ≤ i ≤ m, let T i be the total duration of the tasks in B i . We have m i=1 T i = nT (total work to be executed). From Proposition 1, the expected total execution time is

E = m i=1 e λC
λ (e λ(Ti+C) -1), and by hypothesis we have

E ≤ K. We write E as E = e 2λC λ m i=1 e λTi -m e λC λ .
Consider m i=1 e λTi : by convexity, since m i=1 T i = nT is constant, this sum is minimal when all terms T i are equal, and their common value must be T i = nT m . Hence

E ≥ E 0 = m e λC λ (e λ( nT m +C) -1),
with equality if and only if all the T i 's are equal. We write E 0 = e λC λ g(m), where g(m) = m(e λ( nT m +C) -1), and we differentiate g:

g (m) = 1 - λnT m e λ( nT m +C) -1 g (m) = λ 2 n 2 T 2 m 3 e λ( nT m +C) > 0
Hence g is convex and its first derivative its a strictly increasing function. Then g has a unique minimum which is achieved for m = n, since g (n) = 0. Indeed, we have

g (n) = (1 -λT )e λ(T +C) -1. By hypothesis, we have λ = 1 2T and C = 1 λ (ln(2) -1 2 ). Therefore, e λ(T +C) = e 1 2 +(ln(2)-1 2 ) = e ln(2) = 2,
and finally g (n) = 0.

Altogether, the minimum value of E is uniquely reached for m = n and T i = T for all i, in which case E = K. This shows that B 1 , . . . , B n is a solution for I 1 , which concludes the proof.

V. Linear chains

In this section, we present a polynomial-time dynamic programming algorithm to compute the optimal execution time for applications whose DAG is a linear chain

T 1 → T 2 • • • → T n .
Recall that the execution time of task T i is w i for 1 ≤ i ≤ n. We allow for different checkpoint times and let C i denote the duration of a checkpoint after task T i for 1 ≤ i ≤ n. Similarly, we let R i be the recovery time if the most recent available checkpoint was taken after task T i , for 1 ≤ i ≤ n -1 (no need to recover from after T n ). As before, we have a downtime of duration D after each failure, and failures follow an Exponential law of parameter λ.

Proposition 3. Algorithm 1 provides the optimal solution for a linear chain of n tasks. Its complexity is O(n 2 ).

Proof: In Algorithm 1, DPMAKESPAN(x,n) computes the optimal expectation of the time needed for successfully executing the last (n-x+1) tasks, with 1 ≤ x ≤ n. Our goal is to compute DPMAKESPAN(1,n). Note that DPMAKESPAN(x,n) returns a couple formed by the optimal expectation of the execution time, and the index of the task that precedes the checkpoint in the outermost recursion level (needed to reconstruct the solution).

Algorithm 1 contains a loop of size (n-x) and inside the loop, we perform a recursive call of the function DPMAKESPAN. This recursive call has linear complexity because we only compute each instance DP-MAKESPAN(x,n,) once, using memoization [START_REF] Cormen | Introduction to Algorithms[END_REF] (i.e., storing the result of the recursive calls that are have already been computed). Thus, the complexity of Algorithm 1 is O(n 2 ).

VI. Extensions

In this section we discuss three extensions of this work. In particular, we address the two limitations outlined in Section II, namely full parallelism and Poisson process.

The first extension relates to checkpointing costs. In Section II, we have considered that the time required to checkpoint only depends on the last task executed prior to that checkpoint. In a more general model, the time needed for a checkpoint after task T i may depend on T i itself, but also on some other tasks that have been executed since the last checkpoint. For instance, assume that two independent tasks T i and then T j are executed just after a checkpoint, and that there is a checkpoint after these tasks. The model from Section II states that the cost of this checkpoint is C j , regardless whether there has been a checkpoint between T i and T j or not. In a more general and realistic model, the checkpoint cost would be f (C i , C j ), where f is an application-dependent function. In the general case, the cost of a checkpoint should account for all the tasks that have been executed since the last checkpoint and which have at least a successor task which has not been executed yet. Note that in the case of linear chains (Section V), there is always a single task that needs to be saved, so that the cost model that we used is fully general.

The second extension aims at alleviating the full parallelism assumption. In a model with variable parallelism, we have moldable tasks [START_REF] Dutot | Scheduling Parallel Tasks Approximation Algorithms[END_REF], that can be execute with an arbitrary number of processors. To compute the expected time of a task using any given number of processors, we can use the different workload models described at the end of Section III and then instantiate Equation ( 6). But we now face a challenging resource allocation problem: deciding how many resources to assign to each task. This problem is known to be difficult, but approximation algorithms are available for failure-free environments [START_REF] Dutot | Scheduling Parallel Tasks Approximation Algorithms[END_REF]. It would be very interesting to extend these algorithms to failure-prone platforms.

The third extension would allow for more general failure laws than Exponential distributions. Assuming that processor failures would follow Weibull and/or log-normal distributions [START_REF] Heath | Improving cluster availability using workstation validation[END_REF], [START_REF] Schroeder | A large-scale study of failures in high-performance computing systems[END_REF], [START_REF] Liu | An optimal checkpoint/restart model for a large scale high performance computing system[END_REF], [START_REF] Heien | Modeling and tolerating heterogeneous failures in large parallel systems[END_REF]. there are two main difficulties. The first difficulty is to compute, or better approximate, the failure distribution of a platform with p processors, which is the superposition of p independent and identically distributed distributions (with a single processor). The second difficulty is to estimate the expected execution time of a work of duration W followed by a checkpoint of duration C. No closed-form formula is known. This is because we have to account for time elapsed since the last failure on each processor, since the failure distribution no longer is memoryless. We would have to use heuristic approaches even for linear chains. For instance, instead of aiming at the minimization of the expected execution time, it is possible to (greedily) aim at the maximization of the expected amount of work achieved before the next failure [START_REF] Bougeret | Checkpointing strategies for parallel jobs[END_REF], [START_REF] Bouguerra | Complexity analysis of checkpoint scheduling with variable costs[END_REF]. Dynamic programming heuristics and simulation results are provided in [START_REF] Bougeret | Checkpointing strategies for parallel jobs[END_REF] for single-task applications, using either synthetic traces or failure logs of production clusters [START_REF] Kondo | The failure trace archive: Enabling comparative analysis of failures in diverse distributed systems[END_REF].

VII. Related work

There is a large body of literature on checkpointing strategies for divisible jobs. The corresponding scheduling problem is to partition the job into several chunks and to checkpoint after each of them. In [START_REF] Daly | A higher order estimate of the optimum checkpoint interval for restart dumps[END_REF], Daly studies periodic checkpointing policies (same-size chunks) for Exponentially distributed failures, generalizing the well-known bound obtained by Young [START_REF] Young | A first order approximation to the optimum checkpoint interval[END_REF]. Daly extended his work in [START_REF] Jones | Impact of suboptimal checkpoint intervals on application efficiency in computational clusters[END_REF] to study the impact of sub-optimal checkpointing periods. In [START_REF] Venkatesh | Analysis of Dependencies of Checkpoint Cost and Checkpoint Interval of Fault Tolerant MPI Applications[END_REF], the authors develop an "optimal" checkpointing policy, based on the popular assumption that optimal checkpointing must be periodic. In [START_REF] Bouguerra | A flexible checkpoint/restart model in distributed systems[END_REF], Bouguerra et al. prove that the optimal checkpointing policy is periodic when checkpointing and recovery overheads are constant, for either Exponential or Weibull failures. But their results rely on the unstated assumption that all processors are rejuvenated after each failure and after each checkpoint. In our recent work [START_REF] Bougeret | Checkpointing strategies for parallel jobs[END_REF], we have shown that this assumption is unreasonable for Weibull failures, and we have developed optimal solutions for Exponential failures and dynamic programming solutions for any failure distribution. As already mentioned, solving the problem for arbitrary distributions is difficult because, unlike in the memoryless case, there is no reason for the optimal solution to use a single chunk size [START_REF] Tantawi | Performance analysis of checkpointing strategies[END_REF]. In fact, the optimal solution is very likely to use chunk sizes that depend on additional information that becomes available during the execution (i.e., failure occurrences to date).

The problem studied in this paper is related to the previous line of work, but strongly differs in that checkpoints are allowed only after a task has been completed. In other words, instead of studying a divisible job that can be arbitrarily partitioned into chunks, we study a DAG of non-divisible computational tasks. To the best of our knowledge, there are few papers studying checkpointing strategies for computational workflows. Our work is motivated by the results of Bouguerra, Trystram, and Wagner [START_REF] Bouguerra | Complexity analysis of checkpoint scheduling with variable costs[END_REF], who study the problem instance with linear chains (as in Section V), with a single processor. Since they deal with arbitrary distributions, they cannot aim at minimizing the expected execution time. Instead, they aim at maximizing the amount of work done before the first failure, which is a natural greedy heuristic to minimize the total execution time. They show that their problem is NPcomplete in the weak sense for uniform distributions, and they propose a pseudo-polynomial dynamic programming algorithm. Our results nicely complement those of [START_REF] Bouguerra | Complexity analysis of checkpoint scheduling with variable costs[END_REF], since we solve the original problem for Exponential distributions, while they provide uni-processor heuristics for general distributions.

Other scheduling approaches for the reliability of workflow applications can be classified along two main threads: (i) resource allocation strategies that trade-off between makespan and reliability (bi-criteria optimization problem): and (ii) replication-oriented heuristics. A small list of representative papers is [START_REF] Dongarra | Bi-objective scheduling algorithms for optimizing makespan and reliability on heterogeneous systems[END_REF], [START_REF] Dogan | Matching and scheduling algorithms for minimizing execution time and failure probability of applications in heterogeneous computing[END_REF], [START_REF] Girault | Reliability versus performance for critical applications[END_REF]. Very recently, there have been studies [START_REF] Yi | Using Replication and Checkpointing for Reliable Task Management in Computational Grids[END_REF], [START_REF] Ferreira | Evaluating the Viability of Process Replication Reliability for Exascale Systems[END_REF] on the use of replication as a mechanism complementary to checkpoint-recovery.

VIII. Conclusion

In this work, we have presented preliminary results on the complexity of checkpointing computational workflows. We have used a simplified framework with two main limitations, full parallelism (rigid tasks) and Exponential failure distributions. We have derived several new and important results: (i) a closed-form formula for the expected execution time of a computational workload followed by its checkpoint; (ii) the strong NP-hardness of the problem for independent tasks and constant checkpoint costs; and (iii) a dynamic programming algorithm for linear chains of tasks with arbitrary checkpoint costs. We believe that these results lay the theoretical foundations of the problem and constitute a prerequisite before discussing scheduling strategies for arbitrary DAGS of moldable tasks subject to general failure distributions. We have discussed several directions to tackle such a challenging problem.

  (i) C(p) = R(p) = αV /p = C/p with α some constant: proportional overhead, for cases where the bandwidth of the network card/link at each processor is the I/O bottleneck; (ii) C(p) = R(p) = αV = C with α some constant: constant overhead, for cases where the bandwidth to/from the resilient storage system is the I/O bottleneck.

Algorithm 1 : 1 λ + D e λ j i=x wi +Cj - 1 if

 111 DPMAKESPAN(x, n) if x = n then return e λRn-1 ( 1 λ + D)(e λ(wn+Cn) -1), n best ← e λRx-1 1 λ + D e λ(( n i=x wi)+Cn) -1 numTask ← n for j = x to n -1 do (exp succ, num Task) ← DP M AKESP AN (j + 1, n) Cur ← exp succ +e λRx-1 Cur < best then best ← Cur numTask ← j return (best, numT ask)

Acknowledgments. The authors are with Université de Lyon, France. Y. Robert is with the Institut Universitaire de France. This work was supported in part by the ANR RESCUE project.


Bertrand Jeannet

Pascal Sotin

Inferring Effective Types for Static Analysis of C Programs 1

Keywords: Static Analysis, Type Inference, C Programming Language, Boolean, Finite Types

The C language does not have a specific Boolean type: Boolean values are encoded with integers. This is also true for enumerated types, that may be freely and silently cast to and from integers. On the other hand, verification tools aiming at inferring the possible values of variables at each program point may benefit from the information that some (integer) variables are used solely as Boolean or enumerated type variables, or more generally as finite type variables with a small domain. Indeed, specialized and efficient symbolic representations such as BDDs may be used for representing properties on such variables, whereas approximated representations like intervals and octagons are better suited to larger domain integers and floating-points variables. Driven by this motivation, this paper proposes a static analysis for inferring more precise types for the variables of a C program, corresponding to their effective use. The analysis addresses a subset of the C99 language, including pointers, structures and dynamic allocation.

Introduction

Verification of C programs.

The initial motivation for this work was to infer invariants on C programs with the tool ConcurInterproc [START_REF] Jeannet | Relational interprocedural verification of concurrent programs[END_REF]. There are two main issues when one wants to connect an academic analyser to the C language:

(i) The analyser might encounter features of the C language it was not designed to deal with. This leads in the best case to the use of imprecise fall-back treatments and in the worst case to a silently unsound analysis. (ii) The analyser may not recognize in the C presentation features for which it was designed. This leads to a less precise treatment of the program. Boolean values encoded with integers variables.

The verification tool ConcurInterproc distinguishes numerical, Boolean and finitely enumerated variables. We want to cast C programs as input of this analyser and to exploit its type system. Unfortunately, the C type system is too weak. For example, in Fig. 1, both b and x are declared as int but the analyser would gain precision by considering b as a boolean and x as a number (a disjunctive analysis, depending on the truth value of b would then be performed). Moreover, even if b was declared as a Boolean enumerated type {false=0, true=1}, this does not imply that it is not assigned somewhere else the value 2.

Contribution.

We propose a static analysis for C programs which specializes in a sound way the generic integer type of some variables and structure fields into Booleans or inferred enumerated types. This analysis takes into account aliasing properties raised by procedure calls and pointers. This static analysis allows the initial weakly-typed C program to be transformed into a semantically equivalent, strongly typed program, which can be more efficiently analyzed by verification tools such as ConcurInterproc [START_REF] Jeannet | Relational interprocedural verification of concurrent programs[END_REF]. After a short presentation of the context and related work (Section 2), we first describe our analysis in a simple context involving only procedures and integer variables (Section 3), before extending it to pointers, structures and dynamic allocation (Section 4), and discussing remaining issues in the conclusion.

General Context and Related work

As already mentioned, our motivation is to connect the ConcurInterproc verification tool [START_REF] Jeannet | Relational interprocedural verification of concurrent programs[END_REF], and its extension to pointers PInterproc [START_REF] Sotin | Precise interprocedural analysis in the presence of pointers to the stack[END_REF]. These tools can treat the integer variables of C programs as numerical variables, by representing their possible values using for instance octagons [START_REF] Miné | The octagon abstract domain, Higher-Order and Symbolic Computation[END_REF], but they can handle more precisely (ie., in a disjunctive way) those integer variables that are actually manipulated as Boolean or enumerated variables, using Bdds.

A simple solution to avoid the confusion between Boolean and numerical variables is to use a strongly-typed form of C (eg. Cyclone [START_REF] Jim | Cyclone: A safe dialect of c[END_REF]) offering types like bool and ensuring that the program respects the declared types, but then this does not address ordinary C programs.

Fig. 2. General Syntax

The question of strengthening the typing of a program for analysis purpose has been tackled by [START_REF] Guha | Typing local control and state using flow analysis[END_REF] in the context of interpreted languages, like Javascript, with both weak and dynamic typing. The authors perform a flow-sensitive static analysis which collects the possible types of a variable at a given point. Similarly, for compilation purpose, many techniques have been proposed to infer the possible classes of objects at invocation sites in order to optimize dynamic call resolution into static calls. Compared to our analysis, these analyses infers sets of types in a flow-sensitive way while we are looking for a unique flow-insensitive type for each of our variables.

Programs with procedure calls and scalar variables

We first present our static analysis in the simple context of programs built from a number of procedures manipulating only scalar variables (we exclude pointers from the scalars). This allows to discuss our approach in a simple setting, before investigating the additional issues raised by pointers, casts and dynamic allocation.

The considered input language

We consider a simple subset of C, the grammar3 of which is depicted on Fig. 2. f, g denote procedure names, x, y variable names. As our analysis is

x = expr ∈ stm D(x) ⊇ D(expr ) return expr ∈ stm (f ) D(f ) ⊇ D(expr) x = f (expr 1 , . . . , expr n ) ∈ stm typ f (typ 1 x1, . . . , typ n xn) ∈ proc D(x) ⊇ D(f ) ∀i : D(xi) ⊇ D(expr i ) (2) D(cst ) = {cst } D(boolexpr ) = {0, 1} D(intexpr ) = Z D(expr "?"expr 1 ":"expr 2 ) = D(expr 1 ) ∪ D(expr 2 )
(3) Fig. 3. Inferring possible values for variables in scalar programs flow-insensitive, we do not detail the statements related to control. In short, in this subset all variables are declared as integers, there are no pointers, no structured types, no dynamically allocated data. We assume that all procedures return a value, and that variables are uniquely identified by their name.

We do not consider explicit enumerated type declarations, unlike a tool like SPLint [START_REF] Evans | Improving security using extensible lightweight static analysis[END_REF], which complains about casts from one enumerated type to another one. This is because our analysis is not intended as an help for programmers to discover potential problems due to weak typing.

Inferring the possible values of variables

In this simple setting, the philosophy of our analysis is not really to infer types, but just to discover the set of possible values for any variable in a given procedure. This means that we focus on an attribute-independent, flow-and context-insensitive static analysis, which computes a function

D : Proc ⊎ Var → P(Z) (1)
where

• P(Z) is the complete lattice of subsets of integers; the least upper bound operator of this domain coincides with the set union; • D(f ) denotes the possible return values of the procedure f and D(x) the possible values of the variable x. The functional set D = Proc ⊎ Var → P(Z) ordered pointwise is a complete lattice (the codomain of any D ∈ D is finite).

This inference analysis is formalized on Fig. 3. It is based on the inspection of assignments, procedure call and return statements contained in procedures. We implicitly extend the function D to expressions using Eqn. [START_REF] Guha | Typing local control and state using flow analysis[END_REF]. Observe that we do not exploit the context of expressions: having the subexpression "x+3" or "x?1:0" in a procedure does not allow to infer any information on the possible values contained in x in the C language. This analysis is quite similar to a constant propagation analysis, in which the constant flat lattice is replaced by the lattice P(Z).

The approximation we perform in this analysis is to consider that the set of possible values of any integer expressions (as defined in Fig. 2) is the set of all integer values. For instance, if x may take the values 1 or 3 (ie., D(x) = {1, 3}), our analysis considers that x+1 may take any value (ie., D(x+ 1) = Z), instead of just a value in the set {2, 4}. Without this approximation our analysis is not computable4 , because the lattice D does not satisfy the finite ascending chain condition. An alternative could be not to perform this approximation, but instead to use a widening operator that replaces finite subsets of Z by Z when their cardinality is greater than a given threshold. This alternative corresponds to the disjunctive completion of constant propagation analysis, equipped with a widening operator to ensure convergence.

Given a specific program, the longest chains of elements in P(Z) appearing in the analysis is of length H, being at most the number of numerical constants appearing in the program, plus 3 (because of the "predefined" constants 0, 1 returned by Boolean operators, and the top element Z). Hence the full analysis converges in at most H |Proc|+|Var| steps, where |Proc|, |Var | denotes resp. the number of procedures and variables.

Typing the analyzed program

Once the function D is computed by the previous analysis, we have to translate the weakly-typed C program into a strongly-typed variant of the C language, in which operators are typed as described on Fig. 4(a).

This transformation is based on the fact that a finite value D(x) = {v 1 , . . . , v n } implicitly defines an enumerated type, denoted typ D(x) in formula. If D(x) = Z, then by convention typ D(x) = int. The transformation consists in two operations:

(i) Adding enumerated type declarations:

• for each different finite value D k = {v 1 k , . . . , v n k k } of D we insert the C type declaration "typedef enum { lk1=vk1,...,lkn=vkn } tk";

• we implicitly add the predefined type "typedef enum { false=0, true=1 } bool"; • each variable declaration "int x" with D(x) = D k is then replaced by "tk x". The same holds for the return type of procedures. (ii) Inserting casts between integers and finite types, to ensure proper typing.

Expressions and assignments are translated as defined in Fig. 4, in which we use the following operation on types:

t ⊔ t ′ = t if t = t ′ int otherwise (4)
Jeannet and Sotin

! ♭ : bool → bool -♭ : int → int && ♭ , || ♭ : bool×bool → bool + ♭ , * ♭ , << ♭ , & ♭ , . . .: int×int → int < ♭ , > ♭ , . . . : int×int → bool == ♭ , ! = ♭ : α×α → bool •? ♭ • : ♭ • : bool×α×α → α (a)
Strongly-typed versions of C99 operators. α is a type variable used for polymorphic operators. Observe that the definition of the cast operators cast bool←int and cast int←bool does not follow exactly the same pattern as for ordinary enumerated type, as any non-zero integer values is associated to the Boolean true.

typ(cst ) = int typ(x ) = typ D(x) typ(op ♭ 1 e) = t if op ♭ 1 : t1 → t typ(e1 op ♭ 2 e2) = t if op ♭ 2 : t1 ×t2 → t typ(e1? ♭ e2 : ♭ e3) = typ(e2) ⊔ typ(e3) typ(cast t 2 ←t 1 (e)) = t2 (b) Typing expressions cst b = cst lv b = lv op 1 e b = op ♭ 1 (cast t 1 ←t ′ ( e )) if ( op ♭ 1 : t1 → t t ′ = typ( e ) e1 op 2 e2 b = cast t 1 ←t ′ 1 ( e1 ) op ♭ 2 cast t 2 ←t ′ 2 ( e2 ) if ( op ♭ 2 : t1 ×t2 → t t ′ i = typ( ei ) e1 op 2 e2 b = cast t ′ ←t ′ 1 ( e1 ) op ♭ 2 cast t ′ ←t ′ 2 ( e2 ) if 8 > < > : op ♭ 2 : α×α → bool t ′ = t ′ 1 ⊔ t ′ 2 t ′ i = typ( ei ) e1 ? e2 : e3 b = cast bool←t ′ 1 ( e1 ) ? ♭ cast t ′ ←t ′ 2 ( e2 : ♭ cast t ′ ←t ′ 3 ( e3 if ( t ′ = t ′ 2 ⊔ t ′ 3 t ′ i = typ( ei ) lv = e b = lv = cast t←t ′ ( e ) if ( t = typ(lv) t ′ = typ( e ) lv = f (e1, . . . , en) b = lv = cast t ′ ←t (f (cast t 1 ←t ′ 1 ( e1 , . . . , cast tn←t ′ n ( en )) if 8 > < > : f : t1 ×. . .×tn → t t ′ = typ(lv ) t ′ i = typ( ei ) (c)
(e == v n k -1 k ) ? l n k -1 k : l n k k cast int←t k (l) = (l == l 1 k ) ? v 1 k : . . . (l == l n k -1 k ) ? v n k -1 k : v n k k cast bool←int (e) = (e == 0) ? false : true cast int←bool (e) = e ? 1 : 0 cast t←t ′ = cast t←int • cast int←t ′ if t = t ′ (
to the way it normalizes expressions by pushing operators in the branches of conditional expressions and simplifying trivial tests. For instance, it rewrites the expression if ((x==k0 ? 0 : 1)==0) x=(1==0 ? k0 : k1) in Fig. 5(c) as follows:

if ((x==k0 ? 0 : 1)==0) x=(1==0 ? k0 : k1) ⇒ if (x==k0 ? 0==0 : 1==0) x=k1 ⇒ if (x==k0) x=k1
4 Adding pointers, structures and dynamic allocation

We now add pointers, structured types and dynamic allocation to our language. We extend the grammar of Fig. 2 as follows:

typ ::= typ0 " * " k typ0 ::= int | "typedef struct {"( typ n) * "}"t expr ::= . . . pexpr pexpr ::

= null | "&"x | "&"(x → n) lv ::= x | " * "x stm ::= . . . | lv = alloc( typ ) (5)
We add in particular the operator & which creates a pointer value from a variable or a field of a structure (no function pointers). n, m, . . . denotes names of structures fields, assumed to be unique. We allow only one * operator in left-values (including the implicit * of ->). Assignments like "**x=**y" should be decomposed as "px=*x; py=*y; *px=*py" and "a->n = b->m" as "pa = &(a->n); pb = &(a->m); *pa = *pb;".

The important assumption we do in this section is that there is no (implicit or explicit) cast between the types t 1 * k and t 2 * k ′ with k = k ′ ∨ t 1 = t 2 , and that the program is well-typed in this respect.

Purpose of our inference analysis

In Section 3 our finite type inference reduced to the analysis of possible values of scalar variables. In this new setting, the goal of our type inference is (i) as before to detect the scalar variables that are manipulated as Boolean or enumerated types, and to infer the corresponding type; (ii) but also to do so for the fields of structured types; while taking into account typing and aliasing properties induced by pointers. Our analysis will return a unique type for a given field name, meaning that we renounced to capture distinct (boolean/integer) uses of the same structured type in different contexts.

Consider the program of Fig. 6(a). We want to infer that p may point to x or y. This allows to infer that D(x) = {0, 2, 3} and D(y) = {1, 2, 3}. Now, as x and y may be pointed to by the same pointer p, they should have the same type. Hence we generate the program of Fig. 6(b).

Typing the analyzed program

As mentioned in Section 4.1, assigning types to variables is a bit more complex than in the purely scalar case, because two variables pointed to by the same pointer should be given the same type. Otherwise, the need for a cast may depend on the value of the pointer. Therefore,

• If x (or .n) is initially declared as an integer, typ(x) = typ S {D(y) | ∃p:P (p)⊇{x,y}} ; • If x (or .n) is initially declared as a pointer int * k , k > 0, typ(x) = (typ S y∈P k (x) D(y) ) * k , where P k denotes the k-th iterate of P . The insertion of casts is done exactly as in Section 3.3. Observe that we do not need casts between pointers: we cannot have "t* x; int* y;...; y=x" in the final program, because such an assignment makes the variables and fields pointed to by x and y (hence, also x and y) having the same type.

Discussion

In this section, we extended the proposition of Section 3 to a broader subset of C. However this proposal was done under some assumptions (absence of casts and pointer arithmetic) and should be seen as a demonstration of how the value analysis and points-to analysis interact. It is possible to relax these assumptions by using classical well-studied points-to analysis. In particular, the technique of Steensgarrd [START_REF] Steensgaard | Points-to analysis by type inference of programs with structures and unions[END_REF] seems well-suited, since it is interprocedural, flow-insensitive and it accepts the language of Equation 5. This technique infers the pointing relation and the effective structures manipulated by a C program with casts.

Handling arrays in addition to structures and pointers can be integrated to the points-to analysis by giving a unique type to the whole array and assuming that no out-of-range access occurs.

Note that the condition that variables must be initialized before being read, mentioned in 3.4, should also be satisfied for dynamically allocated memory, but this is more complex to check or to enforce.

Conclusion

We presented a way to determine the set of Boolean and enumerated variables among a set of variables of type int in a C program. This information, of little use for compilation, allows to improve the precision of program verification by assigning these variables to the adequate abstract domain.

The process takes as input a large subset of C (including functions, structures, pointers) and performs a simple points-to analysis followed by a value analysis. The results of these analyses allows to transform the program in a strongly-typed equivalent version by refining the types and by inserting explicit casts in the right place.

Note that this work would not be necessary if the abstract domains used by the analysers where able to dynamically switch the types of the variables they manipulate when the latter are escaping their capabilities. But the abstract domains proposed in the literature tend to be very specialized (eg. floating points [START_REF] Goubault | Asserting the precision of floating-point computations: A simple abstract interpreter[END_REF], numerical arrays [START_REF] Halbwachs | Discovering properties about arrays in simple programs[END_REF]), and taking more general cases into account would add a burden to their complexity.

Our work is complementary with the compilation of C program to intermediate language or to simpler subsets [START_REF] Necula | CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs[END_REF][START_REF] Hymans | Newspeak, Doubleplussimple Minilang for Goodthinkful Static Analysis of C[END_REF]. These proposals can be seen as frontends dedicated to verification by reducing the gap between C and the simpler analyser input language, thus answering Point (i) of the introduction.

An implementation has been developed for ConcurInterproc [START_REF] Jeannet | Relational interprocedural verification of concurrent programs[END_REF], having c2newspeak [START_REF] Hymans | Newspeak, Doubleplussimple Minilang for Goodthinkful Static Analysis of C[END_REF] as a frontend. The analyser only handles scalar types thus does not require the points-to version of the analysis (Section 4) but further developments for analysers with richer memory model will benefit from it.

Fig. 1 .

 1 Fig. 1. Boolean typed int This article address a problem belonging to Point (ii).

  prog ::= decl proc + list of variable and procedure declarations proc ::= typ f ( decl )"{" decl stm ⋆ "}" contains declarations and statements decl ::= ( typ x) ⋆ declaration of typed variables typ ::= int stm ::= lv = expr assignment | lv = p( expr , . . . , expr ) procedure call | return x returnig the value of a variable lv ::= x expr ::= cst | lv constant or left-value | boolexpr | intexpr | expr "?" expr ":" expr conditional expression boolexpr ::= "!" expr | expr bool binop expr Boolean expressions evaluating to 0 or 1 according to C99 stdandard intexpr ::= "-" expr | expr int binop expr "Integer " expressions potentially evaluating to any value cst ::= 0, 1, 2, . . . bool binop ::= "&&"|"||"|"=="|"! ="|"<"| . . . int binop ::= "+"|"-"|" * "|"/"|"&"|"|"| . . .

  Translating expressions and assignments by inserting casts cast t←t(e) = e castt k ←int(e) = (e == v 1

Fig. 4 .

 4 Fig. 4. Generating a strongly typed version of the program

x 6 )Fig. 8 . 7 )Fig. 9 .

 6879 Fig. 8. Points-to analysis x = expr ∈ stm int x ∈ decl D(x) ⊇ D(expr )

This work was supported by the french ANR project ASOPT.

Emails: bertrand.jeannet@inria.fr pascal.sotin@inria.fr c 2012 Published by Elsevier Science B. V.

We ignore details about separators, etc.

or at least very costly, if one considers that all variables are finite machine integers

Discussion

The soundness criterium is that the new program should have the same operational semantics as the original program. It is easy to see that typing error will not occur, given the properties of the function D computed by the analysis and the definition of functions typ and cast.

int main() { int x,y; y = x ? 1 : 0; x = 1; return y; } There is however a problem if some variables are read before being initialized. Look at the program on the right. Our inference analysis assigns to x the type enum { l1=1 }. Hence, seen as a Boolean, x is always true and the function returns 1. The C99 standard specifies on the other hand that the value of x is undefined when y is assigned, which means that it can have any value. To deal with this aspect without complicating our framework, we choose to impose that all variables are initialized before being read. Checking this assumption can be done with the classical dataflow analysis implemented in most C compilers, and enforcing it can be done on the original program by replacing any nonparameter declaration "int x" by "int x=0".

A second important point is related to our motivation to exploit the ability of some tools to analyze more precisely finite-state variables. Because we insert casts from enumerated types to integers, we may loose at first glance the benefit of assigning enumerated types to some original integer variables of a program. This will not happen with the ConcurInterproc tool, thanks Consider now the program of Fig. 7(a). We know that y is a pointer to a structure of type t, by its type. We do not need more information about pointers to structures, as the field n of all structures of a given type may be eventually specialized to a unique type. In other words, all the locations corresponding to the field n are summarized into a single location named .n. We still need to infer that p and q may point to the scalar field .n of an object of type t, and to deduce from this fact that the scalar field may contain a value in the set D(.n) = {0, 1, 2}. This results in the program of Fig. 7(b).

To conclude, we need a weak form of points-to analysis, in which we are only interested in points-to relation between pointers variables, integer variables and fields of structures.

Formalization of the analysis

We still perform a weak form of flow and context-insensitive points-to analysis, that infers a function P : Proc ⊎ Var ⊎ Field → P(Var ⊎ Field) which maps procedure return values, variables and fields of pointer type to variables and fields. P (x) (resp. P (.n)) will be an overapproximation of the set of variables and fields to which x (resp. the field .n of any object) may point to. This function is the smallest solution of the inference rules of Fig. 8, in which Eqn. ( 6) extends P to expressions of type int * k , k > 0.

We then generalize the scalar value analysis of Section 3.2 by inferring a function D : Proc ⊎ Var ⊎ Field → P(Z) which maps integer variables and fields to possible values. This function is the smallest solution of the inference rules of Fig. 9, in which Eqn. [START_REF] Jim | Cyclone: A safe dialect of c[END_REF] extends D to expressions of type int.