Anne Benoit
email: anne.benoit@ens-lyon.fr

Loïc Pottier
email: loic.pottier@ens-lyon.fr

Yves Robert
email: yves.robert@inria.fr

Resilient co-scheduling of malleable applications

Keywords: Resilience, co-scheduling, redistribution, complexity results, heuristics, simulations

Recently, the benefits of co-scheduling several applications have been demonstrated in a fault-free context, both in terms of performance and energy savings. However, large-scale computer systems are confronted by frequent failures, and resilience techniques must be employed for large applications to execute efficiently. Indeed, failures may create severe imbalance between applications, and significantly degrade performance. In this paper, we aim at minimizing the expected completion time of a set of co-scheduled applications. We propose to redistribute the resources assigned to each application upon the occurrence of failures, and upon the completion of some applications, in order to achieve this goal. First, we introduce a formal model and establish complexity results. The problem is NP-complete for malleable applications, even in a faultfree context. Therefore, we design polynomial-time heuristics that perform redistributions and account for processor failures. A fault simulator is used to perform extensive simulations that demonstrate the usefulness of redistribution and the performance of the proposed heuristics.

Introduction

With the advent of multicore platforms, HPC applications can be efficiently parallelized on a flexible number of processors. Usually, a speedup profile determines the performance of the application for a given number of processors. For instance, the applications in [START_REF] Heroux | Improving Performance via Mini-applications[END_REF] were executed on a platform with up to 256 cores, and the corresponding execution times were reported. A perfectly parallel application has an execution time t seq /p, where t seq is the sequential execution time, and p is the number of processors. In practice, because of the overhead due to communications and to the inherently sequential fraction of the application, the parallel execution time is larger than t seq /p. The speedup profile of the application is assumed to be known (or estimated) before execution, through benchmarking studies. A simple scheduling strategy on HPC platforms is to execute each application in dedicated mode, assigning all resources to each application throughout its execution. However, it was shown recently that rather than using the whole platform to run one single application, both the platform and the users may benefit from co-scheduling several applications, thereby minimizing the loss due to the fact that applications are not perfectly parallel. Sharing the platform between two applications already leads to significant performance and energy savings [START_REF] Shantharam | Speedup-aware co-schedules for efficient workload management[END_REF], which become even more important when the number of co-scheduled applications increases [START_REF] Aupy | Co-scheduling algorithms for highthroughput workload execution[END_REF].

To the best of our knowledge, co-scheduling has been investigated so far only in the context of fault-free platforms. However, large-scale platforms are prone to failures. Indeed, for a platform with p processors, even if each node has an individual MTBF (Mean Time Between Failures) of 120 years, we expect a failure likely to occur every 120/p years, for instance every hour for a platform with p = 10 6 nodes. Failures are likely to destroy the load-balancing achieved by co-scheduling algorithms: if all applications were assigned resources by the co-scheduler so as to complete their execution approximately at the same time, the occurrence of a failure will significantly delay the completion time of the corresponding application. In turn, several failures may well create severe imbalance among the applications, thereby significantly degrading performance.

To cope with failures, the de-facto general-purpose error recovery technique in HPC is checkpoint and rollback recovery [START_REF] Elnozahy | A survey of rollback-recovery protocols in message-passing systems[END_REF]. The idea consists in periodically saving the state of the application, so that when an error occurs, the application can be restored into one of its former states. The most widely used protocol is coordinated checkpointing, where all processes periodically stop computing and synchronize to write critical application data onto stable storage. The frequency at which checkpoints are taken should be carefully tuned, so that the overhead in a fault-free execution is not too important, but also so that the price to pay in case of failure remains reasonable. Young and Daly provide good approximations of the optimal checkpointing interval [START_REF] Young | A first order approximation to the optimum checkpoint interval[END_REF][START_REF] Daly | A higher order estimate of the optimum checkpoint interval for restart dumps[END_REF].

This paper investigates co-scheduling on failure-prone platforms. Checkpointing helps to mitigate the impact of a failure on a given application, but it must be complemented by redistributions to re-balance the load among applications. Co-scheduling usually involves partitioning the applications into packs, and then scheduling each pack in sequence, as efficiently as possible. We focus on co-scheduling a given pack of applications that execute in parallel, and leave the partitioning for further work. This is because scheduling a given pack becomes a difficult endeavour with failures (and redistributions), while it was of linear complexity without failures. Also, designing efficient pack scheduling algorithms is needed whenever there are relatively few applications that can be all scheduled simultaneously, and it is a prerequisite before tackling the general problem. Given a pack, i.e., a set of parallel applications that start execution simultaneously, there are two main opportunities for redistributing processors. First, when an application completes, the applications that are still running can claim its processors. Second, when a failure strikes an application, that application is delayed. By adding more resources to it, we can reduce its final completion time. However, we have to be careful, because each redistribution has a cost, which depends on the volume of data that is exchanged, and on the number of processors involved in redistribution. In addition, adding processors to an application increases its probability to fail, so there is a trade-off to achieve in order to minimize the expected completion time of the pack.

The major contributions of this work are the following: (i) the design of a detailed and comprehensive model for scheduling a pack of applications on a failure-prone platform; (ii) the NP-completeness proof for the problem with redistributions; (iii) the design and assessment of several polynomial-time heuristics to deal with the general problem with failures and redistribution costs.

The rest of the paper is organized as follows. First, we discuss related work in Section 2. The model and the optimization problem are formally defined in Section 3. In Section 4 we expose the complexity results. We introduce some polynomial-time heuristics in Section 5, which are assessed through simulations using a fault generator in Section 6. Finally, we conclude and provide directions for future work in Section 7.

Related work

Parallel application models. A parallel application is an application that may use several processors during its execution. Note that the scheduling literature uses the term parallel tasks rather than parallel application. Many parallel application models have been developed, and several types of applications have been defined. In 1986, with the development of multiprocessor systems, B lażewicz et al. [START_REF] Blazewicz | Scheduling multiprocessor tasks to minimize schedule length[END_REF] have modeled the problem of scheduling a set of independent parallel applications on identical processors. The number of processors assigned to each application was fixed during the execution. They showed that the problem is NPcomplete when the number of processors is not fixed. An application that has a fixed number of processors is called rigid. In 1989, Du and Leung [START_REF] Du | Complexity of scheduling parallel task systems[END_REF] developed a model called the Parallel Task System, where an application is executed by one or more processors at the same time, but the number of processors assigned to one application cannot exceed a certain threshold. Contrarily to the B lażewicz's model, the number of processors is not fixed in advance, but once it is determined (between one and the threshold), it remains fixed during the execution. Such applications are called moldable. Finally, a malleable application can have its number of allocated processors vary during the execution. B lażewicz et al. [START_REF] Blazewicz | Approximation algorithms for scheduling independent malleable tasks[END_REF] have designed approximation algorithms to solve the problem of scheduling independent malleable applications. Malleable applications are more flexible than rigid and moldable applications, and they can be implemented with data redistribution techniques (the technique used in this paper) or work stealing. In practice, changing the number of processors at runtime requires specific tools, frameworks and even dedicated programming languages like Cilk [START_REF] Frigo | The Implementation of the Cilk-5 Multithreaded Language[END_REF]. Martín et al. [START_REF] Martín | Enhancing the performance of malleable MPI applications by using performance-aware dynamic reconfiguration[END_REF] have developed an MPI extension, called Flex-MPI, which introduces malleability in MPI. Flex-MPI can achieve a load balancing among applications through a prediction model. The prediction model in Flex-MPI does not take into account resilience aspects.

One contribution of this work is to develop a complete model taking into account resilience aspects. We also provide heuristics able to re-assign processors to applications that need them. We also show that the problem of finding a schedule that minimizes the execution time with fixed redistribution costs and without failures is NP-complete (in the strong sense).

Resilience. One of the most used techniques to handle fail-stop errors in HPC is checkpoint and rollback recovery [START_REF] Elnozahy | A survey of rollback-recovery protocols in message-passing systems[END_REF]. The idea is to periodically save the system state, or the application memory footprint onto a stable storage. Then, after a downtime and a recovery time, the system can be restored into a former valid state (rollback step). Another technique for dealing with fail-stop errors is process replication, which consists in replicating a process and even replicating communications. For instance, the project RedMPI [START_REF] Fiala | Detection and correction of silent data corruption for large-scale high-performance computing[END_REF] implements a process replication mechanism and quadruplicates each communication.

