Raphaël Bleuse
email: raphael.bleuse@uni.lu

Konstantinos Dogeas

Giorgio Lucarelli

Grégory Mounié

Denis Trystram

Interference-Aware Scheduling using Geometric Constraints

The large scale parallel and distributed platforms produce a continuously increasing amount of data which have to be stored, exchanged and used by various jobs allocated on dierent nodes of the platform. The management of this huge communication demand is crucial for the performance of the system. Meanwhile, we have to deal with more interferences as the trend is to use a single all-purpose interconnection network. In this paper, we consider two dierent types of communications: the ows induced by data exchanges during computations and the ows related to Input/Output operations. We propose a general model for interference-aware scheduling, where explicit communications are replaced by external topological constraints. Specically, we limit the interferences of both communication types by adding geometric constraints on the allocation of jobs into machines. The proposed constraints reduce implicitly the data movements by restricting the set of possible allocations for each job. We present this methodology on the case study of simple network topologies, namely the line and the ring. We propose theoretical lower and upper bounds under dierent assumptions with respect to the platform and jobs characteristics. The obtained results illustrate well the diculty of the problem even on simple topologies.

Introduction

In High Performance Computing, the demand for computational power is steadily increasing [START_REF] Strohmaier | Topology-Aware Data Aggregation for Intensive I/O on Large-Scale Supercomputers[END_REF]. To meet up with the challenge of greater performance the architecture of supercomputers also grows in complexity at the whole machine scale. This complexity arises from various factors: i) the size of the machines (supercomputers now integrates millions of cores); ii) the heterogeneity of the resources (various architectures of computing nodes, nodes dedicated to I/O); iii) the interconnection topology. The evolution in the interconnection networks faces two main challenges: rst, the community is proposing new topologies [START_REF] Kathareios | Cost-Eective Diameter-Two Topologies: Analysis and Evaluation[END_REF]; and second, the interconnection network is now unique within the machine (the network is shared for various mixed data ows). Sharing such a single multi-purpose interconnection network creates complex interactions (e.g., network contention) between running applications, which have a strong impact on their performance [START_REF] Bhatele | There Goes the Neighborhood: Performance Degradation due to Nearby Jobs[END_REF][START_REF] Enos | Topology-Aware Job Scheduling Strategies for Torus Networks[END_REF], and limits the understanding of the system by the users [START_REF] Chen | Considering Time in Designing Large-Scale Systems for Scientic Computing[END_REF]. As the volume of processed data increases, so does the impact of the network.

In this work, we introduce a generic framework for interference-aware scheduling. More precisely, we identify two main types of interleaved ows: the ows induced by data exchanges for computations and the ows related to I/O. Rather than explicitly taking into account these network ows, we address the issue of harmful interactions by constraining the shape of the allocations. Such an approach aims at taking into account the structure of the new platforms in a qualitative way that is more likely to scale properly. The scheduling problem is then dened as an optimization problem with the platform (nodes and topology) and the jobs' description as input. The objective is to minimize the maximum completion time while enforcing constraints on the allocations.

Problem Setting

In this work, we model a platform as a set V of m nodes divided in two groups: a set V C of m C nodes dedicated to computations, and a set V I/O of m I/O nodes that are entry points to a high performance le system. As a consequence, we have m = m C + m I/O . We assume that the I/O nodes are exclusively used for communications with the le system and hence, there is no overlap between computing and I/O nodes, i.e., V I/O ∩ V C = ∅. Moreover, a computing or an I/O node is exclusively allocated to a job for its lifespan, i.e., any node cannot be used at the same time by more than one job.

The nodes can communicate using an interconnection network with a given topology, while the localization of every node within the topology is known. In this direction, we study here the instantiation of this framework with unidimensional topologies, namely the line (Figure 1(a)) and the ring (Figure 1(b)). Studying topologies of one dimension is a rst step towards the more complicated state-of-the-art platforms, while these basic topologies provide lower bounds for the later ones. The line may indeed be seen as a degenerate tree. Fat-tree topologies are a common interconnect, and are for example used in the Curie and Oakforest-PACS platforms. On the other hand, the torus topologies, such as the one of Blue Waters and Titan (3D torus) or the K computer (6D torus), may be studied from the ring with classical embedding techniques.

Batch schedulers are a critical part of the software stack managing HPC platforms: their goal is to eciently allocate resources (nodes from V in our case) to the jobs submitted by the users of the platform. The jobs are queued in a set J . The total number of jobs is n. Each job j requires q j computing nodes and one I/O node. We distinguish two cases with respect to I/O requirements: in the pinned model each job asks for a specic I/O node, while in the unpinned model the jobs just need any arbitrary I/O node. The number of allocated computing nodes is xed, i.e., the job is rigid [START_REF] Dror | Theory and Practice in Parallel Job Scheduling[END_REF]. We denote by V(j) the set of nodes allocated to the job j. If needed, we use V C (j) and V I/O (j) to distinguish among the computing and the I/O nodes assigned in j, respectively. Each job j requires a certain time p j to be processed, and it is independent of every other job. Once a job starts being executed, it runs until completion, i.e., it is not preemptive.

As stated above, the goal of this paper is not to nely model the full context of execution. Instead, we propose to model the platform in such a way that (a) Line topology. the network interactions are implicitly taken into account. In this direction, we augment the scheduling problem with geometric constraints on the allocations of the jobs in the resources based on the platform topology and the application requirements. Before presenting these constraints, we need to precisely dene the network ows we target. We distinguish two types of ows, directly deriving from the fact that we are dealing with two kinds of nodes: computational communications which are induced by data exchanges during computations. Such communications occur between two computing nodes allocated to the same application. I/O communications which are induced by data exchanges between computing and I/O nodes. Such communications occur when computing nodes read input data, checkpoint the state of the application, or save output results.

In order to avoid computational communication interactions, we consider the following constraint. Denition 1 (Contiguity [START_REF] Bª¡dek | On contiguous and non-contiguous parallel task scheduling[END_REF][START_REF] Lucarelli | Contiguity and Locality in Backlling Scheduling[END_REF]) An allocation is said to be contiguous if and only if the nodes of the allocation form a contiguous range with respect to the nodes' ordering.

Note that the contiguity constraint relies on the nodes' ordering. For topologies such as lines or rings this ordering is natural (see Fig. 1).

The contiguity constraint is well suited to take into account the computational communications, but not the I/O communications. Indeed, the former type of communications may occur between any pair of computing nodes within an allocation: we usually describe this pattern as all-to-all communication. On the other hand, I/O communications generate trac towards few identied nodes in an all-to-one or one-to-all pattern. Hence, we propose the locality constraint, whose goal is to limit the impact of the I/O ows to the periphery of the job allocations. We must emphasize that the locality constraint proposed here is not related to the locality constraint described in [START_REF] Lucarelli | Contiguity and Locality in Backlling Scheduling[END_REF]. Denition 2 (Locality) A given allocation for a job j is said to be local i it is contiguous, and the I/O node V I/O (j) is adjacent to computing nodes from V C (j), with respect to the underlying topology.

In this paper, we are interested in minimizing the maximum completion time among all jobs (i.e., the makespan of the schedule) while enforcing the contiguity and the locality constraints. Specically, we aim at developing algorithms with performance guarantees by adding geometric constraints on the allocations of jobs into nodes.

Related Work

Most actual implementations of schedulers allocate resources greedily without any topological constraint in the allocation of the computing nodes. However, this naive solution has a bad impact on performances [START_REF] Enos | Topology-Aware Job Scheduling Strategies for Torus Networks[END_REF]. Constraining the allocations to enhance performance is however not a new idea. For example, Lucarelli et al. studied the impact of enforcing contiguity or locality in backlling scheduling [START_REF] Lucarelli | Contiguity and Locality in Backlling Scheduling[END_REF] (for fat trees). They showed that enforcing these constraints can be done at a small cost, and has minimum negative impact on usual metrics such as makespan, ow-time, or stretch.

Tackling the interactions arising from the context of execution, or, more specically, network contention, can be done either by preventing these interactions from happening or by mitigating them. Still, the approaches discussed above require some knowledge about the application communication patterns (either compute or I/O communications). We review briey related work in the prevention/mitigation of interactions before discussing monitoring techniques.

