E Bampis

B Escoffier

S Mladenovic

Lip6

Fair resource allocation over time

We consider the over-time version of the Max-Min Fair Allocation problem. Given a time horizon t = 1, 2, . . . , T , with at each time t a set of demands and a set of available resources that may change over the time defining instance I t , we seek a sequence of solutions S 1 , S 2 , . . . , S T that (1) are near-optimal at each time t, and (2) as stable as possible (inducing small modification costs). We focus on the impact of the knowledge of the future on the quality and the stability of the returned solutions by distinguishing three settings: the off-line setting where the whole set of instances through the time horizon is known in advance, the on-line setting where no future instance is known, and the k-lookahead setting where at time t, the instances at times t + 1, . . . , t + k are known. We first consider the case without restrictions where the set of resources and the set of agents are the same for all instances and where every resource can be allocated to any agent. For the off-line setting, we show that the over-time version of the problem is much harder than the static one, since it becomes N P-hard even for families of instances for which the static problem is trivial. Then, we provide a ρ ρ+1 -approximation algorithm for the off-line setting using as subroutine a ρ-approximation algorithm for the static version. We also give a ρ ρ+1 -competitive algorithm for the online setting using also as subroutine a ρ-approximation algorithm for the static version. Furthermore, for the case with restrictions, we show that in the off-line setting it is possible to get a polynomial-time algorithm with the same approximation ratio as in the case without restrictions. For the online setting, we prove that it is not possible to find an online algorithm with bounded competitive ratio. For the 1lookahead setting however, we give a ρ 2(2ρ+1) -approximation algorithm using as subroutine a ρ-approximation algorithm for the static version.

Introduction

Resource allocation problems have been intensively studied in the past [START_REF] Luss | Equitable Resource Allocation: Models, Algorithms and Applications[END_REF]. In such a problem, the aim is to find an allocation of a set of limited resources to a set of competing agents in a way to optimize a given objective function subject to a set of constraints (availability of resources, level of demands, compatibility between agents and resources). The study of a large variety of combinatorial optimization problems, including facility location, matching, scheduling problems etc..., has been motivated by applications in logistics, computer and telecommunication networks, air traffic management, energy management etc... A special focus on resource allocation problems has been given in multiagent settings, considering a fairness criterion/objective in the allocation [START_REF] Bouveret | Allocation of indivisible goods: a general model and some complexity results[END_REF][START_REF] Golden | Infinite order lorenz dominance for fair multiagent optimization[END_REF][START_REF] Bouveret | Fair allocation of indivisible goods[END_REF]. Typically, these problems are studied in the case where the instance is static, while in many applications the instance changes over time. Take for example an energy company producing electricity on a set of reactors. The electricity demands evolve over time, so the company has to decide a production plan, all along a period of time, in order (1) to satisfy the demand at every time, (2) to minimize the production cost at each time, and (3) to minimize the cost of turning on/off the reactors. The reader is refered to [START_REF] Michel Lemaître | Exploiting a common property resource under a fairness constraint: a case study[END_REF][START_REF] Jonker | Towards a market mechanism for airport traffic control[END_REF] for other applications in dynamic contexts. It is only recently that resource allocation problems start to be studied in such a dynamic context [START_REF] Eisenstat | Facility location in evolving metrics[END_REF][START_REF] Gupta | Changing bases: Multistage optimization for matroids and matchings[END_REF].

More formally, we are given a time horizon: t = 1, 2, . . . , T where at each time t we have a new instance I t of the considered resource allocation problem. It is tempting to try to solve the problem for every new instance. However in most practical applications, there is a non-negligible transition cost for adopting modifications of the current allocation (solution). Hence, the goal is to determine a sequence of solutions S 1 , S 2 , . . . , S T that both (1) are near-optimal (quality), and (2) induce small modification costs (stability). An important aspect in this dynamic setting is the impact of the knowledge of either the whole set of instances (off-line case), or a limited number of instances, say k, in the near future (k-lookahead case), or no future instance at all (on-line case) on the quality and the stability of the returned solutions.

In this paper, we focus on the over-time version of different variants of a basic resource allocation problem, the Max-Min Fair Allocation problem where the aim is to determine an allocation of the resources to the agents in a fair way. An instance of the Max-Min Fair Allocation problem is characterized by a set R of n resources, a set P of m agents and a set of nonnegative values (j, i), for every j ∈ R and every i ∈ P. The value (j, i) corresponds to the valuation of the agent i for the resource j. An allocation is a partition R 1 , . . . , R m of the set of resources and the valuation of agent i is equal to (R i ) = j∈R i (j, i). The objective is to find an allocation with the best possible valuation for the worst-off agent, i.e. an allocation maximizing min i∈P j∈R i (j, i). Another name used in the literature for this problem is the Santa Claus problem where the resources correspond to gifts and the agents to children. The objective is to find an allocation of gifts to the children so as to maximize the happiness of the least happy child. In scheduling terms, this problem corresponds to the problem of scheduling a set of jobs on a set of unrelated machines so as to maximize the load of the least loaded machine. Here the resources are the jobs and the agents are the machines. Important subproblems of the Max-Min Fair Allocation problem is the Restricted Max-Min Fair Allocation problem in which (j, i) ∈ {0, j } (each resource has a fixed value, but only some agents are interested in it), the Homogeneous Max-Min Fair Allocation problem in which (j, i) = j (each resource has a fixed value) and the Uniform Max-Min Fair Allocation problem in which (j, i) = j s i (where s i is the speed of machine i in the scheduling context).

In the Over-Time Max-Min Fair Allocation problem, we are given a sequence I 1 , . . . , I T of instances of the Max-Min Fair Allocation problem, with T ≥ 2. For every instance I t , we have a set of m t agents M t = {1, . . . , m t }, a set of n t resources N t = {1, . . . , n t } and a valuation of the agent i for the resource j, denoted by t (j, i) ∈ R for every j ∈ N t and i ∈ M t . We are also given a reward equal to K ∈ R + for every resource that is allocated to the same agent in two consecutive solutions (this reward for our maximization problem corresponds to the transition cost in [START_REF] Eisenstat | Facility location in evolving metrics[END_REF][START_REF] Gupta | Changing bases: Multistage optimization for matroids and matchings[END_REF] for minimization problems).

A solution sequence S = (O 1 , . . . , O T ), where O t is a solution of I t , defines

• a Santa Claus revenue, (S) = T t=1 t (O t ) such that t (O t ) = min i∈{1,...,mt} nt j=1 l t (j, i) • x t,j,i
with x t,j,i = 1 if the resource j is allocated to the agent i in O t , and 0 otherwise. This corresponds to the sum of the valuations of the worst-off agents over all solutions O t , for t = 1, 2, . . . T ,

• a transition revenue, D(S) = T -1 t=1 D t (S), where

D t (S) = K × |resources remaining on a same agent in O t and O t+1 |.
Intuitively, the larger the transition revenue, the more stable the sequence of the solutions.

Overall, we seek for a solution sequence that yields a good trade-off between quality and stability, and in what follows our goal will be the maximization of the sum of f (S) = (S) + D(S).

Example 1. Suppose that we have n = 4 resources and m = 2 agents, K = 1. We have 3 time steps. We are in the homogeneous case, and here are the valuation of resources:

t = 1 t = 2 t = 3 Resource 1 3 6 2 Resource 2 2 4 1 Resource 3 1 8 2 Resource 4 2 1 3
Let us consider this first solution sequence S 1 (for column t = 1 and line Agent 1, (2, 4) are the resources allocated to Agent 1 at time 1):

t = 1 t = 2 t = 3 Agent 1 (2,4) (1,2) (2,4) Agent 2 (1,3) (3,4) (1,3)
We have (S 1 ) = 4 + 9 + 4 = 17 (these are actually the best solutions at each time step). Since 2 resources remain allocated to the same agent between times 1 and 2, and 2 as well between times 2 and 3, we have D(S 1 ) = 2K + 2K = 4. Hence, f (S 1 ) = 21.

One may consider S 2 which is the same as S 1 but resource 4 is given to agent 1 in time step 2. Then (S 2 ) = (S 1 ) -1 = 16, but D(S 2 ) = 3K + 3K = 6, so f (S 2 ) = 22 > f (S 1 ).

Recall that a ρ-approximation algorithm for an optimization problem is a polynomial-time algorithm returning a solution whose value is within a factor of ρ of the value of an optimal solution for all the instances of the problem [START_REF] Williamson | The Design of Approximation Algorithms[END_REF]. ρ is called the approximation ratio of the algorithm.

For a maximization problem like the Max-Min Fair Allocation problem studied in this paper, 0 ≤ ρ ≤ 1 (ρ = 1 corresponds to an exact algorithm). The definition of a c-competitive algorithm is similar to the one of a ρ-approximation algorithm where the on-line algorithm is compared with respect to the optimal off-line algorithm that knows the entire sequence of the input data.

Variants. We distinguish between two cases: the case where there are restrictions on the set of agents on which a resource can be allocated (Section 3.2) and the case where there are no restrictions (Section 3.1).

Previous results

The (static) problem has been first studied in a game theoretic context [START_REF] Lipton | On approximately fair allocations of indivisible goods[END_REF]. Bezáková and Dani have shown that it is N P-hard to approximate the Max-Min Fair Allocation problem to within a factor better than 1/2 and they provided the first non-trivial approximation algorithm [START_REF] Bezáková | Allocating indivisible goods[END_REF]. Later, Bansal and Sviridenko [START_REF] Bansal | The santa claus problem[END_REF] A lot of progress has been done for the Restricted Max-Min Fair Allocation problem. While the same inapproximability result holds in this case, Bansal and Sviridenko [START_REF] Bansal | The santa claus problem[END_REF] proposed an Ω log log log m log log m -approximation algorithm. Haeupler et al. presented a constant factor approximation algorithm, but the constant was large and unspecified. Asadpour and Saberi [START_REF] Asadpour | An approximation algorithm for max-min fair allocation of indivisible goods[END_REF] showed that the integrality gap of the configuration linear program is bounded by 1/4. Annamalai, Kalaitzis and Svensson proposed recently a combinatorial algorithm with approximation ratio

1 6+2 √ 10+ which runs in |I| 1 2 log( 1 )
, for any > 0 and where |I| is the size of the instance [START_REF] Annamalai | Combinatorial algorithm for restricted max-min fair allocation[END_REF].

For the Homogeneous Max-Min Fair Allocation problem, Deuermeyer, Friesen and Langston [START_REF] Deuermeyer | Scheduling to maximize the minimum processor finish time in a multiprocessor system[END_REF] showed that the classical LPT (Longest Processing Time) algorithm is a 3 4 -approximation algorithm. Csirik, Kellerer and Woeginger [START_REF] Csirik | The exact lpt-bound for maximizing the minimum completion time[END_REF] improved the analysis showing that the approximation ratio of LPT is in fact 3m-1 4m-2 . Woeginger [START_REF] Woeginger | A polynomial-time approximation scheme for maximizing the minimum machine completion time[END_REF] and also Ochel with Voecking [START_REF] Ochel | Approximability of OFDMA scheduling[END_REF] proposed a polynomial time approximation scheme for the problem: for any > 0, there exists a (polynomial time) (1 -)approximation algorithm. Epstein and Sgall proposed a polynomial time approximation scheme for the Uniform Max-Min Fair Allocation problem [START_REF] Epstein | Approximation schemes for scheduling on uniformly related and identical parallel machines[END_REF].

Our results

Our goal is to measure to what extend the over-time setting is harder to solve than the static one, with respect to the quality of solutions an algorithm can compute in polynomial time. In particular, for cases where (j, i) = (j) (homogeneous case) or when (j, i) ∈ {0, (j)}, the static problem has constant ratio approximation algorithms as mentioned above; is it still the case in the over-time setting? We provide some answers which depend on the assumptions made on the knowledge of the future (off-line/online/k-lookahead), and on the possibility to have incompatibilities between resources and agents (case with restriction) or not.

More precisely, in Section 3.1 we study the case without restrictions where the set of resources and the set of agents are the same for all instances and where every resource can be allocated to any agent. For the off-line setting, we first show that the over-time version of the problem is much harder than the static one with respect to the computational complexity. Then, we propose a ρ ρ+1 -approximation algorithm for the off-line setting using as subroutine a ρ-approximation algorithm for the static version, thus getting a constant ratio approximation algorithm for the over-time setting whenever the static problem has one. We improve this approximation ratio when the number of steps T or the number of agents m is bounded. Then, we show that a similar result can be obtained in the on-line setting, since we devise a ρ ρ+1 -competitive algorithm using also as subroutine a ρapproximation algorithm for the static version.

