Paul Iannetta

Laure Gonnord

Lionel Morel

Tomofumi Yuki

Semantic Array Dataflow Analysis

Keywords: polyhedral model, operational semantics Semantic Array Dataflow Analysis modèle polyédrique, sémantique opérationnelle

This paper revisits the polyhedral model's key analysis, dependency analysis. The semantic formulation we propose allows a new definition of the notion of dependency and the computation of the dependency set. We argue that this new formalization will later allow for a new vision of the polyhedral model in terms of semantics, which will help us fully characterize its expressivity and applicability. We also believe that abstract semantics will be the key for designing an approximate abstract model in order to enhance the applicability of the polyhedral model.

Introduction

Multi-core processors, and parallel processing in general, are now broadly used. Their horizon of applications ranges from mobile platforms to high-performance computing. Allowing non-expert programmers to harness the parallelism in recent hardware require significant advances in the entire compilation chain. It also means that the general forms of sequential programs, e.g., with while loops and data-dependent control structures, should be amenable to parallelization.

The polyhedral model [START_REF] Feautrier | The polyhedron model[END_REF] is a powerful algebraic framework that is at the core of many advances in optimization and code generation of numerical kernels. One reason of its success is the practicality of the operations that are expressed in terms of algebraic computations on affine sets.

One of the major limitations of this model is that it only applies to programs with regular control and loops with static bounds. The main issue is that the polyhedral model's algorithms are defined with strong assumptions on the shape of programs under analysis, which make the underlying problems decidable. However, checking those requirements is sometimes not trivial:

• A programmer may have written an algorithm that is inherently polyhedral in a way that is not compliant with the syntactic restrictions of the polyhedral model;

• The compiler may have transformed the polyhedral input program in such a way that the polyhedral structure does not appear syntactically any more.

We argue that this is an important limitation for further extending the polyhedral model. In this paper, we propose to redefine the dataflow analysis based on the operational semantics of programs. By doing so we claim that we leverage the constraints of the previous definitions and increase the range of applicability of the polyhedral model.

From a general viewpoint, our work lies in the semantic consolidation of the polyhedral model to allow its extension with static analysis techniques that opens the door to the parallelization of irregular programs (i.e., with while loops and more general data structures such as trees or maps).

A strategic prerequisite for this long-term goal is to propose a unified formal setting that describes the semantics of general programs. As a first step for this work, the present paper proposes a semantic-based description of the array dataflow analysis [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF]. This paper also proposes a precise definition of covertly regular programs for which the classical algorithms of the polyhedral community are exactly applicable, and a notion of polyhedral approximation for more general programs.

Overview

This work is a first step towards a clear semantic of the polyhedral model. The contributions of the paper are:

• A semantic definition of the notion of dependency à la polyhedral model, on a general imperative language; RR n°9232

• A rephrasing of the classical array dataflow analysis [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF] in our setting, which enables us to recover classical results from the community;

• The definition of the notion of covertly-regular programs for which the polyhedral model algorithms and tools can be applied as-is;

• A notion of approximated polyhedral model for programs with non polyhedral control, on which we can compute an over-approximated set of dependence.

The rest of the paper is organized as follows: section 2 recalls the notion of data dependency set and its classical computation in the polyhedral model framework; section 3 describes our model of program and its semantics enriched with an extended notion of iteration vector; section 4 gives a semantic-based notion of dependencies for our general class of programs. Then, section 5 proves the equivalence of our definition with the initial one on regular polyhedral programs, enabling us to define the notion of covertly regular polyhedral programs. section 6 gives an algorithm to compute an over-approximation of the dependency set for programs with nonpolyhedral control, opening perspectives to a more general approximate polyhedral model; section 7 compares our work to existing works. Finally, we conclude in section 8 with some directions for future work.

Background: Array Dataflow Analysis

The seminal paper Array Dataflow Analysis [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF] proposed exact dependency analysis for loops with static and affine control. In this section, we present an overview of the results and algorithms of this paper, rephrased with our semantic-based formalization in view.

Informally, a data dependency between two operations exists when two operations access to the same memory location, with at least one of them being a write. These include benign dependencies as well as true dependencies, which are defined based on the notion of most recent write. The paper shows that for affine loops the above can be formulated with Integer Linear Programming, hence providing an exact solution, which we recall below.

Tracking Operations

In order to optimize the operations of a given program, a typical polyhedral compilation flow computes the instance-wise and element-wise dependencies. The analysis identifies dependencies between all operations operating on array as long as they are within the affine restrictions. Two operations that do not depend on each other can be parallelized, or at least, rescheduled in an order different than the lexical order of the original program. The notion of dependency between operations is thus central to program transformations.

Those dependencies are expressed by giving a unique identifier to each operation -an iteration vector -whose coordinates are loop counters. The first coordinate is the outermost loop's counter while the last coordinate is the innermost loop's counter. For example, in the listing of Figure 1 the iteration vector on line 3 is i, j while the iteration vector on line 5 is i, j, k . Remark (loop counter). In the context of for loops, the concept of iteration variable is crystal clear since it is the same as loop counters. However, when dealing with while loops, the definition is not as clear and is addressed later. From now on, statements are denoted by s i , instantiated iteration vectors by t j (because such a vector can be seen as a timestamp) and operations by a pair s i , t j . Note that two operations can have the same iteration vector, typically when they are at the same loop level. In order to know which is before the other a boolean T s 1 ,s 2 is set to true if s 1 is before s 2 in the text source program. Intuitively, we define Q s 1 ,s 2 (t) as the set of all the operations involving s 1 that have an influence on the computation of s 2 at time t. And we define K s 1 ,s 2 (t) as the last operation having an influence on the computation of s 2 at time t.

Computation of Dependencies

We now formally define K and Q, and explain how they are computed within the context of the polyhedral model. Let us assume that we are computing values for a matrix M, and that we want to compute the operations on which o 2 = s 2 , t 2 (an operation that needs to read values in M) depends. Moreover, let us assume that o 2 needs to read M[g(t 2 )], where g is an affine function of the iteration vector t 2 .

However, before we can compute Q s 1 ,s 2 (t 2 ) we need to gather candidates for s 1 . We will thus take into account all operations whose statement is of the form M[f(t 1 )] := ... where f is an affine access function of the iteration vector. The research can be restricted to operations that happen before s 2 in the program flow. The operations on which s 2 depend will then be the union of the operations found with s 1 as their statement.

In order to explicitly define and compute Q, the following conditions have to be fulfilled: C 1 : the arrays/matrices cells that s 1 and s 2 try to access should match: f(t 1 ) = g(t 2 ) ; C 2 : (s 1 , t 1 ) should happen before (s 2 , t 2 ) (i.e., t 1 t 2 , or (t 1 = t 2 ) ∧ T s 1 ,s 2 where is the lexicographic ordering on vectors and T the textual ordering). This condition is denoted by s 1 , t 1 ≺ s 2 , t 2 C 3 t 1 must be a valid iteration (denoted as e(t 1 ) ≥ 0, this notation will become clear in Theorem 2.2.)

Hence, the following definition of Q s 1 ,s 2 (t) as:

{ t | f(t ) = g(t), s 1 , t ≺ s 2 , t , e(t ) ≥ 0 } and K s 1 ,s 2 (t 2 ) as: max Q s 1 ,s 2 (t 2 ).
Theorem 1 (Dependencies are computable in the polyhedral model). In the polyhedral model setting (static control), the set of dependencies of a given operation is computable.

Proof. The proof can be found in the original paper [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF]. The 3 conditions above lead to a system of affine constraints whose lexicographic maximum is then computable by a Parametrized Integer Linear Programming solver (such as PIP [START_REF] Feautrier | Parametric integer programming[END_REF]).

Example (Computations of dependencies for the matrix product, shown in Figure 1). This program is made of two statements: s 1 on line 3 and s 2 on line 5, that both write values for the array c. In order to compute the dependencies we need to compute Q s 1 ,s 1 , Q s 1 ,s 2 and Q s 2 ,s 2 . The respective Ks will be computed by taking the lexicographic maximum on the Qs.

Let us start by computing Q s 1 ,s 1 . We can see that s 1 does not need to read any variable. Hence, Q s 1 ,s 1 is empty. Now, let us compute Q s 1 ,s 2 . Let i 1 , j 1 be the iteration vector of statement s 1 and i 2 , j 2 , k 2 the iteration vector of statement s 2 . We can then express C 1 , C 2 and C 3 as affine conditions.

C 1 is i 1 , j 1 = i 2 , j 2 . C 2 is i 1 , j 1 i 2 , j 2 , k 2 . And C 3 is 1 ≤ i, j ≤ n. This leads to Q(s 1 , s 2 )( i 2 , j 2 , k 2 ) being equal to: { i 1 , j 1 | i 1 = i 2 ∧ j 1 = j 2 }.
Lastly, let us compute Q s 2 ,s 2 . Let i 2 , j 2 , k 2 and i 2 , j 2 , k 2 be the iteration vectors of statement s 2 at two distinct instants. All conditions can be expressed as affine conditions:

C 1 is i 2 , j 2 , k 2 = i 2 , j 2 , k 2 , C 2 is i 2 , j 2 , k 2 i 2 , j 2 , k 2 , and C 3 is 1 ≤ i 2 , j 2 , k 2 ≤ n. This gives Q(s 2 , s 2 )( i 2 , j 2 , k 2 ) as: { i 2 , j 2 , k 2 | i 2 = i 2 ∧ j 2 = j 2 ∧ k 2 < k 2 }.

Discussion

The analysis led to an efficient algorithm to store and compute (most recent) dependencies when:

• Loop iterators are easily definable and their domain is easily exactly computable (condition C3);

• Memory accesses are affine functions of loop iterators (condition C1);

• The happens-before relation is a function of syntax elements (condition C2).

What we propose in this paper is to relax these assumptions to rely less on syntactic elements, and to re-formulate the analysis based on an operational semantics of the language.

General Imperative Programs With Iteration Vectors

For the formalization, we use a variant of the classical (small-steps) operational semantics of a general imperative language with scalars and arrays, where we exhibit the notion of iteration vector. The syntax of the mini-language is depicted in subsection 3.1, our extension for iteration vectors in subsection 3.2. The semantics described in subsection 3.3 then enables us to properly define the notion of trace in subsection 3.4.

A Mini Language

The language we propose is a pointer-less imperative language with native support for while loops, if statements as well as arrays of integers (scalars are degenerated arrays with one cell).

In the grammar depicted in Figure 2, capital letters (X, Y, Z) are used as placeholders for variable names. n represents an element of N and terms in lowercase are an instance of the expression rule which shares the same first letter: e.g., a • is an instance of Aexp, b • is an instance of Bexp, and so on. The "κ n :" notation is explained in subsection 3.2 and can be safely ignored at this point.

Aexp ::= n | a 0 Aop a 1 | v 0 Aop ::= '+' | ' * ' | '-' | '/' | 'mod' Bexp ::= 'true' | 'false' | !(b 0 ) | b 0 Bop b 1 | a 0 Cop a 1 Bop ::= 'or' | 'and' | '=' Cop ::= '<=' | '=>' | '<>' | '==' Vexp ::= X | X'['a 0 ']' Sexp ::= κ n ':begin'| 'skip' | s 0 ';' s 1 | κ n ':if' b 0 'then' s 0 'else' s 1 'fi' | κ n ':while' b 0 'do' s 0 'done' | v 0 ':=' a 0 Figure 2: Our Mini-Language: syntax
The grammar itself is permissive and recognizes programs that are syntactically outside of the scope addressed by the polyhedral model.

Semantic Extension: Iteration Variables and Iteration Vectors for our Language

In the classical polyhedral model, for loops naturally introduce counter variables. These are convenient to number the operations and use those as labels when investigating their dependencies. For general programs with tests and while loops, there is no canonical way to implicitly define iteration variables. We thus explicitly introduce them in our language and semantics. This kind of instrumentation is classic in other static program analyses such as Worst-Case Execution Time (WCET) analysis [MRPV + 17] or complexity estimation [START_REF] Gulwani | Speed: Precise and efficient static estimation of program computational complexity[END_REF].

Fresh iteration variables κ i ∈ Name are created so that operations are numbered hierarchically, the first level counts the number of operations at level zero, the second level those at level one, and so on. The iteration vector is the concatenation of those variables. The leftmost coordinate is the iteration variable of the outermost loop and the rightmost coordinate is the iteration variable of the innermost loop. This allows sorting operations by their iteration vector, with respect to the lexicographic order. We illustrate this process with an example in the following. Example. Figure 3 depicts a simple array filling procedure with a while loop. We annotated each control statement with a κ i . These iteration variables are introduced so as to number the operations hierarchically. As for if statements, we have to do some extra work in order to make them compatible with the lexicographic order. In the annotation step, we only annotate the test itself, the actual numbering of the sub-statements will be performed in the semantic rules, as we will later see in Figure 7. Example. Figure 4 shows an example of an if branch annotation. Only the test itself is annotated.

1 c[0] := 0; 2 i := 1; 3 while i <= n do 4 c[i] := c[i-1] + 1; 5 i := i + 1 6 done a) Before annotation 1 κ 0 :begin 2 c[0] := 0; 3 i := 1; 4 κ 1 :while i <= n do 5 c[i] := c[i-1] + 1; 6 i := i + 1; 7 done b) After annotation
1 i := 5; 2 while i <> 1 do 3 if i mod 2 == 0 4 i := i / 2 5 else 6 i := 3 * i + 1 7 done a) Before annotation 1 κ 0 :begin 2 i := 5; 3 κ 1 :while i <> 1 4
κ 2 :if i mod 2 == 0: 5 i := i / 2; 6 else: For example, on line 4 of 4b the (uninstantiated) iteration vector is (κ 0 κ 1 κ 2 ). When the program is run, on line 4, the iteration vector will contain the current values of κ 0 , κ 1 and κ 2 . At the end the iteration vector is κ 0 , 3 , because κ 2 has been dropped at the end of the if and κ 1 as been dropped at the end of the while.

The annotation process is straightforward as it appends κ n just before the construct that goes on one step deeper, and adds a begin annotation with label κ 0 at the beginning of the program. The semantics described in subsection 3.3 takes such an annotated program as input. Remark. Our annotation system is different form the usual notation used in the polyhedral model (the 2n + 1 notation [START_REF] Bastoul | Code Generation in the Polyhedral Model Is Easier Than You Think[END_REF]), which may use two dimensions to represent one loop: one dimension that corresponds to the number of iteration of the loop and one that would number the internal statements.

However, the reason behind the fact that we use only one dimension is that we want to be RR n°9232 able to map each level of the loop nest to a coordinate of the iteration vector.

Execution Environment, Final Semantics of our Mini Language

We now present the semantic rules of our annotated program where the initial statement, and each if and while statements have been prefixed with new fresh variables that constitute our iteration vector.

In our semantics, states σ are composed of:

• An environment µ that maps variables to values as well as the last iteration vector (instance) that wrote this variable: µ :

Vars → Z × (Name × Z) n ;
• The current value of the iteration vector κ ∈ (Name × Z) n . Remark. The Name part of the iteration vector is here to handle imperfect loop nests and in particular it is used to tell κ 0 , 3 , κ 1 , 1 and κ 0 , 3 , κ 2 , 1 apart.

The effect of each statement (in Sexp) is to update the current µ according to classical smallsteps operational semantics while storing the current value of the iteration vector ; and to update the current iteration vector. We use two auxiliary functions upd and inc. Let σ = (µ, κ), then:

• upd(σ, κ i , n) returns a copy of σ where κ i is appended to κ and set to n if κ i is not already a component of κ, otherwise does nothing.

• incr(σ) returns a copy of σ where the current iteration vector κ's rightmost component of the iteration vector has been incremented by one.

We also define σ \ n that removes the component n of the current iteration vector, if it exists.

Figure 5 depicts the semantic rules for basic statements. Example. After the first statement of the program of 4b (begin), the state is , κ 0 , 0 . The initialization of i gives the new state: i → (5, [ κ 0 , 0 ]) , κ 0 , 1 .

For while loops, the semantics also mimics the initialization of its counter to 0 the first time we enter the loop, its incrementation at the end of one body execution; and also the removal of this counter at the end of the loop (σ \ κ n removes κ n ). Figure 6 depicts these two rules. Let us recall that in a small-steps semantics, → + depicts the execution of the body of the loop.

For ifs, we consider that we have a built-in length function that tells us the number of sub-statements contained in a statement s. The "true" part of the test rule is constructed so that the outermost component of the iteration vector grows from -length(c 1 ) to -1; the "false" part makes it grow from 0 to length(c 2 ) -1. Our operations continue to be uniquely numbered. Figure 7 depicts these two rules.

IT σ, b 0 → true upd(σ, κn, -length(s 1 )), s 1 → + σ , skip σ, κn : if b 0 then s 1 else s 2 fi; s → incr(σ \ κn); s IF σ, b 0 → false upd(σ, κn, 0), s 2 → + σ , skip σ, κn : if b 0 then s 1 else s 2 fi; s → incr(σ \ κn), s

Traces

We define traces of general programs based on our semantics. Definition 3.1 (trace on states). A trace on states Σ is a sequence of pairs of the form (state, statement) σ 0 , c 0 → σ 1 , c 1 → . . . . An initial trace is a trace which begins from the empty state.