Interactions Prevention. Some steps have been taken towards integrating more knowledge about the communication patterns of applications into batch schedulers. For instance, Georgiou et al. studied the integration of TreeMatch into SLURM [START_REF] Georgiou | Topology-aware Resource Management for HPC Applications[END_REF]. Given the communication matrix of an application, the scheduler minimizes the load of the network links by smartly mapping the application's processes on the resources. This approach however does not consider the temporality of communications. Targeting the mesh/torus topologies, the works of Tuncer et al. [START_REF] Tuncer | PaCMap: Topology Mapping of Unstructured Communication Patterns onto Non-contiguous Allocations[END_REF] and Pascual et al. [START_REF] Antonio Pascual | Applicationaware metrics for partition selection in cube-shaped topologies[END_REF] are noteworthy. Another way to prevent interactions is to force the scheduler to use only certain allocation shapes with good properties: this strategy has been implemented in the Blue Waters scheduler [START_REF] Enos | Topology-Aware Job Scheduling Strategies for Torus Networks[END_REF]. The administrators of Blue Waters let the scheduler pick a shape among 460 precomputed cuboids. Yet, the works proposed above only target compute communications. HPC applications usually rely on highly tuned libraries such as MPI-IO, parallel netCDF or HDF5 to perform their I/O. Tessier et al. propose to integrate topology awareness into these libraries [17]. They show that performing data aggregation while considering the topology allow to diminish the bandwidth required to perform I/O. Interactions Mitigation. Given a set of applications, Gainaru et al. propose to schedule I/O ows of concurrent applications [START_REF] Gainaru | Scheduling the I/O of HPC Applications Under Congestion[END_REF]. Their work aim at mitigating I/O congestion once applications have been allocated computation resources. To achieve such a goal, their algorithm relies on past I/O patterns of the applications to either maximize the global system utilization, or minimize the maximum slowdown induced by sharing bandwidth.

Application/Platform Instrumentation. A lot of eort have been put into developing tools to better understand the behavior of HPC applications. Characterizing I/O patterns is key as it allows the developers to identify performance bottlenecks, and allows the system administrator to better congure the platforms. A complementary path is to predict I/O performances during execution [START_REF] Dorier | Using Formal Grammars to Predict I/O Behaviors in HPC: The Omnisc'IO Approach[END_REF]. Such instrumentation eorts allow for a better use of the scarce communication resources. However, as they are application-centric, they fail to capture interapplication interactions. Monitoring of the platform is a way of getting insight on the inter-application interactions. We will not address this problem here.

Pinned I/O

In this section, we study the problem with respect to the pinned I/O model, according to which each job requests a specic I/O node. Such a model is representative of HPC platforms where the parallel le system is organized in stripes. For example, this is the case with the conguration of the Lustre le system in Blue Waters, where each I/O node is responsible for an address range (i.e., a stripe). Then, the jobs will request the I/O node corresponding to their data.

Complexity

We start by proving that the studied problem is NP-complete even in the special case where all jobs require unit processing time to be executed, while the platform contains only three I/O nodes. Theorem 1. The problem of scheduling in the pinned model with respect to contiguity and locality constraints is strongly NP-complete even in line topologies, with m I/O = 3 and p j = 1 for each job j ∈ J .

Proof. The problem clearly belongs to NP. We give a reduction from a special case of the Numerical 3-Dimensional Matching (N3DM) problem [START_REF] Randolph | Computers and Intractability: A Guide to the Theory of NP-Completeness[END_REF]. An instance of the classical N3DM problem consists of three disjoint sets W , X and Y , each containing M positive integers, and a bound B ∈ Z + . The objective is to decide whether W ∪X ∪Y can be partitioned into M disjoint sets A 1 , A 2 , . . . , A M such that each A i contains exactly one element from each of W , X, and Y and a∈Ai a = B, for 1 ≤ i ≤ M . Consider now SN3DM be the special case of N3DM in which all integers that belong to the set X are at least B 2 . It is not hard to see that SN3DM is also strongly NP-complete. Indeed, it suces to transform an instance of N3DM to an instance of SN3DM by setting W = W , Y = Y , X = {x + B : ∀x ∈ X} and B = 2B. Then, any solution for N3DM corresponds to a solution for SN3DM, and vice versa.

We propose now a transformation from SN3DM to our problem as follows:

m C = B, m I/O = 3;
the topology is a line starting with an I/O node, followed by B 2 computing nodes, an I/O node, B 2 computing nodes, and nishing with a third I/O node; for each a ∈ W ∪ X ∪ Y , we create a job j with q j = a, and p j = 1. All jobs derived from sets W , X, and Y target the rst, second, and third I/O node, respectively.

With respect to the ordering of the line topology, we refer to the computing nodes as 1, 2, . . . , m C and to the I/O nodes as 1, 2, . . . , m I/O .

We will prove that a solution to SN3DM exists if and only if there is a schedule that satises all constraints and has a makespan at most M .

Assume that there is a solution for SN3DM. Then for each set A i , 1 ≤ i ≤ M , we schedule the three jobs j 1 ∈ W , j 2 ∈ X and j 3 ∈ Y corresponding to this set at time interval (i -1, i]. Specically, j 1 will use the computing nodes 1, . . . , q j1 , j 2 the computing nodes q j1 + 1, . . . , q j1 + q j2 and j 3 the computing nodes q j1 + q j2 + 1, . . . , m C . Note that each of these three jobs is adjacent to the targeted I/O node. Indeed, the j 1 and j 3 are adjacent to the leftmost and the rightmost I/O node, respectively, while j 2 is always adjacent to the middle I/O node, since q j2 ≥ B 2 . The makespan of the created schedule is equal to M . Assume now that there exists a schedule of makespan at most M . As the total work is M • B, no computing node is idle during the time interval (0, M ]. Hence, the partition is directly derived by assigning jobs that start at time i -

1 to A i , 1 ≤ i ≤ M .

Approximation Algorithm

In this section, we rst propose a constant-factor approximation algorithm for line topologies and then we argue that it can be used even for ring topologies. The main idea of our algorithm is to rst determine an allocation of each job to a specic set of computing nodes. We are interested in allocations that are simultaneously contiguous and local, while each job j requires a specic I/O node. As a consequence, there exist at most q j + 1 = O(m C ) valid allocations for each job j (see Fig. 2). Given an allocation of all jobs to computing nodes, our problem coincides with the well-studied Dynamic Storage Allocation (DSA) problem [START_REF] Gergov | Algorithms for Compile-Time Memory Optimization[END_REF]. Then, we use a known approximation algorithm for the latter problem. In order to decide the allocation of computing nodes we use an integer linear program. Let A j be the set of all potential allocations for each job j, where |A j | ≤ q j + 1. Each allocation a ∈ A j contains exactly q j computing nodes as well as the required I/O node. Note that, an allocation may include more I/O nodes that will not be used during the execution of j neither by j nor by the other jobs due to the locality constraint. For example, in Fig. 2 the two rightmost allocations also cover the third I/O node in order to be able to include q j = 3 computing nodes. For each job j ∈ J and allocation a ∈ A j , we introduce a binary indicator variable x j,a which is equal to one if j is executed according to the allocation a, and zero otherwise. Moreover, for each node i ∈ V we introduce a non-negative variable L i which corresponds to the total load of jobs whose assigned allocation includes i. Finally, let Λ be the maximum load among all nodes. Then, we propose the following integer linear program which searches for the allocations that minimize the total load. minimize Λ (ILP)

Λ ≥ L i ∀i ∈ V (1)
L i ≥ j∈J a∈Aj i∈a
x j,a p j ∀i ∈ V

(2) a∈Aj x j,a = 1 ∀j ∈ J

(3)

x j,a ∈ {0, 1} ∀j ∈ J , a ∈ A j (4)
Constraints (2) compute the total load for each node, while Constraints (3) ensure that each job is assigned an allocation. By relaxing the integrity Constraints (4), we can solve the corresponding linear program in polynomial time. Note that there are O(mn) variables and O(m + n) constraints. Moreover, an optimal solution to the above integer linear program is a lower bound to the makespan of an optimal solution for our problem, since it optimizes the maximum load without handling intersections of jobs in time, that is the scheduling phase.

Let Λ, Li and xj,a denote the values of the variables in an optimal solution of the relaxed linear program. Then, the solution of this linear program is rounded to an integral feasible solution whose variables are denoted by Λ, Li and xj,a . Specically, we round the indicator variables independently for each job j ∈ J as follows: consider all possible allocations for the job j ordered with respect to the processors' ordering. The allocation chosen for j is the one with the smallest index k such that k a=1 xj,a ≥ 1 2 . Then, we set xj,k = 1 and xj,a = 0 for all a = k. Figure 3 gives an example of this rounding procedure.

The following lemma provides an upper bound to the integral solution Λ obtained after the rounding procedure.

Lemma 1. Λ ≤ 2 Λ.
Proof. Consider a job j and let k j be the index of the allocation of j in the rounded solution, i.e., xj,kj = 1. Moreover, let V(j) be the set of nodes (both computing and I/O) that are included in this allocation. We will rst prove the following statement:

a∈Aj : i∈a xj,a ≥ 1 2
for every i ∈ k j For example, in Fig. 3 we have that k j = 3 and for each i ∈ {3, . . . , 7} the sum of the fractional variables that correspond to j and include i is at least 0.5. In order to prove the statement, let k j = {i , . . . , i r } be the set of nodes of the allocation k j as these are ordered in the natural way. Recall that V I/O (j) ∈ k j is the I/O node required by j and assume that V I/O (j) coincides with i * , where i ≤ i * ≤ i r . By the denition of k j , the statement is true for i = i . Moreover, the statement holds for each node i ∈ {i , . . . , i * } since

a∈Aj : i∈a xj,a ≥ a∈Aj : i ∈a xj,a ≥ 1 2
It remains to prove it for i ∈ {i * + 1, . . . , i r }. We focus rst on i r . Observe that by the denition of k j it holds that kj -1 a=1 xj,a < 1 2 . Then, we have that

a∈Aj : ir∈a xj,a = a∈Aj xj,a - kj -1 a=1 xj,a > 1 - 1 2 = 1 2
Finally, the statement holds for each node i ∈ {i * + 1, . . . , i r } since

a∈Aj : i∈a xj,a ≥ a∈Aj : ir∈a xj,a ≥ 1 2
In order to nalize the proof of the lemma, consider the load Li of a node i in the rounded solution. We have that

Li = j∈J p j • 1 {if i∈kj } = j∈J p j a∈Aj : i∈a xj,a ≤ j∈J p j 2 a∈Aj : i∈a xj,a
where the last inequality holds by the proven statement and since by Constraint (3) we have that a∈Aj : i∈a xj,a ≤ 1. Hence,

Li ≤ 2 j∈J p j a∈Aj : i∈a xj,a = 2 j∈J p j a∈Aj i∈a xj,a = 2 j∈J a∈Aj i∈a xj,a p j = 2 Li
The lemma follows by considering the node of maximum load in the rounded solution, i.e., Λ = max

i { Li } ≤ 2 max i { Li } = 2 Λ.
As mentioned before, given the allocations of all jobs, our problem coincides with the DSA problem [START_REF] Gergov | Algorithms for Compile-Time Memory Optimization[END_REF]. An instance of the DSA problem consists of a set of n triples. Each triple ( j , r j , s j ) corresponds to a rectangle parallel to x-axis of size (r jj ) × s j . Specically, j and r j are the projections of its leftmost and rightmost points, respectively, in the x-axis while s j is its size projected in the y-axis. In other words, the position of the rectangle is xed with respect to x-axis, but it can be shifted in any position in y-axis. The objective is to pack all rectangles without intersections in a strip of minimum height.

In our scheduling context, each job corresponds to a rectangle whose j and r j values are dened by a given allocation as the leftmost and the rightmost computing nodes respectively, while p j = s j . Moreover, the makespan coincides with the height of the strip.

Gergov [START_REF] Gergov | Algorithms for Compile-Time Memory Optimization[END_REF] presented a greedy 3-approximation algorithm for the DSA problem. The important property of this algorithm is that it uses as lower bound the maximum load over all x-coordinates, which allows as to use it in our analysis. The following theorem describes this property in scheduling terms. Theorem 2. [START_REF] Gergov | Algorithms for Compile-Time Memory Optimization[END_REF] There is an algorithm which computes a feasible schedule whose makespan is at most three times the maximum load of every node.

Due to the equivalence of our problem with DSA, we can apply the algorithm mentioned in Theorem 2 and get a nal solution to our problem. A high-level description of the above described procedure is given in Algorithm 1. Proof. Consider a schedule created by Algorithm 1 and let C max be the makespan of this schedule. Due to the allocation phase, we know that the maximum load over all nodes is equal to Λ. Then, by Theorem 2 and Lemma 1, we have that

C max ≤ 3 Λ ≤ 6 Λ.
Hence, the theorem follows by the fact that the optimal solution to (ILP) is a lower bound to the optimal solution for our problem.

We observe that Gergov's algorithm remains a 3-approximation even in the case of rings. Moreover, the allocation procedure based on the rounding of (ILP) can be also applied for rings; we just need to dene an ordering of the possible allocations of each job. Thus, by considering an clockwise ordering, we can apply Algorithm 1 and get the following theorem. Theorem 4. Algorithm 1 achieves an approximation ratio of 6 for the ring topology in the pinned I/O model.

In this section, we study the unpinned I/O model according to which each job requires any arbitrary I/O node.

Complexity

We start by proving that the studied problem is NP-complete even in the special case where all jobs require unit processing time to be executed, while the platform contains only three I/O nodes. The proof is similar with the proof of Theorem 1 with the dierence that the reduction is done by the classical 3-Partition problem [START_REF] Randolph | Computers and Intractability: A Guide to the Theory of NP-Completeness[END_REF]. For this reason, it is omitted. Theorem 5. The problem of scheduling in the unpinned model with respect to contiguity and locality constraints is strongly NP-complete even in line topologies, with m I/O = 3 and p j = 1 for each job j ∈ J .

An Approximation Algorithm for Equidistant I/O Nodes

In this section, we consider both line and ring topologies and we propose an approximation algorithm in the case where the I/O nodes are uniformly distributed. In other words, the I/O nodes are equidistant from each other. We denote by δ the distance separating two consecutive I/O nodes. Note that, given any instance, in line topologies δ can be either m C m I/O or m C m I/O while the rst value is always the case in ring topologies.

We need some additional notation. We call a job small if it requires fewer computing nodes than the distance between two consecutive I/O nodes, i.e., q C j < δ. In a similar way, we call a job big if q C j ≥ δ. Let J ≤δ and J ≥δ be the sets of small and big jobs, respectively. Our algorithm handles these sets separately.

A small job cannot be adjacent to more than one I/O nodes in any feasible schedule. Moreover, an I/O node along with δ consecutive computing nodes adjacent to it can be considered as a processing unit that can execute a small job. Based on this, we partition the set V C into m C δ groups of consecutive computing units, each one of size at least δ. Assume that these groups as well as the I/O nodes are numbered from left to right and we consider the i-th such group and the i-th I/O node to compose a processing unit. Note that, by the denition of δ, m I/O can be either m C δ or m C δ + 1. In the second case, which can happen only in line topologies, the last I/O node is not used. Then, we can transform our problem for small jobs to an instance of the classical P || C max problem with m C δ machines [START_REF] Hochbaum | Using Dual Approximation Algorithms for Scheduling Problems: Theoretical and Practical Results[END_REF]. Specically, each machine corresponds to one processing unit, while each small job has a processing time as in the initial instance and requires only one processing unit. Then, we solve the created instance of P || C max by using any known approximation algorithm for it. The following lemma, whose proof is omitted, summarizes the above procedure. The additional 2-factor in the line case is due to parity issues. Lemma 2. Any ρ 1 -approximation algorithm for the P || C max scheduling problem, can be used to obtain a 2ρ 1 -approximation algorithm to schedule small jobs in a line and a ρ 1 -approximation algorithm to schedule small jobs in a ring.

Due to the contiguity constraint, the big jobs are structurally guaranteed to be adjacent to at least one I/O node, i.e., we can then ignore the existence of I/O nodes when scheduling big jobs. Hence, the objective is to pack the big jobs and our problem reduces to the strip-packing problem [START_REF] Kenyon | Approximate strip packing[END_REF]. The following lemma, whose proof is omitted, summarizes the above reduction. The additional 2-factor in the ring case is due to the degeneration of the ring to a line. Lemma 3. Any ρ 2 -approximation algorithm for the strip-packing problem, can be used to obtain a ρ 2 -approximation algorithm to schedule big jobs in a line and a 2ρ 2 -approximation algorithm to schedule big jobs in a ring.

By combining Lemmas 2 and 3 the following theorem follows. Theorem 6. For the unpinned model, there is a (2ρ 1 + ρ 2 )-approximation algorithm for line topologies and a (ρ 1 + 2ρ 2 )-approximation algorithm for ring topologies, where ρ 1 and ρ 2 are the approximation ratios for the P || C max and the strip-packing problems, respectively.

Note that a PTAS exists for both P || C max and strip-packing problems [START_REF] Hochbaum | Using Dual Approximation Algorithms for Scheduling Problems: Theoretical and Practical Results[END_REF][START_REF] Kenyon | Approximate strip packing[END_REF], leading for (3 + )-approximation algorithms for line and ring topologies.

Conclusions

