S De Capitani Di Vimercati

S Foresti

S Jajodia
email: jajodia@gmu.edu

S Paraboschi
email: parabosc@unibg.it

P Samarati

Optimizing Integrity Checks for Join Queries in the Cloud

The large adoption of the cloud paradigm is introducing more and more scenarios where users can access data and services with an unprecedented convenience, just relying on the storage and computational power offered by external providers. Also, users can enjoy a diversity and variety of offers, with the possibility of choosing services by different providers as they best suit their needs. With the growth of the market, economic factors have become one of the crucial aspects in the choice of services. However, security remains a major concern and users will be free to actually benefit from the diversity and variety of such offers only if they can also have proper security guarantees on the services. In this paper, we build upon a recent proposal for assessing integrity of computations performed by potentially untrusted providers introducing some optimizations, thus limiting the overhead to be paid for integrity guarantees, and making it suitable to more scenarios.

Introduction

The competitive pressures are driving the IT sector away from the classical model that assumed the processing and storage of an organization data within the internal information system, toward the use of storage and processing capabilities offered by providers, which can benefit from economies of scale deriving from the large size of the infrastructure and service catalogue, together with possible access to less expensive resources. Along this line, we can expect a continuous increase in the differentiation of the market for cloud services. For instance, in the area of cloud architectures, interest has emerged on hybrid clouds and on a distinction between cloud storage and cloud computational services. Storage and computational services respond in fact to separate requirements, with distinct profiles. The first should offer reliability for data storage, typically corresponding to providers with high reputation on the market. The second should offer availability of -possibly cheap -computational power, which can be offered by unknown providers. Reputation of the provider is, in this case, less critical, as it is relatively easy to move computation from one provider to another, and the most important parameter becomes the price of the service. An obstacle to a stronger differentiation in the market between storage and computational resources is however represented by the security concerns of users, who can see the involvement of multiple parties in the processing of their information as increasing the risk of confidentiality and integrity violations.

In this paper, we present an approach for users to protect confidentiality of processed data and to assess the integrity of computations performed by potentially untrusted computational providers, operating over data stored at trusted storage providers. Our approach builds upon a recent proposal [START_REF] Vimercati | Integrity for join queries in the cloud[END_REF], aimed at controlling the behavior of a computational provider that joins data stored at independent trusted storage servers. We address the problem of optimizing integrity controls so to decrease their performance and economic overheads making them suitable to more scenarios and enabling their application with stronger integrity guarantees. In particular, we introduce two optimization techniques. The first technique (Sect. 3) exploits the execution of the join with a semi-join strategy, hence possibly decreasing data communication and consequent performance/economic costs, while leaving unaltered the offered guarantees. The second technique (Sect. 4) limits the application of the integrity checks to a small portion of the data, producing a considerable saving in terms of performance and economic cost, though at the price of a reduced integrity guarantee. The two optimizations are independent and orthogonal and can be used individually or in combination (Sects. 5 and 6).

Scenario and Basic Concepts

We present the basic idea of the approach on which we build our optimization techniques. The scenario is characterized by a client that wishes to evaluate a query involving a join over two relations, B l and B r , stored at storage servers S l and S r , respectively, by using a computational server C s . The storage servers are assumed to be trustworthy while the computational server is not. The query is of the form "select A from B l join B r on B l .I = B r .I where C l and C r and C lr ," where A is a subset of attributes in B l ∪ B r ; I is the set of join attributes; and C l , C r , and C lr are Boolean formulas of conditions over attributes in B l , B r , and B l ∪ B r , respectively. Typically, execution of such a query involves in pushing down, to each of the storage servers, the evaluation of the condition (C l and C r ) on its own relation. We assume that, regardless of the degree of the original schema, relations L and R resulting from the evaluation of C l and C r , respectively, have schema (I, Attr ), where I and Attr represent the set of join attributes and all the other attributes, respectively, as a unit. Without security concerns, relations L and R are then sent to the computational server, which performs the join, evaluates condition C lr and returns the result to the client. Since the computational server is not trusted, the proposal in [START_REF] Vimercati | Integrity for join queries in the cloud[END_REF]: i) provides data confidentiality by encrypting on the fly the relations sent to the computational server, with a key communicated by the client to the storage servers, ii) provides integrity guarantees by using a combination of controls as follows:

markers: each of the storage servers inserts fake control tuples (markers), not recognizable by the computational server, in the relation to be sent to the computational server. Markers are inserted so to join (i.e., belong to the result) and to not collide with real join attribute values (to not create spurious joined tuples). -twins: each of the storage servers duplicates (twins) some of the tuples in its relation before sending it to the computational server. The creation of twins is easily controlled by the client by specifying a percentage of tuples to be twinned and a condition for twinning. -salts/buckets: used in alternative or in combination to destroy recognizable frequencies of combinations in one-to-many joins. Salts consist in salting the encryption at side "many" of the join so that occurrences of a same value become distinct; at the same time salted replicas are created at side "one" of the join so to create the corresponding matching. Bucketization consists in allowing multiple occurrences of the same (encrypted) value at the side many of the join, but in such a way that all the values have the same number of occurrences. Bucketization can help in reducing the number of salts to be inserted, while possibly requiring insertion of dummy tuples (to fill otherwise not complete buckets).

Join computation, illustrated in Fig. 1(a), works now as follows. Each storage server receives in encrypted form its sub-query, together with the key to be used to encrypt the sub-query result, and the needed information to regulate the use of markers, twins, salts and buckets. It then executes the received sub-query (as before), and applies over the resulting relation L (R, resp.) markers, twins, salts and buckets as appropriate, producing a relation L * (R * , resp.). Relation L * (R * , resp.) is then encrypted producing relation L * k (R * k , resp) to be sent to the computational server. Encrypted relation L * k (R * k , resp.) contains two encrypted chunks for each tuple: L * k .I k (R * k .I k , resp.) for the join attribute, and L * k .Tuple k (R * k .Tuple k , resp.) for all the other attributes (including the join attribute). The computational server receives the encrypted relations from the storage servers and performs the join returning the result J * k to the client. The client receives the join result, decrypts it, checks whether the tuples have been correctly joined (i.e., L * .I obtained decrypting L * k .Tuple k is equal to R * .I obtained decrypting R * k .Tuple k ), and discards possible tuples with dummy content. Then, it checks integrity by analyzing markers and twins: an integrity violation is detected if an expected marker is missing or a twinned tuple appears solo. Note that the combined use of markers and twins offers strong protection guarantees. In fact, when omitting a large number of tuples in query results, the probability that the omission goes undetected increases with respect to twins, and decreases with respect to markers (e.g., one marker is sufficient to detect that an empty result is not correct), and vice versa. Figure 1(b) illustrates an example of relations L and R and of their extensions obtained by assuming: the presences of one marker (with value x for the join attribute), twinning tuples with join attribute equal to b, and adopting 2 salts and buckets with 2 tuples each. Figure 1(c) reports the join result J * obtained by the client decrypting relation J * k received from the computational server. 3 Semi-join

The first optimization we illustrate consists in performing the join according to a semi-join strategy. Without security concerns, a semi-join simply implements a join operation by first considering only the projection of the join attribute over the stored relations. Only after the join is computed, the join attribute is extended with the other attributes from the source relations to produce the final result. In our distributed setting, semi-joins -while requiring additional data flows -avoid communication of unnecessary tuples to the client and of non-join attributes to the computational server, producing a saving of the total communication costs for selective joins and/or relations with tuples of considerable size (see Sect. 6). Our approach for executing a semi-join in conjunction with the security techniques illustrated in the previous section works as follows. The execution of the join at the computational server basically works as before: it again receives from the storage servers encrypted relations on which markers, twins, salts and buckets have been applied; it computes the join between them; and it sends the result to the client. However, in this case:

the storage servers do not communicate to the computational server their entire tuples (relation L) but rather much slimmer tuples (relation LI) with The join process is illustrated in Fig. 2, where the striped triangle corresponds to the process in Fig. 1(a).

Note that, while entailing more flows (the previous process is a part of this), the semi-join execution limits the transfer of non-join attributes, thus reducing the amount of data transferred. Note also that while the storage servers and the client are involved in the execution of some computation to combine tuples, this computation does not entail an actual join execution but rather a simple scan/merging of ordered tuples that then requires limited cost. Figure 3 illustrates an example of join computation over relations L and R in Fig. 1(b) according to the semi-join strategy. The semi-join execution strategy leaves unchanged the integrity guarantees offered by our protection techniques. In fact, the join computed by the computational server relies on the same protection techniques used for the computation of a regular join, and the storage servers are assumed to correctly evaluate the queries received from the client. The probability ℘ that the computational server omits o tuples without being detected is then the same of regular joins, that is,

℘ = (1-o f ) m •(1-2 o f +2( o f ) 2 ) t ≈ e -2 t
f o , where f is the cardinality of relation J * with t twin pairs and m markers [START_REF] Vimercati | Integrity for join queries in the cloud[END_REF]. In fact, the probability that no marker is omitted is (1 -o f ) m , while the probability that, for each twin pair, either both tuples are omitted or both are

JI * k Ik L.Tuplek R.Tuplek α λ1 ρ1 α λ1 ρ2 β λ2 ρ3 β λ2 δ1 β λ2 ρ3 β λ2 δ1 χ µ1 µ2 χ µ1 δ3 JI * L * .I L * .T id R * .I R * .T id a l1 a r1 a l1 a r2 b l2 b r3 b l2 b d1 b l2 b r3 b l2 b d1 x m1 x m2 x m1 x d3 JI L.Tid R.Tid
L Tid I Name l1 a Ann l2 b Beth l3 c Cloe LI I T id a l1 b l2 c l3 LI * I T id a l1 a ′ l ′ 1 b l2 b ′ l ′ 2 c l3 c ′ l ′ 3 b l2 b′ l ′ 2 x m1 LI * k Ik L.Tuplek α λ1 α ′ λ ′ 1 β λ2 β ′ λ ′ 2 γ λ3 γ ′ λ ′ 3 β λ2 β′ λ ′ 2 χ µ1 RI * k Ik R.Tuplek α ρ1 α ρ2 β ρ3 β δ1 ǫ ρ4 ǫ ρ5 ǫ ′ ρ6 ǫ ′ δ2 β ρ3 β δ1 χ µ2 χ δ3 RI * I T id a r1 a r2 b r3 b d1 e r4 e r5 e ′ r6 e ′ d2 b r3 b d1 x m2 x d3 RI I T id a r1 a r2 b r3 e r4 e r5
preserved is (1-2 o f +2( o f ) 2 ) t .
This probabilistic analysis has also been confirmed by and experimental analysis [START_REF] Vimercati | Integrity for join queries in the cloud[END_REF].