All the memory accesses are completely deterministic, hence there exists one unique initial trace. This leads to the following remark. Remark. There is a one-to-one mapping between iteration vectors and states.

Therefore, we will from now on work directly on operations rather than states. Indeed, since an operation o is the pair s, t we can retrieve the corresponding state from t if necessary according to the previous remark. Definition 3.2 (trace on operations). A trace on operations O is a sequence of operations o 1 → o 2 → • • • . An initial trace is a trace which begins from the trivial (empty) iteration vector. Remark. From now on, the term trace will always refer to trace on operations unless stated otherwise. Definition 3.3 (reachability/validity). An operation s 1 , t is valid if and only if there exists an initial trace O = {o i } i∈N such that there exists o 0 such that o 0 = s 1 , t . Definition 3.4 (happens-before: <). There exists a natural order < on operations, called happensbefore. s 1 , t 1 < s 2 , t 2 if and only if there is one trace such that there exists i 1 and i 2 such that o i 1 → + o i 2 and t 1 = Vec(o i 1 ) and t 2 = Vec(o i 2 ) where Vec(o i ) denotes the second component of the pair o i = s i , t i . Prop 1 (strict order). Happens-before as defined above is a strict order.

Dependencies for General Programs

The semantics allows defining the key notion of dependency in a general context. Our program traces now contain all elements to define the dependencies: a notion of ordered time, which is induced by the succession of states in a trace (including our iteration vectors), and all information to define a last write notion with respect to a given state or operation. Definition 4.1 (rvars). Let o = s, t be an operation, the set of variables that s needs to read at time t is called rvars(o). Proof. The paths appended by the transitive closure are all about iterations smaller (with respect to the lexicographic order) than the ones originally present in the relation . Hence, the computation of the max on the transitive closure leads to the same result.

∃i 1 , o i 1 = last O,o i 2 (v) ∈ O ∧ ∀i, i 1 < i < i 2 , wvars(o i 1 ) = {v}
Remark. The reason why we keep a clear distinction between direct and most recent direct data dependency is that the transitive closure of is not the same as the transitive closure of (which is the full dependency graph), as can be seen in 4.6. Remark. The notion of most recent dependency will parallel the definition of K (as defined in section 2) as it will be exposed in 3. transitive closure + . In Figure 9, the most recent direct dependence of o 5 is o 3 , noted with double dashed red circle.

Semantic-Driven Dependency Analysis

The semantic based reformulation of dependencies seamlessly extends the possibility for analysing programs that are not written as canonical affine loop nests. In this section, we first show that our formulation gives the same notion when the behavior of a program matches that of an affine loop nest, and express a new Semantic-Driven Dependency Analysis based on this result. Then we describe how our analysis applies to covertly-regular programs: programs that do not exactly correspond to affine loops, but still exhibit a regular behavior expressible within the polyhedral model.

Equivalence on Regular Polyhedral Programs

In this section we prove that, when considering regular programs with respect to the polyhedral model, our approach is strictly equivalent to the one presented in Feautrier's original paper [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF]. Let P be a regular program and P the same program rewritten with while loops in the most straightforward fashion.

That is, for i from start to finish ( * ... * ) done is rewritten to the following "pseudo polyhedral" program: RR n°9232 i := start; while i <= finish ( * ... * ) i = i + 1 done A complication at this point is that what has been presented here does not exactly match with the presentation given in the seminal paper [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF] on array dataflow analysis. Hence, we need to make a bridge between the loop counters used as iteration vectors in the original paper and our iteration vectors. The following example explains how this convert function is computed on a simple program. Example. Let's compute the function convert on the Array filling example of Figure 3, which we recall here:

1 κ 0 :begin 2 c[0] := 0; ( * s1 * ) 3 i := 1; 4 κ 1 :while i <= n do 5 c[i] := c[i-1] + 1; ( * s2 * ) 6 i := i + 1; 7 done 8 end
The key point is to express the relation which describes the transition between two consecutive iterations of the loop: that is the state of the loop at iteration k and the state of the loop at iteration k + 1. Let us denote R this relation. One execution of the loop content can be described as:

(κ 0 , κ 1 , i) R (κ 0 , κ 1 + 2, i + 1).
The relation describes a transition in Presburger arithmetic, which means that its transitive closure is exactly computable. Moreover, we know that when the loop is initialized the following is true:

(κ 0 , κ 1 , i) = (0, 0, 1).
Hence, we can derive the exact expression of the convert function in this example.

κ 1 = 1 + 2(i -1).
This function is the bridge that we want to create between our two approaches. Prop 3. Let o 1 = s 1 , t 1 and o 2 = s 2 , t 2 be two operations in an initial trace O. Then,

o 1 o 2 ⇔ K s 1 ,s 2 (convert(t 2 )) = convert(t 1 )
where convert is the function that converts our iteration vector into the iteration vector introduced in the original paper [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF].

Proof. The existence of the convert function will be assured by 5. In this proof, we will show that if o 1 o 2 then the conditions C 1 , C 2 and C 3 are satisfied.

We need to prove the two directions of the equivalence. Since similar arguments can be used for both directions we only prove the left-to-right direction.

C 1 : The construction of guarantees that o 1 produces a value for o 2 or wrote the same cell as o 2 . This means that the accesses in s 1 and s 2 are on the same cell. The index of that cell is an affine function of the loop counters, which is independent of the use of the convert function.

C 2 : The definition of the function last guarantees that o 1 happens before o 2 . And since the convert function preserves the lexicographic order, we are sure that convert(t 1 ) convert(t 2 )

C 3 : o 1 belongs to the initial trace, therefore, the statement s 1 happens during a valid iteration.

Moreover, the definition of last guarantees that o 1 is the last operation before o 2 that produces a value for o 2 or writes the same cell as o 2 . Therefore, o 1 is the last operation on which o 2 depends.

Example. On the previous example, let s 1 : c[0]:=0 and s 2 : c[i]:=c[i-1]+1. We search t 1 , t 2 instantiations of (κ 0 , κ 1 ) such that o 1 o 2 . The systems of constraints is constructed with C 1 : 0 = i -1, and C 3 = true (s 1 is always valid). For C 2 , we need to transform the constraint (κ 0 ) ≺ (κ 0 , κ 1 ). Since κ 0 has no equivalent in Feautrier's model convert(κ 0 ) = [] (the empty vector), hence, C 2 becomes [] < [1 + 2(i -1)], which is true for all values of i, thus C 2 = true. Finally, Q s 1 ,s 2 has a unique constraint 0 = i -1, equivalent to i = 1. The maximum of this set, K, is also this unique point. After applying the convert function κ 1 = 1 + 2(i -1) we finally get the final result s 1 , κ 0 , 0 s 2 , κ 0 , 0 , κ 1 , 1 . Prop 4. Let o 1 = s 1 , t 1 and o 2 = s 2 , t 2 be two operations. Then,

o 1 + o 2 ⇔ convert(t 1 ) ∈ Q s 1 ,s 2 (convert(t 2 ))
where convert is the function that converts our iteration vector into the iteration vector introduced in the original paper [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF].

Proof. The same proof as for 3 holds. The only difference is that since we take all direct dependencies and the transitive closure we indeed get all the dependencies.

This equivalence proves that our formalization includes the polyhedral model and in this case (for loops rewritten as while loops) our system can harness the classical polyhedral computations. We thus reached our first goal, which is to be able to semantically capture the key notion of dependency and being able to compute it.

The decision process of finding the set of dependencies of a given program thus relies on the ability of effectively computing this convert function. We are thus searching for a relation between the variables of the program which implies a one-to-one relation between the iteration vector and the indices of array accesses.

There is an abundant literature on invariant generation for general imperative programs (a survey [START_REF] Gonnord | Abstract Acceleration in Linear Relation Analysis[END_REF] is available on the subject), and the computation of transitive closures of numerical relations.

In the general case, the transitive closure of an affine relation is not computable, however, there exists sub-classes that are known to be exactly computable. There exist an algorithm [START_REF] Verdoolaege | Transitive Closures of Affine Integer Tuple Relations and their Overapproximations[END_REF] that compute over-approximations of transitive closures of quasi-affine relations (a more general family of relations that encompass affine relations). Moreover, it also returns a boolean value that tells whether this transitive closure is exact.

Prop 5. If a relation is a translation (from the point of view of Presburger arithmetic), its transitive closure is computable.

Proof. For instance, the work by Verdoolaege et al. [START_REF] Verdoolaege | Transitive Closures of Affine Integer Tuple Relations and their Overapproximations[END_REF].

Thus, as long as we are dealing with regular polyhedral programs our model is decidable because our notions as well as those in the original paper [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF] coincide. Remark. 3 and 5 give us a decision procedure to test dependency between two given operations for our model. However, in the case where convert is invertible we do not only have a decision procedure but the full symbolic graph of dependencies. Since, in our setting of this section, it is invertible (convert is a translation), the symbolic graph of dependencies can also be expressed, computed and stored when we analyse a pseudo polyhedral program with while loops.