In Section 3.2, we study the case with restrictions. We show that in the off-line setting it is possible to get a polynomial-time algorithm with the same approximation ratio as in the case without restrictions. For the on-line setting, we prove that it is not possible to find an on-line algorithm with bounded competitive ratio. Interestingly, we show that knowing only one time step in advance (1-lookahead setting) is sufficient to again obtain a constant approximation algorithm whenever the static case has one; more precisely, we give a ρ 4ρ+2 -approximation algorithm using as subroutine a ρ-approximation algorithm for the static version.

The case Without-Restrictions

We consider the case where the set of resources and the set of agents are the same for all the instances. Therefore, n 1 = ... = n T = n and m 1 = ... = m T = m. In addition, every resource can be allocated to any agent.

As a first result, we illustrate the fact that the over-time problem is significantly harder than the static Max-Min Fair Allocation problem, since it remains N P-hard even in a very restricted case.

Theorem 1. Max-Min Fair Allocation is N P-hard even in an off-line setting with no restriction, with only 2 agents and in the homogeneous case, with furthermore t (j, i) = t (j) ∈ {0, 1}.

Note that these instances are trivial in the static case.

Proof. We show this result using a reduction from the Maximum Cut problem. In this problem, known to be N P-hard [START_REF] Garey | Computers and Intractability: A Guide to the Theory of NP-Completeness[END_REF], we are given an undirected graph G = (V, E) and an integer s. The question is whether we can partition the set V of vertices into (V 1 , V 2 ) in such a way that at least s edges have one endpoint in V 1 and one in V 2 .

Given G = (V, E) and s with V = {v 1 , . . . , v |V | } and E = {e 1 , . . . , e |E| }, we build an instance of Max-Min Fair Allocation with 2 agents, |V | resources (call them {v 1 , . . . , v |V | }) and T = |E| time steps. At time step i agents 1 and 2 give valuation 1 to the two endpoints of edge e i , and 0 to all other resources. We set K sufficiently large, say K = |E| + 1. We claim that there is a cut with at least s edges in G if and only if there is a solution sequence of value at leat K(T -1)|V | + s in the instance of Max-Min Fair Allocation.

If there is a cut (V 1 , V 2 ) with at least s edges, then give vertices of V 1 to agent 1 and vertices of V 2 to agent 2, at any time (no modification of solution). Then the transition revenue is K(T -1)|V |. If an edge e i is in the cut, then at time i one endpoint is given to agent 1, the other 1 to agent 2, and the Santa Claus revenue at time i is 1. Then we have a solution sequence of value at least

K(T -1)|V | + s.
Conversely, note that the Santa Claus revenue is at most 1 at any time step, so at most |E| in total. So, if a solution sequence makes at least one modification in the solutions, it will have value at most

K(T -1)|V | - K + |E| < K(T -1)|V |.
Hence, a solution sequence with value at least K(T -1)|V | + s does not make any modification. Let V 1 be the set of resources given to agent 1, and V 2 the ones given to agent 2. The solution sequence has (at least) s time steps with Santa Claus revenue 1. This means that there are at least s edges with one endpoint in V 1 and one in V 2 . Now, we give some approximation algorithms for the problem, first in an off-line setting and then in an on-line setting.

Off-line case

In order to find a good solution sequence for the revenue, we use as a subroutine an algorithm A for the static Max-Min Fair Allocation problem. Then Algorithm 1 works as follows:

• Apply A on each instance I t , denote by Õt the obtained solution.

• Build a first solution sequence S 0 = ( Õ1 , Õ2 , . . . , ÕT ).

• For any t consider the solution sequence S t = ( Õt , Õt , . . . , Õt ) (no modification).

• Output the best of the T + 1 previous solutions.

The idea is that the first solution performs well with respect to the Santa Claus revenue (S), while the others perform well with respect to the transition revenue D(S). More precisely, we have the following result.

Theorem 2. If A is a (polytime) ρ-approximation algorithm for the static case, then Algorithm 1 is a (polytime)

T ρ

(T -1)ρ+T -approximation algorithm for the over-time problem.

Note that this ratio decreases with T down to ρ ρ+1 (T unbounded).

Proof. Let S * = (O * 1 , ..., O * T ) be an optimal solution sequence, and denote by S the solution output by the algorithm. As A is a ρ-approximation algorithm for the static case, we get t ( Õt ) ≥ ρ t (O * t ) for any t. Then:

f (S) ≥ (S 0 ) ≥ ρ T i=1 t (O * t ) = ρ (S * ) (1)
Now, since in S i (i ≥ 1) no modification is made, then clearly S i has maximum transition revenue, so:

f (S) ≥ f (S i ) ≥ ρ i (O * i ) + D(S * ) (2)
Now, sum Equation (2) for i = 1, . . . , T , multiply by ρ and add (T -ρ) times Equation (1). This gives:

(T ρ + T -ρ)f (S) ≥ ρ(ρ (S * ) + T D(S * )) + (T -ρ)ρ (S * )
We derive (T ρ + T -ρ)f (S) ≥ T ρf (S * ), which gives the claimed ratio.

Note that the analysis is tight when ρ = 1, for any T , even in the homogeneous case. Consider the following instance, with T agents and n = T 2 resources (i, t), i = 1, . . . , T , t = 1, . . . , T . The value of resource (i, t) is KT at time t, 0 at time t = t. Then at time t exactly T resources ((i, t), i = 1, . . . , T ) have non zero value KT . So an optimal solution gives at time t (i, t) to agent i. The others have value 0 so they can be placed anywhere. Then consider that Algorithm 1 wrongly allocates these other resources, in such a way that no resource is given to the same agent between time t and time t + 1. Then solution S 0 has value T KT (KT at each time step), while

S i has value KT + (T -1)KT = T KT .
Of course, an optimal solution sequence is to allocate (i, t) to i at any time, with value T KT + (T -1)T K = 2T KT -KT . The ratio is 1 2-1/T , which is the claimed ratio for ρ = 1.

One might note that Algorithm 1 could easily perform better on the previous instance, by optimizing the number of resources that are not reallocated between the solutions computed at times t and t + 1. As a matter of fact, we now show that the previous result can be slightly improved in the homogeneous case when the number of agents is bounded. Indeed, in this case a permutation on the agents does not modify the Santa Claus revenue at a given time step. Then we can improve solution S 0 of algorithm 1 by trying to find a permutation minimizing the number of re-allocations when moving from solution Õt to Õt+1 .

To do this, consider two allocations (R t 1 , . . . , R t m ) and (R t+1 1 , . . . , R t+1 m ) of resources to agents at times t and t + 1. Build the complete bipartite graph with 2m vertices a t 1 , . . . , a t m and a t+1 1 , . . . , a t+1 m where the edge (a t j , a t+1 j ) has weight |R t j ∩ R t+1 j |. Consider a perfect matching on this graph. The weight of this matching is the total number of resources that remain to the same agent if we permute the second allocation according to the matching (if (a t j , a t+1 j ) is in the matching the agent j receives resources R t j at time t and R t+1 j at time t + 1). Then computing a perfect matching of maximum weight in this graph gives the permutation which maximizes the number of resources that remain allocated to the same agent. Consider now Algorithm 1 which is the same as Algorithm 1 up to the fact that, when computing S 0 , we sequentially permute solutions Õt in order to get the maximum number of 'non modified' resources from time t -1 to time t. Proposition 1. If A is a ρ-approximation algorithm, then in the homogeneous case Algorithm 1 is a T ρ-ρ/m (T -1)ρ+T -T /m -approximation algorithm. Proof. Given two allocations at times t and t + 1, if we apply a random permutation (all permutations being chosen with the same probability) on the agents at time t + 1, then a resource remains given to the same agent between time t and t + 1 with probability 1/m. So, in average (among all permutations) a fraction 1/m of resources are not re-allocated. A maximum weight perfect matching performs at least as well as average (since it is optimal), so at least a fraction 1/m of resources are not re-allocated in the computed solution. Then Equation (1) becomes:

f (S) ≥ ρ (S * ) + 1 m D(S * ) (3)
Now, summing Equation (2) for i = 1, . . . , T , multiplying by mρ -1 and adding (T -ρ)m times Equation (3) leads to the claimed ratio.

As pointed out in introduction, Max-Min Fair Allocation has an approximation scheme in the homogeneous case, and a r = 1 6+2 √ 10+ -approximation algorithm in the case where (j, i) ∈ { j , 0}. We get the following: Corollary 1. For any > 0, Over-Time Max-Min Fair Allocation is approximable within ratio:

• T -1m 2T -1-T /m - T →∞ ----→ 1 2-1/m -in the homogenenous case; • T r (T -1)r+T - T →∞ ----→ 1 7+2 √
10 -in the case where t (j, i) ∈ { t (j), 0}. So in the homogeneous case the ratio is (1/2 -) if the number of agents is unbounded. For 2 agents, the improvement with the matching technique allows to increase the ratio up to (3/4 -).

Note that for the case where t (j, i) ∈ { t (j), 0}, the ratio is only slightly decreasing from the static case to the over-time setting, from (nearly) 1/12.3 to 1/13.3.

On-line case

In the on-line setting, we only know the instance I t at time t. We have to build the solution at time t without knowledge on what will be the instances at times t > t.

Algorithm 1 is of course no longer possible in the on-line setting. We cannot build the solution sequences, neither compare them at the beginning of the time period. We now devise an on-line algorithm which gives the same approximation ratio as the off-line one when the number of steps is unbounded. Algorithm 2 also uses as subroutine an algorithm A for the static case, and works as follows:

• Apply A on instance I 1 , denote by Õ1 the obtained solution. Set O 1 = Õ1

• For t from 2 to T :

-Apply A on instance I t .

-If the Santa Claus value of this solution is greater than Kn then set O t = Õt .

-Otherwise set O t = O t-1 .

• Output S = (O 1 , . . . , O T ).

Theorem 3. If A is a ρ-approximation algorithm, then Algorithm 2 is a ρ ρ+1 -approximation algorithm.

Proof. Let S * = (O * 1 , ..., O * T ) be an optimal solution sequence. By construction we have:

• 1 (S) ≥ ρ 1 (O * 1 )
, and for any t = 2, . . . , T , D t-1 (S) + t (S) is at least ρ t (O * t ); so D(S) + (S) ≥ ρ (S * ).

• For any t = 2, . . . , T , D t-1 (S) + t (S) ≥ Kn ≥ D t-1 (S * ), so D(S) + (S) ≥ D(S * ).

A combination of these two inequalities with coefficients 1 and ρ gives the claimed ratio.

Note that the analysis is tight when ρ = 1, even with T = 2 and in the homogeneous case. Consider this example with T = 2, K = 1, with 2 agents and 2 resources. At time 1 resources have respective valuations 0,2 while at time 2 they have valuations 2,2. Suppose that the A gives resource 1 to agent 1 and resource 2 to agent 2 at time 1, and vice-versa at time 2. Then the on-line algorithm produces a solution of value 2, while of course maintaining the same resource to each agent gives value 4.

As in the offline case, this trivial example suggests the same improvement for the homogeneous case: when the algorithm applies A on instance I t , it performs the matching technique and permutes the allocation in order to maximize the number of resources not reallocated, leading to Algorithm 2 . Then at least a fraction of 1/m of the resources are not reallocated, and we get the following result (details omited).

Theorem 4. If A is a ρ-approximation algorithm, in the homogeneous case Algorithm 2 is a ρ ρ+1-1/m -approximation algorithm. If m is unbounded, then we get ratio ρ ρ+1 . Note that this is tight for ρ = 1 even in the homogeneous case, even with T = 2: take n = m 2 resources, and K = 1. At time 1, the first m resources have valuation 1, while the others have 0. Suppose that the algorithm chooses to give all the last m 2 -m resources to agent 1. At time 2, all the resources have valuation m. If the algorithm chooses to keep the same solution it gets transition revenue Km 2 , and Santa Claus revenue 1 + m, so the value is Km 2 + m + 1 = m 2 + m + 1. An optimal solution at time 2 gives m resources to each agent, with Santa Claus revenue m 2 . At best the transition revenue if the algorithm chooses such an optimal solution is K(2m -1) = 2m -1. So in all the solution computed by the algorithm has value at most m 2 + 2m. An optimal solution sequence consists of giving the same m resources at time 1 and 2 for each agent, with a value m + m 2 + m 2 . The ratio goes to 1/2 when m goes to infinity.