Limiting Salts and Buckets to Twins and Markers

The overhead caused by the adoption of our protection techniques is mainly due to salts and buckets [START_REF] Vimercati | Integrity for join queries in the cloud[END_REF], which are used to protect the frequency distribution of the values of the join attribute in case of one-to-many joins. In the following discussion, we refer to the execution of the join according to the process described in Sect. 2. Let s be the number of salts and b be the size of buckets defined by the client. Relation L * includes s copies of each original tuple in L and of each twin. Relation R * instead includes b tuples for each marker (one marker and (b -1) dummy tuples) and between 0 and (b-1) dummy tuples for each value of the join attribute appearing in R and in the twinned tuples. Hence, also the join result J * will have b tuples for each marker and between 0 and (b-1) dummy tuples for each original and twinned value of the join attribute. For instance, with respect to the example in Fig. 1(b), the adoption of our protection techniques causes the presence of six additional tuples in L * and R * , and five additional tuples in J * .

The second optimization we propose aims at limiting the overhead caused by the adoption of salts and buckets by applying them only to twins and markers rather than to the whole relations. Twins and markers (properly bucketized and salted) would form a Verification Object (VO) that can be attached to the original (encrypted) relation. As an example, Fig. 4 illustrates the extended version of relations L and R in Fig. 1(b) where salts and buckets operate only on twins and markers. It is immediate to see that this optimization saves three tuples in L * , two in R * , and one in J * . The strategy of limiting salts and buckets to twins and markers can be adopted in combination with both the regular and the semi-join strategies, reducing the computational overhead in both cases. While providing performance advantages, this strategy may reduce the integrity guarantee provided to the client. Let us consider a relation J * , with f original tuples, t twin pairs, and m markers. We examine the probability ℘ that the computational server omits o original tuples without being detected. We build a probabilistic model considering the worst case scenario, assuming that the computational server: i) is able to recognize the tuples in VO (only the tuples in VO have a flat frequency distribution), ii) knows the number m of markers in VO, iii) but cannot recognize which tuples in VO are twins and which are markers, or which of the original tuples have been twinned. We also consider all the tuples in a bucket as a single tuple. In fact, the computational server either preserves or omits buckets of tuples in their entirety as omissions of subsets of tuples in a bucket can always be detected. If the server omits o tuples out of f , the probability for each twin to be omitted will be o f . To go undetected, the server should provide a configuration of VO consistent with the f -o returned tuples. There is only one such configuration, which contains a number of tuples between m and (m+t). The goal of the computational server is to maximize the probability of being undetected. We can model the behavior of the server considering two phases. In the first phase, the server determines the number of tuples that should belong to VO after the omission. Since there is a uniform and independent probability for the omission of twins, the number of expected tuples in VO follows a binomial distribution. This means that the probability that VO contains (m+t)-k tuples is

℘ omit = t k (1-o f ) t-k ( o f ) k (e.
g., the probability that VO does not miss any tuple, k = 0, is

℘ omit = (1 -o f ) t ).
In the second phase, the server tries to guess the correct configuration including (m + t) -k tuples. The number of such configurations depends on the number of missing tuples: if the server knows that k of the (m+t) tuples in VO are missing, the number of possible configurations is m+t k , and the probability ℘ guess of guessing it right is the inverse of this quantity. For instance, if no tuple is omitted (k = 0), the server is certain of guessing the right configuration, whereas if all the twins have been omitted, the probability of randomly guessing the right configuration with exactly m tuples is 1/ m+t m , that is, m! • t!/(m + t)!. The server can estimate the probability of a correct guess for each strategy by multiplying the first term with the second term, that is, ℘ = ℘ omit • ℘ guess . The server, to maximize the chance of not being detected, will have to choose the strategy that exhibits the greatest value. Since the second term exhibits an exponential growth with the increase in k, the server will typically prefer the strategy where no tuple in VO is omitted.

Figure 5 shows the result of the analysis for configurations with 1 or 2 twins and a variable number of markers. For the configuration with 1 twin in Fig. 5(a), we can see that the strategy that keeps all the elements in VO (independently from the number of markers) is preferable for a large range of omissions. When the number of markers increases, the cutoff between the selection of the strategy that tries to guess the tuple to omit from VO moves progressively to the right. A similar behavior characterizes the configuration with 2 twins described in Fig. 5(b), which shows that there is a range of values for o f where each configuration is preferable, but as the number of markers increases, the "keep all" strategy extends its benefit. The ability to avoid detection when omitting tuples becomes negligible when we consider configurations with the number of twins and markers that we expect to use in real systems.

As said above, it is convenient for the server to keep all the tuples in VO. In this case, the omission goes undetected if the server does not omit any original tuple that has been twinned. The probability ℘ for the server to go undetected is then equal to ℘ = (1 -o f ) t ≈ e -t f •o . Figure 6 compares the results obtained when salts and buckets protect the whole relations ("full salts and buckets" in the figure) with the case where salts and buckets protect only VO ("VO-only salts and buckets" in the figure), assuming t f =15%. We note that limiting salts and buckets to twins and markers offers roughly half the protection of applying salts and buckets to the whole relation. Intuitively, the client can obtain the same protection guarantee by doubling the ratio t f of twins. We note however that, even limiting salts and buckets to VO, the probability that the server is not detected when omitting more than 30 tuples is negligible and is independent from the number f of tuples in the original relation. Since the computational server cannot selectively omit tuples from the join result (i.e., it cannot recognize tuples that have a twin), the advantage obtained from the omission of less than 30 tuples does not justify the risk of being detected in its omission.

Performance Analysis

We now evaluate the performance benefits obtained with the introduction of the semi-join strategy and the use of salts and buckets only on twins and markers. The performance costs depend on both the computational and communication costs. The computational costs are however dominated by the communication costs. In fact, the computational costs at the client and at the storage servers can be considered limited with respect to the computational costs at the computational server, which however can rely on a high amount of computational resources and on traditional techniques for optimizing join evaluation. In the following, we then focus our analysis first on the communication costs when evaluating a join as a regular join (RegJ ) [START_REF] Vimercati | Integrity for join queries in the cloud[END_REF] or as a semi-join (SemiJ ), according to the process described in Sect. 3. We then analyze the communication costs obtained when limiting salts and buckets to twins and markers.

Semi-join vs regular join. This analysis focuses on the amount of data exchanged among the involved parties (i.e., number of tuples transferred multiplied by their size). We first note that both the regular join and the semi-join require a common phase (Phase 1) where there is an exchange of data (tuples) between the storage servers and the computational server and between the computational server and the client. In this phase, regular join and semi-join differ in the size of the tuples transferred among the parties. The semi-join then requires an additional phase (Phase 2) where the client and the storage servers interact to compute the final join result. We analyze each of these two phases in details.

Phase 1 [S l ,S r → C s ; C s → Client]. As already discussed, the only difference between SemiJ and RegJ is the size of the tuples communicated, while the number of tuples in the join operands and in its result is the same for both strategies. SemiJ requires the transmission of the join attribute and of the tuple identifiers only, which are the two attributes forming the schema of relations LI and RI. RegJ requires instead the transmission of all the attributes in L and R.

If the size of the tuples in L and R is higher than the size of the tuples in LI and RI, SemiJ implies a lower communication cost than RegJ . Formally, the amount of data transmitted during this phase is:

SemiJ : |L * | • size L + |R * | • size R + |J * | • (size L + size R ) RegJ : |LI * | • size IT + |RI * | • size IT + |JI * | • 2size IT
where size L is the size of the tuples in L, size R is the size of the tuples in R, size IT is the sum size I + size T id , with size I the size of the join attribute I and size T id the size of the tuple identifier T id. Since LI * (RI * and JI * , resp.) has the same number of tuples as L * (R * and J * , resp.), the difference in the communication cost is:

|L * | • (size L -size IT ) + |R * | • (size R -size IT ) + |J * | • (size L + size R -2size IT ).
Phase 2 [Client →S l ,S r ; S l ,S r → Client]. The number of tuples exchanged between the client and S r is equal to the number of tuples resulting from the join computed by the computational server in the previous phase, after the removal of markers, twins, and dummies (i.e., |JI|=|RJ|). The number of tuples exchanged between the client and S l depends on the type of join. In case of one-to-one joins, the number of tuples coincides with the number of tuples transmitted from the client to S r (i.e., |JI|=|LI|). In case of one-to-many joins, the number of tuples is lower since the same tuple in LI (L, resp.) may appear many times in the join result JI (J, resp.). Assuming a uniform distribution of values, the number of different values for the join attribute in RI is 2|RI| nmax . Given the selectivity σ of the join operation, the number of different values for the join attribute in JI is σ • 2|RI| nmax , which corresponds to the number of tuples exchanged between the client and S l . The size of the tuples transmitted from the client to each storage server is size T id since the client transmits only the values of the tuple identifier T id. The size of the tuples transmitted from the storage servers to the client is equal to the size of the tuples in the original relations L and R (i.e., size L and size R , resp.). Formally, the amount of data exchanged during this phase is: one-to-one join:

2|JI| • size T id + |JI| • size L + |JI| • size R ; one-to-many join: (|JI| + σ • 2|RI| nmax ) • size T id + σ • 2|RI| nmax • size L + |JI| • size R .
By comparing the amount of data transmitted in Phase 2 with the additional amount of data transmitted in Phase 1 caused by the regular join, we note that the semi-join is convenient for relations with large tuples (i.e., size IT << size L and size IT << size R ), as also shown by our experimental analysis (Sect. 6). The advantage of the semi-join with respect to the regular join appears also more evident in case of one-to-many joins where a tuple in the left operand can appear many times in the join result (i.e., |LJ| ≈ σ • 2|RI| nmax << |JI|). In fact, with the semi-join strategy the client receives each tuple in L that belongs to the final result only once, while it receives many copies of the same tuple when adopting the regular join approach.