In this paper, we use a light-weight checkpointing protocol called the double checkpointing algorithm [START_REF] Ni | Hiding Checkpoint Overhead in HPC Applications with a Semi-Blocking Algorithm[END_REF][START_REF] Dongarra | Performance and reliability trade-offs for the double checkpointing algorithm[END_REF]. This is an in-memory checkpointing protocol, which avoids the high overhead of disk checkpoints. Processors are paired: each processor has an associated processor called its buddy processor. When a processor stores its checkpoint file in its own memory, it also sends this file to its buddy, and the buddy does the same. Therefore, each processor stores two checkpoints, its own and that of its buddy. When a failure occurs, the faulty processor loses these two checkpoint files, and the buddy must re-send both checkpoints to the faulty node. If a second failure hits the buddy during this recovery period (which happens with very low probability), we have a fatal failure and the system cannot be recovered.

Co-scheduling algorithms.

This work provides an important extension to our previous work on coschedules [START_REF] Aupy | Co-scheduling algorithms for highthroughput workload execution[END_REF], which already demonstrated that sharing the platform between two or more applications can lead to significant performance and energy savings [START_REF] Shantharam | Speedup-aware co-schedules for efficient workload management[END_REF]. To the best of our knowledge, it is the first work to consider co-schedules and failures, and hence to use malleable applications to allow redistributions of processors between applications. However, we point out that co-scheduling with packs can be seen as the static counterpart of batch scheduling techniques, where jobs are dynamically partitioned into batches as they are submitted to the system (see [START_REF] Muthuvelu | Batch resizing policies and techniques for fine-grain grid tasks: The nuts and bolts[END_REF] and the references therein). Batch scheduling is a complex online problem, where jobs have release times and deadlines, and where only partial information on the whole workload is known when taking scheduling decisions. On the contrary, co-scheduling applies to a set of applications that are all ready for execution. In this paper, as already mentioned, we restrict to a single pack, because scheduling already becomes difficult for a single pack with failures and redistributions.

Framework

We consider a pack of n independent malleable applications {T 1 , . . . , T n }, and an execution platform with p identical processors subject to failures. We assume n ≤ 2p due to the use of the double checkpointing model. The objective is to minimize the expected completion time of the last application. First, we define the fault model in Section 3.1. Then, we show how to compute the execution time of an application in Section 3.2, assuming that no redistribution has occurred. The redistribution mechanism and its associated cost are discussed in Section 3.3. Finally, the objective function is detailed in Section 3.4.

Fault model

We consider fail-stop errors, which are detected instantaneously. To model the rate at which faults occur on one processor, we use an exponential probability law of parameter λ. The mean (or MTBF) of this law is µ = 1 λ . The MTBF of an application depends upon the number of processors it is using, hence changes whenever a redistribution occurs. Specifically, if application T i is (currently) executed on j processors, its MTBF is µ i,j = µ j (see [START_REF] Herault | Fault-Tolerance Techniques for High-Performance Computing[END_REF]Proposition 1.2] for a proof). To recover from fail-stop errors, we use the double checkpointing scheme, or buddy algorithm [START_REF] Ni | Hiding Checkpoint Overhead in HPC Applications with a Semi-Blocking Algorithm[END_REF][START_REF] Dongarra | Performance and reliability trade-offs for the double checkpointing algorithm[END_REF]. Therefore, the number of processors assigned to each application must be even. We enforce periodic checkpointing for each application. Formally, if application T i is executed on j processors, there is a checkpoint every period of length τ i,j , with a cost C i,j .

We now explain how to compute the cost C i,j of a checkpoint when application T i executes with j processors. Recall that we use in-memory checkpointing. Let m i be the memory footprint (total data size) of application T i . Each of the j processors holds mi j data, which it must send to its buddy processor. The time to communicate a message of size s is β + s τ , where β is a start-up latency and τ the link bandwidth. We derive that C i,j = mi jτ + β. As for the checkpointing period τ i,j , we use Young's formula [START_REF] Young | A first order approximation to the optimum checkpoint interval[END_REF] and let

τ i,j = 2µ i,j C i,j + C i,j . (1)
Because τ i,j is a first order approximation, the formula is valid only if C i,j µ i,j . When a fault occurs, there is first a downtime of duration D, and then a recovery period of duration R i,j . We assume that R i,j = C i,j , while the downtime value D is platform-dependent and not application-dependent.

Execution time without redistribution

To compute the expected execution time of a schedule, we first have to compute the expected execution time of an application T i executed on j processors subject to failures. We first consider the case without redistribution (but taking failures into account). Let t i,j be the execution time of application T i on j processors in a fault-free scenario. Let t R i,j (α) be the expected time required to compute a fraction α of the total work for application T i on j processors, with 0 ≤ α ≤ 1. We need to consider such a partial execution of T i on j processors to prepare for the case with redistributions.

Recall that the execution of application T i is periodic, and that the period τ i,j depends only on the number of processors, but not on the remaining execution time (see Equation ( 1)). After a work of duration τ i,j -C i,j , there is a checkpoint of duration C i,j . In a fault-free execution, the time required to execute the fraction of work α is αt i,j , hence a total number of checkpoints of

N ff i,j (α) = αt i,j τ i,j -C i,j . (2)
Next, we have to estimate the expected execution time for each period of work between checkpoints. We are able to calculate the expectation of one period of work according to an MTBF value and a number of processors. The expected time to execute successfully during T units of time with j processors (there are T -C units of work and C units of checkpoint, where T is the period) is equal to 1 λj + D (e λjT -1) [START_REF] Herault | Fault-Tolerance Techniques for High-Performance Computing[END_REF]. Therefore, in order to compute t R i,j (α), we compute the sum of the expected time for each period, plus the expected time for the last (possibly incomplete) period. This last period is denoted as τ last (α) and defined as τ last (α) = αt i,j -N ff i,j (α)(τ i,j -C i,j ). The first N ff i,j (α) periods are equal (of length τ i,j ), hence have the same expected time. Finally, we obtain:

t R i,j (α) = e λjR i,j 1 λj +D N ff i,j (α)(e λjτ i,j -1) + (e λjτ last (α) -1) . (3)
In a fault-free environment, it is natural to assume that the execution time is non-increasing with the number of processors. Here, this assumption would translate into the condition:

t R i,j+1 (α) ≤ t R i,j (α) for 1 ≤ i ≤ n, 1 ≤ j < p, 0 ≤ α ≤ 1. (4)
However, when we allocate more processors to an application, even though the work is further parallelized, the probability of failures increases, and the corresponding waste increases as well. Therefore, adding resources to an application is useful up to a threshold. After this threshold, we have t R i,j+1 ≥ t R i,j . In order to satisfy Equation (4), we restrict the number of processors assigned to each application, and never assign more processors than the previous threshold. In other words, if T i is already assigned j processors, we consider assigning more processors to it only if t R i,j+1 ≤ t R i,j . Formally, this defines a maximum number of processors, time 0 processors

T 3 RC 3 T 3 T 2 T 1 RC 1 T 1 q q 1 q 3
Figure 1: Redistribution at the end of an application, where RC i represents the redistribution cost for task T i . j max (i), for each application T i : j max (i) = min 1≤j≤p {j such that t R i,k ≥ t R i,j for all k > j}, and we assume that t R i,j+1 ≤ t R i,j for all j < j max (i). Another common assumption for malleable applications is that the work is non-decreasing when the number of processors increases [START_REF] Blazewicz | Approximation algorithms for scheduling independent malleable tasks[END_REF]: this amounts to saying that no super-linear speed-up is possible. Hence, we assume here that for 1

W done = te t i,j W todo = α j k t time 0 te te + t t i,j
≤ i ≤ n, 1 ≤ j < p and 0 ≤ α ≤ 1, (j + 1) × t R i,j+1 (α) ≥ j × t R i,j (α).
For convenience, we denote by t U i the current expected finish time of application T i at any point of the execution. Initially, if application T i is allocated to j processors, we have

t U i = t R i,j (1)
.

Redistributing processors

There are two major cases for which it may be useful to redistribute processors: (1) in a fault-free scenario, when an application ends, it releases processors that can be used to accelerate other applications, and (2) when an error occurs, we may want to force the release of processors, so that we can assign more processors to the application that has been slowed down by the error. We first consider a fault-free scenario in Section 3.3.1, and then we account for the checkpoint costs and for redistribution after failures in Section 3.3.2. Finally, we discuss the case of consecutive redistributions in Section 3.3.3.

Fault-free scenario

We first consider a simplified scenario without checkpoint (nor failure), in order to explain how redistribution works. Consider for instance that q processors are released when application T 2 ends. We can allocate q 1 new processors to application T 1 , and q 3 new processors to application T 3 , where q 1 + q 3 = q (see Figure 1). This redistribution will take some time (redistribution cost RC i , detailed below), after which T 1 and T 3 will resume execution, and we first need to compute the new expected completion time for their remaining fraction of work.