For the on-line case, we get: Corollary 2. For any > 0, Over-Time Max-Min Fair Allocation in the on-line setting is approximable within ratio:

• 1 2-1/m -in the homogenenous case; • 1 7+2 √
10 -in the case where t (j, i) ∈ { t (j), 0}.

The case With Restrictions

We consider the variant where some resources cannot be allocated to some agents at some point of the time. In that case, for every i ∈ M , j ∈ N , we have l t (j, i) = -∞ if the agent i cannot receive the resource j at time t.

Off-line case

As in the case without restrictions, we would like to build a first solution S 0 with good Santa Claus revenue (S 0 ), and another solution S 1 with good transition revenue D(S 1 ). However, due to the restrictions, the maximal transition revenue between two consecutive instances is not always nK as it was in the case without restrictions. A first question is then to devise, if possible, a procedure which computes a solution sequence maximizing the transition revenue.

To do this, let us consider Algorithm 3 which greedily affects each resource to the agent where it can stay for the longest period of time. More precisely, let Q(j, i, t) be the number of (consecutive) time steps during which resource j can be allocated to agent i starting at time t (Q(j, i, t) = 0 if j cannot be given to i at time t). Then Algorithm 3 initially allocates resource j to the agent i on which it can stay the longer (argmax i Q(j, i, 1)), and keep it as long as possible (i.e. t = Q(j, i, 1) steps). Then at time t + 1, j has to change, and Algorithm 3 allocates it to argmax i Q(j, i, t + 1), and keeps it as long as possible (i.e. Q(j, i, t + 1) steps), and so on.

We have the following property.

Lemma 1. Algorithm 3 outputs a solution sequence with maximum transition revenue.

Proof. We prove that this is true for each resource. Let S be the solution returned by Algorithm 3. Let D t (S, j) be the contribution of the resource j to the transition revenue of S up to time t, and D t (S , j) the contribution for another solution sequence S .

• At t = 1, D t (S, j) = 0 = D t (S , j).

• Suppose that D p (S, j) ≥ D p (S , j) for p = 1, . . . , t, and consider time t+1. If j remains to the same agent i in S between time t and t+1, or if j moves in S between t and t+1, then clearly D t+1 (S, j) ≥ D t+1 (S , j).

Otherwise, let k be the last time at which j moves in S (between solution at time k -1 and k). Since j can stay in S at time t + 1 and not in S, by principle of the algorithm, j has been given to the same agent i in S before time k, it was already given to i at time k -1. Since D k-1 (S, j) ≥ D k-1 (S , j), and between k -1 and k, j moves in S but not in S, we have D k (S, j) ≥ D k (S , j) + K. Then the next modification is between t and t + 1, so D t (S, j) ≥ D t (S , j) + K and then D t+1 (S, j) ≥ D t+1 (S , j).

This is true for each resource, so the result follows.

Then, consider Algorithm 3 which computes two solutions S 1 and S 2 , and outputs the best one. S 1 is the solution given by Algorithm 3, and S 2 = ( Õ1 , ..., ÕT ), where Õt is obtained by applying a subroutine algorithm A for the static case of the Max-Min Fair Allocation problem on instance I t .

Theorem 5. If A is a (polytime) ρ-approximation algorithm for the static case, then Algorithm 3 is a ρ ρ+1 -approximation for the off-line problem with restrictions.

Proof. Let S * = (O * 1 , . . . , O * T ) be an optimal solution sequence. By Lemma 1, D(S 1 ) is maximum so D(S 1 ) ≥ D(S * ). Consequently, f (S 1 ) ≥ D(S * ). We also have t ( Õt ) ≥ ρ • t (O * t ) for every t ∈ {1, ..., T }, so (S 2 ) =

T t=1 t ( Õt ) ≥ ρ • T t=1 t (O * t ) = ρ • (S * ), and this gives f (S 2 ) ≥ ρ • (S * ). This implies ρ • f (S 1 ) + f (S 2 ) ≥ ρ • ( (S * ) + D(S * )) ≥ ρ • f (S * ). Then, (ρ + 1) • f (S) ≥ ρ • f (S * ).
So, S is a ρ ρ+1 -approximate solution sequence.

Let us consider an instance with T = 2 time steps, three agents and three resources. There is no restriction at time 1, but at time 2 resource i cannot be given to agent i. Their respective valuations are 0,0,0 at time 1, and 3,3,3 at time 2. K = 1. Then Algorithm 3 may choose a solution S 1 where resources 1 and 3 are given to agent 2 and resource 2 to agent 1, both at time 1 and 2. It has transition revenue 3, but (S 1 ) = 0. S 2 may give resource i to agent i at time 1, and then at time 2 a solution of value 3 (one resource per agent) but with no transition revenue (because of the constraints). An optimal solution would be to give resource 1 to agent 2, 2 to 3 and 3 to 1 both at time 1 and 2, with value 3 + 3 = 6. The ratio is 1/2 (with ρ = 1).

On-line case

Now, we consider the on-line case where at time t we have not any knowledge on what will be happen at time t > t. Interestingly, while in the unrestricted case we can devise an on-line algorithm with (nearly) the same ratio as in the off-line case, we show that in the case with restrictions being blind makes it impossible to get any algorithm with guaranteed competitive ratio.

Proposition 2. There is no on-line algorithm with bounded competitive ratio even for the homogeneous case with restrictions.

Proof. Consider two agents, one single resource, and K the transition reward. Let us also consider two time-steps, T = 2. At time t = 1, the valuation of the resource is 0 for both agents. The resource could be allocated to any agent. Suppose w.l.o.g. that it is allocated to the first agent by an on-line algorithm. At t = 2, the resource is allowed to be allocated only to the second agent, and has valuation 0 for this agent. Hence, the on-line algorithm is forced to allocate the resource to agent two. In this way, it gets a revenue of 0, while the optimum would be to allocate the resource to the second agent in both timesteps resulting to a total revenue of K.

1-lookahead case

As mentioned in the introduction, in the setting of over-time optimization it seems reasonable to consider limited lookahead: we may have rather good information on what will happen tomorrow or in a few days (time steps) from today, while we may have no clue on what will be the situation one month from now. Motivated by the dramatic difference on what can be obtained in the off-line case (ratio ρ/(ρ + 1), Theorem 5) and in the online case (no competitive ratio), we consider now the situation where we have lookahead 1: at time t when we have to decide the allocation of the resources for instance I t , we know also I t+1 . We show in the following that this is sufficient to get a good (constant) approximation ratio.

We use the same idea as previously, namely at each time we try to maximize either the Santa Claus revenue, or the transition revenue. However, because of the restrictions, we introduce a third option: choose an allocation maximizing the transition revenue between the current instance and the instance that will follow. We choose the third option when the potential transition revenue is at least two times larger than the revenue of the two other options.

Let us now present Algorithm 4, where A is, as previously, an algorithm for the static problem. Also, for every t ∈ {1, . . . , T -1}, P 1 t and P 2 t denote two allocations for I t and I t+1 respectively, such that D t (P 1 t , P 2 t ) is maximum (simply affect a resource to the same agent at time t and t + 1 if possible). We denote by D max t = D t (P 1 t , P 2 t ). The solution S = (O 1 , . . . , O T ) is built in the following way:

• At t = 1: compute Õ1 = A(I 1 ) and two allocations P 1 1 on I 1 and P 2 1 on I 2 . We compute max l 1 ( Õ1 ),

(O 1 = Õ1 if l 1 ( Õ1 ) ≥ D max 1 2 , otherwise O 1 = P 1 1 ).
• At time t = 2, . . . , T -1: Similarly, compute Õt = A(I t ) and two allocations P 1 t on I t and P 2 t on I 2 . We distinguish two cases:

-If at time t -1 we have selected O t-1 = P • At time T , we do the same up to the fact that there is no D max T (no P 1 T , P 2 T ). Theorem 6. If A is a (polytime) ρ-approximation algorithm for the static case, then Algorithm 4 has an approximation ratio of

ρ 4ρ+2-2ρ+1 2 T -1 T →∞ ----→ ρ 4ρ+2 .
Proof. Let V be the set of time-steps where we selected O t = P 2 t-1 or O t = Õt (but not O t = P 1 t ). Note that T ∈ V . In the proof we partition the time period into |V | periods which end at some time t ∈ V . Intuitively, we prove the claimed ratio in each of these sub-periods.

Formally, let u, u + 1, ..., v -1, v be consecutive time-steps such that u, u + 1, ..., v -1 ∈ V , and v ∈ V . Suppose first that u ≤ v -1 (meaning v -1 ∈ V ). For every t ∈ {u, ..., v -1}, we have selected O t = P 1 t . This means that:

• D max t 2 ≥ D max t-1 , implying: D max v-1 ≥ 2D max v-2 ≥ 2 2 D max v-3 ≥ ... ≥ 2 v-u-1 D max u (4) • D max t ≥ 2 t ( Õt ). Since from the previous item D max v-1 ≥ 2 v-t-1 D max t , we have : D max v-1 ≥ 2 v-t t ( Õt ) (5)
Summing Equation (4) for t from u to v -1 we get:

v-1 t=u D max t ≤ D max v-1 v-1 t=u 1 2 v-t-1 = D max v-1 2 - 1 2 v-u-1 (6)
Doing the same with Equation (5) we get:

v-1 t=u t ( Õt ) ≤ D max v-1 v-1 t=u 1 2 v-t = D max v-1 1 - 1 2 v-u (7)
At time v, the algorithm chooses either P 2 v-1 or Õv , with a reward r v at least max

D max v-1 , v ( Õv ), D max v 2
. This reward r v verifies thanks to Equation (6) (and using v -u ≤ T -1)

v t=u D max t ≤ D max v-1 2 - 1 2 v-u-1 + D max v ≤ r v 4 - 1 2 T -2 (8)
Thanks to Equation (7) we have also

v t=u t ( Õt ) ≤ D max v-1 1 - 1 2 v-u + v ( Õv ) ≤ r v 2 - 1 2 T -1 (
f u,v (S * ) ≤ v t=u D max t + t ( Õt ) ρ ≤ r v 4 + 2 ρ - 2 + 1/ρ 2 T -1 (10)
Note that this is also trivially true if u = v. 1 Hence, in each of our sub-periods, we get a reward which is a fraction of at least

1 4+ 2 ρ - 2+1/ρ 2 T -1
of the reward of the optimal solution on the same period. The result follows.

Consider an example with T time steps, such that for t ∈ {1, ..., T -1}, T . Using an exact algorithm A, the solution obtained by the algorithm would be S = (P 1 1 , ..., P 1 T -1 , ÕT ). This would give 1 = u, ..., T -1 ∈ V and T = v ∈ V . The approximation ratio of S in this case tends to 1 6 when T → ∞, indicating that the previous analysis is tight.

From Theorem 6 we get: Corollary 3. For any > 0, Over-Time Max-Min Fair Allocation with restriction and lookahead 1 is approximable within (constant) ratio:

• 1 6 -in the homogenenous case;

• 1 16+4 √ 10 -in the case where t (j, i) ∈ { t (j), 0}.

1 we get rv ≥ max lv( Õv),

D max v 2
, so fv,v(S * ) ≤ (2 + 1 ρ )rv.

Conclusion

We have provided several constant ratio approximation algorithms for an over-time version of the Max-Min Fair Allocation, based on a recently introduced [START_REF] Gupta | Changing bases: Multistage optimization for matroids and matchings[END_REF] model which combines quality and stability of allocations over time. One striking point of this work is the introduction in this setting of the notion of k-lookahead, which allows tradeoffs between on-line and off-line settings. We show an application of this concept for the problem we consider, since 1-lookahead is sufficient to reach constant approximation algorithm for the problem with restriction, while no ratio can be guaranteed in the on-line case. We do believe that this notion is worth being studied for other multiagent optimization problems over time. Another direction that might be studied deals with the agregation function: in this work we made a sum of the value of solutions at each time step, and of the transition revenues. There are many other ways to combine two objectives (bounding the number of modifications, finding Pareto-efficient solutions,. . . ) that could be investigated. Finally, dealing with allocation of resources, other criteria or properties (fairness in average and not step by step, envy-freeness, non manipulability,. . . ) could be also considered.

  presented a configuration linear program for the problem with an integrality gap of Ω 1 √ m . Asadpour and Saberi [AS10] proposed an Ω 1 √ m log 3 (m) -approximation algorithm. This result has been improved by Saha and Srinivasan who gave an Ω log log m √ m log m -approximation algorithm [SS10]. The best result with respect to the number of resources is an Ω 1 n -approximation algorithm running in O(n 1 ), for any > 0 [BCG09, CCK09].

  t-1 for t ∈ {1, ..., T -1} and also max T > D max T -1 and max T > D max

  If not, then we compute max l t ( Õt ),

				1 t-1 , then, at t, we
	compute max D max t-1 , t ( Õt ),	D max t 2	and we choose for O t between
	P 2 t-1 , Õt and P 1 t accordingly.
	-D max t 2	and we choose for O t
	between Õt and P 1 t accordingly.

  9)Let S * = (O * 1 , ..., O * T ) be an optimal solution. Let us denote f u,v (S) =