We studied the makespan minimization problem on line and ring topologies, when the allocations are constrained to be both contiguous and local. We proved that both the pinned and unpinned models are NP-complete and we presented constant-factor approximation algorithms for them. The proposed algorithms can be also applied in dierent settings (the proofs will be developed in an extended version of this work). For example, in the case where the I/O nodes can be shared by more than one jobs, then the 6-approximation algorithm of Section 4.2 can be simply adapted by excluding the requested I/O node from the allocation of the job in the denition of the indicator variables of (ILP). Note that due to the locality constraint an I/O node cannot be shared by more than two jobs. Another example is the case where each job requires more than one I/O nodes. However, this assumption in conjunction with the locality constraint could lead to several unused nodes, limiting its interest.

As future steps, one could implement the proposed algorithms, and study their performances through simulation. From a theoretical point of view, the tightness results show the limits of the two-phase approach in Section 4.2. The approximation ratios might be improved by scheduling the problem in a single phase. Finally, the study of more enhanced topologies, like two-dimensional ones, is a very interesting direction. In this case, contiguity could be replaced by more general constraints implying the convexity of the shape of the allocations.

Fig. 1 .

 1 Fig. 1. Example of platforms with unidimensional topologies. The nodes are numbered using the natural order. White nodes represent computing nodes, and black nodes represent I/O nodes.

Fig. 2 .

 2 Fig. 2. Potential allocations for a job j requesting the middle I/O node with qj = 3.

Fig. 3 .

 3 Fig. 3. Rounding procedure for the variables that correspond to job j: xj,3 = 1 and xj,1 = xj,2 = xj,4 = xj,5 = 0.

Algorithm 1 : 1 3 Find 2 4

 1132 Solve the relaxed version of (ILP) 2 for each job j ∈ J do the smallest index k such that k a=1 xj,a ≥ 1 Set xj,k = 1 and xj,a = 0 for all a = k 5 Create a feasible schedule by applying the algorithm proposed in Theorem 2 using the allocations determined by the xj,a variables Theorem 3. Algorithm 1 achieves an approximation ratio of 6 for the line topology in the pinned I/O model.


Matthieu Journault

Antoine Miné

Abdelraouf Ouadjaout

Modular static analysis of string manipulations in C programs

We present a modular analysis able to tackle out-of-bounds accesses in C strings. This analyzer is modular in the sense that it infers and tabulates (for reuse) input/output relations, automatically partitioned according to the shape of the input state. We show how the inter-procedural iterator discovers and generalizes contracts in order to improve their reusability for further analysis. This analyzer was implemented and was able to successfully analyze and infer relational contracts for functions such as strcpy, strcat.

analyzer, that manipulates predicates and can perform modular analysis, upon an existing analyzer able to deal with low level features of C.

An analyzer computing invariants by induction on the syntax of programs requires abstract transformers for function calls. A straightforward way to achieve this, provided that there is no recursivity, is to analyze the body of the function at each call site. Therefore a way to improve scalability is to design modular analyzers able to reuse previous analysis results so that reanalysis is not always needed (as emphasized in [START_REF] Cousot | Modular static program analysis[END_REF]). As an example, in a project containing an incrementation function, we want to be able to express and to infer that ∀x, incr(x) = x + 1. Once this relation discovered, no further analysis of the body of incr is required. Abstract interpretation is always sound and inferred invariants describe an overapproximation of the reachable set of states. Therefore the use of input/output relations discovered on statements must yield an over-approximation. Nonetheless we do not want to give up too much precision to achieve scalability. This was done by using classical techniques to express input/output relations on numerical variables as performed in [START_REF] Cousot | Modular static program analysis[END_REF], partitioning these relations according to symbolic conditions in the abstract state as proposed by Bourdoncle [START_REF] Bourdoncle | Abstract interpretation by dynamic partitioning[END_REF], and generalizing them using widening operations.

By mixing the idea of representing a string as its length using a numeric abstraction and input/output relations, our analyzer is able to handle the strcpy example. More precisely, consider that char* p points to some char [START_REF] Cousot | Static determination of dynamic properties of generalized type unions[END_REF] dest string and char* q points to some char [START_REF] Sharma | A new abstraction framework for affine transformers[END_REF] src string with dest = src, furthermore let variables o q , o p denote the initial offset of p and q, variable l src codes for the length of src, and variable a dest denotes the size of the allocated memory of the string pointed to by dest. Our analyzer is able to prove that if l src < a src and l src -o q < a dest -o p then no out of bounds access are performed. Moreover enabling modular analysis would yield that l src = l src and l dest = l src where primed variables (resp. unprimed variables) denote the state at the beginning (resp. at the end) of the analysis of the body of the function. Therefore these two relations state that the length of src was not modified by the call to strcpy, while the length of dest is now that of src.

Outline. Section 2 describes the subset of C we wish to analyze, Sect. 3 defines a low-level C abstraction upon which our analyzer is based, Sect. 4 details the String abstract domain, Sect. 5 outlines the lifting of our analyzer to a modular analysis, Sect. 6 contains a few remarks on the implementation of the analyzer. Finally Sect. 7 gives an overview of related works, while Sect. 8 concludes.

Contributions. The main contributions of this article are : [START_REF] Xavier Allamigeon | Static analysis of string manipulations in critical embedded C programs[END_REF] The development of a static analyzer able to reason on low level C, while performing higher level abstractions (such as the String domain that will be presented thereafter) [START_REF] Balakrishnan | Reps. Recency-abstraction for heap-allocated storage[END_REF] The lifting of this analyzer to a precise modular framework based on numerical input/output relations [START_REF] Cousot | Modular static program analysis[END_REF], partitioning [START_REF] Bourdoncle | Abstract interpretation by dynamic partitioning[END_REF] and input generalizations.

= v = malloc(e) v ∈ V, e ∈ expr | type v v ∈ V | • • • Fig. 1: The syntax of the C--subset of C.

Syntax and concrete semantics

Syntax. We will thereafter call C--the language defined in Figure 1 and denote by V a set of variables. The description of Figure 1 omits some classical statements but make precise some low-level features of the language. Note moreover that int-types are denoted by their signededness (s for signed integers, u for unsigned integers) and their length in bits, instead of char or unsigned long. This transformation is made before the analysis, and depends on the platform. Moreover, in order to simplify the presentation we will consider strings as arrays of u8 (or unsigned char), results can be easily extended to arrays of s8 (char).

Cells. Our C-like language features a rich type system. In a classic way, we will present the semantics of operations on scalar data-types: integers of various size and pointers, and reduce structured data-types, such as arrays, struct and unions, malloced blocks, to collections of scalar objects, we call cells. A simple solution would be to use the type of a structured variable and decompose it statically into such collections; left-values thus become access paths. Unfortunately, this static view does not hold for programs that abuse the type system and access some block of memory with various types, which is possible (and even common) in C using union types and pointer casts. One solution would be to model the memory as arrays of bytes or even bits, and synthesize non-byte access (for instance, reading a 16-bit integer a would be expressed as a[0]+256*a [START_REF] Xavier Allamigeon | Static analysis of string manipulations in critical embedded C programs[END_REF]), but such a complex modeling would put a great strain on numeric abstract domains and cause huge precision losses. We thus rely on previous work [START_REF] Miné | Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics[END_REF], that proposes to model memory blocks as collections of (possibly multi-byte) scalar cells, that are inferred and maintained dynamically during the analysis, according to the memory access pattern effectively employed by the program at run-time. For our purpose, we can assume that all memory accesses have the form * τ e, where τ is a scalar type and e is a pointer expression using pointer arithmetic at the byte level (this reduction can be performed statically as a pre-processing).

Remark 1. In addition to the definitions of Figure 1, we assume that we are given a function typeof ∈ (V → type). The type of a variable is given by its declaration in a C--program. Moreover we assume given a sizeof function from type to N that gives the size in bytes of each type (e.g. sizeof(int) = 4).

A cell denotes an addressable group of bytes to store a scalar value, it is represented by a base variable (V ), an integer coding for the offset of the cell (o), and the type of the cell (t). Therefore we define the following set of cells:

Cell ∆ = { V, o, t | V ∈ V, t ∈ scalar-type, 0 ≤ o ≤ sizeof(typeof(V )) -sizeof(t)}.
By construction Cell represents the set of all addressable memory locations. The abstract states we will build contain a subset of those cells. Cells might denote overlapping portions of the memory. In such cases the underlying state satisfies every constraint implied by a cell : cells are understood conjunctively. Therefore removing cells induces a loss of information. A key aspect of [START_REF] Miné | Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics[END_REF] we reuse is that new cells from Cell are added to the current environment dynamically to account for the access patterns encountered during the analysis, in a flow-sensitive way. As we do not rely on static type information, which can be misleading in C, we can handle union types, type-punning, and untyped allocated blocks transparently.