Consider that a redistribution is conducted at time t e (the end time of an application), and that application T i , initially with j processors, now has k = j + q > j processors. What will be the new finish time of T i ? The fraction of work already executed for T i is te ti,j , because the application was supposed to finish at time t i,j (see Figure 2). The remaining fraction of work is α = 1 -te ti,j , and the time required to complete this work with k processors is t , where t t i,k = α, hence t = αt i,k = 1 -te ti,j t i,k . Furthermore, we need to add a redistribution cost: when moving from j to k = j + q processors, the application T i must redistribute its data across the processors. The application keeps its initial j processors, which now hold too much data, and enrolls q = k -j new processors, which have no data yet. Recall that m i is the memory footprint (total data size) of application T i . Each of the original j processors initially holds mi j data and will keep only mi k after the redistribution; it sends mi jk data to each of the newly enrolled q processors, thereby keeping mi j -(k -j) mi jk = mi k data. In turn, each new processor receives mi jk data from j processors and duly gets mi k data in the end. What is the best schedule for such a redistribution, and what time does it require? We first account for a constant start-up overhead S, paid for initiating the redistribution call. Then we adopt a realistic one-port communication model [START_REF] Bhat | Efficient collective communication in distributed heterogeneous systems[END_REF] where a processor can send and receive at most one message at any time-step. Independent communications, involving distinct sender/receiver pairs, can take place in parallel: however, two messages sent by the same processor will be serialized. Recall that the time to communicate a message of size s is β + s τ . To schedule the redistribution, we build a bipartite graph G with j nodes on the left and q nodes on the right. In the one-port model, there can be up to j simultaneous communications (each of size mi jk ) involving j distinct processor pairs. Let us call a round such a set of simultaneous (independent) communications. How many rounds are required to schedule the redistribution? We transform this problem into an edge coloring problem, with one color for one round (see Figure 3). The number of rounds required is equal to the edge chromatic number χ (G). Konig's theorem [START_REF] Bondy | Graph theory with applications[END_REF] states that this edge chromatic number is equal to the maximum degree in G so χ (G) = ∆(G) when G is bipartite. Clearly, we have here ∆(G) = max(j, k -j). Therefore, the number of rounds is equal to max(j, k -j), and the redistribution cost is RC j→k i = S + max(j, k -j) × mi jkτ + β . Needless to say, we would perform a redistribution if the cost of redistribution is lower than the benefit of allocating new processors to the application, i.e., if t i,j -(t e + t ) > RC j→k i .

j 1 j 2 j 3 j 4 q 5 q 6 j q = k -j

Accounting for failures

When struck by a fault, an application needs to recover from the failure and to re-execute some work. While the application loads were well-balanced initially in order to minimize total execution time, now the faulty application is likely to exceed its expected execution time. If it becomes the longest application of the schedule, we try to assign it more processors so as to reduce its completion time, hence redistributing processors.

Because we use the double checkpointing algorithm as the resilience model, we consider processors by pairs. We aim at redistributing pairs of processors either when an application is finished, at time t e (as in the fault-free scenario discussed in Section 3.3.1), or when a failure occurs, say at time t f . In each case, we need to compute the remaining work, and the new expected completion time of the applications that have been affected by the event. Given an application T i , we keep track of the time when the last redistribution or failure occurred for this application, denoted as t lastRi . At time t (corresponding to the end of an application or to a failure), we know exactly how many checkpoints have been taken by application T i executed on j processors since t lastRi , and we let this number be N i,j :

N i,j = t -t lastRi τ i,j . (5)
We begin with the case of an application completion: consider that an application finishes its execution at time t e , hence releasing some processors. We consider assigning some of these processors to an application T i currently running on j processors. The fraction of work executed by T i since the last redistribution is te-t lastR i -Ni,j Ci,j ti,j

, because we have to remove the cost of the checkpoints, during which the application did not execute useful work.

We apply the same reasoning for the second case, when a fault occurs. In this case, we need to consider the application T i where the failure stroke, and other applications T i from which we would remove some processors (in order to give them to T i ).

• Consider that application T i is running on j processors and subject to a failure at time t f . Therefore, T i needs to recover from its last valid checkpoint, and the fraction of work executed by T i corresponds to the number of entire periods completed since the last failure or redistribution t lastRi , each followed by a checkpoint. We can express it as

Ni,j ×(τi,j -Ci,j ) ti,j . • At time t f , consider application T i , on which we perform a redistribution, moving from j to j -q processors, with q > 0. The fraction of work executed by T i can be computed as in the application ending case scenario: it is

time t lastR i = 0 processors C i,j C i,j Fault t D R i,j RC j→j+q i C i,j+q t lastR i T i C i ,j C i ,j RC j →j -q i C i ,j -q T i t lastR i C i ,j C i ,j T i
Figure 4: Example of redistribution when a fault strikes application T i . The colored rectangles correspond to useful work done by T i and T i before the failure. T i is not affected by the failure as it does not perform a redistribution.

Finally, for any application subject to a redistribution or a failure, let α i be the remaining fraction of work to be executed by T i , that is 1 minus the sum of the fraction of work executed before t lastRi and the fraction of work expressed above (computed between t lastRi and t).

Similarly to the fault-free scenario, RC j→k i denotes the redistribution cost for application T i when moving from j to k processors. Redistribution can now add (k > j) or remove (k < j) processors to application T i , and the cost is expressed as:

RC j→k i = S + max(min(j, k), |k -j|) × m i kjτ + β . (6)
We are now ready to compute the new values of t lastRi for all applications subject to a failure or a redistribution, and we illustrate the different scenarios in Figure 4. Let t be the time of the event (end of application t = t e , or failure t = t f ), and consider that a redistribution is done either for a faulty application T i or for another application T i . After a redistribution, we always start by taking a checkpoint before computing with the new period. Therefore, if a fault occurs, we do not have to redistribute again.

For the faulty application T i , the new value of t lastRi hence becomes t lastRi = t + D + R i,j + RC j→k i + C i,k (we need to account for the downtime and recovery). However, if T i is performing a redistribution but it was not struck by a failure, it can start the redistribution at time t: either it is getting new processors that are available following the end of an application, or it is using fewer processors and can perform its redistribution. In all cases, we have t lastR i = t+RC j →k i +C i ,k . Note that we can have processors involved simultaneously in two redistributions, as they will only receive data from the other processors of the faulty application T i , and send data to the other processors of the non-faulty application T i . We assume that sends and receives can be done in parallel without slowdown.

Finally, the expected finish time of an application T i for which we have updated t lastRi becomes t

U i = t lastRi + t R i,k (α i ),
where k is the new number of processors on which T i is executed, and α i the remaining fraction of work. Similarly to the fault-free scenario, we give extra processors to an application only if the new expected finish time t U i is lower than the one with no redistribution.

When multiple redistributions overlap

Here, we deal with the problem of chaining redistributions. If another event (application completion or fault) occurs during the current redistribution, we cannot enroll the processors that have not yet finished the current redistribution. On Figure 5, at the end of the application T 3 , there are no available applications to whom we may try to give its processors. T 1 will be able to start a new redistribution at time-step t 1 , and T 2 at time-step r 2 .

Objective function

We can now state the objective function: Given n malleable applications {T 1 , . . . , T n }, their speedup profiles, and an execution platform with p identical processors subject to failures with individual rate λ, CoSched aims at minimizing the maximum of the expected completion times of the applications. Redistributions are allowed only when an application completes execution or is struck by a failure (with a cost specified in Section 3.3).

Complexity results

We first consider the CoSched problem without redistributions and provide an optimal polynomial-time algorithm. Then, we prove that the problem becomes NP-complete with redistributions, even in a fault-free scenario.

Aupy et al. [START_REF] Aupy | Co-scheduling algorithms for highthroughput workload execution[END_REF] designed a greedy algorithm to solve the problem with no redistribution, in a faultfree scenario. Their algorithm (called Optimal-1-pack-schedule) therefore works with t i,j values instead of t R i,j , and minimizes the execution time of the applications. As a minor detail, it does not take into account the fact that the number of processors assigned to an application must always be even in our setting, because we use the double checkpointing algorithm. It is not difficult to extend this algorithm to solve the problem with failures, but still without redistributions: the idea is to give initially two processors per applications, to sort them by expected execution time, and to greedily give two extra processors to the longest application, if it decreases its expected execution time. This algorithm is called Opt-NoRedistrib. We can therefore prove the following theorem (see [START_REF] Benoit | Resilient application co-scheduling with processor redistribution[END_REF] for the proof).

Theorem 1. The CoSched problem without redistributions can be solved in polynomial time O(n), where n is the number of applications.

We show through a few examples the difficulty of CoSched when redistributions are allowed, even when there are no failures. The first example shows that the previous algorithm Opt-NoRedistrib is no longer optimal. Consider two applications T 1 and T 2 and three processors, and further assume that there is no cost for redistribution. We use the following speedup profiles:

T 1 = t1,1 = 10, w1,1 = 10 t1,2 = 9,
w1,2 = 18 t1,3 = 6, w1,3 = 18