v t=u (D t (S * ) + t (O * t )) (with by convention D T (S * ) = 0). Since D t (S * ) ≤ D max t and t (O * t ) ≤ t( Õt) ρ , we have:

Acknowledgements

This work has been supported by the project ANR-14-CE24-0007-01 "CoCoRICo-CoDec" funded by ANR. It benefited also from the support of the FMJH program "Gaspard Monge in optimization and Operation Research" and from the support to this program from EDF, via the project 2016-1760H/C16/1507 "Stability versus Optimality in Dynamic Environment Algorithmics".


Sylvain Conchon

Amit Goel

Sava Krstić

Rupak Majumdar

Mattias Roux

FAR-Cubicle -A new reachability algorithm for Cubicle

We present a fully automatic algorithm for verifying safety properties of parameterized software systems. This algorithm is based on both IC3 and Lazy Annotation. We implemented it in Cubicle, a model checker for verifying safety properties of array-based systems. Cache-coherence protocols and mutual exclusion algorithms are known examples of such systems. Our algorithm iteratively builds an abstract reachability graph refining the set of reachable states from counter-examples. Refining is made through counter-example approximation. We show the effectiveness and limitations of this algorithm and tradeoffs that results from it.

Introduction

We describe FAR (Forward Abstracted Reachability), an algorithm for fully automatic verification of parameterized software systems. A parameterized system describes a family of programs such as cache coherence protocols where the number of processes involved can change but the algorithm handling their behaviour is the same for all of them. Thus, the parameter allows to talk about these algorithms without knowing the actual number of processes that will be involved and then to prove its safety regardless of this number.

Safety properties state that "nothing bad happens" in our parameterized system. Verifying them can be reduced to finding an invariant of it. Finding an invariant can be hard (and even undecidable [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF]). The standard approach to find one is to find a formula Φ such that Φ is an inductive invariant of the system (i.e. the initial state of the system satisfies Φ and taking a transition from a state satisfying Φ leads to another state satisfying Φ).

In this paper we describe an algorithm for the automatic construction of inductive invariants for array-based systems (Section 2). This algorithm, based on both IC3 [START_REF] Bradley | Sat-based model checking without unrolling[END_REF] and Lazy Abstraction [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF], builds an inductive invariant by unwinding a graph (Section 3) building a forward abstract reachability of our system. This unwinding is described as a set of non deterministic rules. We then provide an implementation in Cubicle [START_REF] Mebsout | Inférence d'invariants pour le model checking de systèmes paramétrés[END_REF], [START_REF] Conchon | Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems -Tool Paper[END_REF], [START_REF]Invariants for finite instances and beyond[END_REF] (Section 5) of these rules and test its effectiveness on several cache coherence protocols (Section 6).

Array-based Systems

An array-based system is described in [START_REF] Ghilardi | Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis[END_REF] as first-order logic formulas on arrays. Such a system can be described as a set of basic types, a set X of system variables associated to type (built as usual with basic types and standard constructions), a formula init representing the initial states and a set ∆ of transition rules τ i (X, X ′ ) (X ′ is the set X where all the variables are primed which represents the next state reached after the application of a transition). Since we work on parameterized programs, our arrays are indexed by an infinite type proc.

We describe the Dekker mutual exclusion algorithm as an array-based system. Each process has two boolean variables, want (stating that the process wants to enter in critical section or not) and crit (stating that the process is in critical section or not). There is a global variable turn of type proc that tracks which process can go into the critical section. Since we work in the array-based systems fragment, we represent the local variables as arrays indexed by processes and containing booleans. The set X contains two arrays, want[proc] : bool and crit[proc] : bool and the global variable turn : proc. Initially, no process is or wants to be in critical section. Three transitions can be triggered, one to require an access to the critical section, one to enter in it and one to exit it. According to the previous description, we write this algorithm as in Figure 1.

Since we focus on safety problems (nothing bad happens), we need to define what is considered as bad states. In that case these states would be defined with the following formula :

unsaf e ≡ ∃p 1 , p 2 . p 1 = p 2 ∧ crit[p 1 ] ∧ crit[p 2 ]
Our goal is then to prove that no state represented by unsaf e is reachable from init (which can be seen as : there exists no path init = X 0 p1 -→ X 1 ... -→ . . . pn -→ X n = unsaf e with p i ∈ {req, enter, exit}). To do so on parameterized system, one of the main algorithm came from Ghilardi et al. with MCMT [START_REF] Ghilardi | Towards SMT model checking of array-based systems[END_REF] and builds the set of all reachable states by backward reachability (starting, then, from the unsafe state)

turn : proc crit[proc] : bool want[proc] : bool init : ∀p. ¬want[p] ∧ ¬crit[p] req : ∃p. ¬want[p] want ′ [p] enter : ∃p. want[p] ∧ turn = p crit ′ [p] exit : ∃p 1 , p 2 . crit[p 1 ] ¬want ′ [p 1 ] ∧ ¬crit ′ [p 1 ] ∧turn ′ = p 2 Figure 1
. Dekker algorithm as array-based system and checks if this set contains an initial state. In this paper, we implement a different algorithm which offers a wider range of possibilities in terms of reachabilty construction.

Program unwinding

This algorithm starts also from the unsaf e formula but tries to build an invariant of the system that does not contain it. Before going into details, we give a brief explanation. This invariant is iteratively built as an inductive invariant Θ that does not contain unsaf e :

• if Θ ∧ ∆ ∧ ¬Θ ′ is unsatisfiable then we found an inductive invariant • if Θ ∧ ∆ ∧ ¬Θ ′ is
satisfiable, our candidate invariant is not inductive and we try to refine it until we either discover that there is no such refinement or we find some.

For Dekker's algorithm, for example, let's take

Θ = ¬unsaf e = ∀p 1 = p 2 .¬crit[p 1 ] ∨ ¬crit[p 2 ] : • Θ ∧ ∆ ∧
¬Θ ′ is satisfiable (if we take, for example, the following state :

ϕ 1 = crit[p 1 ] ∧ want[p 2 ] ∧ turn = p 2 ∧ ¬crit[p 2 ], ϕ 1 |= Θ but if we apply enter to it we obtain the state ϕ 2 = crit[p 1 ] ∧ crit[p 2 ] ∧ . . . and ϕ 2 |= Θ.) • We need to create Θ ′ = Θ ∧ ρ which is a refinement of Θ that does not contain ϕ 1 .
To do so, we build an unwinding of the algorithm as a quadruple V, E, W, B , where: We call

V ǫ = {v ∈ V, ǫ * -→ v ∈ E} (i.
e. the set of vertices that are linked to the root).

W(v) |= τ W(v ′ ) ≡ W(v) ∧ τ |= W(v ′ )
The idea behind this unwinding it that if we manage to create a graph G of a system S = init, ∆ where every vertex in V ǫ does not contain a bad part and from which no more transition can be taken, then the disjunction of their worlds (Θ = v∈V ǫ W(v)) is an invariant of the system (init |= Θ and Θ |= ∆ Θ).

We now propose a set of non-deterministic rules for building this unwinding. Let X, init, ∆, unsaf e be an array-based system. Initially, G is defined as follow :

-V = {ǫ, ω, β} -E = ∅
unwinding works by the non-deterministic application of the following rules :

Rule 1 (Extend). If ∃v ∈ V, τ ∈ ∆. W(v) |= τ ⊤ and ∄v ′ .v τ -→ v ′ ∈ E then E = E ∪ {v τ -→ β} Rule 2 (Refine). If ∃v, v ′ ∈ V, τ ∈ ∆. v τ -→ v ′ ∈ E, B(v ′ ) = ⊥, ∃ϕ.W(v) |= τ ϕ and ϕ |= ¬B(v ′ ) then we create a new vertex v ′′ such that W(v ′′ ) = W(v ′ ) ∧ ϕ and E = E ∪ {v τ -→ v ′′ } \ {v τ -→ v ′ } Rule 3 (Propagate). If ∃v, v ′ ∈ V, τ ∈ ∆. v τ -→ v ′ ∈ E, B(v ′ ) = ⊥, ∃γ. γ |= W(v), and γ |= τ B(v ′ ) then B(v) ← γ Rule 4 (Cover). If ∃v, v ′ ∈ V, τ ∈ ∆. v τ -→ v ′ ∈ E, v ′′ ∈ V such that W(v ′′ ) |= W(v ′ ) and W(v) |= τ W(v ′′ ) then E = E ∪ {v τ -→ v ′′ } \ {v τ -→ v ′ } Rule 5 (Sink). If ∃v ∈ V, τ ∈ ∆. W(v) |= τ ⊥ and ∄v ′ .v τ -→ v ′ ∈ E then E = E ∪ {v τ -→ ω}
S is safe if and only if no rule can be applied to G, an unwinding S and B(ǫ) = ⊥. Intuitively, since no more transitions can be taken and all the vertices connected to the root are not bad, root will never be able to lead to unsafe.

Example

The example shown in Figure 2 describes the first four runs of the unwinding on the Dekker's algorithm (we decided not to show ω since it just serves as a sink for the transitions that can not be taken from a vertex) :

(a) initially, the only rule that can be applied is the Extend rule from ǫ (with W(ǫ) ≡ init ≡ ∀p. ¬want[p] ∧ ¬crit[p]) with req; (b) we can only apply, then, the Refine rule because init req unsaf e ≡ B(β). We create a new vertex called v 1 ; (c) we can chose, here, to apply the Extend rule from the new vertex with any transition. We chose to take the transition req; (d) W(v 1 ) req B(β) and W(v 1 ) |= req W(v 1 ) so we can apply the cover rule; (e) if we keep applying these rules, we reach a fixpoint at the third created vertex.

Implementation

We implemented this unwinding in Cubicle 1 . To do so we had to chose a deterministic strategy depending on multiple parameters :

• the order in which the rules are applied;

• which vertex and transition should be taken for the Extend rule;

• which formula ϕ should we take for the Refine rule;

• which formula γ should we take for the Propagate rule;

• which vertex v ′′ should we take for the Cover rule.

Based on this problems, we came out with the following algorithm (we write v = (W, B) to denote the fact that W(v) = W and B(v) = B) :

Algorithm 1 Graph unwinding -main loop procedure FAR-CUBICLE(S = init, ∆, unsaf e ) ǫ ← (init, ⊥) β ← (⊤, unsaf e) ω ← (⊥, ⊥) V ← {ǫ, β, ω} E = ∅ PUSH(Q, ǫ) ⊲ Q is a priority queue while NOT_EMPTY(Q) do v ←POP(Q) for all τ ∈ ∆ do if W(v) |= τ ⊤ then E = E ∪ {v τ -→ β} UNWIND(v τ -→ β) else E = E ∪ {v τ -→ ω} return safe
This algorithm picks a vertex v from a priority queue (which initially contains only the root vertex) and for all the transitions, adds an edge to the graph from this transition to the sink vertex if the formula represented by v is inconsistent with the transition or to the unsafe vertex if the transition 1. cubicle.lri.fr/far Algorithm 2 Graph unwinding -unwinding procedure