Concrete semantic. We will not detail here the complete concrete semantic of the C--language, however we give a definition of the set of concrete environments using cells, noted E. An environment is a set of cells C and a function ρ mapping each cell to a value. A value can be either a numerical value or a pointer. A pointer is represented by: the base variable towards which it points and its offset. The set of pointer Ptr is augmented with two special values: the NULL pointer and the invalid pointer :

Ptr ∆ = (V × Z) ∪ {NULL, invalid} E ∆ = C⊆Cell { C, ρ | ρ ∈ R ∆ = C → (N ∪ Ptr)}

Cell abstract domain

Let us consider the Cell abstraction [START_REF] Miné | Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics[END_REF], an abstract domain able to abstract the semantic of C programs manipulating pointers. This abstract domain comes with an abstract interpreter that can successfully analyze C programs with no recursion and no dynamic memory allocation. The abstraction we propose here is built upon the cell abstract domain, it extends this domain so as to handle dynamic allocations and higher level string manipulations.

Pointers bases. When C ⊆ Cell is a set of cells, we define C to be the set of cells denoting pointers :

C ∆ = { V, o, t ∈ C | t = ptr}.
Upon this we define P C = C → ℘(V ∪ {NULL, invalid}). P C represents the possible memory locations pointed to by cells representing pointers (note that P C only accounts for the base variable that is pointed to and not for the offset).

Numerical domain. We assume that for any set of variables V we are given a numerical domain N V abstracting ℘(V → N) with concretization function γ V ∈ N V → ℘(V → N). For example we can use the polyhedra domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] or the interval domain [START_REF] Cousot | Static determination of dynamic properties of generalized type unions[END_REF]. These domains come with an environment change operator |V such that: ∀V , if S ∈ N V then S |V ∈ N V . S |V is obtained by removing all variables not in V and adding all variables in V but not in V (with unconstrained value), so that the result is defined exactly over the variable set V. Furthermore we assume given a function range(x, S V ), yielding an interval of N containing all concrete values associated to variable x in N V . For any subset C ⊆ Cell we can therefore rely on a numerical abstraction N C abstracting ℘(C → N). We give the numerical domain of our abstraction a double role:

-For a cell containing a pointer, the variable (from the numerical domain) assigned to this cell codes for possible offsets of the pointer (thus paired with information from P C we will describe completely the pointer contained in the cell) -For other cells (containing e.g. a u8, a s32) the variable (from the numerical domain) codes for values contained in the cell.

Abstract states. We define the domain D m with concretization γ m ∈ D m → E as:

D m ∆ = { C, R , P | C ⊆ Cell, R ∈ N C , P ∈ P C } γ m C, R , P ∆ = C, {ρ ∈ R, ∃ρ ∈ γ C (R ), ∀c = V, o, t ∈ C,    ρ (c) = ρ(c) if t = ptr ρ (c) = p, ρ(c) if t = ptr ∧ p ∈ P (c) ∩ V ρ (c) = p if t = ptr ∧ p ∈ P (c) \ V } Example 1.
Consider the abstract state: S = { a, 0, u64 }, { a, 0, u64 = 2 32 + 2}, ∅ . Moreover we assume that due to some cast operations, cells { a, 0, u32 } and { a, 4, u32 } are needed (imagine for example the encoding in little-endian of a pair of u32 as a u64). S is equivalent to: { a, 0, u64 , a, 0, u32 , a, 4, u32 }, { a, 0, u64 = 2 32 + 2, a, 0, u32 = 2 (= (2 32 + 2) mod 2 32 )), a, 4, u32 = 1 (= (2 32 + 2) /2 32 )}, ∅ .

1 int a = 1; 2 int p = & a ; 3 * p = * p + 1;

Program 1.2: Dereferencing

Abstract operators and abstract transformers. Abstract operators (join, meet, widening) are defined by first unifying the operands, and then performing the operation in the underlying unified numerical domain and pointer map. The unification operator transforms two abstract elements into abstract elements with the same set of cells. This is done by adding cells in both elements so that the resulting set of cells in both elements is the union of the initial sets of cells. We do not give here the definition of all the abstract transformers operating on our abstract states, however the following example emphasizes how an abstract state is modified by expressions and statements of the C language. In particular, we note that when cells are available, most expressions are treated as expressions on a language where cells are the variables. When cells mentioned in the expressions are not available, they are added to the set of cells of the abstract state, by collecting information available in the overlapping cells, such as joining two byte-cells to synthesize the initial value of a new u16-cell at the same position.

Example 2. Consider Program 1.2, starting from = ∅, ∅, ∅ . The first statement requires the existence of the cell a = a, 0, s32 . The set of cells constrained by our abstract state is dynamically updated to mention a, yielding: {a}, ∅, ∅ , then we rewrite the statement in the following manner: a = 1. We execute this statement in the underlying numerical domain, and get: {a}, {a = 1}, ∅ .

The second statement adds a new cell p = p, 0, ptr and an element to the pointer map: {a, p}, {a = 1, p = 0}, {p → {a}} . Note that p = 0 codes for the value of the offset of pointer p. Finally the expression *p of the third statement is evaluated by following the P component of the abstract state, therefore the statement is transformed into a = a + 1. Thus yielding: {a, p}, {a = 2, p = 0}, {p → {a}} . Henceforth, in order to clarify the presentation, a denotes a, 0, τ when τ is the declared type of variable a.

4 String abstract domain

Domain definition

The introductory example shows that describing a string by a set of cells (one cell per character of the string) was usually not necessary to prove the absence of buffer overrun in string manipulations. Therefore we propose to add to our existing low-level abstraction of C--, an abstraction of strings that sums up all of its characters into two variables, one coding for the length of the string and the other for the allocated size of the buffer in which it is contained. Memory blocks will therefore be abstracted either by the cell abstract domain or by the string abstract domain. In order to simplify the presentation we assume given a set of memory locations V for which we will use a string summary, however this set can be dynamically modified and reductions could be proposed in order to store information on some memory locations in both the String domain and the Cell domain. We assume that for each memory location s ∈ V, we are given two variables denoted s l and s a . Those variables code for the length and the allocated size of the string, they will be added to the numerical domain of the cell abstract domain so that we are able to describe relations between length of variables and offsets of pointers. In the following V denotes s∈V {s a , s l }, this is the set of all numerical variables needed to describe strings in V.

Definition of the String abstract domain. We define the String abstract domain to be:

S m ∆ = { C, R , P | C ⊆ Cell \ { V, , | V ∈ V}, R ∈ N C∪V , P ∈ P C }.
This abstract domain is ordered by the same relation as the cell abstract domain:

S m ∆ = D m .
We recall that Dm will test the inclusion of the two numerical domains once cell sets have been unified, therefore our definition of S S m S amounts to verifying that the constraints on the string variables (s l and s a ) are stronger in the left member of the inequality.

Galois connection with the Cell abstract domain. The String abstract domain is an abstraction of the Cell abstract domain. Indeed we forget information that do not help us track the position of the first '\0' character. We define the Galois connection between the Cell domain and the String domain using two functions : to cell and from cell. The to cell(s, S ) function computes the range of s l in the numeric abstract domain, for each possible length value we set the cells placed before (resp. at) the length to [1; 255] (resp. 0), this yields an abstract element per possible value in the range, those are then joined. Conversely from cell(s, S ) computes the minimum length value (the index of the first cell whose range contains 0), and the maximum length value (the index of the first cell whose range is exactly {0}), finally those constraints are added to the numerical domain. If a string does not contain any '\0' character, we define its length to be the allocated size of the buffer it is contained in. Both functions can be found in Appendix A.1. With V = {s 0 , . . . , s n-1 }, we can define:

γ S m ,D m (S ) = to cell(s 0 , . . . , (to cell(s n-1 , S )) . . . ) α S m ,D m (S ) = from cell(s 0 , . . . , (from cell(s n-1 , S )) . . . ) Example 3. Consider the string abstract elements ∅, {s l = 2, s a = 4}, ∅ when sizeof(type(s)) = 4. We have: γ S m ,D m = { s, 0, u8 , s, 1, u8 , s, 2, u8 }, { s, 2, u8 = 0, s, 0, u8 = 0, s, 1, u8 = 0}, ∅} .
The corresponding concrete state is the set of states in which there is a memory location where the first two bytes are non zero bytes, the third byte is set to zero and the fourth byte is unconstrained.