T 2 = t 2,1 = 6, w 2,1 = 6 t 2,2 = 3, w 2,2 = 6
where w i,j represents the work for application i with j processors, i.e., w i,j = j × t i,j . Opt-NoRedistrib initially assigns one processor to each application, and then the remaining one to the longest application T 1 . At time 6, when T 2 finishes and releases its processor, we redistribute T 1 over the three processors. At time 6, the application T 1 has done 2/3 of its work, it remains 1/3×t 1,3 = 1/3×6 = 2 time units with 3 processors, therefore T 1 ends at time 6+2 = 8 (see Figure 6a). We obtain a smaller makespan if we do not use Opt-NoRedistrib but instead the variant GreedySpeedupProfile, where remaining processors are allocated to the application with the best speedup profile. In the example, GreedySpeedupProfile initially allocates the third processor to T 2 because the execution time with two processors is divided by two, i.e., perfect speedup with w 2,2 /w 2,1 = 1. Then T 2 finishes at time 3. At this time, T 1 has still to complete 7/10 of its load, so the remaining time for T 1 is equal to 7/10 × t 1,3 = 7/10 × 6 = 4.2. The makespan in this second configuration becomes 3 + 4.2 = 7.2, which is better! Since Opt-NoRedistrib is no longer optimal, a natural question is whether GreedySpeedupProfile is optimal. The following example answers negatively. Consider the following speedup profiles (with two applications and three processors as before): GreedySpeedupProfile allocates two processors to T 2 (best speedup profile) and one processor to T 1 . So at time 3, the application T 2 completes and its two processors are given to T 1 . The execution time for T 1 is 3 + 7/10 × 5 = 6.5. But if we allocate two processors to T 1 and one to T 2 , we finish both applications at time 6 without any redistribution! Intuitively, these little examples show that CoSched seems to be of combinatorial nature when redistributions are taken into account, even with zero cost.

T 1 = t 1,1 = 10, w 1,1 = 10 t 1,2 = 6, w 1,2 = 12 t 1,3 = 5, w 1,3 = 15 T 2 = t 2,1 = 6, w 2,1 = 6 t 2,2 = 3, w 2,2 = 6
To establish the complexity of the problem with redistributions, we consider the simple case with no failures. Therefore, redistributions occur only at the end of an application, and any application changes at most n times its number of processors, where n is the total number of applications. We further consider that the redistribution cost is a constant equal to S, i.e., we let β = 0 and τ = +∞ in Equation [START_REF] Daly | A higher order estimate of the optimum checkpoint interval for restart dumps[END_REF]. Even in this simplified scenario, the problem is NP-complete: Theorem 2. With constant redistribution costs and without failures, CoSched is NP-complete (in the strong sense).

The proof is available in the associated research report [START_REF] Benoit | Resilient application co-scheduling with processor redistribution[END_REF]. Note that we conjecture that CoSched remains NP-complete with zero redistribution cost. This is because of the combinatorial exploration suggested by the examples. But this remains an open problem!

Heuristics

In this section, we introduce polynomial-time heuristics to solve the general CoSched problem with both failures and redistributions. Before performing any redistribution, we need to choose an initial allocation of the p processors to the n applications. We use the optimal algorithm without redistribution discussed in Section 4 (Opt-NoRedistrib).

We first discuss the general structure of the heuristics. Then, we explain how to redistribute available processors, and the two strategies to redistribute when failures occur. The pseudo-codes for all algorithms are available in the companion research report [START_REF] Benoit | Resilient application co-scheduling with processor redistribution[END_REF].

General structure. All heuristics share the same skeleton: we iterate over each event (either a failure or an application termination) until total remaining work is equal to zero. If some applications are still working for a previous redistribution, (i.e., the current time t is smaller than t lastRi for these applications), then we exclude them for the next redistribution, and add them back into the list of applications after the current redistribution is completed. If an application ends, we redistribute available processors as will be discussed in Section 5. Then, if there is a failure, we calculate the new expected execution time of the faulty application. Also, we remove from the list the applications that end before t lastR f , and we release their processors.

Afterwards, we have to choose between trying to redistribute or do nothing. If the faulty application is not the longest application, the total execution time has not changed since the last redistribution. Therefore, because it is the best execution time that we could reach, there is no need to try to improve it. However, if the faulty application is the longest application, we apply a heuristic to redistribute processors (see below).

Redistribution when an application ends. When an application ends, the idea is to redistribute the processors that it releases in order to decrease the expected execution time. The easiest way to proceed consists in adding processors greedily to the application with the longest execution time, as was done in Opt-NoRedistrib to compute an optimal schedule. This time, we further account for the redistribution cost, and update the values of α i , t lastRi and t U i for each application i that encountered a redistribution. Therefore, this heuristic, called EndLocal, returns a new distribution of processors.

Rather than using only local decisions to redistribute available processors at time t, it is possible to recompute an entirely new schedule, using Opt-NoRedistrib again, but further accounting for the cost of redistributions. This heuristic is called EndGreedy. Now, we need to compute the remaining fraction of work for each application, and we obtain an estimation of the expected finish time when each application is mapped on two processors. Similarly to Opt-NoRedistrib, we then add two processors to the longest application while we can improve it, accounting for redistribution costs.

Note that we effectively update the values of α i and t lastRi for application T i only if a redistribution was conducted for this application. It may happen that the algorithm assigns the same number of processors as was used before. Therefore, we keep the updated value of the fraction of work in a temporary variable α t i and update it whenever needed at the end of the procedure.

Redistribution when there is a failure. Similarly to the case of an application ending, we propose two heuristics to redistribute in case of failures. The first one, ShortestapplicationsFirst, takes only local decisions. First, we allocate the k available processors (if any) to the faulty application if that application is improvable. Then, if the faulty application is still improvable, we try to take processors from shortest applications (denoted T s ) in the schedule, and give these processors to the faulty application, until the faulty application is no longer improvable, or there are no more processors to take from other applications. We take processors from an application only if its new execution time is smaller than the execution time of the faulty application.

The second heuristic, IteratedGreedy, uses a modified version of the greedy algorithm that initializes the schedule (Opt-NoRedistrib) each time there is a failure, while accounting for the cost of redistributions. This is done similarly to the redistribution of EndGreedy explained above, except that we need to handle the faulty application differently to update the values of α f and t lastR f .

Simulations

To assess the efficiency of the heuristics defined in Section 5, we have performed extensive simulations. The simulation settings are discussed in Section 6.1, and results are presented in Section 6.2. Note that the code is publicly available at http://graal.ens-lyon.fr/ ~abenoit/code/redistrib, so that interested readers can experiment with their own parameters.

Simulation settings

To evaluate the quality of the heuristics, we conduct several simulations, using realistic parameters. The first step is to generate a fault distribution: we use an existing fault simulator developed in [START_REF] Bougeret | Checkpointing strategies for parallel jobs[END_REF][START_REF] Bosilca | Unified model for assessing checkpointing protocols at extreme-scale[END_REF]. In our case, we use this simulator with an exponential law of parameter λ. The second step is to generate a fault-free execution time for each application (the t i,j value). We use a synthetic model to generate the execution profiles in order to represent a large set of scientific applications. The application model that we use is a classical one, similar to the one used in [START_REF] Aupy | Co-scheduling algorithms for highthroughput workload execution[END_REF]. For a problem of size m, we define the sequential time: t(m, 1) = 2 × m × log 2 (m). Then we can define the parallel execution time on q processors:

t(m, q) = f × t(m, 1) + (1 -f ) t(m, 1) q + m q log 2 (m). (7)
The parameter f is the sequential fraction of time, we fix it to f = 0.08. So 92% of time is considered as parallel. The factor m q log 2 (m) represents the overhead due to communications and synchronizations. Finally, we have t i,j (m i ) = t(m i , j) where t i,j (m i ) is the execution time for application T i with a problem of size m i on j identical processors.

Finally, we assign to each application T i a random value for the number of data m i such that:

m inf ≤ m i ≤ m sup . If m inf
m sup then the data distribution between applications is very heterogeneous. On the contrary, if m inf is close to m sup , the data distribution is homogeneous, in other words all applications have (almost) the same execution time. Unless stated otherwise, we set m inf = 1, 500, 000 and m sup = 2, 500, 000 to have execution times long enough so that several failures are likely to strike during execution. With such a value for m sup , the longest execution time in a fault-free execution is around 100 days. We also consider two different data distribution cases, (i) very heterogeneous with m inf = 1, 500, and (ii) homogeneous with m inf = 2, 499, 000.

The cost of checkpoints for an application T i with j processors is C i,j = C i /j, where C i is proportional to the memory footprint of the application. We have C i = m i × c, where c is the time needed to checkpoint one data unit of m i . The default value is c = 1 , unless stated otherwise. The synchronisation cost value S is fixed to S = 0 for all following experiments. Finally, the MTBF of a single processor is fixed to 100 years, unless stated otherwise.