procedure UNWIND(v τ -→ v ′ ) if B(v) = ⊥ ∧ B(v ′ ) = ⊥ then switch CLOSE(v τ -→ v ′ ) do case Covered v" E = E ∪ {v τ -→ v ′′ } \ {v τ -→ v ′ } UNWIND(v τ -→ v ′′ ) case Bad ϕ if v = ǫ then return unsafe else B(v) ← ϕ for all u τ ′ -→ v do UNWIND(u τ -→ v) case Refined v" E = E ∪ {v τ -→ v ′′ } \ {v τ -→ v ′ } PUSH(Q, v ′′ )
can be taken. If the edge goes to a vertex v ′ that is not the sink, the procedure UNWIND is called on it. This procedure checks if B(v) = ⊥ or if the B(v ′ ) = ⊥ and if both these conditions are false it tries to close the edge. An edge is closed if :

• W(v) |= τ B(v ′ ).
In this case, all the edges coming to it must be unwinded again;

• there exists another vertex v ′′ such that v |= τ v ′′ and ⊑ ′′ |= W(v ′ ). In this case, the edge from v to v ′ is deleted and a new one from v to v ′′ is created and unwinded;

• W(v) |= τ B(v ′ ). A counter example ϕ is found a new node v ′′ is created with W(v ′′ ) ≡ W(v ′ ) ∧ ϕ and pushed in the queue.
If all the edges are closed and the queue is empty, the system is safe. If the propagation of bad parts reaches the root vertex, the system is unsafe.

As we can see on line 5 of the CLOSE procedure, the formula γ chosen for the Propagate rule is the pre image of the bad formula of the vertex v ′ . Also, on line 7 of the CLOSE procedure, the formula ϕ chosen for the Refine rule is a generalization of the negation of the bad part of the vertex v ′ . These are, of course, implementation choices. Other implementation could involve model finding, interpolants ... In our case, the generalization is a naive one consisting in taking the smallest part of the resulting formula that was Algorithm 3 Graph unwinding -closing edge procedure

1: procedure CLOSE(v τ -→ v ′ ) 2: if ∃v ′′ . W(v ′′ ) |= W(v ′ ) ∧ W(v) |= τ W(v ′′ ) then 3: return Covered v ′′ 4: else if W(v) |= τ B(v ′ ) then 5:
return Bad PRE(B(v ′ ), τ ) 6:

else 7: v ′′ ← (W(v ′ ) ∧ GENERALIZE(¬B(v ′ )), ⊥) 8:
return Refined v" not already taken and that still satifies the conditions of the Refine rule.

Benchmarks