Remark 2. The interest of the definition of γ S m ,D m and α S m ,D m is twofold: it enables us to define the semantic of the String abstract domain, but we also note that both functions to cell and from cell are computable. Therefore the set of memory locations dealt with by each domain can easily evolve during the analysis. Moreover with γ S m ,D m and α S m ,D m being both computable, we can define a reduction operator between the String abstract domain and the Cell abstract domain. For efficiency reasons we can remove some information from the Cell domain, knowing that information from the String domain can be brought back to the Cell domain. This situation is similar to a reduction between octagons and the, strictly less expressive, interval domain as proposed in [START_REF] Cousot | Combination of abstractions in the astrée static analyzer[END_REF].

Operators and transformers

Operators. As for the definition of the S m operator, the join ( S m ), meet ( S m ) and widening ( S m ) of two abstract elements is defined by applying the according operator in the underlying numerical abstract domain (after the addition on both sides of potentially missing variables and the unification of the set of cells).

Example 4. Consider Program 1.1 of the introductory example where typeof(p) = typeof(q) = u8*, if S 1 = {p, q}, {p = 0, q = 0, src l ≥ 0, src a ≥ src l , dest l ≥ 0, dest a ≥ dest l }, {p → {dest}, q → {src}} is the abstract state from which we start the analysis then S 2 = {p, q}, {p = 1, q = 1, src l ≥ 1, src a ≥ dest l , dest l ≥ 1, dest a ≥ 1, dest a ≥ dest l }, {p → {dest}, q → {src}} is the abstract state after one analysis of the body of the while loop (constraint

≤ o ∧ o < l ∧ o < a [1; 255] at 0 ≤ o ∧ o = l ∧ o < a 0 after 0 ≤ o ∧ o > l ∧ o < a [0; 255] eerror o > a ∨ o < 0 ∅
Fig. 2: Evaluation of a dereferencing.

src a ≥ dest l comes from the fact that we collect error free executions). Therefore our analyzer has to perform the join of those two abstract states before reanalyzing the body of the loop.

S 1 S m S 2 = {p, q}, {p = q, p ≤ 1, p ≥ 0, p ≤ dest l , dest a ≥ dest l , p ≤ src l , p ≤ src a }, {p → {dest}, q → {src}} .
The state transformations induced on our abstract state by the semantic of the C language is mainly dealt with by the Cell abstraction. In order to ease the presentation of the relation between the Cell abstraction and the String abstraction, we add expressions of the form @[v,e] with e ∈ expr and v ∈ V to the C--language. Such expressions denote pointers to variable v, with offset e: ((char *) &v) + e.

Example 5. We want to perform the analysis of the statement

stmt = * u8 t = * u8 (p + * s32 (&u + 2))
(where typeof(p) = typeof(t) = u8*) in the following abstract state: S = {p, u, 2, s32 , t}, R , {p → s , t → s} where R is a numerical abstract state built from the set of constraints we do not need to explicit for this example. The Cell abstraction rewrites stmt into: * u8 @[s,t] = * u8 (@[s ,p + u, 2, s32 ]). The operations that remain to be defined are therefore:

S * τ @[s,e 1 ] = e 2 (S ) where s ∈ V, e 1 ∈ expr, e 2 ∈ expr, τ ∈ scalar-type E * τ @[s,e] (S ) where s ∈ V, e ∈ expr, τ ∈ scalar-type Abstract evaluation. Let us first consider the evaluation of the dereferencing of a pointer to a string. The analyzer we want to define performs partitioning on the abstract state during the evaluation of expressions, therefore evaluation results are pairs (evaluated expression × abstract state). This set is understood disjunctively and greatly improves the precision of the analyzer. The result of an evaluation is therefore a finite element of ℘(exp × S m ). Five cases can be distinguished during the evaluation of * τ @[s,e]:

-before: τ = u8 and @[s,e] points before the first '\0' character. In this case the evaluation can yield any character that is not '\0'. -at: τ = u8 and @[s,e] points at the first '\0' character. In this case the evaluation yields '\0'. -after: τ = u8 and @[s,e] points after the first '\0' character. In this case the evaluation can yield any character. -eerror: τ = u8 and @[s,e] points after the end of the allocated memory. In such a case we generate an out of bounds error.

function tests on offsets tests on rhs transformation τ = u8, in this case we over-approximate the evaluation by the range of the type τ . Figure 2 summarizes those cases and gives the example of the before function. In this table o is the offset of the pointer, l and a are the length and the allocated size of the string. The definition of these functions can be found in in Appendix A.2. We can now define E * τ =u8 @[s,e] (S ) = {before(e , s, S ) ∪ at(e , s, S ) ∪ after(e , s, S ) ∪ eerror(e , s, S ) | (e , S ) ∈ E e (S )} and E * τ =u8 @[s,e] (S ) = {(range(τ ), S )}.

set0 o ≥ 0 ∧ o ≤ l ∧ o < a c = 0 l ← o setnon0 o ≥ 0 ∧ o = l ∧ o < a c = 0 l ← [o + 1; a] unchanged o ≥ 0 ∧ o < l ∧ o < a c = 0 unchanged o ≥ 0 ∧ o > l ∧ o < a l unchanged o ≥ 0 ∧ o > l ∧ o + r ≤ a forget o ≥ 0 ∧ o ≤ l ∧ o + r ≤ a l ← [o; a] serror o + r > a ∨ o < 0 out of bounds
Abstract transformations. In order to complete the definition of our abstract interpreter, we need to provide the abstract semantic of an assignment in a string * τ @[s,e 1 ] = e 2 . We can distinguish 6 cases in such an assignment:

-set0: τ = u8 and a character that appears before the first '\0' is assigned to '\0', in which case we need to set the variable coding for the length of the string to its new value (the offset of the pointer to the string). -setnon0: τ = u8 and the first '\0' is replaced with a non-'\0' character, in which case we need to set the variable coding for the length of the string to its new value (it can be anything greater than the offset of the pointer to the string). -unchanged: τ = u8 and we are performing an assignment that does not change the position of the first '\0' character. Either because we are replacing a character placed before the first '\0' character by a non-'\0' character, or because we are assigning a character after the position of the first '\0' character. -l unchanged: τ = u8 and we are performing an assignment that does not change the position of the first '\0' character: the only modified characters are placed after the first '\0' character. -forget: τ = u8 and the offset of the pointer is less than the length of the string, in this case the position of the first '\0' character is greater than the offset of the pointer. -serror: The writing generates an out of bounds, in which cases we generate an out of bounds warning. Figure 3 summarizes these cases. In this table l and a denote respectively the length and the allocated size of string s, o denotes the offset of the pointer, c denotes the evaluated right-hand side of the assignment, and finally r denotes sizeof(τ ). The definitions of all these functions can be found in Appendix A.3 and they are similar to the definition of before in Figure 2. Using the 6 transformations aforementioned we can now define: Example 6. Going back to Example 5, we now assume that R is a numerical abstract state built from the constraint set: {t < s a , t = s l , p + u, 2, s32 < s l , s l < s a }. Moreover in the following S [E] denotes the abstract state S in which the numerical component has been extended with the constraints set E, and e denotes the expression p + u, 2, s32 . E *(@[s ,e]) (S ) = {([1; 255], S [{e ≥ 0, e < s l , e < s a }]), (0, S [{e ≥ 0, e = s l , e < s a }]), ([0; 255], S [{e ≥ 0, e > s l , e < s a }])}. With a precise enough numerical domain (e.g. polyhedra), S [{e ≥ 0, e = s l , e < s a }], S [{e ≥ 0, e > s l , e < s a }] and S [{e < 0 ∨ e ≥ s a }] form empty partitions, meaning that in this example, they represent impossible cases. For similar reasons S stmt (S ) will compute abstract elements that are reduced to ⊥ for functions set0, unchanged and serror. Therefore: S stmt (S ) = {p, u, 2, s32 , t}, R , {p → s , t → s} with R = {t < s a , t + 1 ≤ s l , p + u, 2, s32 < s l , s l < s a }. This assignment made our abstraction lose the position of the first '\0' character, as it wrote a non-'\0' character in its place.