In the following section, we vary the number of processors, the number of applications, the checkpointing cost and the data distribution, in order to study their impact on performance. Note that we assume that a failure can strike during checkpoints but not during downtime, recovery and while the processor is performing some redistribution.

Results

To evaluate the heuristics, we execute each heuristic x = 50 times and we compute the average makespan, i.e., the longest execution time in the pack. We compare the makespan obtained by the heuristics to the makespan (i) in a faulty context without any redistribution (worst case), and (ii) in a fault-free context with redistributions (best case). We normalize the results by the makespan obtained in a faulty context without any redistribution, which is expected to be the worst case. The execution in a fault-free setting provides us an optimistic value of the execution of the application in the ideal case where no failures occur.

We consider four heuristics: IteratedGreedy-EndGreedy where we greedily recompute a new schedule at each application termination and each failure; IteratedGreedy-EndLocal where we use EndLocal at each application termination, but IteratedGreedy in case of failures; Shortestapplications-First-EndGreedy where we greedily recompute a new schedule at each application termination, but use ShortestapplicationsFirst in case of failures; and ShortestapplicationsFirst-EndLocal where we only use the local variants.

Performance in a fault-free context. Figure 7 shows the impact of redistribution in a fault-free context with 100 applications, where we vary the number of processors from 200 to 2000. In this case, we compare EndLocal with EndGreedy (see Section 5). The two heuristics have a very similar behavior, leading to a gain of a least 20% with less than 500 processors, and a slightly better gain for the EndGreedy global heuristic. When the number of processors increases, the efficiency of both heuristics decreases to converge to the performance without redistribution. Indeed, there are then enough processors so that each application does not make use of the extra processors released by ending applications. In the heterogeneous context (with m inf = 1500), the gain due to redistribution is even larger.

Figure 8 shows the impact of redistribution in a fault-free context with 1000 applications, we vary the number of processors from 2000 to 10000. We compare EndLocal with EndGreedy, the two heuristics have a similar behavior. As showed in Figure 7, the redistribution is more efficient in the heterogeneous context (with m inf = 1500).

In the homogeneous case (Figure 8c), the results clearly show how the number of processors is directly linked to the efficiency of redistribution. If p/n is even, as each application has almost the same size, we assign p/n processors to each application. Consequently each application will finish at the same time and redistributions have very limited use. When p is not divisible by n or if p/n is odd, at least one application will have more processors than the others. So, at least one application will finish before the others and the redistribution will be more efficient. We note that the redistribution has a larger impact when few processors are involved, this is due to the fact that the speedup is better with fewer processors (sublinear speedup). In other words, it is more useful to upgrade from 2 processors to 4 processors rather than from 500 to 502, in terms of speedup.

Impact of n. Figure 9 shows the impact of the number of applications n when the number of processors is fixed to 5000. The results show that having more applications increases the efficiency of both heuristics. With n = 1000, we obtain a gain of more than 40% due to redistributions. The reason is that when n increases, the number of processors assigned to each application decreases, then heuristics have more flexibility to redistribute. Note that, as expected, IteratedGreedy is better than ShortestapplicationsFirst, because it recomputes a complete new schedule at each fault, instead of just allocating available processors from shortest applications to the faulty application. Using EndGreedy with IteratedGreedy does not improve the performance, while EndGreedy is useful with ShortestapplicationsFirst, hence showing that complete redistributions are useful, even when only performed at the end of an application.

We also observe that results in the heterogeneous cases are slightly better than in the homogeneous case, but the difference in the homogeneous case when n = 1000 is very tiny due to the large number of applications (i.e., fewer processors allocated to applications so the redistribution is more efficient). Impact of p. Figure 10 shows the impact of the number of processors p when the number of applications is fixed. We vary p between 200 and 5000 processors. The results show that having more processors decreases the efficiency of both heuristics, but, in the heterogeneous cases, there is always a gain of at least 10% thanks to redistributions. As noted in the fault-free case, the redistribution is more efficient when the data distribution is very heterogeneous (Figure 10a). On the contrary, in the homogeneous case (Figure 10c) the redistribution is less efficient (gain around 10%). The same observations hold, i.e., the use of EndGreedy vs EndLocal impacts only ShortestapplicationsFirst. In average, with IteratedGreedy, we obtain a gain of 25%, while ShortestapplicationsFirst provides a gain around 15% when it is not combined with EndGreedy. This figure also allows us to observe the impact of the MTBF on performance. Indeed, the MTBF is set to 100 years for each processor, but the overall MTBF for an application (µ i,j value) decreases when the number of processors increases, so the gain obtained by the heuristics decreases due to the increasing number of failures. Heuristic behaviors. Figure 11 compares IteratedGreedy and ShortestapplicationsFirst, when combined with EndLocal, on a single execution. We depict both the evolution of the makespan (see Figure 11a) and the standard deviation, in terms of number of processors (see Figure 11b). IteratedGreedy is clearly superior in terms of makespan, and this can be explained by the fact that it allocates more processors to the longest application, earlier in time than ShortestapplicationsFirst, hence resulting in a larger standard deviation. Because ShortestapplicationsFirst takes only local decisions, it takes more time before enough processors are given to the longest application.

Impact of MTBF. Figures 12 and13 show the impact of the MTBF on the performance of redistributions. We vary the MTBF of a single processor between 5 years and 125 years. When the MTBF decreases, the number of failures increases, consequently the performance of both heuristics decreases. In Figure 12, the performance of IteratedGreedy is closely linked to the MTBF value. Indeed, it tends to favor a heterogeneous distribution of processors (i.e., applications with many processors and applications with few processors). If an application is executed on many processors, its MTBF becomes very small and this application will be hit by more failures, hence it becomes even worse than without redistribution!

We observe the same result in Figure 13, especially in the homogeneous case (Figure 13c). This effect is even amplified due the number of processors (p = 5000) which directly decreases the MTBF and deteriorate the performance (increasing number of faults).

Figure 2 :

 2 Figure 2: Work representation for application T i at time te.

Figure 3 :

 3 Figure 3: Bipartite graph G representing a redistribution from j = 4 to k = 6 processors, with each communication round colored. We have χ (G) = ∆(G) = 4.

3 T 2 T 1 Figure 5 :

 3215 Figure 5: Illustration of two consecutive events.

1 ( b )Figure 6 :

 1b6 Figure 6: Examples: coordinates are execution time (x-axis) and processors (y-axis).

  m inf = 2499000.

Figure 7 :

 7 Figure 7: Performance of redistribution in a fault-free context with msup = 2500000.

Figure 8 :

 8 Figure 8: Performance of redistribution in a fault-free context with msup = 2500000.

  (a) Makespan at each failure dealt with.

  Standard deviation at each failure dealt with.

Figure 11 :

 11 Heuristic behaviors with n = 100, p = 1000, MTBF of 50 years, for a single execution.

  Impact of n with p = 5000 processors.(c) m inf = 2499000. Figure10: Impact of p with n = 100 applications and msup = 2500000.

	Normalized execution time	0.75 1	Fault context without ReDistrib IteratedGreedy-EndGreedy IteratedGreedy-EndLocal ShortestApplicationsFirst-EndGreedy ShortestApplicationsFirst-EndLocal Fault-free context with ReDistrib (EndLocal)	Normalized execution time	0.75 1	Fault context without ReDistrib IteratedGreedy-EndGreedy IteratedGreedy-EndLocal ShortestApplicationsFirst-EndGreedy ShortestApplicationsFirst-EndLocal Fault-free context with ReDistrib (EndLocal)		Normalized execution time	0.75 1	Fault context without ReDistrib IteratedGreedy-EndGreedy IteratedGreedy-EndLocal ShortestApplicationsFirst-EndGreedy ShortestApplicationsFirst-EndLocal Fault-free context with ReDistrib (EndLocal)
	Normalized execution time Makespan (s)	0.5 0.75 1 100 1.6x10 7 200 500 1.8x10 7 2.8x10 7 3x10 7 0 1000 Figure 9: 0.5 300 400 500 600 700 800 900 1000 #tasks Fault context without ReDistrib IteratedGreedy-EndGreedy IteratedGreedy-EndLocal ShortestApplicationsFirst-EndGreedy ShortestApplicationsFirst-EndLocal Fault-free context with ReDistrib (EndLocal) (a) m inf = 1500. 0.5 0.75 1 100 Normalized execution time 1500 2000 2500 3000 3500 4000 4500 5000 #procs (a) m inf = 1500. 0.5 2 x 1 0 6 4 x 1 0 6 6 x 1 0 6 8 x 1 0 6 1 x 1 0 7 1 .2 x 1 0 7 1 .4 x 1 0 7 1 .6 x 1 500 0 7 1 200 .8 1000 (b) m inf = 1500000. 300 400 500 600 700 #tasks Fault context without ReDistrib 800 900 IteratedGreedy-EndGreedy IteratedGreedy-EndLocal ShortestApplicationsFirst-EndGreedy ShortestApplicationsFirst-EndLocal Fault-free context with ReDistrib (EndLocal) 1500 2000 2500 3000 3500 4000 4500 #procs (b) m inf = 1500000. x 1 0 7 2 x 1 0 7 Date of faults (s) No ReDistrib IteratedGreedy+EndLocal 2x10 7 2.2x10 7 2.4x10 7 2.6x10 7 ShortestApplicationsFirst+EndLocal	1000 5000	Normalized execution time	0.5 0.75 1 100 0.5	500	200	300 (c) m inf = 2499000. 400 500 600 700 #tasks Fault context without ReDistrib 800 900 IteratedGreedy-EndGreedy IteratedGreedy-EndLocal ShortestApplicationsFirst-EndGreedy ShortestApplicationsFirst-EndLocal Fault-free context with ReDistrib (EndLocal) 1000 1500 2000 2500 3000 3500 4000 4500 #procs	1000 5000