We compared our implementation to the backward reachability algorithm already implemented in Cubicle (without the invariants inference implemented with BRAB [START_REF] Mebsout | Inférence d'invariants pour le model checking de systèmes paramétrés[END_REF], [START_REF]Invariants for finite instances and beyond[END_REF]) and obtained the following results (the timeout was set to 5 minutes and the α version uses an abstraction engine related to the approximation implemented in BRAB to get better refinement): As we can see in this table, this algorithm is competitive and even better when good refinements can be found.

Related Works

There has been a lot of research in software model checking and Property-Driven Reachability. This type of algorithm was first introduced by Bradley in [START_REF] Bradley | Sat-based model checking without unrolling[END_REF] and McMillan revisited his Lazy Annotation (which shares similarities with PDR algorithms) in [START_REF] Mcmillan | Lazy annotation revisited[END_REF] or the recent approach from Cimatti et al. [START_REF] Cimatti | Infinite-state invariant checking with IC3 and predicate abstraction[END_REF] and Z3 with a PDR approach in [START_REF] Hoder | Generalized property directed reachability[END_REF] and [START_REF] Hoder | µZ-an efficient engine for fixed points with constraints[END_REF]. Even though some of these tools are supposed to work on parameterized systems, we were either not able to find them or they were not able to prove our examples.

Conclusion

We presented the problem of parameterized protocol verification and gave an algorithm to automatically do it. This new algorithm was implemented in Cubicle and successfully applied to many cache coherence protocols. This algorithm could be improved with a better generalisation engine (allowing to explore less vertices), an incremental approach (the parameterized aspect of our language makes it hard to remember the state of our SMT solver). Other optimizations could involve a novel way of refining our formulas (it is clear that the best refinements are inductive invariants but it is still an open problem as how to find these). Some optimizations were not documented in this article such as • Set-theoretic test : some formulas are trivially unsatisfiable and don't require call to the SMT solver;

• relevant instantiations : handling universally quantified formulas can lead to multiple useless instantiations that are trivially unsatisfiable or valid and do not help the SMT solver to solve the whole formula. This optimization allows to gain a significant time in the SMT solver.

selecting good bads : handling bad parts from the ones with less processes involved allows to control the number of processes that have to be instantiated when checking the satisfiability of formulas. It is mandatory, if we want to have a competitive algorithm, that we handle the bad parts cleverly (this can be done in the priority queue).

•

  V, E is a rooted graph with edges labeled by transitions from ∆; • W associates a formula (called world of the vertex) to each vertex; B associates a formula (called bad part of the vertex) to each vertex. This graph contains three initial vertices : ǫ : the root vertex, W(ǫ) = init and B(ǫ) = ⊥; β : the unsafe vertex, W(β) = ⊤ and B(β) = unsaf e; ω : the sink vertex, W(ω) = ⊥ and B(ω) = ⊥.

Figure 2 .

 2 Figure 2. First four steps of the unwinding and final state of the graph (sink rules are not shown)


Xavier Bultel

Radu Ciucanu

Matthieu Giraud

Pascal Lafourcade

Secure Matrix Multiplication with MapReduce

Keywords: Communication cost: 3n 2, Communication cost: 2n 2, Computation cost: C : 3n 3, Communication cost: 4n 3, Computation cost: C Communication cost: n 2, Communication cost: n 2, Computation cost: 2n 2, Computation cost: (1 + C Communication cost: 2n 3, Communication cost: 2n 3, Communication cost: 2n 3

The MapReduce programming paradigm allows to process big data sets in parallel on a large cluster of commodity machines. The MapReduce users often outsource their data and computations to a public cloud provider. We focus on the fundamental problem of matrix multiplication, and address the inherent security and privacy concerns that occur when outsourcing to a public cloud. Our goal is to enhance the two state-of-the-art algorithms for MapReduce matrix multiplication with privacy guarantees such as: none of the nodes storing an input matrix can learn the other input matrix or the output matrix, and moreover, none of the nodes computing an intermediate result can learn the input or the output matrices. To achieve our goal, we rely on the well-known Paillier's cryptosystem and we use its partially homomorphic property to develop efficient algorithms that satisfy our problem statement. We develop two different approaches called Secure-Private (SP) and Collision-Resistant-Secure-Private (CRSP), and compare their trade-offs with respect to three fundamental criteria: computation cost, communication cost, and privacy guarantees. Finally, we give security proofs of our protocols. Computation cost: 2n 2 . Computation cost: (C + + 2C E )n 2 . Computation cost: 2C E n 2 . Communication cost: 2n 2 .

Introduction

MapReduce [START_REF] Dean | Mapreduce: Simplified data processing on large clusters[END_REF] is a programming paradigm for processing big data sets. The MapReduce programs are automatically parallelized and executed on a large cluster of commodity machines. The users need to specify two functions (map and reduce), whereas the system takes care of several aspects such as partitioning the data, scheduling the program's execution across the machines, handling machine failures, and managing the communication between different machines.

In practice, the MapReduce users often outsource their data and computations i.e., they rent storage and computing resources from a public cloud provider (e.g., Google Cloud Platform, Amazon Web Services, Microsoft Azure). On the positive side, using a public cloud makes the big data processing accessible to users who cannot afford to build their own clusters. However, outsourcing the data and computations to a public cloud involves inherent security and privacy concerns. Indeed, the MapReduce users are no longer in control of their data, which may be communicated over an untrusted network and processed on some untrusted machine, where malicious public cloud users may breach their privacy.

We address the fundamental problem of MapReduce matrix multiplication from a privacy-preserving perspective i.e., we develop algorithms for which the public cloud cannot learn neither the input nor the output data. The matrix multiplication is also the original purpose for which the Google implementation of MapReduce was created. Such multiplications are needed by Google in the computation of the PageRank algorithm. The standard algorithms for MapReduce matrix multiplication use either two or one communications rounds, and moreover, their communication and computation cost analysis have been throughly analysed in Chapter 2 of [START_REF] Leskovec | Mining of Massive Datasets[END_REF].

Problem statement. Two compatible matrices M and N are stored in the distributed file system of some public cloud provider. A user (who does not know the matrices M and N ) wants their product P = M × N . We assume that the matrix M is initially spread over a set M of nodes, each of them storing a chunk of M i.e., a set of elements of M . Similarly, the matrix N is initially spread over a set N of nodes. In the case of one round (Figure 1), the final result P is spread over a set R of nodes before it is sent to the user's nodes P; in the case of two rounds (Figure 2), intermediate results are spread over a set R 1 of nodes and the final result P is spread over a set R 2 of nodes before it is sent to the user's nodes P. We expect the following properties:

1. the user cannot learn any information about input matrices M and N , 2. none of the nodes in M can learn any information about matrices N and P , 3. none of the nodes in N can learn any information about matrices M and P , 4. none of the nodes in R (for one round), or in R 1 and R 2 (for two rounds) can learn any information about matrices M , N , and P . The second and third condition state that none of the nodes storing an input matrix can learn the other input matrix or the output matrix, whereas the fourth condition states that none of the public cloud's nodes storing intermediate or final result can learn the input or the output matrices.

Two 2n 2 + (C × + C + )n 3 n 3 + 3n 2 None One 2n 3 + n 2 Secure-Private (SP) Two (C + + 2C E )n 2 + (2C × + 2C exp + C D )n 3 3n 3 + 4n 2 All † One (1 + C E )n 2 + (C × + C exp )n 3 2n 3 + n 2 Only (1)-(3) CRSP Two 2C E n 2 + (4C E + 7C × + 2C D + 2C exp )n 3 4n 3 + 3n
Notice that a straightforward solution would require the use of a fully homomorphic encryption scheme e.g., Gentry [START_REF] Gentry | Fully homomorphic encryption using ideal lattices[END_REF]. Indeed, a fully homomorphic encryption scheme would allow to execute directly in the encrypted domain all multiplications and additions needed for computing a matrix multiplication. Unfortunately, such an approach would solve our problem only from a theoretical point of view because making a fully homomorphic encryption scheme work in practice remains an open question (as noted e.g., in [START_REF] Gentry | Fully homomorphic encryption using ideal lattices[END_REF]).

Summary of contributions. We propose algorithms that extend the two standard algorithms for MapReduce matrix multiplication (as found in Chapter 2 from [START_REF] Leskovec | Mining of Massive Datasets[END_REF]) while ensuring data privacy, and remaining efficient from both computational and communication points of view.

Our technique is based on the well-known Paillier's cryptosystem [START_REF] Paillier | Public-key cryptosystems based on composite degree residuosity classes[END_REF], which is partially homomorphic i.e., it is additively homomorphic. The integration of this cryptosystem into the standard MapReduce algorithms for matrix multiplication is not trivial. Indeed, Paillier's cryptosystem does not allow to execute directly in the encrypted domain the multiplications that are needed for matrix multiplication.

Assuming that the public cloud's nodes do not collude, we design the Secure-Private (SP) approach which satisfies all afeorementionned conditions. Indeed, we show that if nodes N collude with nodes R 2 , then R 2 can retrieve all elements of matrix N . The second approach designs a sophisticated algorithm that relies on additional communications to overcome these risks of collusions; this idea led to our Collision-Resistant-Secure-Private (CRSP) approach, which satisfies all conditions enumerated in the problem statement.

We summarize in Figure 3 the trade-offs between computation cost, communication cost, and privacy guarantees for our two approaches and the two standard MapReduce algorithms for matrix multiplication. In our communication cost analysis, we measure the total size of the data that is emitted from a map or reduce node, and the additional data that needs to be communicated to realize the interactive multiplication in the encrypted domain. The CRSP approach satisfies all privacy constraints and resists to collusions, but requires a communication overhead.

Related work. Chapter 2 of [START_REF] Leskovec | Mining of Massive Datasets[END_REF] presents an introduction to the MapReduce paradigm. In particular, it includes the two MapReduce algorithms for matrix multiplication that we enhance with privacy preservation. The security and privacy concerns of MapReduce have been summarized in a recent survey [START_REF] Derbeko | Security and privacy aspects in mapreduce on clouds: A survey[END_REF]. To the best of our knowledge, no existing work has addressed the problem of matrix multiplication, on which we focus in this paper. More precisely, the state-of-the-art techniques for execution of MapReduce computations while preserving privacy focus on problems such as word search [START_REF] Blass | PRISM -privacy-preserving search in mapreduce[END_REF][START_REF] Dolev | Private and secure secret shared mapreduce[END_REF], information retrieval [START_REF] Mayberry | PIRMAP: efficient private information retrieval for mapreduce[END_REF][START_REF] Dolev | Private and secure secret shared mapreduce[END_REF], count queries [START_REF] Triet | Epic: Efficient privacy-preserving counting for mapreduce[END_REF][START_REF] Dolev | Private and secure secret shared mapreduce[END_REF], equijoins [START_REF] Dolev | Private and secure secret shared mapreduce[END_REF], and range queries [START_REF] Dolev | Private and secure secret shared mapreduce[END_REF]. The general goal of these works is to execute MapReduce computations such that the public cloud cannot learn the data. This is precisely our goal too, but for a fundamentally different task i.e., matrix multiplication.

Distributed matrix multiplication has been thoroughly investigated in the secure multi-party computation model (MPC) [START_REF] Du | Privacy-preserving cooperative statistical analysis[END_REF][START_REF] Amirbekyan | A new efficient privacy-preserving scalar product protocol[END_REF][START_REF] Wang | Towards empirical aspects of secure scalar product[END_REF][START_REF] Dumas | Private multi-party matrix multiplication and trust computations[END_REF], whose goal is to allow different nodes to jointly compute a function over their private inputs without revealing them. The aforementioned works on secure distributed matrix multiplication have different assumptions compared to our MapReduce framework: (i) they assume that nodes contain entire vectors, whereas the division of the initial matrices in chunks as done in MapReduce does not have such assumptions, and (ii) in MapReduce, the functions specified by the user [START_REF] Dean | Mapreduce: Simplified data processing on large clusters[END_REF] are limited to map (process a key/value pair to generate a set of intermediate key/value pairs) and reduce (merge all intermediate values associated with the same intermediate key), and the matrix multiplication is done in one or two communication rounds [START_REF] Leskovec | Mining of Massive Datasets[END_REF]; on the other hand, the works in the MPC model assume arbitrary numbers of communication rounds, relying on more complex functions than map and reduce.

Moreover, generic MPC protocols [START_REF] Ma | Secure multi-party protocols for privacy preserving data mining[END_REF][START_REF] Cramer | Multiparty computation from threshold homomorphic encryption[END_REF] allow several nodes to securely evaluate any function. Such protocols could be used to secure MapReduce. However, due to their generic nature, they are inefficient and require a lot of interactions between parties. Our goal is to design an optimized protocol to secure MapReduce.

Paper organization. We introduce the needed cryptographic tools in Section 2 and the standard algorithms for matrix multiplication with MapReduce in Section 3. We present our SP algorithm for secure matrix multiplication with MapReduce and its analysis in Section 4, and the CRSP algorithm in Section 5. We prove the security of our algorithms in Section 6. We outline conclusion and future work in Section 7.

Cryptographic Tools

We start by recalling the definition of negligible function used in security proofs and definition, and security requirements of public key cryptosystems. [START_REF] Bellare | Public-key encryption in a multi-user setting: Security proofs and improvements[END_REF] if for any probalistic polynomial time adversary A, the difference between 1 2 and the probability that A wins the IND-CPA experiment in Figure 4 is negligible, where the oracle E pk (LR b (•, •)) takes (m 0 , m 1 ) as input and returns E pk (m b ). The standard definition of CPA experiment allows the adversary to call this oracle only one time. However, in [START_REF] Bellare | Public-key encryption in a multi-user setting: Security proofs and improvements[END_REF] authors prove that the two definitions of CPA security are equivalent using an hybrid argument.

A PKE scheme Π = (G, E, D) is indistinguishable under chosen-plaintext attack (IND-CPA)
In the following, we require an additive homomorphic encryption scheme to secure the computation of matrix multiplication with MapReduce. There exist several schemes that have this property [START_REF] Okamoto | A new public-key cryptosystem as secure as factoring[END_REF][START_REF] Paillier | Public-key cryptosystems based on composite degree residuosity classes[END_REF][START_REF] Damgård | A generalisation, a simplification and some applications of paillier's probabilistic public-key system[END_REF][START_REF] Naccache | A new public key cryptosystem based on higher residues[END_REF]. We choose Paillier's public key encryption scheme [START_REF] Paillier | Public-key cryptosystems based on composite degree residuosity classes[END_REF] to illustrate specific required homomorphic properties. Our results and proofs are generic, since any other encryption schemes having such properties can be used instead of Paillier's scheme.

Exp IND-CPA Π,A (η): b $ ← {0, 1} (pk, sk) ← G(η); b * ← A E pk (LR b (•,•)) (pk) return (b = b * ) Figure 4: IND-CPA experiment [2]. A B Knows c 1 = E pk A (m 1 ) and c 2 = E pk A (m 2 ) Picks two randoms δ 1 , δ 2 ∈ Z n D sk A (α 1 ) = m 1 + δ 1 and D sk A (α 2 ) = m 2 + δ 2 α 1 ,α 2 ←---α 1 = c 1 × E pk A (δ 1 ) and α 2 = c 2 × E pk A (δ 2 ) β = E pk A ((m 1 + δ 1 ) × (m 2 + δ 2 )) β -→ E pk A (m 1 × m 2 ) = β E pk A (δ 1 ×δ 2 )×c δ 2 1 ×c δ 1 2

Paillier's Scheme

Paillier's scheme is an IND-CPA scheme [START_REF] Sako | Goldwasser-micali encryption scheme[END_REF], we recall the key generation, the encryption and decryption algorithms.

Key Generation. We denote by Z n , the ring of integers modulo n and by Z * n the set of inversible elements of Z n . The public key pk of Paillier's encryption scheme is (n, g), where g ∈ Z * n 2 and n = p × q is the product of two prime numbers such that gcd(p, q) = 1.

The corresponding private key sk is (λ, µ), where λ is the least common multiple of p -1 and q -1 and µ = (L(g λ mod n 2 )) -1 mod n, where L(x) = x-1 n .

Encryption Algorithm. Let m be a message such that m ∈ Z n . Let g be an element of Z * n 2 and r be a random element of Z * n . We denote by E pk the encryption function that produces the ciphertext c from a given plaintext m with the public key pk = (n, g) as follows: c = g m × r n mod n 2 . Decryption Algorithm. Let c be the ciphertext such that c ∈ Z n 2 . We denote by D sk the decryption function of the plaintext c with the secret key sk = (λ, µ) defined as follows: m = L c λ mod n 2 × µ mod n .

Homomorphic Properties

Paillier's cryptosystem is a partial homomorphic encryption scheme. We present these properties.

Homomorphic Addition of Plaintexts. Let m 1 and m 2 be two plaintexts in Z n . The product of the two associated ciphertexts with the public key pk = (n, g),

denoted c 1 = E pk (m 1 ) = g m 1 × r n 1 mod n 2 and c 2 = E pk (m 2 ) = g m 2 × r n 2 mod n 2 , is the encryption of the sum of m 1 and m 2 . E pk (m 1 ) × E pk (m 2 ) = c 1 × c 2 mod n 2 = (g m 1 × r n 1 ) × (g m 2 × r n 2 ) mod n 2 = g m 1 +m 2 × (r 1 × r 2 ) n mod n 2 = E pk (m 1 + m 2 mod n) .
We also remark that:

E pk (m 1 ) E pk (m 2 ) = E pk (m 1 -m 2 ).
Specific Homomorphic Multiplication of Plaintexts. Let m 1 and m 2 be two plaintexts in

Z n and c 1 ∈ Z * n 2
be the ciphertext of m 1 with the public key pk (c 1 = E pk (m 1 )). With Paillier's scheme, c 1 raised to the power of m 2 is the encryption of the product of the two plaintexts m 1 and m 2 .

E pk (m 1 ) m 2 = c m 2 1 mod n 2 = (g m 1 × r n 1 ) m 2 mod n 2 = (g m 1 •m 2 × (r m 2 1 ) n ) mod n 2 = E pk (m 1 × m 2 mod n) .
Interactive Homomorphic Multiplication of Ciphertexts. Cramer et al. [START_REF] Cramer | Multiparty computation from threshold homomorphic encryption[END_REF] show that an interactive protocol makes possible to perform multiplication over ciphertexts using additive homomorphic encryption schemes as Paillier's encryption scheme. More precisely, Bob knows two ciphertexts c 1 , c 2 ∈ Z * n 2 of the plaintexts m 1 , m 2 ∈ Z n with the public key of Alice, he wants to obtain the cipher of the product of m 1 and m 2 without revealing to Alice m 1 and m 2 . For this Bob has to interact with Alice as described in Figure 5. Bob first picks two randoms δ 1 and δ 2 and sends to Alice

α 1 = c 1 × E pk A (δ 1 ) and α 2 = c 2 × E pk A (δ 2 )
. By decrypting respectively α 1 and α 2 , Alice recovers respectively m 1 + δ 1 and m 2 + δ 2 . She sends to Bob

β = E pk A ((m 1 + δ 1 ) × (m 2 + δ 2 )). Then, Bob can deduce the value of E(m 1 • m 2 ) by computing: β E pk A (δ 1 ×δ 2 )×c δ 1 1 ×c δ 2 2 , since E pk A ((m 1 + δ 1 ) × (m 2 + δ 2 )) = E pk A (m 1 × m 2 ) × E pk A (m 1 × δ 2 ) × E pk A (m 2 × δ 1 ) × E pk A (δ 1 × δ 2 ).

Matrix Multiplication

Let M and N be two compatible matrices, respectively of size a × b and b × c. We denote by m ij the element of the matrix M which is in the i-th row and the j-th column with 1 ≤ i ≤ a and 1 ≤ j ≤ b. In the same way, we denote by n jk the element of the matrix N which is in the j-th row and k-th column with 1 ≤ j ≤ b and 1 ≤ k ≤ c. Moreover, we denote by P the product M × N . The First Map Function (Figure 6(a)). 2R-M1 consists of rewriting each element of matrices M and N in the form of key-value pairs such that elements needed to compute each element of the product M × N share the same key. Hence, nodes M create pairs of the form (j, (M, i, m ij )), where 1 ≤ i ≤ a and 1 ≤ j ≤ b and send them to the set of nodes R 1 . In the same way, nodes N create pairs of the form (j, (N, k, n jk )) where 1 ≤ j ≤ b and 1 ≤ k ≤ c and send them to R 1 . We stress that M and N in the values are the names of matrices, that can be encoded with a single bit, and not the matrices themselves.

Two MapReduce Rounds

The First Reduce Function (Figure 6(b)). To compute elements of P , the first step is to compute each product m ij × n jk for 1 ≤ j ≤ b. Hence 2R-M1 executed on R 1 creates key-values pairs and sends them to R 2 where for a key (i, k) with 1 ≤ i ≤ a and 1

≤ k ≤ c, values are m ij × n jk for 1 ≤ j ≤ b.
The Second Map Function. In this second round, 2R-M2 is the identity function, hence we further omit it from the analysis of the computation and communication costs.

The Second Reduce Function (Figure 6(c)). It is executed by nodes of type R 2 and aggregates all values with the same key to obtain key-value pairs ((i, k), b j=1 m ij × n jk ). Then R 2 sends results to P.

One MapReduce Round

The matrix multiplication with one MapReduce round is composed of two functions: the Map function (1R-M) and the Reduce function (1R-R).

The Map Function (Figure 7(a)). It is executed on M and N , and creates the sets of matrix elements that are needed to compute each element of the product M × N . Since an element of M or N is used for many elements of the final result, the output of the Map function sent to R gives key-value pairs where keys are (i, k) where i is the row of M and k is the column of N , and values are of the form (N, j, m ij ) and (N, j, n jk ).

The Reduce Function (Figure 7(b)). With the previous Map function, we obtain for a key (i, k) a set of values of the form (M, j, m ij ) and (N, j, n jk ) with 1 ≤ j ≤ b. Then, 1R-R executed by R computes the sum of m ij × n jk Input: (key, value) // key: id of a chunk of M or N // value: collection of (i, j, m ij ) // or (j, k, n jk )

foreach (i, j, m ij ) ∈ value do emit M→R 1 (j, (M, i, m ij )) foreach (j, k, n jk ) ∈ value do emit N →R 1 (j, (N, k, n jk ))
(a) 1st Map function (2R-M1).

Input: (key, value) // key: id of a chunk of M or N // value: collection of (i, j, m ij ) // or (j, k, n jk )

foreach (i, j, m ij ) ∈ value do emit M→R 1 (j, (M, i, E pk p (m ij ))) foreach (j, k, n jk ) ∈ value do emit N →R 1 (j, (N, k,(n jk + τ jk , E pk r 2 (τ jk )))) (d) 1st Map function (2R-SP-M1).
Input: (key, value) // key: id of a chunk of M or N // value: collection of (i, j, m ij ) // or (j, k, n jk )

foreach (i, j, m ij ) ∈ value do emit M→R 1 (j, (M, i, E pk p (m ij ))) foreach (j, k, n jk ) ∈ value do emit N →R 1 (j, (N, k, E pk p (n jk ))) (g) 1st Map function (2R-CRSP-M1). Input: (key, values) //key: 1 ≤ j ≤ b //values: collection of (M, i, m ij ) // or (N, k, n jk ) foreach (M, i, m ij ) ∈ values do foreach (N, k, n jk ) ∈ values do emit R 1 →R 2 ((i, k), (m ij × n jk )) (

b) 1st Reduce function (2R-R1).

Input: (key, values) //key: 1

≤ j ≤ b //values: collection of (M, i, E pk p (m ij )) // or (N, k,(n jk + τ jk , E pk r 2 (τ jk ))) foreach (M, i, E pk p (m ij )) ∈ values do foreach (N, k,(n jk + τ jk , E pk r 2 (τ jk ))) ∈ values do emit R 1 →R 2 ((i, k), (E pk p (m ij ) n jk +τ jk , E pk p (m ij ), E pk r 2 (τ jk )))
(e) 1st Reduce function (2R-SP-R1).

Input: (key, values) //key: 1

≤ j ≤ b //values: collection of (M, i, E pk p (m ij )) // or (N, k, E pk p (n jk )) foreach (M, i, E pk p (m ij )) ∈ values do foreach (N, k, E pk p (n jk )) ∈ values do emit R 1 →R 2 ((i, k), inter (E pk p (m ij ), E pk p (n jk ))) (

h) 1st Reduce function (2R-CRSP-R1).