Limiting salts and buckets to twins and markers. The saving, in terms of communication cost, provided applying salts and buckets to markers and twins rather than to the whole relation can be computed by analyzing the difference in the number of tuples in L * , R * , and J * . We analyze each relation in detail.

-L * . Since only twin tuples are salted, we save the salted copies of the tuples in L, that is, (s -1) • |L| tuples. -R * . Since buckets operate only on twins and markers, we save the dummy tuples of the buckets formed with the tuples in R. Since for each value of the join attribute, there is at most one bucket with dummy tuples with, on average, b-1 2 dummy tuples, and there are 2|R| nmax distinct values for the join attribute (again assuming a uniform distribution of values), we save b-1 nmax •|R| tuples.

-J * . The join result contains the subset of the tuples in R * that combine with the tuples in L * . The number of tuples saved in J * is then a fraction of the number of tuples saved in R * , that is, σ

• b-1 nmax • |R|.
The overall advantage provided by limiting salts and buckets to twins and markers is: (s -1)

• |L| • size L + b-1 nmax • |R| • size R + σ • b-1 nmax • |R| • (size L + size R ).

Experimental Results

To assess the performance advantage of the semi-join strategy with respect to the regular join and of limiting salts and buckets to twins and markets, we implemented a prototype enforcing our protection techniques, and run a set of experiments. We used for the computational server a machine with 2 Intel Xeon Quad 2.0GHz, 12GB RAM. The client machine and the storage servers were standard PCs running an Intel Core 2 Duo CPU at 2.4 GHz, with 4GB RAM, connected to the computational server through a WAN connection with a 4 Mbps throughput. The values reported are the average over six runs.

Regular join vs semi-join. A first set of experiments was dedicated to the comparison between the regular join and the semi-join. The experiments also evaluated the impact of latency on the computation, comparing the response times for queries over local networks (local client configuration) with those obtained with a client residing on a PC at a distance of 1,000 Km connected through a shared channel that in tests demonstrated to offer a sustained throughput near to 80 Mbit/s (remote client configuration). The experiments used a synthetic database with two tables, each with between 10 4 and 10 6 tuples, with size equal to 30 and 2,000 bytes. We computed one-to-one joins between these tables, using 500 markers and 10% of twins. The results of these experiments are reported in Fig. 7.

The results confirm that the use of semi-join (SemiJ in the figure) gives an advantage with respect to regular join (RegJ in the figure) when the tuples have a large size, whereas the advantage becomes negligible when executing a join over compact tuples. This is consistent with the structure of the semi-join computation, which increases the number of exchanges between the different parties, but limits the number of transfers of non-join attributes. When the tuples are large, the benefit from the reduced transfer of the additional attributes compensates the increased number of operations, whereas for compact tuples this benefit is limited. The experiments also show that the impact of latency is modest, as the comparison between local client and remote client configurations of the response times for the same query shows a limited advantage for the local client scenario, consistent with the limited difference in available bandwidth.

The results obtained also confirm the scalability of the technique, which can be applied over large tables (up to 2 GB in each table in our experiments) with millions of tuples without a significant overhead.

Limiting salts and buckets to twins and markers. A second set of experiments was dedicated to the analysis of the use of salts and buckets. The experiments considered a one-to-many join, evaluated as a regular join, over a synthetic database containing 1,000 tuples in both join operands. We tested configurations with at most 50 occurrences of each value, and used a number of salts s varying between 1 and 100 and buckets of size b=⌈ 50 s ⌉. The experiments evaluating the overhead of the protection techniques when salts and buckets are used only on markers and twins show that the overhead due to salts and buckets is proportional to the fraction of tuples that are twinned. For instance, if we add a 10% of twins, the overhead for salts and buckets will be one tenth of what we would have observed if applying the protection to all the tuples. Figure 8 compares the response time observed when executing the query without using our protection techniques ("base" in the figure), when using 50 markers and 15% of twins with salts and buckets on the whole table ("full salts and buckets" in the figure), and a configuration with 50 markers and 30% of twins with salts and buckets only on markers and twins ("VO-only salts and buckets" in the figure ). The experiments confirm that the increase in response time represents a fraction t f (with t the number of twins and f the cardinality of the join result) of the increase that would otherwise be observed using salts and buckets over all the tuples. The figure also shows that the overhead due to the adoption of our protection techniques is limited. Economic analysis. Besides the response time perceived by the user, the choice between regular and semi-join needs to take into consideration also the economic cost of each alternative. We focused on evaluating the economic advantage of the availability of the semi-join, besides regular join, strategy when executing queries [START_REF] Kossmann | An evaluation of alternative architectures for transaction processing in the cloud[END_REF]. In fact, in many situations the semi-join approach can be less expensive, since it entails smaller flows of information among the parties.

In our analysis, we assumed economic costs varying in line with available solutions (e.g., Amazon S3 and EC2, Windows Azure, GoGrid), number of tuples to reflect realistic query plans, and reasonable numbers for twins and markers. In particular, we considered the following parameters: i) cost of transferring data out of each storage server (from 0.00 to 0.30 USD per GB), of the computational server (from 0.00 to 0.10 USD per GB), and of the client (from 0.00 to 1.00 USD per GB); ii) cost of transferring data to the client (from 0.00 to 1.00 USD per GB);4 iii) cost of CPU usage for each storage server (from 0.05 to 2.50 USD per hour), for the computational server (from 0.00 to 0.85 USD per hour), and for the client (from 1.00 to 4.00 USD per hour); iv) bandwidth of the channel reaching the client (from 4 to 80 Mbit/s); v) size size IT = size I + size T id of the join attribute and the tuple identifier (from 1 to 100 bytes); vi) number of tuples in L (from 10 to 1,000) and the size of the other attributes size Lsize IT (from 1 to 300 bytes); vii) number of tuples in R (from 10 to 10,000) and the size of the other attributes size Rsize IT (from 1 to 200 bytes); viii) number m of markers (from 0 to 50); ix) percentage t f of twins (from 0 to 0.30); x) number s of salts (from 1 to 100); xi) maximum number nmax of occurrences of a value in R.I (from 1 to 100); xii) selectivity σ of the join operation (from 0.30 to 1.00). Similarly to what is usually done in finance and economics to compare alternative strategies in systems whose behavior is driven by a large number of parameters assuming values following a probability distribution, we used a Monte Carlo method to generate 2,000 simulations varying the parameters above and, for each simulation, we evaluated the cost of executing a join operation as a regular and as a semi-join. We compared the cost of evaluating 2,000 one-to-one and 2,000 one-to-many join queries with (and without resp.) the availability of the semi-join technique for query evaluation. We assume that the query optimizer can assess which of the two strategies (i.e., RegJ , SemiJ ) is less expensive for each query. Figures 9(a) and 9(b) illustrate the total costs as the number of query grows for the two scenarios, considering one-to-one and one-to-many queries, respectively. As visible in the figure, if all the queries are evaluated adopting the regular join approach, the total cost (continuous line) reaches higher values than with the availability of the semi-join approach (dotted line). This trend is more visible for one-tomany joins, where the total cost reached when all the queries are evaluated as regular joins is 2,475 USD while with the availability of the semi-join approach it remains at 1,321 USD, with a total saving of 1,160 USD (corresponding to 46,85%). In fact, out of the 2,000 one-to-many queries, 1784 were evaluated as semi-joins, while for the remaining 216 the regular join solution was cheaper. For one-to-one joins, as expected, the total saving is lower (24.77%) since half of the 2,000 queries considered are cheaper when evaluated as regular joins.

Related Work

Our work falls in the area of security and privacy in emerging outsourcing and cloud scenarios [START_REF] Damiani | Balancing confidentiality and efficiency in untrusted relational DBMSs[END_REF][START_REF] Hacigümüş | Executing SQL over encrypted data in the database-service-provider model[END_REF]. In this context, researchers have proposed solutions addressing a variety of issues, including data protection, access control, fault tolerance, data and query integrity (e.g., [START_REF] Basu | Privacy-preserving collaborative filtering on the cloud and practical implementation experiences[END_REF][START_REF] Vimercati | Enforcing subscription-based authorization policies in cloud scenarios[END_REF][START_REF] Vimercati | Encryption policies for regulating access to outsourced data[END_REF][START_REF] Vimercati | Managing and accessing data in the cloud: Privacy risks and approaches[END_REF][START_REF] Jhawar | Fault tolerance and resilience in cloud computing environments[END_REF][START_REF] Jhawar | Fault tolerance management in cloud computing: A system-level perspective[END_REF][START_REF] Ren | Security challenges for the public cloud[END_REF]). In particular, current solutions addressing the problem of verifying the integrity (i.e., completeness, correctness, and freshness) of query results are based on the definition of a verification object returned with the query result. Different approaches differ in the definition of the verification object and/or in the kind of guarantees offered, which can be deterministic or probabilistic. For instance, some proposals are based on the definition of an authenticated data structure (e.g., Merkle hash tree or a variation of it [START_REF] Li | Authenticated index structures for aggregation queries[END_REF][START_REF] Yang | Authentication of range query results in MapReduce environments[END_REF] or of a signature-based schemas [START_REF] Mykletun | Authentication and integrity in outsourced databases[END_REF][START_REF] Pang | Verifying completeness of relational query results in data publishing[END_REF]) that allow the verification of the correctness and completeness of query results. These proposals provide deterministic guarantees, that is, they can detect integrity violations with certainty but only for queries involving the attribute(s) on which the authenticated data structure has been created. Some proposals have also addressed the problem of verifying the freshness of query results (e.g., [START_REF] Li | Dynamic authenticated index structures for outsourced databases[END_REF][START_REF] Xie | Providing freshness guarantees for outsourced databases[END_REF]). The idea consists in periodically updating a timestamp included in the authenticated data structure or in periodically changing the data generated for integrity verification.