t f -t lastR i -N i ,j C i ,j t i ,j.

Impact of checkpointing cost. Figure 14 shows the impact of the checkpointing cost on a platform with 100 applications and 1000 processors. To do so, we multiply the checkpointing cost by c in Figure 14 (recall that c is the time needed to checkpoint one data unit). When c decreases, the performance of the heuristics increases and the gap between the execution time in a fault-free context and a fault context becomes small. Indeed, if checkpoints are cheap, a lot of checkpoints can be taken, and the average time lost due to failures decreases. We observe that when the checkpointing cost c tends to 1, the checkpointing costs are more important and the redistribution (specially IteratedGreedy) becomes more unstable. This effect is amplified in a homogeneous context, because applications and checkpoints are larger than in a heterogeneous context. We see the same effect on Figure 15.

Impact of the sequential fraction of time. Figure 16 shows the impact of the sequential fraction of time. We vary f from 0 (applications are fully parallel) to 0.5 (50% of the time is sequential). The results show that when applications are more parallel, the redistribution is more efficient. This result is expected, because if applications are not parallel, there is less gain when trying to allocate more processors to help them complete.

In the homogeneous case (Figure 16c), the IteratedGreedy heuristic is worse than the result without redistribution when f is greater than 0.3. It is due to the fact that all applications are large and not fully parallel, so when we greedily recompute a new schedule at each fault, we might deteriorate the performance. Summary. To conclude, we note that IteratedGreedy achieves better performance than Shortestap-plicationsFirst, mainly because it rebuilds a complete schedule at each fault, which is very efficient but also costly. Nevertheless, when the MTBF is low (around 10 years or less), ShortestapplicationsFirst becomes better than IteratedGreedy. In a faulty context, we gain flexibility from the failures and we can achieve a better load balance. We observe that the ratio between the number of applications and the number of processors plays an important role, because having too many processors for few applications leads to a deterioration of performance (especially in a homogeneous context).

About the data distributions, we observe that the best context to take advantage of redistributions is a heterogeneous context with large and short applications. In the homogeneous context, when we assign the same weight to each application, redistributions become much less interesting. We also show that the cost of checkpointing and the fraction of sequential time have a significant impact on performance.

Finally, we point out that all four heuristics run within a few seconds, while the total execution time of the application takes several days, hence even the more costly combination IteratedGreedy-EndGreedy incurs a negligible overhead.

Conclusion

In this paper, we have designed a detailed and comprehensive model for scheduling a pack of applications on a failure-prone platform, with processor redistributions. We have introduced a greedy polynomial-time algorithm that returns the optimal solution when there are failures but no processor redistribution is allowed. We have shown that the problem of finding a schedule that minimizes the execution time when accounting for redistributions is NP-complete in the strong sense, even with constant redistribution costs and no failures. Finally, we have provided several polynomial-time heuristics to redistribute efficiently processors at each failure or when an application ends its execution and releases processors. The heuristics are tested through extensive simulations, and the results demonstrate their usefulness: a significant improvement of the execution time can be achieved thanks to the redistributions.

There remains to validate the model on a real system by conducting real experiments, even though this is beyond the scope of this paper. Further work will also consider partitioning the applications into several consecutive packs (rather than one) and conduct further simulations (and experiments) in this context. On the theoretical side, we plan to investigate the complexity of the online redistribution algorithms in terms of competitiveness. It would also be interesting to deal not only with fail-stop errors, but also with silent errors. This would require adding verification mechanisms to detect such errors.


Gilles Dowek
email: gilles.dowek@ens-paris-saclay.fr

Analyzing individual proofs as the basis of interoperability between proof systems

Introduction

Sciences study both individual objects and generic ones. For example, Astronomy studies both the individual planets of the Solar system: Mercury, Venus, etc. determining their radius, mass, composition, etc., but also the motion of generic planets: Kepler's laws, that do not just apply to the six planets known at the time of Kepler, but also to those that have been discovered after, and those that may be discovered in the future. Computer science studies both algorithms that apply to generic data, but also specific pieces of data. Mathematics mostly studies generic objects, but sometimes also specific ones, such as the number π or the function ζ .

Proof theory mostly studies generic proofs. For example, Gentzen's cut elimination theorem for Predicate logic applies to any proof expressed in Predicate logic, those that were known at the time of Gentzen, those that have been constructed after, and those that will be constructed in the future. Much less effort is dedicated to studying the individual mathematical proofs, with a few exceptions, for example [START_REF] Leitsch | On proof mining by cut-elimination[END_REF].

Considering the proofs that we have, instead of all those that we may build in some logic, sometimes changes the perspective. For example, consider a cut elimination theorem for a logic L . The stronger the logic L , the stronger the theorem. In contrast, consider a specific proof π, say a proof of Fermat's little theorem, and consider a theorem of the form: the proof π can be expressed in the logic L . In this case, the weaker the logic, the stronger the theorem. So, studying generic proofs leads to focus on stronger and stronger logics, while studying individual proofs, on weaker and weaker ones.

In this paper, we present a program of analyzing the formal proofs that have been developed in computerized proof systems such as COQ 1 , MATITA 2 , HOL LIGHT 3 , ISABELLE/HOL 4 , PVS 5 , FO-CALIZE 6 , etc. In particular, we want to be able to analyze in which logicsa each of these proofs can be expressed.

Such a project is largely inspired by the reverse mathematics project [START_REF] Friedman | Systems of second-order arithmetic with restricted induction, I, II[END_REF][START_REF] Simpson | Subsystems of second-order arithmetic[END_REF], but has some differences. First, we do not propose to classify theorems according to the logics in which they can be proved, but to classify the proofs according to the logics in which they can be expressed. Some theorems, for example, the prime number theorem, have very different proofs, some very elementary and some very complex. Second, we focus on formal proofs, that is proofs expressed and checked in computerized proof systems. Third, our project is in some sense less ambitious, as it focuses on stronger theories than reverse mathematics. We typically address the question of the possibility to express a proof in the Calculus of constructions [START_REF] Coquand | The Calculus of Constructions[END_REF], or in Simple type theory [START_REF] Church | A formulation of the simple theory of types[END_REF], while reverse mathematics focuses on fragments of Second-order arithmetic.

Knowing in which logics, which proof can be expressed is a fundamental question, as it is part of our understanding of these proofs. It is also a practical one, as it opens the way to interoperability between computerized proof systems. In the domain of formal proofs, we currently have COQ proofs, HOL LIGHT proofs, etc. of various theorems. And, when we have a COQ proof of a theorem, we do not necessarily have a HOL LIGHT proof of this theorem, and vice versa. The problem of exchanging proofs between proof systems is not just a problem of translation, as these systems cannot express the same proofs. It is primarily the problem of analyzing the logics in which these proofs can or cannot be expressed.

2 From logics to theories

Logical Frameworks

When a proof is expressed in a logic L , analyzing the logics in which this proof can be expressed amounts to analyzing the ingredients of the logic L that it uses. This requires to analyze this logic into a number of ingredients, for example into a number of axioms. Set theory, for example, is naturally analyzed into a number of axioms and axiom schemes, including, for example, the axiom of choice, and this analysis permits to classify the proofs according to the axioms they use: the proof that every vector has a unique decomposition in a given basis does not use the axiom of choice, the proof that every vector space has a basis does. These ingredients of set theory are expressed in a logical framework: Predicate logic. So, analyzing a logic amounts to expressing it as a theory in a logical framework.

To express set theory, it is also possible to choose another logical framework: Constructive predicate logic and add the excluded middle as an axiom scheme. Then, we can express that the proof that every vector has a unique decomposition in a given basis does not use the excluded middle, while the proof of the Bolzano-Weierstrass theorem does.