S * τ @[s ∈ V,e 1 ]=e 2 (S ) = • {set0(s,

String declaration. When encountering a local variable declaration (u8 s[n]

with n ∈ N ≥0 and s ∈ V) we can set the allocated size of the string to n, and set the length to the range [0, n] as shown in the following example: S u8 s[27] ( ∅, ∅, ∅ ) = ∅, {s l ≥ 0, s l ≤ 27, s a = 27}, ∅} . The formal definition is straightforward (see Appendix A.4).

Example 7. Consider again Program 1.1 from the introductory example, analyzed starting from an abstract state S = {p, q}, {p = 0, q = 0, 0 ≤ s l < s a , 0 ≤ s l < s a }, {p → s, q → s } . Note that the input state contains the information that p and q do not alias. The numerical invariant (the rest of the abstract state is not modified by the analysis) found at the beginning of line 2 is: {-p + q = 0, s l ≥ p + 1, s a -s l ≥ 0, p ≥ 0, s l ≥ p}. An out of bounds error is generated at line 3, indeed in the starting abstract state, no hypothesis is made on the relation between s l and s a therefore there might be a buffer overrun at line 3. Finally the numerical invariant discovered at the end of line 6 is: {s l = s l , q = s l , p = s l , s a ≥ s l + 1, s l ≥ 0, s a ≥ s l + 1}, thus showing that we were able to infer that the two strings pointed to by p and q have the same size at the end of the analysis. Dynamic memory allocation. As mentioned in Figure 1, we allow dynamic memory allocations. The Cell abstract domain as presented in Section 3 is not able to handle those. To model dyamic memory allocation, we consider a finite set A of heap addresses, derived from the allocation site using recency abstraction [START_REF] Balakrishnan | Reps. Recency-abstraction for heap-allocated storage[END_REF]: for each allocation site a, one abstract address, a s , is used to model the last block allocated at a, and another one, a w , to summarize the blocks allocated previously at a. While we perform weak updates on the later, we can perform strong updates on the former, which ensures a gain in precision.

Example 8. Consider now Program 1.3, and assume that a s and a w (resp. b s and b w ) are addresses for which we perform strong and weak update at program point 1 (resp. 2 ). Starting from the analysis of the body of function main, we get: {x}, {0 ≤ a w l ≤ a w a , 10 ≤ a w a ≤ 20, 0 ≤ a s l ≤ a s a , a s a = 30, b s a = 40, b s l = 0, x = 0}, {x → b s } This state gives us that x points to a memory location starting from a '\0' character. We also note that information about the two first allocations made at program point a have been collapsed into the a w address. In a C project that manipulates strings, calls to functions such as strcpy, strcat are performed many times and at many different call sites. Performing a modular analysis of such functions and inferring a summary that is reusable at subsequent calls has potential to greatly improve scalability. We chose to perform our modular analysis in a classic top-down fashion. This ensures that when a function is analyzed, we already have some information on its context (in particular, the possible pointer aliasing and variable range), which helps maintaining the precision of the function analysis. Therefore we would like to be able to infer a partial function that, given an input abstract state and a statement, can produce an output abstract state that is an over approximation of the abstract state we would have obtained by performing the analysis of the statement. Such a function will be called a summary. Note that substituting some of the statement analysis by a call to a summary is sound.

Example 9. Given stmt ∈ stmt, (I , O ) ∈ (S m × S m ) such that S stmt (I ) O , let us define R = λ(stmt , S ), if stmt = stmt ∧ S I then O else undefined.
R is a summary function, built using an input/output relation. This can be easily generalized using a set of input/output relations. Moreover we can remove constraints on I before the analysis of the body of the function in order to improve the reusability of the input/output relation obtained, the drawback being that the corresponding output abstract value will be greater thus losing precision. Furthermore computing and storing new (I , O ) relations whenever no existing summary could be used can cause the computation of input/output relations that will never be reused, hence the importance of generalizing I in the direction of newly discovered call contexts, so as to tailor summaries to actual call sites abstract values.

Remark 3. Consider the statement stmt = x = x + 1, and assume our abstract domain to be the interval domain [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF]. For every input state of the form {x → [α, β]}, the output state will be of the form {x → [α + 1, β + 1]}. A summary function R defined on {stmt} × S m in the manner of Example 9 (with a finite list of input/output relations) will never yield an analyzer able to express that for every input [γ, δ] the output is [γ + 1, δ + 1]. Indeed the interval domain would produce a set of input/output relations {[α i , β i ] → [α i + 1, β i + 1]}, and for an input [γ, δ] [α 0 , β 0 ] we could only use as output abstract state [α 0 + 1,

β 0 + 1], thus losing information compared to [γ + 1, δ + 1].
Using relational domains. Relational domains are able to express relations of the form y = x + 1. Such a relation can grasp the semantic of stmt from the previous remark. We use the relational aspect of the numerical domain to express relations not only between the values of variables, but also between their values and their input values. This idea was introduced in [START_REF] Cousot | Static determination of dynamic properties of recursive procedures[END_REF] and is also used in [START_REF] Cousot | Modular static program analysis[END_REF]. Consider two sets of variables V = {x, y} and V = {x , y } and the abstract element: S = {x = y , y = x }. Moreover assume at input that {x = 3, y = 5}, then using the meet provided by the numerical domain in order to instantiate S with input constraints: {x = 3, y = 5} |{x ,y , x,y} {x = y , y = x } = {x = 3, y = 5, x = 5, y = 3}, and finally {x = 3, y = 5, x = 5, y = 3} |{x,y} = {x = 5, y = 3}. This example emphasized how relational domains are used to express precise input/output relations between numerical variables.

Building the summary function. We feel that two analyses starting from different aliasing patterns should be kept separated in order to improve precision. Indeed, analyzing strcat(p,q) (see Figure 1.4) without any hypothesis on the possible aliasing of p and q would result in a huge loss of precision and in false alarms being raised at every call (p and q might be aliased, which would raise a segmentation fault). Therefore we must use partitioning of the abstract domain, performing an analysis for every possible aliasing scheme would result in a combinatorial blow up, moreover we might perform analysis for partitions that will never occur at any call site. For these reasons we will only analyze partitions on demand. Our goal is therefore to build a summary that is a set of numerical relations such as defined above. The decision to extend a partition or to build a new one will be based on the "symbolic" part of the abstract domain. The heuristic we chose was to separate abstract states with different aliasing, but also those where the unification of the cell or string sets would induce major differences in the numerical domain set. Moreover the summary function is extended on demand, meaning that when the analyzer encounters a function call, it tries to use an existing relation and if none can be found it builds a new relation or it generalizes an existing one. Generalization of a relation is done in the following way: assume known a relation with input I and an abstract state S , such that S I . If the analyzer deems that S and I should be in the same relation (e.g. because they have the same aliasing), we perform a new analysis of the function starting from I (S I ), that is a generalization, of I , by the mean of the widening operator. This ensures that, given an aliasing, a function will be analyzed only a finite number of times and that the input of the obtained relation is tailored to the actual values at call site. Building numerical relations does not require a transformation of the intra-procedural iterator. Indeed variables are added to the numerical domain with equality constraints between primed and unprimed variables. Analysis is then performed as if primed variables were not present in the numerical domain and they are removed after storing the summary.

Example 10. Consider the statement s32 x = a + 1 (with typeof(a) = s32), from input state: {a }, {a = a, a ≥ 0}, ∅ . The output state is then {a , x }, {a = a, x = a + 1, a ≥ 0}, ∅ . From this we deduce the relation: let I α be some input state, if the set of cells of I α is precisely {a} and if the numerical domain of I α satisfies the condition a = α and if the pointer map is empty, then the best possible output state is {a, x}, {a = α, x = α + 1}, ∅ .

Example 11. Consider now the function strcat of Figure 1.4. The modular analysis of this function yields a relation stating that: if dest points (at offset 0) to some memory location s, with length s l and allocated size s a , and if src points (at offset 0) to some memory location t with equivalent length and allocated size definition and t = s then {s l = t l + s l , s a = s a , t a = t a , t l = t l , t l ≥ 0, t l ≤ t a -1, t l ≤ s l , s l ≤ s a -1} Therefore thanks to the s l = t l +s l relation, if another call to strcat is performed in a state where s l = α and t l = β for some α and β, our analyzer, can conclude (without reanalysis) that the length of the string t l at the end of the analysis is α + β. Remark 4. The following improvements were added:

in order to improve reusability, we increase the input state by removing some memory blocks (meaning we leave out constraints on these regions) from the input state. This plays the role of the framing rule in separation logic. Note that this improvement does not induce any precision loss. when a summary is created, some memory blocks are quantified universally, therefore when trying to apply a summary we try to unify the memory blocks from the actual input state with those of the summary input state.

Implementation

The [START_REF] Xavier Allamigeon | Static analysis of string manipulations in critical embedded C programs[END_REF], [START_REF] Dor | Cleanness checking of string manipulations in C programs via integer analysis[END_REF].

In related works, Allamigeon et al. mentioned in [START_REF] Xavier Allamigeon | Static analysis of string manipulations in critical embedded C programs[END_REF], Section 5, that the most difficult example they had to deal with were calls to strcpy performed on string placed in a structure, itself placed in a matrix, and accessed via pointer manipulations (see Program 1.6, in Appendix B). This example was successfully analyzed with the version of strcpy defined in Program 1.1 and with an alternate implementation found in Qmail (see Program 1.7), the second case was more complex and required the use of partitioning. Our ability to easily deal with such manipulations comes from the use of the Cell domain to deal with low-level features of C. We are able to tackle most of the programs from web2c mentioned in [START_REF] Dor | Cleanness checking of string manipulations in C programs via integer analysis[END_REF] (7 out of 9, programs that could not be analyzed are due to the fact that we do not have yet implemented all the features of the C language). The precision of this analysis (number of errors and false alarms) is similar to that of [START_REF] Dor | Cleanness checking of string manipulations in C programs via integer analysis[END_REF] and the execution time of the analyzer was always below 2 seconds. As an example consider Prog. 1.5, starting the analysis under the conditions that: cp points to buf, a buffer of size BUFSIZ before the first '\0' character produces alarms at line 9 and 10. Indeed under such hypothesis strcpy tries to write outside of tbuf. Note moreover that both [START_REF] Xavier Allamigeon | Static analysis of string manipulations in critical embedded C programs[END_REF] and [START_REF] Dor | Cleanness checking of string manipulations in C programs via integer analysis[END_REF] defined special abstract transformations for strcpy, whereas we perform a modular analysis of the function.

Related works

Modular Static Analysis. Cousot and Cousot mentioned in [START_REF] Cousot | Modular static program analysis[END_REF] the importance of performing modular analyses and described several methods to design them. An efficient way is to use user-provided contracts as in [START_REF] Fähndrich | Static contract checking with abstract interpretation[END_REF]. Our goal was to infer contracts, as in [START_REF] Cousot | Precondition inference from intermittent assertions and application to contracts on collections[END_REF], therefore works closest to ours would be the input/output inference performed by Bourdoncle in [START_REF] Bourdoncle | Abstract interpretation by dynamic partitioning[END_REF], however this method was limited to non-relational (interval) domains, unlike our method, which is thus more expressive (see Remark 3). In [START_REF] Cousot | Modular static program analysis[END_REF], numerical relations are used to represent the semantic of a set of statements, however this is limited to numerical programs whereas we extend the method to consider both numbers and pointers, including pointer arithmetic. The analyzer proposed by Sotin and Jeannet in [START_REF] Sotin | Precise interprocedural analysis in the presence of pointers to the stack[END_REF] is able to infer input/output relations of the form proposed in Section 5. Nevertheless they consider a subset of C that does not contain pointer arithmetic, union types nor pointer casts. Müller-Olm and Seidl [START_REF] Müller | Analysis of modular arithmetic[END_REF] and Sharma and Reps [START_REF] Sharma | A new abstraction framework for affine transformers[END_REF] proposed domains specialized in the discovery of numerical input/output relations on statements, in both cases the relations discovery is performed during the analysis of the statement by a special domain. In Sec. 5 we mentioned that we implemented a mechanism to infer framing in order to improve analysis reusability, framing mechanisms are fundamentals in tools base on separation logic such as Smallfoot [START_REF] Berdine | Smallfoot: Modular automatic assertion checking with separation logic[END_REF] or Infer [START_REF] Calcagno | Moving fast with software verification[END_REF].

String analysis. One popular technique to avoid buffer overflows is dynamic analysis. There is a long history of such technique (see [START_REF] Wilander | A comparison of publicly available tools for dynamic buffer overflow prevention[END_REF] for some examples). These methods induce an overhead cost and do not prevent program failures. By contrast we employ static analysis. String are arrays of characters, therefore analysis methods proposed in [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF] and [START_REF] Cousot | Verification by abstract interpretation[END_REF] could be used to design static analyzers handling strings. The three following works are the closest to ours and all follow the idea introduced in [START_REF] Wagner | A first step towards automated detection of buffer overrun vulnerabilities[END_REF] to track the length of strings. Dor et al. [START_REF] Dor | Cleanness checking of string manipulations in C programs via integer analysis[END_REF] tackled the problem by rewriting string manipulating statements into statements over a numerical variable language, however this transformation induced the usage of a number of variables quadratic in the number of strings present in the analysis, in order to account for pointer aliasing. Simon and King [START_REF] Simon | Analyzing string buffers in C[END_REF] proposed an analyzer for a sub-C language manipulating strings, and allowing dynamic memory allocation, but some pointer manipulations could not be handled. They improved their results in [START_REF] Simon | Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities[END_REF], the string domain presented here is a combination of results from [START_REF] Simon | Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities[END_REF] and the cell abstract domain, moreover we provided a way to dynamically balance strings dealt with by the string abstract domain and by the cell domain. Additionally string length and allocated size are bound to pointers (whereas we bind them to the actual memory location containing the string), and this approach seems to prevent the modular integration of this domain in a full C language analyzer. Allamigeon et al. [START_REF] Xavier Allamigeon | Static analysis of string manipulations in critical embedded C programs[END_REF] also proposed an analyzer that keeps track of the position of the first '\0' character, however their analysis is non-relational, can not handle arbitrary pointer cast, and uses static information on string length, therefore preventing the domain reusability for dynamically allocated strings. We believe that our analysis is the first one that is both modular, able to reason both on the C at a low-level (including pointer casts and unions), and at a higher-level (on strings using dedicated abstractions).

Conclusion

In this article we proposed an abstract domain able to tackle C string of parametric size, built as an add-on to an existing domain [START_REF] Miné | Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics[END_REF] capable of dealing with most of the features of the C language. We have shown how our analyzer can be tuned dynamically (by choosing whether the String or Cell domain should deal with certain memory regions, by changing the partitioning heuristics in the inter-procedural iterator or by changing the underlying numerical domain) so as to adjust its precision. Upon the aforementioned analyzer we defined an interprocedural iterator designed to increase statement analysis reusability without having to lose precision.

=

  s8 | s16 | s32 | s64 | u8 | u16 | u32 | u64 scalar-type ∆ = int-type | ptr type ∆ = scalar-type | type[n] n ∈ N | struct{u0 : type, . . . , un-1 : type} | union{u0 : type, . . . , un-1 : type} lval ∆ = * scalar-type expr | v ∈ V expr ∆ = cst cst ∈ N | &lval | expr expr ∈ {+, ≤, . . . } stmt ∆

  before(e, s, S ) = {([1; 255], C, R {0 ≤ e, e < s l , e < sa}, P } function tests on offset evaluation before 0

Fig. 3 :

 3 Fig. 3: Summary of transformations.

  e 1 , e 2 , S ) serror(s, e 1 , 1, S ) unchanged(s, e 1 , e 2 , S ) setnon0(s, e 1 , e 2 , S ) | (e 1 , S ) ∈ E e 1 (S ), (e 2 , S ) ∈ E e 2 (S )} if τ = u8 • {l unchanged(s, e 1 , sizeof(τ ), S ) forget(s, e 1 , sizeof(τ ), S ) serror(s, e 1 , sizeof(τ ), S ) | (e 1 , S ) ∈ E e 1 (S )} if τ = u8