Probabilistic approaches can offer a more general control than deterministic approaches but they can detect an integrity violation only with a given probability (e.g., [START_REF] Vimercati | Integrity for join queries in the cloud[END_REF][START_REF] Wang | Dual encryption for query integrity assurance[END_REF][START_REF] Xie | Integrity auditing of outsourced data[END_REF]). Typically, there is a trade-off between the amount of protection offered and the computational and communication overhead caused. The proposal in [START_REF] Wang | Dual encryption for query integrity assurance[END_REF] consists in replicating a given percentage of tuples and in encrypting them with a key different from the key used for encrypting the original data. Since the replicated tuples are not recognizable as such by the server, the completeness of a query result is guaranteed by the presence of two instances of the tuples that satisfy the query and are among the tuples that have been replicated. The proposal in [START_REF] Xie | Integrity auditing of outsourced data[END_REF] consists in statically introducing a given number of fake tuples in the data stored at the external server. Fake tuples are generated so that some of them should be part of query results. Consequently, whenever the expected fake tuples are not retrieved in the query result, the completeness of the query result is compromised. In [START_REF] Vimercati | Integrity for join queries in the cloud[END_REF] we have introduced the idea of using markers, twins, salts and buckets for assessing the integrity of join queries. This paper extends such a solution proposing two optimizations that limit the overhead introduced by our protection techniques.

Conclusions

We presented two variations to markers, twins, salts and buckets proposed for assessing query integrity, offering significant performance benefits. In particular, we illustrated how markers, twins, salts and buckets can be easily adapted when a join query is executed as a semi-join, and how salts and buckets can be limited to twins and markers. The experimental evaluation clearly showed that these two variations limit the computational and communication overhead due to the integrity checks.

Fig. 1 .

 1 Fig. 1. Join computation as a regular join (a) and an example of relations L and R and their extensions with markers, twins, salts and buckets (b) along with the join computed over them (c)

Fig. 2 .

 2 Fig. 2. Join execution as a semi-join

Fig. 3 .

 3 Fig.3. An example of query evaluation process with twins on b, one marker, two salts, and buckets of size two

2 Fig. 4 .

 24 Fig. 4. An example of extensions of relations L and R in Fig. 1(b) and their join when salts and buckets are limited to twins and markers

Fig. 5 .

 5 Fig. 5. Probability ℘ that the server omits a fraction o f of the tuples without being detected, considering several strategies, assuming t = 1 (a) and t = 2 (b)

Fig. 6 .

 6 Fig.6. Probability of the omission of o tuples to go undetected when applying salts and buckets on the whole relations and on twins and markers only

Fig. 7 .

 7 Fig. 7. Response time for regular join and semi-join

Fig. 8 .

 8 Fig. 8. Response time without adopting protection techniques, with salts and buckets on the whole relation, and with salts and buckets only on markers and twins

Fig. 9 .

 9 Fig.9. Total economic cost of executing 2,000 one-to-one (a) and 2,000 one-to-many (b) join queries as a regular join or as the less expensive between regular and semi-join

We did not consider the cost of input data for the storage and computational servers since all the price lists we accessed let in-bound traffic be free.

Acknowledgements. The authors would like to thank Michele Mangili for support in the implementation of the system and in the experimental evaluation. This work was supported in part by the EC within the 7FP under grant agreement 312797 (ABC4EU) and by the Italian Ministry of Research within PRIN project "GenData 2020" (2010RTFWBH). The work of Sushil Jajodia was partially supported by NSF grant IIP-1266147.


Lise Cary

Patrick Ollivier

Géraldine Picot-Colbeaux

Philippe Leroy

Jérôme Labille

Hélène Pauwels

Tracing Tio

Tracing TiO 2 nanoparticles in a hard rock aquifer

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Tracing TiO 2 nanoparticles in a hard rock aquifer Lise Cary 1,* , Patrick Ollivier 1 , Géraldine Picot 1 , Philippe Leroy 1 , Jérôme Labille 2 , Hélène The increasing use of TiO 2 nanoparticles (NPs) is inevitably leading to its introduction into different environmental compartments, including soils, surface water and groundwater. Where groundwater is widely used for drinking water, any contamination could have an adverse impact on human health as already shown for TiO 2 NPs on living organisms and human lymphocytes. Consequently, the potential exposure of TiO 2 NPs through groundwater contamination needs to be studied and assessed.

The small-scale tracer experiment conducted in a schist aquifer constitutes an attempt to understand the physical and chemical processes occurring if TiO 2 NPs happen to penetrate in a hard rock aquifer. The schist aquifer can be represented by a dual-porosity medium constituted of fractures with low longitudinal dispersivity in which water and solute transport is relatively fast, and of a network of smaller fissures with high longitudinal dispersivity in which transport is slower.

One of the major results is that TiO 2 NPs were mobile and transferred in a heterogeneous schist aquifer through its conductive zones under aggregate forms. NPs do not penetrate the entire poral network during transfer, especially the one with very low porosity, due to electrostatic interactions between NPs aggregates and rock. During their transfer, a large amount of NPs was also deposited onto the rock surface, i.e. affected by sedimentation, clogging and adsorption. Weakly negatively charged NPs may be adsorbed onto the rock surface and especially on the positively charged iron oxi-hydroxides that coat the main pathways due to natural denitrification process. NPs aggregation is reversible due to the mineralogical heterogeneity of the schist and is likely to evolve rapidly after injection and during transport according to the environmental conditions.

Any modification of the aquifer chemical conditions is likely to impact the groundwater pH, the nitrate content and the denitrification process that controls the precipitation of iron oxides in the flow pathways, and thus change NPs aggregation and sorption.

  C. Guillemin, BP 6009, 45060 Orléans, France 2 Aix-Marseille Université, CNRS, IRD, CEREGE UMR 7330, Europôle Méditerranéen de l'Arbois BP80, 13545 Aix-en-Provence, France


Frédéric Loulergue

Wadoud Bousdira

Julien Tesson
email: julien.tesson@lacl.fr

Calculating Parallel Programs in Coq using List Homomorphisms

Keywords: Parallel programming, algorithmic skeletons, constructive algorithms, proof assistant

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Nowadays parallel architectures are everywhere, but not parallel programmers. High-level programming abstractions and methods are needed, in particular for distributed memory models. Our goal is to provide a framework to ease the systematic development of correct parallel programs.

In the Bird Meertens Formalism (BMF) [START_REF] Bird | Algebra of Programming[END_REF], an efficient program is obtained from a naive functional program considered as a specification, through program transformations. BMF can be applied to parallel programming (e.g. [START_REF] Cole | Parallel Programming with List Homomorphisms[END_REF]). In these approaches, however, the transformations are pen-and-paper proofs and the transition from an efficient functional expression to a parallel program (often in an imperative language, for example a library of algorithmic skeletons hosted in C++) is not grounded on a formal basis.

We develop the framework SyDPaCC [START_REF] Loulergue | Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem[END_REF][START_REF] Emoto | A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction[END_REF] for the Coq proof assistant [START_REF]The Coq Development Team: The Coq Proof Assistant[END_REF] to ease the use of methods based on program transformation and algorithmic skeletons and make them more reliable. More specifically the contributions of this paper are:

the support of list homomorphisms in SyDPaCC that previously only supported BSP homomorphisms [START_REF] Loulergue | Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem[END_REF] and the GTA paradigm [START_REF] Emoto | A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction[END_REF], improvements of the formalisation of the parallel functional language Bulk Synchronous Parallel ML (BSML) [START_REF] Loulergue | Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction[END_REF] and algorithmic skeletons in Coq, an application of the framework to produce a parallel program for the maximum prefix sum problem.

We first give an overview of the features of Coq. The paper does not assume any prior knowledge of Coq, but familiarity with functional programming is necessary. Then we present how a function written as a composition of sequential map and reduce could be automatically parallelised in SyDPaCC based on a formalisation of BSML (Section 3) and verified parallel versions of map and reduce (Section 4). In Section 5 we present the modelling in Coq of two important list homomorphism theorems that are used to prove that a function having three simple properties can be expressed as a composition of sequential map and reduce and therefore be parallelised. The framework is exemplified on the maximum prefix sum problem in Section 6. Comparison with related work (Section 7) and conclusion (Section 8) close the paper.

An Overview of the Coq Proof Assistant

Coq [START_REF]The Coq Development Team: The Coq Proof Assistant[END_REF] is an interactive theorem prover. It is based on the Curry-Howard correspondence relating terms of a typed λ-calculus (the calculus of (co)-inductive constructions) with proof trees of a logical system in natural deduction form. From a more practical side, Coq can be seen as a functional programming language, close to OCaml or Haskell but with a richer type system that allows to express logical properties. There are many cases where programs are developed in Coq and their properties are also proved in Coq. This is for example the case of the CompCert compiler, a compiler for the C language, implemented and certified using Coq [START_REF] Leroy | Formal verification of a realistic compiler[END_REF]. Our SyDPaCC system also uses this style.

In Coq, data structures are defined only by induction. For example the list data structure is defined in Coq, Haskell and OCaml in Figure 1. In all three cases, a list is built using the constructor for empty list (Nil), or the constructor that adds an element at the beginning of a given list (Cons). In Haskell and OCaml, a and α respectively are type variables. In the Coq version, A is simply a variable and we indicate this variable is a Type.

In Coq, values and types can be mixed together, and types may depend on values. For example the definition for lists of a given size begins with: In this definition A is a parameter: all the applications of the inductive definition t should be applied only to A in the body of the definition of t. t has a second argument: a natural number indicating the size of the vector. As in the declaration of t different values are passed for this argument, it cannot be a parameter, hence its position after the : symbol. In summary in new type declarations in Coq, parameters/arguments of the type could be both types and values. Figure 1 also shows the definitions of the map function in the three considered languages. All the definitions are recursive and by pattern matching on the list argument. They are quite similar but in their arguments: in Coq there are two arguments A and B that are types. Note that we could write (A B:Type) instead, but we prefer to let Coq infer the type. We also let Coq infer that the type of xs is list A. Considering the type arguments as regular arguments is very expressive. However, it may be verbose to explicitly apply a polymorphic function to the types it is parametric in. The Set Implicit Arguments command tells Coq to make this kind of arguments implicit (and inferred by Coq). In the recursive call of map these arguments are actually omitted and the code looks very similar to the Haskell and OCaml code.