The examples of the axiom of choice and of the excluded middle show that, even in everyday mathematics, we do care about the analysis of proofs, even if this analysis is often restricted to the very specific cases of the axiom of choice and of the excluded middle.

Axioms and rewrite rules

Predicate logic is certainly the most widely used logical framework. But it also has some limitations. For example, many theories are expressed with an infinite number of axioms and eliminating axiom schemes, like in Von Neumann-Bernays-Gödel set theory, is often cumbersome [START_REF] Kirchner | A Finite First-Order Theory of Classes[END_REF]. Moreover, if Simple type theory can easily be expressed in Predicate logic, expressing the Calculus of constructions, the Calculus of inductive constructions, etc. is more cumbersome.

Another logical framework is that of Pure type systems [START_REF] Barendregt | Lambda calculi with types[END_REF], where it is possible to express Simple type theory, the λ Π-calculus, the system F, the Calculus of constructions, etc. and analyze these logics into sorts, axioms, and rules. This permits to classify the proofs expressed, for example, in the Calculus of constructions, into those that use the polymorphic rules and those that do not. But this logical framework also has limitations as the Calculus of inductive constructions cannot be expressed in it.

Another logical framework is the λ Π-calculus, that is the λ -calculus with dependent types [START_REF] Harper | A framework for defining logics[END_REF]. Like in Predicate logic, the ingredients of a logic expressed in this framework are axioms and it is difficult to express in the λ Π-calculus the logics that include a computational, or definitional, equality that identifies some terms.

So, we shall use another logical framework that is a synthesis of Predicate logic, Pure type systems and the λ Π-calculus: the λ Π-calculus modulo theory [START_REF] Cousineau | Embedding Pure Type Systems in the lambda-Pi-calculus modulo[END_REF], also called the Martin-Löf logical framework [START_REF] Nordström | Martin-Löf's type theory[END_REF], where the ingredients of a logic are axioms and rewrite rules, like in Deduction modulo theory [START_REF] Dowek | Theorem proving modulo[END_REF][START_REF] Dowek | Proof normalization modulo[END_REF]. Simple type theory can easily be expressed as a theory in the λ Π-calculus modulo theory, with three rewrite rules, and the Calculus of constructions as a theory with just four rules. Moreover, the λ Π-calculus modulo theory has an efficient implementation: the system DEDUKTI [START_REF] Assaf | Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo Theory[END_REF], whose first implementation has been presented in [START_REF] Boespflug | Conception d'un noyau de vérification de preuves pour le lambda-Pi-calcul modulo[END_REF] and its most recent in [START_REF] Saillard | Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice[END_REF].

Translating proofs expressed in the Calculus of constructions into proofs in Simple type theory

We show, in this section, how to express constructive Simple type theory and the Calculus of constructions, in the λ Π-calculus modulo theory. We then discuss how this can be used to analyze if a proof, expressed in the Calculus of constructions, can be reformulated in Simple type theory or not, according to these expressions of these theories in the λ Π-calculus modulo theory.

Simple type theory as a theory in the λ Π-calculus modulo theory

Simple type theory can be expressed in Deduction modulo theory [START_REF] Dowek | HOL-lambda-sigma: an intentional first-order expression of higher-order logic[END_REF] and hence in the λ Π-calculus modulo theory [START_REF] Assaf | A Calculus of Constructions with explicit subtyping[END_REF][START_REF] Assaf | A framework for defining computational higher-order logics[END_REF]. The types of Simple type theory are expressed as terms of type type, with three constants o, nat, and arrow. The type o is that of propositions, the type nat that of individuals, often written ι, and those built with the constant arrow are the functional types. For example, the type of Simple type theory nat → nat is expressed as the term (arrow nat nat) of type type. Then, to each term t of type type, is associated a type (η t) of the λ Π-calculus modulo theory, using a constant η of type type → Type and the rewrite rule (η (arrow x y)) -→ (η x) → (η y)

For example, to the term (arrow nat nat), is associated the type (η (arrow nat nat)) that reduces to

(η nat) → (η nat).
The terms of Simple type theory of type t are then expressed as terms of type (η t). For example, the term λ x : nat x of Simple type theory is expressed as the term λ x : (η nat) x of type (η nat) → (η nat).

In particular, the propositions are expressed as terms of type (η o), using two constants ⇒ and ∀. For example, the proposition ∀X : o (X ⇒ X) is expressed as the term ∀ o λ X : (η o) (⇒ X X). Note that, in this expression of Simple type theory in the λ Π-calculus modulo theory, we do not have a quantifier ∀ A for each type A, but a single quantifier ∀, that is applied to a term A of type type. Then, to each term p of type (η o), is associated a type (ε p) of the λ Π-calculus modulo theory, using a constant ε of type (η o) → Type and the rewrite rules

(ε (⇒ x y)) -→ (ε x) → (ε y) type : Type η : type → Type o : type nat : type arrow : type → type → type ε : (η o) → Type ⇒ : (η o) → (η o) → (η o) ∀ : Πa : type (((η a) → (η o)) → (η o)) (η (arrow x y)) -→ (η x) → (η y) (ε (⇒ x y)) -→ (ε x) → (ε y) (ε (∀ x y)) -→ Πz : (η x) (ε (y z))
Figure 1: Simple type theory

(ε (∀ x y)) -→ Πz : (η x) (ε (y z))
For example, to the term ∀ o λ X :

(η o) (⇒ X X), is associated the type (ε (∀ o λ X : (η o) (⇒ X X))) that reduces to ΠX : (η o) ((ε X) → (ε X)).
Finally, the proofs of a proposition p in Simple type theory are expressed as terms of type (ε p). For example, the usual proof of the proposition ∀X : o (X ⇒ X) is expressed as the term λ X :

(η o) λ α : (ε X) α.
This leads to the theory presented in Figure 1.

The Calculus of constructions as a theory in the λ Π-calculus modulo theory

We consider a slight extension of the Calculus of constructions with a symbol nat of type Kind. Such an extension can be obtained just by adding a constant nat and a rule assigning it the type Kind, a rule allowing to declare a variable of type Kind, or an extra sort allowing to declare a variable of type Kind [START_REF] Geuvers | Logics and Type systems[END_REF][START_REF] Geuvers | The Calculus of Constructions and Higher Order Logic[END_REF]. This logic can be expressed, in the λ Π-calculus modulo theory [START_REF] Cousineau | Embedding Pure Type Systems in the lambda-Pi-calculus modulo[END_REF], as the theory presented in Figure 2. Note that this presentation slightly differs from that of [START_REF] Cousineau | Embedding Pure Type Systems in the lambda-Pi-calculus modulo[END_REF]: the symbol U Type has been replaced everywhere by the term ε Kind ( Ṫype) allowing to drop the rule

ε Kind ( Ṫype) -→ U Type
Then, to keep the notations similar to those of Simple type theory, the constant U Kind is written type, the constant Ṫype, o, the constant ε Kind , η, the constant ε Type , ε, the constant Π Kind,Kind,Kind , arrow, the constant Π Type,Type,Type , ⇒, the constant Π Kind,Type,Type , ∀, and the constant Π Type,Kind,Kind , π. Finally, a symbol nat is added, as we consider an extension of the Calculus of constructions with such a symbol.

Comparing Simple type theory and the Calculus of constructions

Now that the theories have been formulated in the same logical framework, we can compare their expressions.

type

: in the Calculus of constructions. This reflects the fact that this symbol is non-dependent in Simple type theory and dependent in the Calculus of constructions, where, in the type A → B, written Πx : A B, the type B may contain a variable x of type A.

Type η : type → Type o : type nat : type arrow : Πx : type (((η x) → type) → type) ε : (η o) → Type ⇒ : Πx : (η o) (((ε x) → (η o)) → (η o)) ∀ : Πx : type (((η x) → (η o)) → (η o)) π : Πx : (η o) (((ε x) → type) → type) (η (arrow x y)) -→ Πz : (η x) (η (y z)) (ε (⇒ x y)) -→ Πz : (ε x) (ε (y z)) (ε (∀ x y)) -→ Πz : (η x) (ε (y z)) (η (π x y)) -→ Πz : (ε x) (η (y z))
In the same way, the symbol ⇒ is non-dependent in Simple type theory, but it is dependent in the Calculus of constructions, where, in the proposition A ⇒ B, also written Πx : A B, the proposition B may contain a variable x, that is a proof of A.

In contrast, the symbol ∀ is dependent is both theories: in the expression ∀x : A B, the proposition B may always contain the variable x of type A.

Finally, there is an extra constant π in the Calculus of constructions, with its associated rewrite rule. This symbol permits to type functions mapping proofs to terms, for example a function mapping a proof of ∃x P(x) to a term t verifying the predicate P.