Input: (key, values) //key:

(i, k) ∈ 1, a × 1, c //values: collection of v = m ij × n jk emit R 2 →P ((i, k), ((i,k),v) v) (c) 2nd Reduce function (2R-R2). Input: (key, values) //key: (i, k) ∈ 1, a × 1, c //values: collection of (v 1 , v 2 , v 3 ) = // (E pk p (m ij ) n jk +τ jk , E pk p (m ij ), E pk r 2 (τ jk )) emit R 2 →P ((i, k), ((i,k),(v 1 ,v 2 ,v 3 )) v 1 /(v D skr 2 (v 3 ) 2
))

(f) 2nd Reduce function (2R-SP-R2).

Input: (key, values) //key: Input: (key, value) //key: id of a chunk of M or N //value: collection of (i, j, m ij ) or (j, k, n jk )

(i, k) ∈ 1, a × 1, c //values: collection of v = E pk p (m ij × n jk ) emit R 2 →P ((i, k), ((i,k),v) v) (i) 2nd Reduce function (2R-CRSP- R2).
foreach (i, j, m ij ) ∈ value do foreach 1 ≤ k ≤ b do emit M→R ((i, k), (M, j, m ij )) foreach (j, k, n jk ) ∈ value do foreach 1 ≤ i ≤ a do emit N →R ((i, k), (N, j, n jk ))
(a) Map function (1R-M).

Input: (key, value) //key: id of a chunk of M or N //value: collection of (i, j, m ij ) or (j, k, n jk )