If we request the various systems to give the type of map, Coq returns the type ∀ A B:Type,(A→B)→list A→list B whereas OCaml returns the type (α→β)→α list→β list and Haskell (t→a)→List t→List a. The ∀(x:A), B construction is a primitive one, it is called the depend product. This type is the type of the expression fun(x:A)⇒e where e has type B considering x has type A. A→B is syntactic sugar when B does not contain free occurrences of x.

It is also possible to define usual OCaml (or Haskell) notations for lists in Coq. In the remaining of the paper we will use [] for the empty list, and :: in infix notation for Cons.

Dependent product, function abstraction, inductive definitions and (dependent) pattern matching are the key constructions of Coq. Logical elements can be built using them. We refer to [START_REF]The Coq Development Team: The Coq Proof Assistant[END_REF] for the details, and just show an example of a lemma statement1 from the Coq standard library about lists:

Lemma in inv : ∀ A (a b:A) (l:list A), In b (a :: l) → a = b ∨ In b l.
In this statement, → may be thought as logical implication rather than functional arrow (actually these notions are in correspondence by the Curry-Howard correspondence). The predicate In could be defined as: In the Curry-Howard correspondence, a type and a logical statement are the same and a program and a proof are the same. The notation in inv : ( * ... * ) indicates that the name in inv has what follows the colon as type. For the definition of a function or a value, the body of the definition (for example for function map) follows after symbol :=; it is actually a syntax friendly λterm of the calculus of inductive constructions. If we follow the Curry-Howard correspondence, the proof of the lemma in inv could be also written as a λterm/program. However, it is not convenient to do so and Coq provides a language of tactics to write scripts that build λ-terms that are proofs. For in inv one possible script is:

Inductive
Proof. intros A a b l H. inversion H; subst; [left | right]; trivial. Qed.
We will not explain what exactly this script means, but only emphasise that Coq enters an interactive proof mode that helps the user to write the script and that just before Qed a λ-term is built. The command Qed then checks that this term has actually the type given as the statement of lemma in inv. Only after this check is done, the lemma is added to Coq definitions. This means the only part of Coq that should be trusted is the type checking part: the kernel. Buggy tactics could build incorrect proofs but these proofs would be rejected by the kernel.

One additional strength of Coq is that the functional programming realm and the logical realm could be mixed together. The simplest example of doing so is the dependent pair:

Inductive sig (A:Type)(P:A→Prop): Type := exist : ∀ x : A, P x → sig P.

For a predicate P over value of type A, a value of type 2 sig A P is a pair composed of: a value a of type A together with a proof that P a holds. There exists a Coq notation for sig P A which is quite intuitive: {x:A | P x}. In particular, this type could be used to express pre-and post-conditions of functions in Coq. For example, the head of a list is only defined on non empty lists, but only total and terminating functions can be defined in Coq. Therefore one can use a pre-condition and write: Here we use the Program feature of Coq that allows to consider that xs is of type list A in the definition of the body of the function and to omit some parts of the body using the symbol on the right of ⇒ for the empty list case.

Program then generates a proof obligation, for each hole in the body. In this case we do not have to write a proof script for the proof obligation because Coq proves it by itself. This proof is a proof by contradiction: l is both empty (from pattern matching) and non-empty (pre-condition). Coq has a module system similar to OCaml's. A module is a collection of inductive definitions, value and function definitions, theorems and so on. A module type is a collection of the same items that can be found in a module, plus more abstract elements: "parameters" that are names together with types but without a body. For a value or a function this corresponds to the usual notion of type signature. For a theorem, it means a theorem without a proof, in other words an axiom. The general syntax for parameters is Parameter name : type and a synonym is Axiom. An example of module type is given in Figure 4.

A module realises a module type if it provides the bodies of all the parameters of the module type. A module can be parametric, i.e it can depend on the implementation of one or several other modules. For example a module implementing a data-structure of sets using trees could depend on a module defining the type and ordering of the elements. The definition of such a module would look like Module Set (E : OrderedType). ( * ... * ) End Set. where OrderedType is a module type.

As a motivation for introducing the last feature of Coq we need, let us consider join-lists. Join-lists and list homomorphisms suit very well to the divide-and-conquer paradigm and are therefore very interesting as formal basis for a parallel program development system. The SyDPaCC framework uses this kind of functions as a foundation.

A join-list is a finite sequence of values of the same type. It can be: the empty list [], a singleton [a] (for some element a) or a concatenation xs + + ys of two lists xs and ys. The concatenation is associative and [] is its identity element. map and reduce can be defined on join-lists as:

map f [ ] = [ ] map f [x] = [f x] map f (xs + + ys) = (map f xs) + + (map f ys) reduce ⊕ [ ] = id ⊕ reduce ⊕ [x] = [x] reduce ⊕ (xs + + ys) = (reduce ⊕ xs) ⊕ (reduce ⊕ ys)
where ⊕ is an associative operator with identity element id ⊕ .

Of course in Coq join-list cannot be defined as is because this definition has logical properties on the constructors; However, join-lists are isomorphic to cons-lists as defined in Figure 1. Function map corresponds to function map in Coq. For reduce there are two difficulties: first we assume that ⊕ and i ⊕ form a monoid, and second reduce is defined, as it is traditional in the Bird Meertens Formalism, as a binary operation taking ⊕ and a list. The first difficulty can be simply overcome: these logical properties could be added as a pre-condition to an argument containing both ⊕ and i ⊕ :

Fixpoint reduce A (m:{(op,e):(A→A→A) * A|Monoid A op e})(l:list A):=( * ..

. * )

As A would be implicit, reduce would be a binary operation where the m argument is a complex value containing the binary operator, its identity element, and the fact that they form a monoid with A. A better solution would be:

Fixpoint reduce A (op:A→A→A) (H:Monoid A op e) (l:list A) : A := ( * ... * )
in such a way that H is made implicit: the identity element of op and the fact they form a monoid with A should come from some information of the context where reduce is used.

Monoid could be defined as a conjunction of properties about op and e. A convenient way to do so is to use a record that is in fact syntactic sugar for an inductive definition plus the dot notation to access the fields: It is possible to compute in Coq: Eval compute in reduce plus [1;2;3]. Coq answers = 6 : nat to this last command. First note that reduce is used as a binary operation and that its first argument is also a binary operator (here the addition on natural numbers). To infer the implicit arguments, Coq internals detect that the argument name H has as type a type class Monoid. Therefore it looks into its database of instances: it finds the last defined instance which has plus as an operator. In our setting it is the instance m plus O. This instance provides e and therefore all the implicit arguments are inferred.

Record
mkpar f = f 0 , . . . , f (p -1) apply f 0 , . . . , f p-1 v 0 , . . . , v p-1 = f 0 v 0 , . . . , f p-1 v p-1 proj v 0 , . . . , v p-1 = λi → v i put f 0 , . . . , f p-1 = λj → f j 0 , . . . , λj → f j (p -1)
Fig. 2 BSML Primitives -Informal Semantics

Bulk Synchronous Parallel ML in Coq

An Overview of BSML. Bulk Synchronous Parallel ML or BSML is a functional programming language currently implemented as a library for the functional programming language OCaml. The BSML library [START_REF] Loulergue | Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction[END_REF] provides two different implementations of the BSML primitives, a sequential implementation and a parallel implementation on top of MPI, as well as a standard library of parallel functions. Compared to a full language, the library does not provide the specific type system useful to ensure some properties about BSML programs [START_REF] Gava | Type System for a Safe Execution of Parallel Programs in BSML[END_REF]. We present here the classic syntax of BSML. A revised, more friendly syntax exists, but as programming in this style is based on OCaml pre-processing, it is not possible to have it in Coq. BSML is based on the BSP model [START_REF] Valiant | A bridging model for parallel computation[END_REF] and there is a cost model for each primitive, however for the sake of conciseness, we omit the costs in this presentation, as our framework currently does not use them. A BSP computer is a set of processor and memory pairs interconnected through a network together with a global synchronisation unit. A BSP program is a sequence of super-steps, each one being composed of: a pure computation phase where processors compute using only the data they have in local memory, a communication phase where processors exchange data, and a synchronisation barrier that ensures that all data exchanges are completed during the super-step.

BSML offers a global view of programs: a parallel program is structured as a usual sequential program but operates on a parallel data structure through dedicated primitives. This parallel data structure is called "parallel vector". A parallel vector is composed of p values, one per processor. p is the number of processes of the underlying BSP computer. p does not change during the execution of a program. From the typing point-of-view, a parallel vector has type α par: all the processors have values of the same type. Nesting of parallel vectors is not allowed, i.e. α cannot contain a parallel type: This is one of the properties enforced by the BSML type system. In the remaining, we informally write v 0 , . . . , v p-1 for a parallel vector.

BSML provides four constants to access the BSP parameters of the parallel machine. The only one used in this paper is bsp p, the number of processors of the BSP computer. BSML also provides four primitives to manipulate parallel vectors. mkpar and apply are evaluated in the pure computation phases of BSP supersteps whereas proj and put need a full super-step to be evaluated, in particular there is an implicit synchronisation barrier at the end of proj and put. The informal semantics of BSML primitives is given in Figure 2.