So, the Calculus of constructions is an extension of Simple type theory, because the symbols arrow and ⇒ are dependent and because it includes a symbol π.

Analyzing proofs expressed in the Calculus of constructions

We can define a subset S of the proofs, expressed in the Calculus of constructions, that do not use the dependency of the symbol arrow, do not use the dependency of the symbol ⇒, and do not use the symbol π, where we say that a proof does not use the dependency of the symbol arrow if each time the symbol arrow is used, it is applied to two terms, the second one being a λ -abstraction where the abstracted variable does not occur in the body of the abstraction: (arrow A λ x : (η A) B) with x not free in B, and that it does not use the dependency of the symbol ⇒ if each time the symbol ⇒ is used, it is applied to two terms, the second being a λ -abstraction where the abstracted variable does not occur in the body of the abstraction: (⇒ A λ x : (ε A) B) with x not free in B.

As we shall see, many proofs expressed in the Calculus of constructions are in this subset.

Translating proofs to Simple type theory

When a proof expressed in the Calculus of constructions is in the subset S, it can easily be translated to Simple type theory. All that needs to be done is to replace the terms of the form (arrow A λ x : (η A) B) with (arrow A B) and the terms of the form (⇒ A λ x :

(ε A) B) with (⇒ A B).
If, in contrast a proof is not in the set S, then it genuinely uses a feature of the Calculus of constructions that does not exist in Simple type theory and it cannot be expressed in Simple type theory. In the same way a proof expressed in ZFC, that genuinely uses the axiom of choice, cannot be expressed in ZF.

When a proof, expressed in the Calculus of constructions, is an element of the set S and is translated to Simple type theory, we say that the proof and its translation are the same mathematical proof, expressed in different theories, although they are different linguistic objects. Generalizing this notion of identity of proofs across theories remains to be done.

An arithmetic library

The example of the translation of proofs from the Calculus of constructions to Simple type theory is a toy example, because there is no implementation of the Calculus of constructions per se. The systems COQ and MATITA, for example, implement extensions of the Calculus of constructions with various features, at least inductive types and universes.

M. Boespflug and G. Burel [START_REF] Boespflug | CoqInE : Translating the Calculus of Inductive Constructions into the lambda-Pi-calculus modulo[END_REF] have shown how to extend the theory presented in Figure 2 to inductive types and A. Assaf [START_REF] Assaf | A Calculus of Constructions with explicit subtyping[END_REF][START_REF] Assaf | A framework for defining computational higher-order logics[END_REF] has shown how to extend it to universes. This has permitted to express a large library of MATITA proofs in DEDUKTI, including a proof of Fermat's little theorem.

F. Thiré [START_REF] Thiré | [END_REF] has then shown that the symbol π, and the dependency of the symbols arrow and ⇒ could be eliminated from this library, but also that universes could be eliminated and that inductive type could be replaced by a very simple principle: an induction principle on natural numbers, that permits to prove propositions by induction and to define functions by induction.

So, we now have an evidence that Fermat's little theorem not only has a proof in the Calculus of inductive constructions with universes, but also in constructive Simple type theory. Such a result was expected, but note that neither proving Fermat's little theorem in MATITA, that contains dependent products, inductive types, universes, etc. nor proving it in HOL LIGHT, that contains the excluded middle, extensionality, choice, etc., provides a proof in such a weak theory.

On the more practical side, this has permited to export this library from DEDUKTI to HOL LIGHT, ISABELLE/HOL, HOL4, COQ, etc. [START_REF] Thiré | Sharing Arithmetic Proofs from Dedukti to HOL[END_REF], HOL LIGHT, ISABELLE/HOL, and HOL4 sharing a common input language: OPENTHEORY [START_REF] Hurd | The OpenTheory standard theory library[END_REF].

The size of this library is 1.5 Mo. It contains around 340 lemmas. It is checked in DEDUKTI in a few milliseconds.

5 Abstracting enough

Natural numbers

Both in the Calculus of inductive constructions and in Simple type theory, it is possible to prove propositions by induction and to define functions by induction. But these principles are justified in different ways.

In the Calculus of inductive constructions, the declaration of the inductive type nat comes with a recursion operator that permits to define functions by induction and, as proofs are functions, this operator permits also to build proofs by induction.

In Simple type theory, in contrast, the set of natural numbers is impredicatively defined as the intersection of all sets containing zero and closed by successor. From this definition, the induction principle can be proved. Then, this induction principle and other properties of natural numbers permit to prove the existence of functions defined by induction [START_REF] Henkin | On Mathematical Induction[END_REF].

These details should be ignored by the arithmetic library, that should be exported to any system that contains a notion of natural number, an induction principle and a way to define functions by induction, regardless the way this induction principle is proved and this induction operator is defined there [START_REF] Thiré | Sharing Arithmetic Proofs from Dedukti to HOL[END_REF]. Using such an abstract definition of the natural numbers, R. Cauderlier and C. Dubois [START_REF] Cauderlier | FoCaLiZe and Dedukti to the Rescue for Proof Interoperability[END_REF] have built a proof of the correctness of Eratosthenes' sieve in the expression of FOCALIZE in DEDUKTI, using definitions coming from COQ and lemmas coming from HOL LIGHT.

Connectives and quantifiers

The same holds for the connectives and quantifiers, that are primitive neither in the Calculus of inductive constructions nor in Simple type theory. They are defined as inductive types in the Calculus of inductive constructions. They are defined from equality in Simple type theory [START_REF] Henkin | A theory of propositional types[END_REF][START_REF] Andrews | A reduction of the axioms for the theory of propositional types[END_REF][START_REF] Andrews | An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof[END_REF].

But these details should be ignored by the library, that only needs to specify that A should be provable when A ∧ B is, etc. regardless the way this connective ∧ is defined.

So, developing a library of proofs that can be exported to different proof systems gives a formal counterpart to the slogan that defining real numbers with Cauchy's construction or with Dedekind's is immaterial, or that defining complex numbers as ordered pairs of real numbers, as similarities, or as classes of polynomials is immaterial. Here, the notions of structure and isomorphic structures are essential, even when all the structures of a class-such as that of the complete Archimedean totally ordered fields-are isomorphic.

Eventually, this should lead to defining algorithms to transform proofs of structural propositions, about objects in a given structure to proofs about objects in an isomorphic structure [START_REF] Huffman | Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL[END_REF][START_REF] Zimmermann | Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant[END_REF].

Classical and constructive logics

An important difference between logics, and proof systems implementing these logics, is that some of them are classical and others are constructive, that is the excluded middle A ∨ ¬A is provable in some but not in others. For example, Simple type theory, and HOL LIGHT, are classical and the Calculus of inductive constructions, and MATITA, are constructive.

A logical framework, such as the λ Π-calculus modulo theory, and its implementation DEDUKTI, should not make any choice on the excluded middle, but should be able to express both classical and constructive logics as theories. A possibility is to not assume the excluded middle in the framework and include it as an axiom in the definition of some theories. Then, the proofs of Simple type theory, for instance those developed in the system HOL LIGHT, can be expressed in DEDUKTI using the excluded middle and just like in Section 3, we can analyze which of these proofs use the excluded middle and which do not, and translate these to another theory: constructive Simple type theory.

An alternative is to use the idea, defended for example in [START_REF] Girard | On the Unity of Logic[END_REF][START_REF] Prawitz | Classical versus intuitionistic logic[END_REF][START_REF] Dowek | On the definition of the classical connectives and quantifiers[END_REF][START_REF] Pereira | [END_REF], that the excluded middle is not a question of theory, but a question of meaning of the connectives and quantifiers. This leads to introduce two existential quantifiers: the constructive, ∃, and the classical, ∃ c , two disjunctions, etc. and deduction rules defining the meaning of these connectives and quantifiers, in such a way that A ∨ ¬A is not provable, but A ∨ c ¬ c A is.

This permits to define connectives and quantifiers once for all in the framework and to use various quantifiers in various theories, as well as translating proofs using one set of quantifiers into proofs using another [START_REF] Gilbert | Automated Constructivization of Proofs[END_REF][START_REF] Cauderlier | A Rewrite System for Proof Constructivization[END_REF], changing, in this case, the statement of the theorem.

Future work

The arithmetic library, described in Section 4, is, of course, only the beginning of a library of proofs, that could be shared by various proof systems. Each proof in this library should be labeled with the ingredients it uses, hence the systems to which it may be exported.

Also, we now have a formal proof of Fermat's little theorem, in constructive Simple type theory, but we should continue to transform it, to express it in weaker theories, such as predicative type theory, Heyting arithmetic, and beyond.

Figure 2 :

 2 Figure 2: The Calculus of constructions

Acknowledgments

Many thanks to Catherine Dubois, Stéphane Graham-Lengrand, Bruno Woltzenlogel Paleo, and Franc ¸ois Thiré for very useful remarks on a first draft of this paper.