Once we have the relations between the artificial variables that were introduced and the variables appearing in the program we can express our iteration vector as linear combinations of the variables of the program.

Covertly-Regular Polyhedral Programs

Our analysis also extends to programs with while loops that are not straightforward translations of for loops. We are also interested in capturing programs with affine control that are not necessarily written as affine while loops. A possible example of such case is some kind of state machine with affine transitions. The programmer may decide to write such computation in a way that does not syntactically match affine loops, or a different pass in the compiler may strip away syntactic elements that are necessary to (syntactically) view them as affine loops.

Our analysis may be directly applied to such programs, and provide exact dependency information. However, the convert function that connects the iteration variables to syntactic elements can be difficult to find. For instance, an affine state machine with multiple variableswhich may correspond to multi-dimensional loops -would require invariants involving polynomials in general.

We propose an algorithm that reintroduces structure to the programs such that computing the convert function becomes easier. We also give a precise characterization of the class of programs "equivalent" to polyhedral programs, which we call covertly-regular programs. Prop 6. A polyhedral program (i.e., a loop nest) can be represented as

A i + c ≤ 0
where A is a lower-triangular matrix with ones on the diagonal, i is the vector whose coordinates are the loop counters, and c is a vector of constants expressions that may contain structure parameters.

Proof. A polyhedral program is a for loop nest. Without loss of generality we can assume that all loop counters are lower-bounded by 0, if they were not we would apply a translation on the iteration range. Moreover, the upper-bound of a loop counter cannot be a function of loop counters deeper in the loop nest. Hence, the bound on the loop counters can be written as A i + c ≤ 0 where A is a lower-triangular matrix with ones on the diagonal, i is the vector whose coordinates are the loop counters in the order as they appear in the loop nest, and c is a vector of constants.

From now on, we will denote a polyhedral program P by a triple A, i, c . Definition 5.1 (Covertly regular polyhedral program). A covertly regular program A, i, c is such that there exists an orthogonal matrix O with det(O) = 1, such that OAO -1 , O i, O c is a regular program. Remark. The change of basis affect the whole program including arrays accesses. Remark. Effectively computing such a base changing is in general undecidable. However, in the case of covertly regular programs, we might expect to be in practise able to decide if a given program is covertly regular or not, because transition matrices are in practice not too complex. Of course, such an affirmation needs to be experimentally validated. Such an experimentation is left for future work.

Conclusion

This section exposed how we could cover the exact computation of dependencies both in the regular and covertly regular cases in the case where the basis change is exactly computable. This is a first step to relax the initial syntactic restrictions of the polyhedral model and this enables a new definition of (covertly) regular programs on which the exact computation of dependencies is expressible and coincides with our new semantic definition of dependencies.

Approximate Polyhedral Model for General Imperative Programs

Irregular programs have complex control and non-affine accesses to arrays. In this section we propose to address the problem of non polyhedral control. Non affine accesses are left for future work.

In the previous sections, the key characterization is that the relation linking the program variables (including our annotation) was (in the favorable case) exactly computable. For general programs, we will rely on an over-approximation of this relation.

Dependence Analysis for Non-Affine Control

Let us recall the result of 3: if we are able to link our iteration vectors to the scalar variables of the program with an invertible convert function κ i = convert i (i, j, k), then we can exactly compute the dependencies of a given program. A first remark is that instead of computing the sets K or Q with initial variables, we can equivalently write the equivalent equations on κ i variables, and add the definition of convert as additional constraints, as is illustrated in subsection 6.1. Example. On the Array filling example we obtained C 1 : 0 = i -1, C 2 : (κ 0 ) ≺ (κ 0 , κ 1 ), and C 3 = true. Instead of replacing κ i with their image by convert, we can solve the same constraint system augmented with the constraint κ 1 = 1 + 2(i -1). Now the set Q s 1 ,s 2 is a polyhedron on i and the κ i variables whose projection on i gives the same result Q s 1 ,s 2 = {i = 0} as in 5.1. Now that we have work on general programs, we do not have a convert function any more, we thus compute an over-approximation of the relationship between the scalar variables of the programs and the κ i variables. Definition 6.1. Let P s 1 ( i, κ) (resp. P s 2 ( i, κ)) be polyhedral invariants at statement s 1 (resp. s 2 ). Let us denote by cons(P) the set of constraints of P. Let us define Q s 1 ,s 2 = C 1 ∪ C 2 ∪ cons(P s 1 ) ∪ cons(P s 2 ) the union of C 1 and C 2 constraints and these over-approximations and Q is the projection on the κ i variables. Prop 7. Let o 1 = s 1 , t 1 and o 2 = s 2 , t 2 be two operations in an initial trace O. Then,

o 1 + o 2 ⇒ t 2 ∈ Q s 1 ,s 2 (t 1 )
Proof. As cons(P s 1 ) is an over-approximation of C 3 (s 1 should be a valid iteration), and cons(P s 2 )∪ C 2 is an over-approximation of C 2 (happens-before), all initial dependencies satisfy Q .

Remark. An important issue here is that we do not have any result about the most recent dependence (K) since computing the lexicographic maximum of Q may led to picking a spurious dependency.

As we already mentioned in subsection 5.1, computing polyhedral over-approximations can be done by various methods including abstract interpretation. The precision of our analysis will thus rely on the precision of the underlying invariant generator. In the case of regular or covertly regular programs, if the invariant generator gives us the most precise invariants, then we will recover the result of 3 and 4 (equivalence). Example. Let us consider the following example: A good invariant generator would enable us to find that s 3 does not depend on any iteration of s 1 since its corresponding invariant is empty. However, any over-approximation P s 1 is safe, and we would find out that s 3 depends on s 1 for some values of scalar variables satisfying cons(P s 1 ), thus compute spurious dependencies.

Work in Progress: Dealing with Non-Affine Accesses

To deal with non-affine accesses, we might find inspiration from the recently proposed nonpolyhedral dependency analysis [START_REF] Feautrier | The power of polynomials[END_REF], which uses a variant of the Handelman's algorithm for solving multivariate polynomials. The abundant literature on linear relaxations of polynomials constraints has been recently been put to the attention of the program verification community that now uses it to compute over-approximations [MFK + 16, RVS16] that could be useful for solving our non-linear set of constraints. However we should be careful about their complexity in practice.

Related Work

The array dataflow analysis [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF] and the Omega test [START_REF] Pugh | The omega test: a fast and practical integer programming algorithm for dependence analysis[END_REF] proposed exact dependency analysis for loops with affine controls and array accesses. Both of these work rely on RR n°9232 the ability to characterize the three conditions that define dependency (recall subsection 2.2) as affine functions of syntax elements in the source program-loop iterators. The semantics of the target language are abstracted away and are assumed to provide the required properties. In contrast, our work formulates the dependency analysis based on the semantics, and the connection to syntax elements is later established through the convert function or its approximation. This provides additional flexibility on how the programmer can express their computation. For instance, while loops that can be rewritten as for loops are seamlessly handled as we have shown in subsection 5.1.

Polly [START_REF] Grosser | Polly-performing polyhedral optimizations on a low-level intermediate representation[END_REF] performs polyhedral optimizations to LLVM-IR, which is a low-level IR without high-level information such as loop iterators. The semantic polyhedral regions in a program are identified by searching for a single induction variable (with affine lower bounds and upper bounds) for each loop. Combined with additional analyses and transformations in LLVM, Polly can recognize program regions that are syntactically far from the canonical polyhedral loops in the original high-level specification. In the context of our work, the analysis in Polly can be viewed as a low-level version of our covertly regular loops detection without loop instrumentation. Our specificity is to fully characterize these semantically polyhedral loops and also to leave room for handling non-polyhedral programs through approximations of the convert function.

The original exact dependency analyses were later extended to expand the scope of the analysis, including while loops, non-affine if guards, and non-affine array accesses [BCF97, PW96, BPCB10, VNS13]. In Fuzzy Array Dataflow Analysis [START_REF] Barthou | Fuzzy array dataflow analysis[END_REF], the non-affine conditions are expressed as predicates encoded with additional parameters, whereas the extension to the Omega test [START_REF] Pugh | Non-Linear Array Dependence Analysis[END_REF] express them with uninterpreted function symbols. Exact analysis is possible in some cases, but these extensions require runtime checks or over-approximations in general.

These extensions treat while loops as unbounded for loops with a predicate that defines the exit condition [BCF97, PW96, BPCB10]. The unbounded for loop uses an iterator that is not in the original program, which is analogous to the iteration variables in our work. There are two key differences: (i) we use iteration variables uniformly to both for and while loops, and (ii) we (attempt to) compute connections to syntax elements to express dependencies in terms of integer variables in the source program. For instance, the while loop in subsection 3.2 is viewed as:

1 c[0] := 0; 2 i := 1; 3 for t from 0 4 c[i] := c[i-1] + 1; 5 i := i + 1;
where the variable i is treated as data, and all array accesses are now data-dependent. Our work identifies the relation between i and t, linking the variable i to the iteration count of the while loop.

Alphabets [START_REF] Sanjay Rajopadhye | Alphabets: An extended polyhedral equational language[END_REF] is an equational language that can be viewed as an intermediate representation for polyhedral compilers. The language supports while loops in a manner similar to other work [BCF97, PW96, BPCB10]: unbounded domain with exit condition. The crucial difference 1 is that the dependencies are expressed as affine functions of the domain indices, 1 Alphabets can express such computations as data-dependent dependencies like other work, but this is not the RR n°9232 including the unbounded domain corresponding to while loops. In other words, there are only (semantic) iteration variables in the language. A potential application of our analysis is to construct Alphabets representations of programs including while loops.

Apollo [START_REF] Sukumaran | The polyhedral model of nonlinear loops[END_REF] is a framework for runtime optimization that detects (affine) regularity in program behavior and applies polyhedral optimizations, speculating that the regularity persists. Runtime analysis enables code regions that cannot be determined to be polyhedral at compile-time to be found and optimized. Our work shares some similarities with the dynamically polyhedral programs targeted by Apollo. The main difference is that we target statically regular programs, but with more flexibility on how the program is written.

Conclusion

In this paper we proposed a new semantic formalization of the key analysis of the polyhedral literature, namely Array Dataflow Analysis. We formalized the notion of dependency in a semantic fashion and showed the relevance of this notion by demonstrating its applicability to the traditional syntactic polyhedral programs as well as to covertly regular programs. We also proposed an approximated computation of dependencies in the general case of non-regular control flows.

Future work includes extensions of our analyses for more general programs including nonaffine accesses and more complex data structures such as trees. Based on a proper definition of our general approximated dependence analysis, we will then be able to revisit and extend other classical polyhedral activities such as loop transformations and code generation to allow for optimization and parallelization of programs with while loops and loosened control structures.