mkpar:(int→α)→α par is used to create a parallel vector from a function describing its components. For readers familiar with OCaml standard library, it is similar to the function Array.init: int→(int→α)→α array but missing the first argument (the size of the create array), as the size of parallel vectors is always bsp p. OCaml being a higher-order functional language, it is possible to have a parallel vector of functions. Such a parallel vector cannot be applied to values as a parallel vector of functions is not a function, thus BSML provides the primitive apply:(α→β)par→α par→β par to apply a parallel vector of functions to a parallel vector of values. proj:α par→(int→α) is the inverse of mkpar: it creates a function from a parallel vector. Note that as processor names are represented by values of type int in OCaml, proj is only the inverse of mkpar on the interval [0,bsp p-1]. The communication pattern of proj is a total exchange (each processor as to make its value available to all other processors). For more finely tuned communication patterns, BSML provides put:(int→α)par→(int→α)par. This primitive takes as input a parallel vector of functions describing the messages to be sent to other processors. For example if at processor 2, this parallel vector contains a function f 2 , and that f 2 4 returns a certain value v, it means that processor 2 will send message v to processor 4. The result of put is also a parallel vector of functions, but these functions describe the messages received by the processors. Continuing the same example, after having performed the put, the function g 4 at processor 4 is such that g 4 2 returns v: processor 4 received message v from processor 2. By convention, the first constant constructor of a type is considered to represent the absence of message and therefore does not incur any communication. The empty list is such a value.

BSML in Coq.

There are two main ways to model the semantics of programming languages in a proof assistant: shallow embedding and deep embedding [START_REF] Wildmoser | Certifying machine code safety: Shallow versus deep embedding[END_REF]. Deep embedding is well suited to reason about the general properties of the language such as typing is preserved by reduction/evaluation. However it is much less convenient to reason about individual programs.

When the base language is a functional one, another possibility is to use the proof assistant as a functional language, and add the new primitives and their semantics as signatures and axioms: This is a shallow embedding. In this setting, one cannot reason about general properties of the language as it would mean to reason about the interactive prover itself, but it is much more convenient for writing and reasoning about individual programs. All the proof assistant libraries could be used.

For modelling BSML in Coq we follow the shallow embedding approach. Moreover rather than adding signatures and axioms at the top-level of Coq, which may lead to logical inconsistencies, we write a module type. All the applications of BSML in Coq are then written as parametric modules that take an implementation of such a module type. After we extract from Coq to OCaml, we obtain OCaml functors and we apply them to the module implementing BSML: either the sequential implementation or the parallel implementation. Note that we also provide an implementation of this module type in Coq: it is meant to check that the axioms we provide are consistent with Coq's logic, and as a by-product it is a verified sequential implementation of BSML.

Module Type BSP PARAMETERS.

Parameter p : nat. Axiom p spec : 0 < p. End BSP PARAMETERS. Axiom put spec: ∀ (A:Type)(vf:par(pid→A))(i j:pid), get (put vf) i j = get vf j i. Parameter proj: ∀ {A:Type}(v: par A), pid → A. Axiom proj spec: ∀ (A:Type)(v: par A)(i: pid), (proj v) i = get v i. End Primitives. End BSML.

Fig. 4 BSML Primitives in Coq

The presented formalisation improves on previous ones [START_REF] Gava | Formal Proofs of Functional BSP Programs[END_REF][START_REF] Tesson | A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation[END_REF]. It is defined as a module type and it avoids to rely too much on sigma types. Proofs using this model are easier to do than using the previous ones.

First, there is a module type for BSP parameters (Figure 3), we only consider the bsp p parameter here, and we assume at least one processor in the BSP machine. The module type BSML models the BSML primitives. It contains a module Bsp of module type BSP PARAMETERS and the following notation: Notation pid := { n:nat | ltb n Bsp.p = true } meaning that a pid is a natural number n together with a proof that n is strictly smaller than Bsp.p. ltb:nat→nat→bool is a function testing the strict ordering of two natural numbers. The remaining of the module type BSML is given in full in Figure 4.

Section Parallel vectors models the type of parallel vectors. We called it par as in the OCaml implementation of BSML. It is an abstract type and the notation differs from an abstract type in OCaml: it takes as input a type (the type of the sequential components) and returns the type of parallel vectors of this sequential type. In order to model the semantics of BSML primitives, we need to be able to describe the value at a specific processor in a parallel vector: that is what the get operation does. Note that this operation is not a programming primitive of BSML. It should only be used in the logical parts. The axiom associated to this operation means that two parallel vectors are equal if and only if their components are equal. Some representation of parallel vectors (for example functions) may not satisfy this property, thus it is important to explicitly state this property as we want to have it.

Section Primitives describe the BSML primitives. For each primitive we give its signature in a style very close to their signature in OCaml, but in the handling of polymorphism. The semantics of the primitive is given by an axiom whose name ends by spec. For example the axiom of mkpar, ∀ i:pid, get (mkpar f) i = f i clearly states that for all process identifiers i, the value held at processor i in parallel vector mkpar f is equal to f i. It is exactly a quantified version of the informal semantics of mkpar shown in Figure 2.

Using this module type, it is possible to write BSML programs in Coq and to reason about their semantics using the specifications of the BSML primitives. One possible application is to program BSML algorithmic skeletons in Coq.

Algorithmic Skeletons and Automatic Parallelisation in Coq

Algorithmic Skeletons in Coq. Writing algorithmic skeletons using BSML primitives in Coq is actually very close to doing the same in OCaml and BSML. We illustrate this on the implementation of map and reduce skeletons. To implement programs using the BSML primitives, one needs to implement a parametric module taking as argument a module that implements the BSML primitives:

Module MapReduce (Bsml : BSML).

We use two utility functions for that:

Definition replicate A (x:A) : par A := mkpar(fun ⇒ x). Lemma replicate spec: ∀ A (x:A) i, get (replicate x) i = x. Definition parfun A B (f:A→B)(v:par A) : par B := apply (replicate f) v. Lemma parfun spec: ∀ A B (f:A→B) v i, get(parfun f v) i=f(get v i).

For these functions we follow the same modelling convention as for the primitives, but here the terms are given, by first defining a function then a lemma describing its specification. We omit the proof scripts but using automated tactics, they are very short. It is then easy to define a parallel map on distributed lists (here distributed lists means parallel vectors of lists):

Definition par map A B (f:A→B) : par(list A)→par(list B) := parfun (map' f).

where map' is a tail recursive version of map. The parallel reduce can be defined using the proj primitive for communications: ( * reduction of the partial reductions * )

In the previous definition, symbol ' in '{var:ty} indicates that the free variables in ty should be generalised, i.e. introduced before {var:ty} as additional implicit arguments. In this version of par reduce the final result is not a parallel value. We can also have an alternative version where the result is a parallel vector with the same value on each of the processors. We choose here a simple algorithm, using put: In this alternative version, the return type is a parallel vector, and we use the ability of Coq to express post-conditions: this vector has the same value on all the processors. The Program feature of Coq allows to define the function as if no post-condition was present. It generates a proof obligation (corresponding here to this post-condition). The proof script is omitted here, but is short.

Program
To verify that the implementations correspond to the semantics we have in mind, we could write spec lemmas associated to each of these functions. However, it is not convenient to express the specification of par map and par reduce by describing the content of their output at each processor. As these functions are algorithmic skeletons, we rather prefer to express the correspondence they have with sequential functions.

Types and Functions Correspondences. To do so, we rely on two main type classes (defined in the Core.Parallelisation library of SyDPaCC). First we need to express that a parallel type is a correct parallelisation of a sequential type.

Definition 1 (Type correspondence)

There is a correspondence between a type A and a parallel type A p (i.e. that contains at least one par) if and only if there exists a total surjective function join A : A p → A.

The totality of the function ensures that we can construct a sequential value for any value in A p and its surjectivity ensures the existence of at least one parallel representation for any sequential element.

In Coq we formalise these notions as type classes:

Class Surjective A B (f:A→B) := { surjective : ∀ y : B, ∃ x : A, f x = y }. Class TypeCorr (seq type:Type) (par type:Type) (join:par type→seq type) := { type corr :> Surjective join }.

Examples of type correspondences are given in Figure 5. In module ParList, the join function transforms a parallel vector of lists into a list. This sequential list also provides a "global view" of the parallel vector of lists: We think of the parallel vector as a big list obtained by concatenation of the lists hold by the processors, in increasing order of processor identifier. The proof that join is surjective is quite easy: For a sequential list, it is enough to build the parallel vector that contains this list at one specific processor (for example the first one) and empty lists on all other processors.

In module ReplicatePar, join takes as input parallel vectors that contain the same value at all the processors, and returns this value. It is straightforward to show join is surjective, as it is enough to replicate the sequential value.

Using type correspondence, we can define a relation between sequential and parallel functions.

Definition 2 (Function correspondence) Given two types A and B, and their parallel correspondent A p and B p , there is a correspondence between the sequential function f : A → B and the parallel function

f p : A p → B p if and only if join B • f p = f • join A .
In other words, the following diagram commutes:

A B A p B p f p join B join A f
This notion is also modelled as a type class:

Class FunCorr '{ACorr:TypeCorr A Ap join A}'{BCorr:TypeCorr B Bp join B} (f:A→B) (fp:Ap→Bp) := { fun corr : ∀ ap, join B (fp ap) = f (join A ap) }.

Of course a parallel function may take a sequential value as input and returns a parallel value, or may take as input a parallel value and returns a sequential value (such as the first version of par reduce does). In these cases the diagrams are: The composition of the two sequential functions corresponds to the composition of the two corresponding parallel functions. Note that the directions of the arrows in our diagrams are important to have such a compositional notion. Now that we can express the correspondence between a sequential function and a skeleton, we can do it for par map:

A B B p f p join B f A B A p f p join A f
Program Instance map par A B (f:A→B): FunCorr (map f) (par map f). Next Obligation. ( * Omitted, 5 lines * ) Qed.

This piece of code assumes that the instance defined in the module ParList described above (Figure 5) is in the context. It is this type correspondence that is used both for input and output.

In the case of par reduce, the same type correspondence is used only for input, as the output is the same type A in the sequential and parallel cases:

Program Instance reduce par reduce '(op:A→A→A) '{Monoid A op e} :

LeftFunCorr (reduce op) (par reduce op). Next Obligation. ( * Omitted, 8 lines * ) Qed.

The correctness of the last skeleton par reduce' uses the type correspondence defined in the module ReplicatePar (Figure 5):

Program Instance reduce par reduce' '(op:A→A→A) '{Monoid A op e} : FunCorr (reduce op) (par reduce' op).