8 }

 8 =0; dest [ i ]!= ' \0 '; i ++) ; 5 for ( j =0; src [ j ]!= ' \0 '; j ++) 6 dest [ i + j ] = src [ j ]; 7 dest [ i + j ] = ' \0 '; Program 1.4: strcat

12 }

 12 =0;& buf [ i ] < cp ;++ i ) 7 tbuf [ i ] = buf [ i ];8 strcpy (& tbuf [ i ] , " ( long ) " ) ; 9 strcpy (& tbuf [ i + 6] , cp ) ; Program 1.5: insert long from web2c

  analyzer was implemented in OCaml in the novel and still in development Mopsa framework. Mopsa enables a modular development of static analyzers defined by abstract interpretation. An analyzer is built by choosing abstract domains, and combining them according to the user specification. Abstract domains are either predefined (e.g. Cell abstract domain, loop iterators, . . . ) or user-defined (e.g. String abstract domain). The String abstract domain was added to the library of existing domains, and a new inter-procedural iterator was added to implement the modular analysis presented in Section 5. The current analyzer is in development, it is able to analyze all C code fragments presented in this article, but can not tackle complete realist C projects yet. To test our modular string analysis, we thus considered the examples and benchmarks used in previous works on string analysis

Accordingly we need to build our

This work is supported by the European Research Council under Consolidator Grant Agreement 681393 -MOPSA.

A Tool functions

Using functions to cells and from cells, and under the hypothesis that V = {s 0 , . . . , s n-1 }, we can define the Galois connection between the Cell abstract domain and the String abstract domain: [START_REF] Cousot | Static determination of dynamic properties of generalized type unions[END_REF];