(Figure 1 :

 1 Figure 1: Product of matrices with a for loop.

Figure 3 :

 3 Figure 3: Array filling with increasing values

Figure 4 :

 4 Figure 4: The Syracuse algorithm

Figure 5 :

 5 Figure 5: Our semantics 1/3

Figure 6 :

 6 Figure 6: Our semantics 2/3 (while)

Figure 7 :

 7 Figure 7: Our semantics 3/3 (if)

  Definition 4.2 (wvars). Let o = s, t be an operation, the set of variables that s will write at time t is called wvars(o). wvars(o) is either a singleton or the empty set. Example. Let us consider the operation defined by o = (a[i] := a[i-1]+a[i]+1, t). Let us assume that at time t the variable i is equal to 1 (This information is accessible since for t we can recover the whole state corresponding to t and therefore access the content of the memory at this state). Then rvars(o) = { a[0], a[1] } and wvars(o) = { a[1] }. Definition 4.3 (Last write). Given an initial trace O and an operation o i 2 which belongs to O, the function last returns the operation o i 1 (which belongs to O) that last wrote the cell containing the variable v before o i 2 reads it. The function last satisfies the following formula:

Example.

  In 3b, consider statement s 4 , on line 4. The operation s 4 , [ κ 0 , 2 , κ 1 , 0 ] writes in cell c[1] and needs to read c[0] which was last wrote by s 1 , [ κ 0 , 0 ] . Definition 4.4 (Direct Data Dependencies). Let o 2 = s 2 , t 2 be an operation, o 2 directly depends on operation o 1 = s 1 , t 1 if there exists v ∈ rvars(o 2 ) ∪ wvars(o 2 ) such that o 1 ∈ last o 2 (v). It is denoted by o 1 o 2 . Definition 4.5 (Data Dependencies). Operation o 2 depends on operation o 1 if and only if o 1 + o 2 , where + is the transitive closure of . Definition 4.6 (Most Recent Direct Data Dependencies). Let o 2 = s 2 , t 2 be an operation, and D the set of operations on which o 2 directly depends. The most recent operation on which o 2 depends is o 1 = max < D. It is denoted by o 1 o 2 . Prop 2. The most recent dependency of an operation can be either computed from the set of all dependencies or from the set of direct dependencies. In other words, max = max +

0 o 1 o 2 o 3 o 4 o 5 Figure 8 :Figure 9 :

 589 Figure 8: Direct (dashed) and indirect (dotted, obtained by transitive closure) data dependencies of operation o 5 .

3

  default/intended use in Alphabets. Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Computation of Dependencies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 General Imperative Programs With Iteration Vectors 6 3.1 A Mini Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.2 Semantic Extension: Iteration Variables and Iteration Vectors for our Language . 7 3.3 Execution Environment, Final Semantics of our Mini Language . . . . . . . . . . 9 3.4 Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 4 Dependencies for General Programs 11 5 Semantic-Driven Dependency Analysis 12 5.1 Equivalence on Regular Polyhedral Programs . . . . . . . . . . . . . . . . . . . . . 12 5.2 Covertly-Regular Polyhedral Programs . . . . . . . . . . . . . . . . . . . . . . . . 15 5.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 6 Approximate Polyhedral Model for General Imperative Programs 16 6.1 Dependence Analysis for Non-Affine Control . . . . . . . . . . . . . . . . . . . . . 16 6.2 Work in Progress: Dealing with Non-Affine Accesses . . . . . . . . . . . . . . . . 17Campus universitaire de Beaulieu 35042 Rennes Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr

RR n°9232


Grisha Weintraub

Ehud Gudes

Data Integrity Verification in Column-Oriented NoSQL Databases

Keywords: data integrity, database outsourcing, NoSQL

Data integrity in cloud databases is a topic that has received a much of attention from the research community. However, existing solutions mainly focus on the cloud providers that store data in relational databases, whereas nowadays many cloud providers store data in nonrelational databases as well. In this paper, we focus on the particular family of non-relational databases -column-oriented stores, and present a protocol that will allow cloud users to verify the integrity of their data that resides on cloud databases of this type. We like our solution to be easily integrated with the existing real-world systems and therefore assume that we cannot modify the cloud; our protocol is implemented solely on the client side. We have implemented a prototype of our solution, that uses Cloud BigTable as a cloud database, and have evaluated its performance and correctness.

Introduction

For a long time, relational database management systems (RDBMS) have been the only solution for persistent data storage. However, with the phenomenal growth of data, this conventional way of storing has become problematic. To manage the exponentially growing data volumes, the largest information technology companies, such as Google and Amazon, have developed alternative solutions that store data in what have become to be known as NoSQL databases [START_REF] Leavitt | Will NoSQL databases live up to their promise?[END_REF][START_REF] Cattell | Scalable SQL and NoSQL data stores[END_REF]. Some of the NoSQL features are flexible schema, horizontal scaling, and relaxed consistency. Rather than store data in heavily structured tables, NoSQL systems prefer simpler data schema such as key-value pairs or collections of documents. They store and replicate data in distributed systems, commonly across datacenters, thereby achieving scalability and high availability. NoSQL databases are usually classified into three groups, according to their data model: key-value stores, document-based stores, and column-oriented stores. The latter group was inspired by BigTable [START_REF] Chang | Bigtable: A distributed storage system for structured data[END_REF] -a distributed storage system developed by Google that is designed to manage very large amounts of structured data.

In column-oriented stores data is organized in tables, which consist of row keys and column keys. Column keys are grouped into sets called column families.

Column-oriented stores can be used either as internal database systems (just like BigTable inside Google) or as cloud databases -cloud services that provide users with access to data without the need for managing hardware or software. However, storing data in a cloud introduces several security concerns. In particular, since cloud users do not physically possess their data, data integrity may be at risk. Cloud providers (or some malicious entity) can change users' data, omit some of the data from query results or return a version of the data which is not the latest. In other words, data correctness, completeness and freshness might be compromised.

Data integrity in outsourced relational databases has been studied for several years [START_REF] Devanbu | Authentic data publication over the internet[END_REF][START_REF] Li | Dynamic authenticated index structures for outsourced databases[END_REF][START_REF] Yang | Authenticated join processing in outsourced databases[END_REF][START_REF] Li | Authenticated index structures for aggregation queries[END_REF][START_REF] Wei | Integrity assurance for outsourced databases without DBMS modification[END_REF][START_REF] Mykletun | Authentication and integrity in outsourced databases[END_REF][START_REF] Narasimha | DSAC: integrity for outsourced databases with signature aggregation and chaining[END_REF][START_REF] Xie | Integrity auditing of outsourced data[END_REF][START_REF] Wang | Dual encryption for query integrity assurance[END_REF]. Nevertheless, existing solutions are inappropriate for columnoriented NoSQL databases for the following reasons:

1. Data volumes in NoSQL are expected to be much higher than in RDBMS. 2. Data model of column-oriented systems significantly differs from relational model (e.g. a single row in column-oriented database may contain millions of columns). 3. The query model in NoSQL is much simpler than in RDBMS (e.g. joins are usually not supported).

These differences between RDBMS and NoSQL introduce both challenges and opportunities. On the one hand, data integrity assurance in NoSQL systems requires more sophisticated solutions due to its unusual data model. On the other hand, extremely simple query model of NoSQL may allow us to design much simpler and efficient protocols for data integrity verification. The goal of this paper is to demonstrate that data integrity of column-oriented NoSQL databases in the cloud can be verified better (in terms of efficiency and applicability) than it was proposed in previous work. Our main contributions are as follows:

-Development of a novel probabilistic method that allows users to verify data integrity of the data that resides in cloud column-oriented stores and its analysis. -A demonstration of the feasibility of our method by a prototype implementation and its experimental evaluation.

The rest of the paper is structured as follows: Section 2 provides background information and overviews related work. Section 3 presents our method for data integrity verification in column-oriented stores. Security analysis of our approach is presented in section 4. Section 5 introduces our proof-of-concept implementation and provides an experimental evaluation thereof. Section 6 presents our conclusions.

Background and Related Work

As mentioned earlier, the main goal of this paper is to propose a novel method that provides data integrity assurance for column-oriented NoSQL databases in the cloud. In this section, the relevant background is provided. In particular, an overview of column-oriented NoSQL systems is presented in Section 2.1, the cloud model is described in Section 2.2 and possible data integrity attacks are discussed in Section 2.3. Section 2.4 reviews related work.

Column-Oriented Stores

Column-oriented stores, also called wide column stores, extensible record stores, and column-oriented NoSQL databases are storage systems that were built after Google's BigTable [START_REF] Chang | Bigtable: A distributed storage system for structured data[END_REF]. A thorough review of BigTable is given in [START_REF] Weintraub | Dynamo and BigTable -Review and comparison[END_REF], below is a brief summary.

BigTable is a distributed storage system. Data in BigTable is organized in tables consisting of rows. Rows are composed of cells identified by a combination of a row key and a column key. Column key consists of a mandatory column family and an optional column qualifier. Table 1

provides an example of a typical table in BigTable:

-User ID -is a row key.

-Personal Data and Financial Data -are column families.

-Name, Phone, Email, City and Card -are column qualifiers.

-Bob -is a value located in a cell ("1457","Personal Data: Name") Phone = "781455", Name = "Bob" Card = "9875" 1885 Email = "john@g.com", Name = "John" 2501 Phone="781526", City="NY", Email="k@zzz.com", Name="Alice" Card = "6652" 3456

Name="Carol", City="Paris" Card = "6663"

Supported data operations are:

get -returns values from individual rows.

scan -iterates over multiple rows.

put -inserts a value into a specified table's cell.

delete -deletes a whole row or a specified cell inside a particular row.

System Model and Assumptions

Database-as-a-service paradigm (DBaaS), firstly introduced more than a decade ago [START_REF] Hacigms | Providing database as a service[END_REF], has become a prevalent service of today's cloud providers. Microsoft's Azure SQL Database, Amazon's DynamoDB and Google's Cloud BigTable are just a few examples. We assume that there are 3 entities in the DBaaS model (Fig. 1):

-Data owner (DO) -uploads the data to the cloud.

-Cloud provider (CP) -stores and provides access to the data.

-Clients -retrieve the data from the cloud.

Fig. 1: DBaaS Model

There is only one instance of DO and CP in our model, whereas the number of clients is not limited. The data uploaded to the cloud is stored in a columnoriented NoSQL database and all data operations (the DO's writes and clients' reads) are performed according to the column-oriented data model, described in the previous section. Our system model is both write and read intensive. The DO uploads data to the cloud by bulk loading (the rows in a bulk are not necessarily consecutive). We assume that the DO writes only append new rows to the database; existing rows are not updated. We are interested in a highly applicable solution and therefore we assume that no server changes can be performed on the cloud side. Some of the use cases that may suit our system model are:

-Historical financial data -a stock exchange uploads historical stock prices to the cloud for public use. -Open science data -a scientific organization uploads results of the scientific activities to the cloud for anyone to analyze and reuse. -Server metrics -various server metrics (e.g. CPU, memory and network usage) are periodically uploaded to the cloud for further monitoring and analysis.

Integrity and Attack Model

We assume that the CP is trusted neither by the DO nor by the clients and that it can behave maliciously in any possible way to break data integrity. For example, the CP (or somebody that had penetrated the CP machine) may modify values of particular table cells, add or delete new rows or column families, or return partial (or empty) results to the clients' queries. We focus on data integrity protection in the following two dimensions:

1. Correctness -Data received by the clients was originally uploaded to the cloud by the DO and has not been modified maliciously or mistakenly in the cloud side. 2. Completeness -the CP returns to the clients all the data that matches the query. In other words, no data is omitted from the result.

Freshness is another important dimension of data integrity, meaning that the clients get the most current version of the data that was uploaded to the cloud. However, since in our system model there are no updates, freshness is not an issue.

Related Work

Existing solutions can be mainly categorized into three types. The first type is based on the Merkle Hash Tree (MHT), the second is based on digital signatures (DS), and the third uses a probabilistic approach. In the following sections, we review each of these approaches and describe their limitations pertaining to our system model.

MHT-based approach

MHT [START_REF] Merkle | A certified digital signature[END_REF] is a binary tree, where each leaf is a hash of a data block, and each internal node is a hash of the concatenation of its two children. Devanbu et al. in [START_REF] Devanbu | Authentic data publication over the internet[END_REF] introduce a method that uses MHT as Authenticated Data Structure (ADS) to provide data integrity assurance in the DBaaS model. The general idea is to build an MHT for every database table such that MHT leaves are hashes of table's records ordered by a search key. To reduce the I/O operations cost in both client and server sides, instead of using binary trees, trees of higher fanout (MB-Trees) can be used [START_REF] Li | Dynamic authenticated index structures for outsourced databases[END_REF]. Different MHT-based techniques to provide efficient integrity assurance for join and aggregate queries are presented in [START_REF] Yang | Authenticated join processing in outsourced databases[END_REF] and [START_REF] Li | Authenticated index structures for aggregation queries[END_REF] respectively. One of the difficulties in adopting the MHT-based approaches in practice is that RDBMS modification is required for managing ADS on the cloud side. Wei et al. in [START_REF] Wei | Integrity assurance for outsourced databases without DBMS modification[END_REF] propose to serialize ADS into RDBMS thereby providing integrity assurance without RDBMS modification. All of the MHT-based approaches discussed so far assume that the outsourced database is RDBMS. Among other things, it implies that the data is organized in accordance with the relational model and the CP stores the database and the ADS's on a single node. These assumptions are not valid for column-oriented stores and hence another solution is required.

iBigTable [START_REF] Wei | iBigTable: practical data integrity for bigtable in public cloud[END_REF] is a BigTable [START_REF] Chang | Bigtable: A distributed storage system for structured data[END_REF] enhancement that utilizes an MHT to provide scalable data integrity assurance in column-oriented NoSQL databases. It uses Merkle B+ tree -the combination of MHT and B+ tree as an ADS. iBigTable overcomes the limitations of the MHT-based approaches for RDBMS mentioned above. However, it requires modifications of core components of BigTable and hence cannot be applied directly to existing BigTable implementations. Moreover, since iBigTable relies on BigTable internal architecture it cannot be applied to column-oriented stores that have different infrastructure (e.g. Cassandra).

DS-based approach

A natural and intuitive approach to provide data integrity in RDBMS is to use the digital signatures scheme (e.g. RSA [START_REF] Rivest | A method for obtaining digital signatures and public-key cryptosystems[END_REF]) in the following way:

-An additional column containing a hash of concatenated record values signed by the DO's private key is added to every table. -Clients verify record integrity by using the DO's public key.

To reduce the communication cost between client and server and the computation cost on the client side, signature aggregation technique [START_REF] Mykletun | Authentication and integrity in outsourced databases[END_REF] can be used to combine multiple record signatures into a single one. To guarantee completeness, rather than sign individual records, the DO signs consecutive pairs of records [START_REF] Narasimha | DSAC: integrity for outsourced databases with signature aggregation and chaining[END_REF].

Signature based technique for RDBMS uses row-level granularity of integrity -every single row is signed by the DO and hence the smallest unit of the data retrieval is a whole row. Whereas row-level granularity is a natural decision for relational databases, it does not fit column-oriented stores design, where rows may contain millions of column values.

Probabilistic approach

Probabilistic approaches provide only probabilistic integrity assurance, but do not require DBMS modifications and have better performance than MHT-based and DS-based approaches. In this approach, a number of additional records is uploaded to the cloud along with the original records. The more additional records are being uploaded, the higher is the probability to detect data integrity attack. All data is encrypted on a client side so the CP cannot distinguish between the original and the additional records. These additional records may be completely fake as was proposed in [START_REF] Xie | Integrity auditing of outsourced data[END_REF] or original records encrypted with a different (secondary) secret key as was proposed in the dual encryption scheme of [START_REF] Wang | Dual encryption for query integrity assurance[END_REF].

Applying probabilistic approach to column-oriented stores raises difficulties similar to those of the signature-based approach. In addition to the granularity of a signature, granularity of additional data should be chosen according to the column-oriented data model. Another limitation is that in probabilistic approach the whole database must be encrypted.

Summary

In this section we have shown that as of today there is no practical solution for data integrity assurance in column-oriented NoSQL databases; RDBMS approaches cannot be applied directly and the only column stores approach (iBigTable) proposes a customized solution. In the next section, we will introduce our novel approach for data integrity protection in column-oriented NoSQL databases that overcomes the limitations of existing approaches presented above. Some initial ideas of our approach were outlined in [START_REF] Weintraub | Crowdsourced Data Integrity Verification for Key-Value Stores in the Cloud[END_REF], but were limited to keyvalue stores only.

Our approach

Inspired by the existing probabilistic approaches for RDBMS [START_REF] Xie | Integrity auditing of outsourced data[END_REF][START_REF] Wang | Dual encryption for query integrity assurance[END_REF], we propose a novel method that provides probabilistic data integrity assurance in columnoriented NoSQL databases without DBMS modification. In our solution, we also eliminate the main limitation of the existing probabilistic approaches -a requirement that the whole database must be encrypted. Below we describe our protection techniques for correctness and completeness verification.

Preliminaries

In this section we present the basic notions and concepts necessary for the implementation and analysis of approach.

Hash function: We use collision-resistant hash function that has a property that it is computationally hard to find two inputs that hash to the same output. SHA-256 and SHA-512 [START_REF] Standard | FIPS Publication 180-2[END_REF] are examples of such functions. Hash operation on value x is denoted by H(x).

Secret keys: We assume that the DO and the clients share two secret keys -one for data encryption and another one for data authenticity.

Data authentication: To verify data authenticity we use message authentication codes (MAC's). The DO signs its data according to the MAC scheme (e.g. HMAC [START_REF] Krawczyk | HMAC: Keyed-hashing for message authentication[END_REF]) and stores the MAC value in the cloud along with the signed data. Then, based on the MAC value and the received data, clients can verify data authenticity.

Data encryption: Sensitive data that is stored in the cloud is encrypted by the DO and then decrypted by the clients by using symmetric encryption (e.g. AES [START_REF] Pub | 197: Advanced encryption standard (AES)[END_REF]).

Bloom filter: Bloom filters [START_REF] Bloom | Space/time trade-offs in hash coding with allowable errors[END_REF] are randomized data structures that are used to test whether an element is a member of a set. To reduce storage and network overhead Bloom filters can be compressed [START_REF] Mitzenmacher | Compressed bloom filters[END_REF].

The notation we use is presented in Table 2.

Correctness

We have to provide correctness assurance to the following types of client queries:

1. Get row by row key.

2. Get column family by row key and family name.

3. Get column(s) by row key, column family and column name(s).

In order to support these queries, we use the MAC scheme in the following way: When the DO inserts a new row, it calculates hash values for all of the column families and stores them in a special "I-META" column family. After that it calculates the row hash (hash of the concatenation of all of the column family hashes), calculates the MAC of the row hash, and stores it under the special "Row-Mac" column in "I-META" family. Then the correctness of queries is verified as follows.

Verification of queries of type 1 Correctness of the queries of type ( 1) is simply based on the computation and verification of the row MAC.

Verification of queries of type 2 Queries of type (2) are verified as follows:

1. Client receives the requested column family and computes its hash value. 2. Client computes the row hash from the column family hash (step 1) and all other column families' hashes from "I-META" family.

Client computes and verifies the row MAC

Verification of queries of type 3

There is no trivial solution for queries of type (3). One possible approach would be to transform queries of type (3) into queries of type (2) by omitting column names, and then, after correctness verification for all columns, filter out all the columns but the requested ones. Another way would be to sign each column separately. However, since the number of columns in column stores may be very large, both these approaches are inevitably going to produce an enormous overhead.

In our approach, for queries of type (3) we use Bloom filters. For each column family the DO computes a Bloom filter that contains all column values of this family and stores it as a column in "I-META" family. To verify data correctness of the particular column values, clients retrieve the corresponding Bloom filter and use it to check the existence of the received values. If one of the values does not exist in the Bloom filter, the client can be completely sure that data integrity was compromised. If all the values exist, the client has a certain level of confidence (a detailed analysis is provided in Section 4) that the data was not tampered in the cloud side.

A malicious CP may modify the Bloom filters on the cloud side. To avoid that, we compute hash values for all of the Bloom filters and insert them into the row hash along with the column family hashes. We also add to the row hash the row key, so the CP will not be able to return unrelated data values.

Hence, the formal definitions of the row hash is as follows:

Definition 1. Row hash H(r) = H(r key ||H(cf 1 )||H(BF cf1 )||H(cf 2 )||H(BF cf2 )...H(cf N r cf )||H(BF cf N r cf
))

If we would apply the scheme above to the Table 1 it would look as in Table 3. The row hash of the row 1457 would be computed 1 User ID Personal Data Financial Data I-META 1457 Phone = "781455", Name = "Bob" Card = "9875"

Personal-Data-Hash = "2873992" Financial-Data-Hash = "1976503" Personal-Data-Bloom-Value = "0010010" Financial-Data-Bloom-Value = "1000000" Personal-Data-Bloom-Hash = "8703341" Financial-Data-Bloom-Hash = "5848258" Row-Mac = "A73Djd@83393k"

Note that our solution does not require DBMS modification but only slight schema changes (an addition of the I-META column family).

Completeness

Rows linking The intuition behind the rows linking is that every row knows some information about the data stored in some other rows. For example, if we would apply rows linking to the sample data from Table 1, it might look as in Table 4. Row 1457 knows that row 1885 has columns "Email" and "Name" and row 3456 has columns "Name", "City" and "Card". Row 1885 knows what columns exist in rows 2501 and 3456, etc. The formal definition of rows linking is as follows: Definition 2. Rows Linking ∀ x,y ∈ D, x is linked to y ⇐⇒ x contains y's row key and all its column names The DO is responsible for the linking between the rows when uploading the data to the cloud. This linking data then encrypted and stored under "I-META" column family. Afterwards, the clients can rely on linking data to verify the result completeness. For example, consider a query "get all users with id between 1000 and 2000" on Table 1 with linking data from Table 4 and the result that contains only row with id 1457. By checking linking data of the row 1457, the client knows that row 1885 should be a part of the result and thus detects the attack. Here too, the addition of linking data does not require any DBMS modification, only an addition of the new column.

To increase the probability of assurance that all inserted rows are present we use the crowdsourced verification technique. Crowdsourced verification In crowdsourcing (CS) systems [START_REF] Doan | Crowdsourcing systems on the world-wide web[END_REF] users collaborate to achieve a goal that is beneficial to the whole community. The collaboration may be explicit (e.g. Wikipedia and Linux projects) or implicit as in ESP game [START_REF] Von Ahn | Labeling images with a computer game[END_REF] where users label images as a side effect of playing the game. In our approach we build CS system where users implicitly collaborate to achieve a mutual goal -database integrity assurance. It works as illustrated in Fig. 2: 1. A client sends a query to the CP. 2. The CP sends the query result along with the linking data back to the client.

3. The client builds verification queries based on the received linking data and sends them to the CP. 4. The CP sends the result of the verification queries back to the client. 5. The client verifies that the result of the verification queries matches the linking data.

Verification queries (step 3) are built such that the CP cannot distinguish between them and the regular client queries (step 1). Thanks to that, CP's malicious behavior with the client queries will inevitably cause malicious behavior with the verification queries as well and thus will be detected. Note that there is no dependency between the client query (step 1) and the verification queries (step 3) and hence steps 3-5 can be executed asynchronously (i.e. without hurting reads latency).

Fig. 2: Crowdsourced Verification

To ensure that all types of queries are covered (without performing all types of queries each time) we build verification queries according to the original query type. So if the original query was of type 1, in order to build verification query we use only row keys from the linking data. For queries of type 2 and 3 we use column families and column names respectively.

Security Analysis

Correctness

In section 3.2 above we presented our technique for data correctness verification. We considered three different types of queries that might be executed by the clients. Verification of the queries of type ( 1) and ( 2) is based on provably secure primitives -MAC scheme and collision resistant hash function, and hence provides 100% data correctness assurance.

Correctness verification of the queries of type ( 3) is based on Bloom filters and hence provides probabilistic correctness assurance. The DO calculates a Bloom filter for each column family cf as follows: ∀c ∈ cf , c.name||c.value is inserted as a value to BF cf Clients verify the correctness of the retrieved columns by testing their existence in the corresponding Bloom filter. If a particular column is not present in the Bloom filter, they know for sure that its value was changed. In the opposite direction, since the probability of a false positive for an element not in the Bloom filter is:

(1 -(1 -1 m ) kn ) k
where k is the number of the used hash functions, m is a Bloom filter size and n is a number of elements in a Bloom filter [START_REF] Mitzenmacher | Compressed bloom filters[END_REF], if it does exist they know that the value is correct with the following probability:

1 -(1 -(1 -1 m ) kN cf col ) k
where N cf col is a number of columns in a column family.

Parameters m and k are chosen by the DO according to the desired level of the correctness assurance, and storage and computation time constraints. For example, for column family containing 1, 000 columns, m = 8, 192 and k = 5, the client knows with the probability of 98% that the retrieved column value is correct. With a doubled Bloom filter size (i.e. m = 16, 384) the probability to detect modified column increases to 99.8%.

Completeness

Our approach for completeness verification is based on two techniques: rows linking and crowdsourced verification, described in Section 3.3. Simply put, rows linking means that existence of every database row is known to p other rows and crowdsourced verification means that, in addition to their regular queries, clients perform verification queries to verify that rows whose existence is known to other rows do actually exist.

Assuming a uniform distribution of both deleted rows (denoted by d) and range of queries (denoted by q), the probability that after a single query the client will not be able to detect that at least one of the d rows was deleted from the database with |D| rows (or omitted from the result) is:

|D|-pd |D|
Hence, the probability of detecting an attack after q queries is:

1

-( |D|-pd |D| ) q
Fig. 6 shows the probability to detect an attack as a function of a number of queries performed by the clients with |D| = 1, 000, 000, p = 4 and d ∈ {1, 5, 10, 20}. It can be seen that even with p as small as 4, after a relatively small number of queries (production systems receive tens of thousands of queries per second [START_REF] Atikoglu | Workload analysis of a large-scale key-value store[END_REF]) and deleted rows, the chance of the CP to escape from being caught is very low. It looks like the addition of verification queries should slow client queries, however as it is shown in the next section, since these queries are run asynchronously, they do not hurt reads latency. Some overhead in terms of CPU, I/O, and other resources on both client and server sides is still expected, but since this overhead does not affect user experience, it seems to be a reasonable price for the achieved data integrity protection.

Implementation and Experimental Results

For experimental evaluation, we have implemented a prototype of our solution. As a cloud column-oriented store we use Cloud BigTable -Google's NoSQL Big Data database service based on BigTable [START_REF] Chang | Bigtable: A distributed storage system for structured data[END_REF]. To evaluate our solution, we use Yahoo! Cloud Serving Benchmark (YCSB) framework [START_REF] Cooper | Benchmarking cloud serving systems with YCSB[END_REF]. YCSB is a framework for benchmarking database systems. The only thing which needs to be done to benchmark a database with YCSB is to implement a database interface layer. This will allow a framework client to perform operations like "read row" or "insert row" without having to understand the specific API of the database.

We use YCSB in the following way (see Fig. 3

below):

-YCSB framework already has BigTable client implementation.

-We implemented our version of BigTabgle client (BigTable-I) based on the techniques presented in Section 3. Our implementation is available online [START_REF]BigTable-I-Client[END_REF]. -For performance analysis, we executed different workloads on both clients (BigTable and BigTable-I) and compared their execution time. -For correctness analysis, we used our client to upload data to the cloud.

Then we deleted random rows from the database and performed random read queries until the deletion of the rows was detected. For our experiments, we created Cloud BigTable cluster with 3 nodes. We configured "zone" to be "europe-west1-b" and storage type to be "HDD". For all workloads, we used random rows of 1KB size (10 columns, 100 bytes each, plus key).

Performance Analysis

We used the following types of workloads:

-Workload A (Inserts only): Predefined number of rows are inserted into the database. -Workload B (Reads only): Predefined number of rows are retrieved from the database.

We executed each workload three times for each client with 1, 000, 3, 000 and 5, 000 operations and with parameter p (parameter of the linking factor) set to 4 (runs with the different p values are presented in Section 5.3 below). The results below represent the average value of these three executions.

Workload A (Inserts Only) The cost of Bigtable-I insert operation is dominated by two encryption and one hash operations (MAC calculation and encryption of linking data). Experimental results of workload A (Fig. 4) show that this overhead increases insert execution time by 5% in average for the client.

Workload B (Reads Only)

The cost of BigTable-I read operations is similar to the cost of inserts (MAC calculation and linking data decryption) with an additional cost of p verification queries. Since in our implementation we perform verification queries asynchronously, they do not impact read execution time. According to the workload B results (Fig. 5), our protocol increases read execution time by 5% in average for the client.

Correctness Analysis

To demonstrate that our approach works as expected, we uploaded 10, 000 rows to the cloud via BigTable-I client. Then we deleted random rows from the cloud database (up to 20 rows) and ran "random reads" workload until the deletion of rows was detected. We performed this experiment with different values of parameter p -4, 6 and 8. For each value of p and the number of deleted rows, we ran "random reads" workload 3 times. The results presented in Fig. 7 represent the average value of these three executions. Our experimental results support our security analysis (Section 4.2) -even after a relatively small number of queries and deleted rows the attack detection is inevitable. Only for the rare case of very few deletions, many queries are required.

Conclusions and Future Directions

In this paper, we present our novel method for data integrity assurance in cloud column-oriented stores. Our method provides both data correctness and data completeness guarantees. To verify data correctness of rows and column families we use a MAC scheme similar to the DS-based approach [START_REF] Mykletun | Authentication and integrity in outsourced databases[END_REF], while columns correctness is verified probabilistically by using Bloom Filters [START_REF] Bloom | Space/time trade-offs in hash coding with allowable errors[END_REF]. Our method for data completeness verification is inspired by crowdsourcing systems [START_REF] Doan | Crowdsourcing systems on the world-wide web[END_REF] users collaborate to achieve a mutual goal -database integrity assurance. To the best of our knowledge, our work is the first work that utilizes Bloom Filters and crowdsourcing model for data correctness and data completeness verification, respectively.

The main advantage of our method over existing approaches is its high applicability -it can be applied to existing systems without modifying the serverside. We demonstrate its applicability through a proof-of-concept implementation. While using cloud column-oriented NoSQL database (Cloud BigTable) as a black-box, we have implemented our protocol solely on the client side and conducted experimental evaluation thereof. The experimental results show that our scheme imposes a reasonable overhead (around 5% in average) while it can detect an attack after a relatively small number of client queries (in most cases less than 2% of the database is queried before the attack is detected).

The challenge of data integrity in cloud databases is far from being solved. There are many different types of databases that may be addressed (e.g. documentoriented, graph databases, time-series databases). Different system models may be considered (e.g. multi-data-owner model, multi-cloud model, support for updates and freshness guarantees). For future work, we plan to address some of these challenges by using techniques developed in this work and by investigating other techniques as well.

  as follows: H(Row-Key || Personal-Data-Hash || Financial-Data-Hash || Personal-Data-Bloom-Hash || Financial-Data-Bloom-Hash) = H(1457 || 2873992 || 1976503 || 8703341 || 5848258)

Fig. 3 :

 3 Fig. 3: Experimental evaluation with YCSB framework

Fig. 4 :

 4 Fig. 4: Workload A results Fig. 5: Workload B results

Fig. 6 : 7 :

 67 Fig. 6: Completeness verification analysis Fig. 7: Correctness analysis results

Table 1 :

 1 Sample "Users" Table in Column-Orientes Store

	User ID	Personal Data	Financial Data
	1457

Table 2 :

 2 Notation

	Symbol	Description
	||	String concatenation
	D	A database
	r	A database row
	cf	A column family
	N r cf	Number of column families in row r
	r key	Row key of the row r
	BF cf Bloom filter containing all the columns of the family cf
	p	Number of rows linked to each DB row

Table 3 :

 3 Correctness scheme example for data from Table

Table 4 :

 4 Rows linking example for data from Table1

	Row Key	Linking Data
	1457	1885:email,name; 3456:name,city,card
	1885	2501:phone,email,city,name,card; 3456:name,city,card
	2501	1457:phone,name,card; 1885:email,name
	3456	1457:phone,name,card; 2501:phone,email,city,name,card