Note that as the instances we have do not overlap, the instance resolution mechanism has no problem to find the instance we expect. In a richer library with overlapping instances (e.g. with different joins on parallel vectors of lists) the function correspondence might need to be specified more carefully by the user (i.e. some implicit arguments might need to be made explicit). However, as the library is organised in a modular way, the user has control over the visibility of overlapping instances.

Automatic Parallelisation. If a sequential function h is defined as a composition of maps and reduces, the instances we defined can actually serve as an automatic parallelisation mechanism. Consider the following function:

Definition parallel '(f:A→B) '{ACorr: TypeCorr A Ap joinA} '{BCorr : TypeCorr B Bp joinB} '{fCorr: @FunCorr A Ap joinA ACorr B Bp joinB BCorr f fp} : Ap→Bp := fp.

This function seems uninteresting as the result it returns is one of its arguments. However all the arguments, except the sequential function f, are implicit and are instances of type classes. It means that Definition par h:=parallel h launches the instance resolution mechanism of Coq. Function h will first be decomposed if it is a composition, until instances of correspondence between a sequential function and a skeleton are found, and the parallel version par h of h will be automatically built as a composition of skeletons.

The last component of the framework we need is thus a way to prove that certain classes of functions can be written as compositions of sequential functions that correspond to skeletons. The Bird Meertens Formalism, with the theory of list homomorphisms is a convenient formalism for this purpose.

List Homomorphisms and their Theorems in Coq

In our parallelisation framework, we need functions defined as compositions of map and reduce. We consider the class of ⊕-homomorphic functions.

Definition 3 (⊕-homomorphic)

A function h on lists is ⊕-homomorphic if for all lists x and y, h(x

+ + y) = (h x) ⊕ (h y). Fact 1 If h is ⊕-homomorphic, then (img h, , h []) is a monoid.
Note this it is not true in general on the codomain of h. There are two useful theorems for our framework: the first and the third homomorphism theorems [START_REF] Gibbons | The third homomorphism theorem[END_REF].

Theorem 1 (Third Homomorphism Theorem) If a function h is both:

-⊕-leftwards, i.e. there exists ⊕ such that h(

[x] + + xs) = x ⊕ (h xs), -⊗-rightwards, i.e. there exists ⊗ such that h(xs + + [x]) = (h xs) ⊗ x,
then there exist such that h is -homomorphic.

Theorem 2 (First Homomorphism Theorem

) If h is -homomorphic then h = (reduce ) • (map f ) where ∀x, f x = h[x].
In this first theorem, we consider the restriction of on the image of h, as in general (codomain h, , h []) is not a monoid (and reduce requires a monoid).

In Coq, we model the homomorphic property as a class:

Class Homomorphic '(h:list A→B) '(op:B→B→B) := { homomorphic : ∀ x y, h (x++y) = op (h x) (h y) }.

Fact 1 is actually a result that is not trivial in Coq. First we need to define the image of h, and definitions to build the restriction of ⊕ (named op from now on) to the image of h: To express the first homomorphism theorem, we define a function that produces the composition of map and reduce from an op-homomorphic function and possibly optimised versions of op and of fun (x:A)⇒h[a]: Definition hom to map reduce '(h:list A→B) '{H:Homomorphic A B h op} '{@Optimised op A B h op H}'{@Optimised f A B h op H} : list A→img h := (reduce (optimised op h)) • (List.map (optimised f h)).

Definition img '(h:list A→B) := { b:B | ∃ l,
There are default instances of the Optimised op and Optimised f that relate op and fun (x:A)⇒h[a] to themselves. We omit the details of the optimisation aspects and refer to the source code of the framework. The theorem then checks that this function produces a function equal to h: Theorem first homomorphism theorem: ∀ '{H:Homomorphic A B h op} '{@Optimised op A B h op H}'{@Optimised f A B h op H}, ∀ l, h l = of img (hom to map reduce h l). Proof. ( * 12 lines * ) Qed.

The classical proof of the third homomorphism theorem relies on the notion of weak right inverse, i.e. a function h such that for all x, h x = h(h (h x)). In [START_REF] Gibbons | The third homomorphism theorem[END_REF], a lemma states that for every computable total function h with enumerable domain, there exists a weak right inverse of h. The proof however is the following: "To compute g t for some t simply enumerate the domain of h and return the first x such that h x = t. If t is in the range of h then this process terminates." The problem with this proof is that: function g may not terminate but it is not possible to define non-terminating functions in Coq. Moreover even if it could be defined, its efficiency would be in general catastrophic.

Therefore we state and prove a weak form of the third homomorphism theorem using the following classes: To parallelise a function h, we should prove instances of Rightwards h oplus, Leftwards h otimes and Right inverse h h' and call the hom to map reduce function on h. The resolution instance mechanism of Coq would then produce an instance of Homomorphic for h using the third homomorphism theorem.

The obtained composition could then be parallelised using parallel (or variant left parallel) explained in the previous section. We illustrate this process on an application example in the following section.

An Example: Maximum Prefix Sum

The goal is to obtain a parallel function that solves the maximum prefix sum problem. An example of evaluation of the sequential function mps follows (the prefix whose sum is maximum is underlined): mps [1; 2; -1; 2; -1; 3; -4] = 6.

A trivial solution that we consider to be a specification follows, where prefix returns the list of all the prefixes of its input and t is the type of an abstract representation of mathematical integers (module type Number):

Program Definition sum : list t → t := reduce add. Definition maximum : ∀(l:list t), NonEmpty l→t := NE.reduce max. Program Definition mps spec : list t → t := maximum•'(map sum) •''prefix. maximum is not defined on the empty list: we use a version of reduce that also requires to be applied to a non-empty list. The property NonEmpty is a class: Class NonEmpty '(l:list A) := { non emptiness : l<> [] }.

The variants of composition handle the additional arguments concerning nonemptiness. This is transparent to the user as there are instances of the NonEmpty class that state that prefix always returns a non-empty list and that map preserves non-emptiness. mps spec is not leftwards. But it is possible to tuple mps spec with sum:

Definition tupling A B C(f:A→B)(g:A→C) := fun x ⇒ (f x, g x).

Definition ms spec := tupling mps spec sum. The third homomorphism is applied to show that ms spec is -homomorphic where =fun l r⇒ms spec(ms' l++ms' r). In the pen-and-paper proof, usually one shows that (a m , a s ) (b m , b s ) = (0 ↑ a m ↑ (a s +b m ), a s +b s ) where ↑ returns the maximum of two numbers. Using the Optimised op class, it is also possible to do it in Coq, in a process similar to the pen-and-paper proof (i.e. the final version is not known before the proof starts). This requires about 30 more lines using several short lemmas on mps spec and sum.

To parallelise, we need to instantiate the parametric modules presented in the previsous sections and then call the left parallel function (or the parallel function using the ReplicatePar in addition to ParList). Finally to obtain only the mps component of the result, we compose with projections (Figure 6).

The Coq code can then be extracted towards OCaml. The extraction mechanisms removes the logical parts to keep only the computational parts. What we obtain is an OCaml functor: module MPS=functor(Bsml:BSML)→functor(N:Number)→struct ( * ... * ) end A parallel implementation on top of MPI results from applying this functor to a Bsml module that is a wrapper around the Bsmlmpi uncertified implementation of BSML in OCaml, C and MPI. The main difference between Bsml and Bsmlmpi is that in the former pid is the type nat and in the latter it is type int. As we dealt with an abstract representation of integers, we also need to provide an OCaml module that follows the extraction of the module type Number The framework and results of scalability experiments are available online3 . The framework only requires Coq 8.4, OCaml 4 or above, and an MPI library.

Related Work

To our knowledge SyDPaCC is the only approach in which actual source code of scalable and correct parallel programs can be obtained from a development in a proof assistant. The theory of constructive parallel algorithms provides various ways to ease the systematic development of correct parallel programs. However, the transformations are not mechanically verified and the transition from an efficient functional expression to a parallel program is not based on a formal basis. Most often, with the exception of [START_REF] Cavarra | A formal model for the parallel semantics of P3L[END_REF][START_REF] Aldinucci | Skeleton-based parallel programming: Functional and parallel semantics in a single shot[END_REF], the semantics of algorithmic skeletons remains informal.

There exist several logics to reason about BSP programs, for example [START_REF] Stewart | Barrier synchronisation: Axiomatisation and relaxation[END_REF], but none of them is mechanised in a proof assistant, and only one of them is related to a tool that can provide actual source code [START_REF] Zhou | Generating C code from LOGS specifications[END_REF]. The main differences with our approach is that: LOGS starts from an imperative and local view of parts of the program to build a larger one by parallel composition whereas we start from a functional and global view and our framework is in Coq. BSP-Why [START_REF] Fortin | BSP-Why: A tool for deductive verification of BSP algorithms with subgroup synchronisation[END_REF] is an extension of the Why2 system for the deductive verification of imperative BSP programs. The tool is based on the generation of verification conditions from users annotations, those conditions being automatically proved by SMT solvers, or interactively with Coq. BSP-Why does not support program transformation and higher-order functions.

Although there are systems to support program calculation (for example [START_REF] Yokoyama | Yicho: A system for programming program calculations[END_REF]) they lack the rich set of theories that exist for Coq and that can be reused for program transformation. Moreover Coq offers a more trusted framework through its kernel. The work on polytypic programming and program transformation in Coq [START_REF] Mu | Algebra of programming using dependent types[END_REF] and Agda [START_REF] Mu | Algebra of programming in Agda: Dependent types for relational program derivation[END_REF] is also related. Our framework follows more closely a simple functional programming style with additional pre/post conditions or statements about the simple functional programs. Moreover for the parallel aspects it would be a challenge to provide correspondence between polytypic sequential functions and efficient parallel ones.