foreach (i, j, m ij ) ∈ value do foreach 1 ≤ k ≤ c do emit M→R ((i, k), (M, j, E pk p (m ij ))) foreach (j, k, n jk ) ∈ value do foreach 1 ≤ i ≤ a do emit N →R ((i, k), (N, j, n jk ) (c) Map function (1R-SP-M).
Input: (key, value) //key: id of a chunk of M or N //value: collection of (i, j, m ij ) or (j, k, n jk )

foreach (i, j, m ij ) ∈ value do foreach 1 ≤ k ≤ c do emit M→R ((i, k), (M, j, E pk p (m ij ))) foreach (j, k, n jk ) ∈ value do foreach 1 ≤ i ≤ a do emit N →R ((i, k), (N, j, E pk p (n jk )))
(e) Map function (1R-CRSP-M).

Input: (key, values) //key:

(i, k) ∈ 1, a × 1, c //values: collection of (M, j, m ij ) // or (N, j, n jk ) foreach j ∈ 1, b do emit R→P ((i, k), b j=1 (m ij × n jk )) (b) Reduce function (1R-R). Input: (key, values) //key: (i, k) ∈ 1, a × 1, c //values: collection of (M, j, E pk p (m ij )) // or (N, j, n jk ) foreach (i, k) ∈ 1, a × 1, c do emit R→P ((i, k), b j=1 E pk p (m ij ) n jk ) (d) Reduce function (1R-SP-R). Input: (key, values) //key: (i, k) ∈ 1, a × 1, c //values: collection of (M, j, E pk p (m ij )) // or (N, j, E pk p (n jk )) foreach (i, k) ∈ 1, a × 1, c do emit R→P ((i, k), b j=1 inter (E pk p (m ij ), E pk p (n jk ))) (f) Reduce function (1R-CRSP- R).
Computation cost:

(C + + C × )n 3 . Computation cost: (C × + Cexp)n 3 . Computation cost (4C E + 7C × + 2C D + 2Cexp)n 3 . Communication cost: n 2 .
Communication cost: n 2 . Communication cost: 3n 3 + n 2 with 1 ≤ j ≤ b for each key (i, k). These results are paired to the keys (i, k) for 1 ≤ i ≤ a and 1 ≤ k ≤ c in the output of 1R-R and sent to the MapReduce user P.

SP Matrix Multiplication

The SP matrix multiplication with MapReduce uses the Paillier's scheme and the idea of adding a random mask to ensure privacy of elements of matrices.

SP Two MapReduce Rounds

The The First SP Map Function (Figure 6(d)). 2R-SP-M1 encrypts all elements m ij of the matrix M using Paillier's cryptosystem with the public key pk p of user P and masks all elements n jk of the matrix N by adding a random element τ jk ∈ Z n to n jk . Moreover, 2R-SP-M1 encrypts and sends each τ jk with the public key pk r 2 of nodes R 2 .

The First SP Reduce Function (Figure 6(e)). 2R-SP-R1 is executed on the set of nodes R 1 . As we have seen in the standard MapReduce, 2R-R1 produces key-value pairs where the key is equal to (i, k) and values is equal to m ij • n jk for 1 ≤ j ≤ b. In the SP approach, keys are also equal to (i, k) but values are tuples equal to

(E pk p (m ij ) n jk +τ jk , E pk p (m ij ), E pk R 2 (τ jk )). Thus, R 1 can compute E pk p (m ij × n jk ) × E pk p (m ij ) τ jk
using homomorphic properties of Paillier's cryptosystem which is equal to E pk p (m ij ) n jk +τ jk in the tuple. The mask removal is later on done in nodes R 2 .

The Second SP Map Function. It is also the identity.

The Second SP Reduce Function (Figure 6(f )). 2R-SP-R2, executed on R 2 , multiplies all values associated to the same key (i, k). Moreover, R 2 removes all masks for each value using E pk p (m ij ) and E pk r 2 (τ jk ) emitted by R 1 . In fact, to compute

E pk p (m ij × n jk ), R 2 computes E pk p (m ij ) n jk +τ jk / E pk p (m ij ) D skr 2 (E skr 2 (τ jk )) =E pk p (m ij ) n jk × E pk p (m ij ) τ jk /E pk p (m ij ) τ jk =E pk p (m ij × n jk ) .

SP One MapReduce Round

The matrix multiplication for SP one MapReduce round is composed of two functions: the Map function (1R-SP-M) and the Reduce function (1R-SP-R). Unlike in two MapReduce rounds, elements of matrix N cannot be masked since there is only one reduce function.

The SP Map Function (Figure 7(c)). In 1R-SP-M, only elements of matrix M are encrypted with the public key pk p of the user P using Paillier's cryptosystem.

The SP Reduce Function (Figure 7(d)). 1R-SP-R uses the homomorphic property of Paillier's cryptosystem. In fact, instead to summing all products m ij × n jk ; 1R-SP-R mutltiplies, for each key (i, k), all encrypted values

E pk p (m ij ) n jk corresponding to E pk p (m ij × n jk ).

CRSP Matrix Multiplication

The MapReduce matrix multiplication with one and two rounds reveals all intermediate results to each set of nodes of the cluster. For example, when matrix multiplication is performed with two MapReduce rounds, R 1 knows all elements of matrices M and N . We describe below MapReduce algorithms with the CRSP approach, which precludes the cluster nodes from learning elements of the matrices.

CRSP Two MapReduce Rounds

The matrix multiplication for CRSP two MapReduce rounds is composed of four functions: the first Map function (2R-CRSP-M1), the first Reduce function (2R-CRSP-R1), the second Map function (2R-CRSP-M2) and the second Reduce function (2R-CRSP-R2).

The First CRSP Map Function (Figure 6(g)). Unlike 2R-SP-M1, 2R-CRSP-M1 encrypts all elements m ij of the matrix M and all elements n jk of the matrix N with the public key pk p of the user P. Hence, when 2R-CRSP-M1 emits the key-value pairs to R 1 , which learns nothing about elements of matrices M and N .

The First CRSP Reduce Function (Figure 6(h)). It has to perform multiplications of encrypted values having the same key on R 1 , i.e. for a key (i, k), R 1 multiplies E pk p (m ij ) by E pk p (n jk ) for 1 ≤ j ≤ b. We use the interactive protocol in Figure 5 to perform mutiplication of two ciphertexts with the Paillier's cryptosystem. Hence, R 1 interacts with the client P to perform the multiplications.

The Second CRSP Map Function. It is also the identity.

The Second CRSP Reduce Function (Figure 6(i)). Since R 2 receives key-value pairs where values v equal to E pk p (m ij × n jk ), R 2 uses the homomorphic property of Paillier's cryptosystem to compute the sum of all encrypted values associated to the same key (i, k). Pricisely, 2R-CRSP-R2 computes ((i,k),v) v for a key (i, k) which represents E pk p ( ((i,k),v) v).

CRSP One MapReduce Round

Finally, we present the matrix multiplication for CRSP one MapReduce round composed of two functions: the Map function (1R-CRSP-M) and the Reduce function (1R-CRSP-R).

The CRSP Map Function (Figure 7(e)). 1R-CRSP-M creates the sets of matrix elements used to compute the product of matrices M and N . All these matrix elements are encrypted with the public key pk p of the user P. Hence, M, N and R cannot learn any information on elements of these matrices.

The CRSP Reduce Function (Figure 7(f )). For a key (i, k), it takes as input values of the form (M, j, E pk p (m ij )) and (N, j, E pk p (n jk )), for 1 ≤ j ≤ b. To compute b j=1 m ij × n jk from these encrypted values, 1R-CRSP-R uses Paillier's interactive multiplicative homomorphic protocol.

Security Proofs

We provide formal security proof of our two rounds CRSP protocol. Proofs for the one round CRSP protocol and for SP protocols are quite similar but having no space for all four, we focus on the most technically interesting.

We use the standard multi-party computations definition of security against semi-honest adversaries [START_REF] Ma | Secure multi-party protocols for privacy preserving data mining[END_REF]. We consider several entities that run a secure protocol in order to evaluate a multivariate function f . For example, consider two parties A and B using respectively inputs a and b that run a secure two-party protocol to evaluate the multivariate function f = (f A , f B ). At the end of the protocol, A learns f A (a, b) and B learns f B (a, b). Such a protocol is secure when A (resp. B) learns nothing else than f A (a, b) about b (resp. f B (a, b) about a). We consider semi-honest adversaries in the sense that A and B run honestly the protocols, but they try to exploit all intermediate information that they have received during the protocol.

We model our protocol with five entities M, N , R 1 , R 2 and P using respective inputs

I = (I M , I N , I R 1 , I R 2 , I P ) and a function f = (f M , f N , f R 1 , f R 2 , f P ) such that:
• M has the input I M = (M, pk p ) where M is a matrix and pk p is a Paillier's public key, and returns f M (I) =⊥ (where ⊥ denotes that the function returns nothing), because M does not learn anything. • N has the input I N = (N, pk p ) where N is a matrix and pk p is a Paillier's public key, and returns f N (I) =⊥, because N does not learn anything. • R 1 has the input I R 1 = pk p where pk p is a Paillier's public key, and returns f R 1 (I) =⊥, because R 1 does not learn anything. • R 2 has the input I R 2 = pk p where pk p is a Paillier's public key, and returns f R 2 (I) =⊥, because R 2 does not learn anything. • P has the input I P = (pk p , sk p ) where (pk p , sk p ) is a Paillier's key pair, and returns f P (I) = M × N . Note that for the sake of clarity, we consider that R 2 sends the product of the encrypted matrices to P instead of storing them in a database. Moreover, we show that our two-rounds protocol is secure even if the two reduce nodes R 1 and R 2 collude, i.e. they share all their information.

We start by formally defining the Computational Indistinguishability and the view of an entity before formally presenting the security of CRSP MapReduce protocols. Definition 3 (Computational indistinguishability). Let η be a security parameter and X η and Y η two distributions. We say that X η and Y η are Computationally Indistinguishable, denoted X η c ≡ Y η , if for every probabilistic polynomial-time distinguisher D we have:

|Pr[x ← X η : 1 ← D(x)] -Pr[y ← Y η : 1 ← D(y)]| ≤ (η) ,
where is a negligible function in η. Definition 4 (view). Let π be a n-parties protocol that computes the function f = (f i ) 1≤i≤n for the entites (E i ) 1≤i≤n using inputs I = (I i ) 1≤i≤n . The view of a party E i (where 1 ≤ i ≤ n) during an execution of π, denoted view π E i (I), is the set of all values sent and received by E i during the protocol. We denote by view π E i ,E j (I) = (view π E i (I), view π E j (I)) (where 1 ≤ i, j ≤ n) the view of a collusion between E i and E j .

To prove that a party E learns nothing during execution of the protocol, we show that E can run a simulator algorithm that simulates the protocol, such that E (or any polynomialy bounded algorithm) is not able to differentiate an execution of the simulator and an execution of the real protocol. The idea is the following: since the entity E is able to generate his view using the simulator without the secret inputs of other entities, E cannot extract any information from his view during the protocol. This notion is formalized in Definition 5.

Definition 5 (Security with respect to semi-honest behavior). Let π be a n-parties protocol that computes the function f = (f i ) 1≤i≤n for entites (E i ) 1≤i≤n using inputs I = (I i ) 1≤i≤n ∈ I. We say that π securely computes f in the presence of semi-honest adversaries if for each E i (where 1 ≤ i ≤ n) there exists probabilistic polynomial-time simulators S E i such that:

S E i (I i , f E i (I)) c ≡ view π E i (I) .
We say that π is secure against collusions between E i and E j (where 1 ≤ i, j ≤ n) if there exist probabilistic polynomial-time simulators S E i ,E j such that:

S E i ,E j ((I i , f E i (I)), (I j , f E j (I))) c ≡ view π E i ,E j (I) .
The security of CRSP two MapReduce rounds is given by Theorem 1.

Theorem 1. Assume Paillier's cryptosystem is IND-CPA, then the CRSP two-rounds protocol securely computes the matrix mutiplication in the presence of semi-honest adversaries even if R 1 and R 2 collude. Moreover, the CRSP one-round protocol securely computes the matrix multiplication in the presence of semi-honest adversaries.

In a security point of view, the only difference between the two protocols is that the collusion of the nodes R 1 and R 2 in the two-rounds protocol becomes a unique node R in the one-round protocol, then the security of the two-rounds protocol implies the security of the one-round one.

The security proof for the two-rounds protocol (Theorem 1) is decomposed in Lemma 1 for M and N , Lemma 2 for R 1 and R 2 and Lemma 3 for P. Proof. We build the simulator S M presented in Algorithm 1. The view of M only contains the encryption of M that is sent to R 1 . We remark that S M ((M, pk p ), ⊥) uses exactly the same algorithm as the real protocol of CRSP, then it describes exactly the same distribution as view CRSP M (I), which concludes the proof. Building the simulator S N as S M , we prove that S N ((N, pk p ), ⊥) describes exactly the same distribution as view CRSP N (I). Proof. We build the simulator S P presented in Algorithm 4. The view of P contains the couple of ciphertexts (x ijk , y ijk ) sent by R 1 and the answer z ijk that contains the encryption of the multiplication of x ijk and y ijk . Since x ijk and y ijk are randomized by R 1 , there are indistinguishable to random ciphertexts in the P point of view. The view of P also contains P = E pk p (P ) encrypted by pk p that is sent by R 2 . Finally, S P ((pk p , sk P ), P ) describes exactly the same distribution as view CRSP P (I), which concludes the proof.

Conclusion and Future Works

We have presented efficient algorithms for MapReduce matrix multiplication that enjoy privacy guarantees such as: none of the nodes storing an input matrix can learn the other input matrix or the output matrix, and moreover, none of the nodes computing an intermediate result can learn the input or the output matrices. To achieve our goal, we have relied on Paillier's cryptosystem and we developed two different approaches: one resisting to collusions between nodes (Collision-Resistant-Secure-Private) and an other which does not require communication overhead (Secure-Private). We have thoroughly compared these two approaches with respect to three fundamental criteria: computation cost, communication cost, and privacy guarantees.

Looking forward to future work, we plan to study the practical performance of our algorithms in an open-source system that implements the MapReduce paradigm. Additionally, we aim to investigate the matrix multiplication with privacy guarantees in different big data systems (such as Spark or Flink) whose users also tend to outsource data and computations similarly to MapReduce.

  Figure 1: One Round.

Figure 3 :

 3 Figure 3: Summary of results. Let n be max(a, b, c), and C × (resp. C + , C exp , C E , C D ) is the cost of multiplication (resp. addition, exponentiation, encryption, decryption).

Definition 1 (

 1 Negligible function). A function : N → N is negligible in η if for every positive polynomial p(•) and sufficiently large η, (η) < 1/p(η). Definition 2 (Public Key Encryption (PKE)). Let η be a security parameter. A PKE scheme is defined by three algorithms (G, E, D): G(η): returns a public/private key pair (pk, sk). E pk (m): returns the ciphertext c. D sk (c): returns the plaintext m.

Figure 5 :

 5 Figure 5: Paillier interactive mutiplicative homomorphic protocol, of computation cost O(4C E +6C × +2C D +2C exp ) and communication cost O(3).

  The matrix multiplication with two MapReduce rounds is composed of four functions: first Map function (2R-M1), first Reduce function (2R-R1), second Map function (2R-M2) and second Reduce function (2R-R2).

Figure 6 :

 6 Figure 6: Algorithms for two MapReduce rounds, the highlighting emphasizes differences between algorithms of the first column and the second one, and between algorithms of the second column and the third one. By n we denote max(a, b, c). Computation and communication costs are given in big-O notation.

Figure 7 :

 7 Figure 7: Algorithms for one MapReduce round, the highlighting emphasizes differences between algorithms of the first column and the second one, and between algorithms of the second column and the third one. By n we denote max(a, b, c). Computation and communication costs are given in big-O notation.

  matrix multiplication for SP two MapReduce rounds is composed of four functions: the first Map function (2R-SP-M1), the first Reduce function (2R-SP-R1), the second Map function (2R-SP-M2) and the second Reduce function (2R-SP-R2).

Lemma 1 .

 1 There exists probabilistic polynomial-time simulators S M and S N such that for all I = (I M , I N , I R 1 , I R 2 , I P ) we have: S M (I M , f M (I)) c ≡ view CRSP M (I) , S N (I N , f N (I)) c ≡ view CRSP N (I) .

SAlgorithm 1 :

 1 M ((M, pk p ), ⊥):M ← E pk p (m ij ) Simulator S M .Lemma 2. Assume Paillier's cryptosystem is IND-CPA, then there exists a probabilistic polynomial-time simulator S R 1 ,R 2 such that for all I = (I M , I N , I R 1 , I R 2 , I P ) we have:S R 1 ,R 2 ((I R 1 , f R 1 (I)), (I R 2 , f R 2 (I))) c ≡ view CRSP R 1 ,R

Lemma 3 .

 3 There exist a probabilistic polynomial-time simulator S P such that for all I = (I M , I N , I R 1 , I R 2 , I P ) we have: S P (I P , f P (I)) c ≡ view CRSP P (I) .

  R 1 ,R 2 ((pk p , ⊥), (pk p , ⊥)):for 1 ≤ i ≤ a do for 1 ≤ j ≤ b do α ij ; for 1 ≤ j ≤ b do for 1 ≤ k ≤ c do β jk ; M ← (E pk p (α ij )) 1≤i≤a,1≤j≤b ; N ← (E pk p (β jk )) 1≤j≤b,1≤k≤c ; for 1 ≤ i ≤ a do for 1 ≤ k ≤ c do for 1 ≤ j ≤ b do (r ijk , s ijk , t ijk ) ) 3 ; x ijk ← E pk p (α ij ) × E pk p (r ijk ) ; y ijk ← E pk p (β jk ) × E pk p (s ijk ) ; z ijk ← E pk p (t ijk ) ; u ik = b j=1 z ijk ; view R 1 = (M , N , {(x ijk , y ijk ), z ijk } 1≤i≤a,1≤j≤b,1≤k≤c ) ; view R 2 = ({z ijk } 1≤i≤a,1≤j≤b,1≤k≤c , {u ik } 1≤i≤a,1≤k≤c ) ; return view = (view R 1 , view R 2 ).Algorithm 2: Simulator S R 1 ,R 2 .

2 (I) . S $ ← Z n $ ← Z n $ ← (Z n

Acknowledgements

This research was conducted with the support of the FEDER program of 2014-2020, the region council of Auvergne-Rhône-Alpes, the support of the "Digital Trust" Chair from the University of Auvergne Foundation, the Indo-French Centre for the Promotion of Advanced Research (IFCPAR) and the Center Franco-Indien Pour La Promo-

Proof. Let S R 1 ,R 2 be the simulator presented in Algorithm 2. It outputs the view of R 1 that contains the two encrypted matrices M and N sent by M and N , all couples of ciphertexts (x ijk , y ijk ) sent to P and all corresponding ciphertexts z ijk returned by P to compute multiplication on encrypted coefficients, and all the values z ijk that are forwarded to R 2 . It also outputs the view of R 2 that contains all values z ijk sent by R 1 and coefficients u ik of the encrypted matrix P sent to P.

Let η be the security parameter used for the Paillier's cryptosystem. Assume there exists a polynomial-time distinguisher D such that for all I ∈ I:

where is a non-negligible function in η. We show how to build a probabilistic polynomial-time adversary A such that A has a non-negligible advantage to win the IND-CPA experiment on the Paillier's cryptosystem. Then we conclude the proof by contraposition. Adversary A is presented in Algorithm 3. At the end of its execution, A uses the distinguisher D to compute the bit b * before returning it. First, we remark that:

Indeed, when b = 0, the view that A uses as input for D is computed as in the real protocol CRSP. Then the probability that the experiment returns 1 (which is the probability that b * = b = 0) is equal to the probability that the distinguisher returns 0 on inputs computed as in the real protocol. On the other hand, we have:

When b = 1, the view that A uses as input for D is computed as in the simulator S R 1 ,R 2 . Then the probability that the experiment returns 1 (which is the probability that b * = b = 1) is equal to the probability that the distinguisher returns 1 on inputs computed as in the simulator. Finally, we evaluate the probability that A wins the experiment, i.e. b * = b:

We deduce the advantage of A:

Which concludes the proof by contraposition.

A(pk p ):

Algorithm 3: Adversary A.

S P (pk p , sk P ), P :