To our knowledge, there are only three works associating data parallelism and proof assistants. The operational semantics of a type safe subset of Data Parallel C is formalised in Isabell/HOL [START_REF] Daum | Reasoning on Data-Parallel Programs in Isabelle/Hol[END_REF]. In this approach Isabelle/HOL expressions that represent programs are generated and manipulated. It is therefore a deep embedding approach. Swierstra [START_REF] Swierstra | More dependent types for distributed arrays[END_REF] formalised mutable arrays in Agda, and added explicit distributions to these arrays. He used it to reason about a distributed map and distributed sum on these arrays. In BSML the distribution of parallel vectors is fixed but it is possible to define a higher-level data structure on top of parallel vector and consider various distributions of the data structure in parallel vectors [START_REF] Bousdira | A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays[END_REF]. Moreover it is possible to formalise mutable arrays, and even extract such imperative programs to OCaml as done by Malecha et al. [START_REF] Malecha | Trace-based verification of imperative programs with i/o[END_REF]. Lupinski et al. [START_REF] Lupinski | Sémantique d'une langage de squelettes[END_REF] formalised the semantics of a skeletal parallel programming language. It is also a deep embedding that models both the high-level semantics of skeletons and their implementations in a formalised JoCaml. BSML shallow embedding is more convenient.

Conclusion

The SyDPaCC framework shows that the Coq proof assistant is suited for program calculation in the Bird Meertens Formalism tradition, and that when using the right features of Coq, the additional work to have machine checked proofs rather than pen-and-paper proofs is quite manageable. Coq also allows automatic parallelisation using algorithmic skeletons. The key points in this respect is that we provide a shallow embedding of a pure functional parallel programming library in Coq; that one can program and verify algorithmic skeletons in Coq based on this embedding; and that expressing the correctness of algorithmic skeletons with respect to usually sequential functions in a compositional way as instances of type classes makes possible the use of the instance resolution mechanism of Coq for automatic parallelisation. Actual programs are obtained through the extraction feature. The extracted code is combined with the unverified parallel implementation of BSML in OCaml and C+MPI. The core SyDPaCC presented in this paper is very concise (2 kLoC of Coq, 600 LoC of OCaml 120 LoC of C). Experimental results on the generated programs are presented in [START_REF] Emoto | A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction[END_REF][START_REF] Loulergue | Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem[END_REF][START_REF] Tesson | A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation[END_REF] and in the SyDPaCC website.

(Fig. 1

 1 Fig. 1 Lists in Coq, Haskell & OCaml

  In A (x:A): list A→Prop := ( * Prop is the kind of ''logical'' types * ) | Inhead: ∀ (xs:list A), In x (x::xs) | Intail: ∀ (y:A) (xs:list A), In x xs→In x (y::xs).

Program

  Definition head A (xs:{l:list A| l<> []}) : A := match xs with | [] ⇒ | x::xs ⇒ x end.

  Monoid A (op:A→A→A) (e:A) : Prop := { left unit: ∀ a:A, op e a = a; right unit: ∀ a:A, op a e = a; associative: ∀ a b c : A, op a (op b c) = op (op a b) c }. Note that all the fields are logical statements. Therefore we use the proof mode to define a value of type Monoid: Definition monoid plus O : Monoid plus O. Proof. constructor; auto. Defined. It is possible to use the notation {name:type} instead of (name:type) in a definition to make an argument implicit. However even if we do that in the proposed signature of reduce, Coq will have no way to infer this implicit argument. The necessary Coq feature are type classes. A class is similar to a record but values of these classes are defined by the keyword Instance that defines them and stores them into a database that is queried by the Coq inference mechanism when it encounters an implicit argument whose type is a class. The class Monoid only differs from the record Monoid in using the command Class instead of Record. Then we can define instances as follows: Instance m plus O : Monoid plus O. Proof. ( * ... * ). Defined. Instance m app nil A: Monoid (@app A) []. ( * @ makes all arguments explicit * ) where app is the concatenation of lists as defined in the Coq standard library. One possible definition for reduce is then: Unset Implicit Arguments. ( * We prefer to control the implicit status * ) Fixpoint reduce {A} (op:A→A→A) {e} {H:Monoid op e} (l:list A) : A := match l with | [] ⇒ e | x::xs ⇒ op x (reduce op xs) end.

Fig. 3 BSP

 3 Fig. 3 BSP Parameters in Coq

Definition

  par reduce'(op:A→A→A)'{H:Monoid op e}(v:par(list A)) : A := let local := parfun (reduce op) v in ( * local reductions * ) let list := List.map (proj local) pids in ( * vector → list * ) reduce op list.

  Definition par reduce' {A}(op:A→A→A){e:A}{H:Monoid op e} (v: par(list A)) : {v:par A | ∀ i, get v i = get v first } := let local := parfun (reduce op) v in let msgs := put(apply(mkpar(fun pid msg dst⇒msg)) local) in let lists := parfun (fun f⇒List.map f pids) msgs in parfun (reduce op) lists. Next Obligation. ( * omitted, 9 lines * ) Qed.

Module

  ParList (Import Bsml: BSML)(Import Pid : Pid.TYPE Bsml.Bsp). Program Definition join A (v:par(list A)) : list A := List.flat map (proj v) pids. Program Instance surjective join A : Surjective (join(A:=A)). Next Obligation. ( * Omitted, 12 lines * ) Qed. Program Instance list par list corr A : TypeCorr (@join A). End ParList. Module ReplicatePar (Import Bsml: BSML)(Import Pid : Pid.TYPE Bsml.Bsp). Program Definition join A (r:{v:par A|∀ i,get v i=get v first}) : A := (proj (proj1 sig r)) first. Program Instance surjective join A : Surjective (join (A:=A)). Next Obligation. ( * Omitted, 5 lines * ) Qed. Program Instance replicate par corr A : TypeCorr (@join A). End ReplicatePar.

Fig. 5

 5 Fig. 5 Type Correspondences

  and the type classes are: Class LeftFunCorr '{ACorr:TypeCorr A Ap}{B}'(f:A→B)(fp:Ap→B) := { left fun corr : ∀ ap, fp ap = f (join ap) }. Class RightFunCorr {A}'{BCorr:TypeCorr B Bp}'(f:A→B)(fp:A→Bp) := { right fun corr : ∀ a, join (fp a) = f a }. There are two kinds of instances for the function correspondences: general ones and instances stating the correspondence of a specific parallel function and a specific sequential function. The former are also given in the library Parallelisation, the other are together with the skeleton definitions. There are several general instances that state facts about the correspondence of compositions. For two instances of FunCorr, we have for example: Program Instance fun corr comp fun corr '{ACorr : TypeCorr A Ap join A} '{BCorr : TypeCorr B Bp join B} '{CCorr : TypeCorr C Cp join C} '{fCorr : @FunCorr A Ap join A ACorr B Bp join B BCorr f fp} '{gCorr : @FunCorr B Bp join B BCorr C Cp join C CCorr g gp} : FunCorr (compose g f) (compose gp fp). Next Obligation. ( * Omitted, 3 lines * ) Qed.

  h l = b }. Program Definition restrict op '(op:B→B→B) '{Homomorphic A B h op} : img h → img h → img h := op. ( * ... * ) Definition to img A B (h:list A→B)(xs:list A) : img h := ( * ... * ). Fact 1 is then written: Program Instance homomorphic restrict op monoid '{Homomorphic A B h op} : Monoid (A:=(img h)) (restrict op op) (to img h []). Actually, we need a slightly more general result, where we replace the restriction of the operator by a function that is extensionally equivalent: Program Definition restrict '{Homomorphic A B h op} '(Eq:∀ a b, op' a b= ' (restrict op op a b)): img h→img h→img h:=op'( * ... * ) Program Instance homomorphic restrict monoid '{Homomorphic A B h op} '(Eq:∀ a b, op' a b = ' (restrict op op a b)) : Monoid (restrict Eq) (h []). ( * 20 lines+usage of several omitted lemmas * ) This allows to replace the output of the third homomorphism theorem by a simplified version of the binary operator.

Class

  Rightwards '(h:list A→B)'(op:B→A→B)'(e:B) := { rightwards: ∀ l, h l = List.fold left op l e }. Class Leftwards '(h:list A→B)'(op:A→B→B)'(e:B) := { leftwards: ∀ l, h l = List.fold right op e l }. Class Right inverse '(h:list A →B)(h':B→list A) := { right inverse: ∀ l, h l = h(h'(h l)) }. Instance third homomorphism theorem '{h:list A→B} '{inv:Right inverse A B h h'} '{Hl:Leftwards A B h opl e}'{Hr:Rightwards A B h opr e} : Homomorphic h (fun l r ⇒h( (h' l)++(h' r))). Proof. ( * 20 lines + usage of a 10 lines lemma + lemmas on folds * ) Qed.

  ms spec is opl-leftwards and opr-rigthwards: Definition opl (a:t) (b:t * t) : t * t := ( max 0 (a + fst b), a + (snd b) ). Instance ms leftwards : Leftwards ms spec opl (0,0). Proof. ( * ... * ) Qed. Definition opr (a:t * t) (b:t) : t * t := (max (fst a) ((snd a)+b),(snd a)+b). Instance ms rightwards : Rightwards ms spec opr (0,0). The proofs of the instances are about 20 lines long and they both use two 10 lines lemmas about maximum and sum. Then we need to find a weak right inverse of ms spec: Definition ms' (p:t * t) := let (m,s) := p in [ m; s + -m]. Program Instance ms right inverse : Right inverse ms spec ms'. Next Obligation. ( * 25 lines * ) Qed.

Module

  MPS (Import Bsml: Core.BSML)(N: Number). Module Pid := Pid.Make Bsml.Bsp. Module ParList := Correspondences.ParList Bsml Pid. Module MapReduce := MapReduce.Make Bsml Pid ParList ReplPar. Module Mps := Make N. Definition par ms := Eval sydpacc in left parallel (hom to map reduce Mps.ms spec). Definition par mps := Eval simpl in fst • of img • par ms. End MPS.

Fig. 6

 6 Fig. 6 Parallelisation

In Coq all the following commands are synonym: Fact, Lemma, Proposition, Theorem.

http://traclifo.univ-orleans.fr/SyDPaCC, version core-0.2

Acknowledgements This work is partly supported by ANR (France) and JST (Japan) (project PaPDAS ANR-2010-INTB-0205-02 and JST 10102704).