V Allombert
email: victor.allombert@lacl.fr

F Gava

J Tesson

Multi-ML: Programming Multi-BSP Algorithms in ML

Keywords: multi-bsp, ml, Parallel Programming

bsp is a bridging model between abstract execution and concrete parallel systems. Structure and abstraction brought by bsp allow to have portable parallel programs with scalable performance predictions, without dealing with low-level details of architectures. In the past, we designed bsml for programming bsp algorithms in ml. However, the simplicity of the bsp model does not fit the complexity of today's hierarchical architectures such as clusters of machines with multiple multi-core processors. The multi-bsp model is an extension of the bsp model which brings a tree-based view of nested components of hierarchical architectures. To program multi-bsp algorithms in ml, we propose the multi-ml language as an extension of bsml where a specific kind of recursion is used to go through a hierarchy of computing nodes. We define a formal semantics of the language and present preliminary experiments which show performance improvements with respect to bsml.

Introduction

Context of work. Nowadays, parallel programming is the norm in many areas but it remains a hard task. And the more complex the parallel architectures become, the harder the task of programming them efficiently is. As we moved from unstructured sequential code cluttered with goto statement toward structured code, there has been a move in parallel programming community to leave unstructured parallelism, with pairwise communications, in favour of global communication schemes [START_REF] Bisseling | Parallel Scientific Computation. A structured approach using bsp and mpi[END_REF][START_REF] Cappello | On Communication Determinism in Parallel hpc Applications[END_REF][START_REF] Loidl | Comparing Parallel Functional Languages: Programming and Performance[END_REF] and of structured abstract models like bsp [START_REF] Bisseling | Parallel Scientific Computation. A structured approach using bsp and mpi[END_REF][START_REF] Valiant | A Bridging Model for Parallel Computation[END_REF] or of higher-level concepts like algorithmic skeletons [START_REF] González-Vélez | A Survey of Algorithmic Skeleton Frameworks: Highlevel Structured Parallel Programming Enablers[END_REF].

Programming in the context of a bridging model, such as bsp, allows to simplify the task of the programmer, to ease the reasoning on cost and to ensure a better portability from one system to another [START_REF] Bisseling | Parallel Scientific Computation. A structured approach using bsp and mpi[END_REF][START_REF] Hinsen | Using bsp and python to Simplify Parallel Programming[END_REF][START_REF] Valiant | A Bridging Model for Parallel Computation[END_REF]. However, designing a programming language [START_REF] Gu | JBSP: A bsp programming library in java[END_REF][START_REF] Hill | bsplib: The bsp Programming Library[END_REF] for such a model requires to choose a trade-off between the possibility to control parallel aspects -necessary for predictable efficiency but which makes programs more difficult to write, to prove and to port -and the abstraction of such features, which makes programming easier but which may hampers efficiency and performance prediction.

With flat homogeneous architectures, like clusters of mono-processors, bsp has been proved to be an effective target model for the design of efficient algorithms and languages [START_REF] Yzelman | An Object-oriented Bulk Synchronous Parallel Library for Multicore Programming[END_REF]: while its structured nature allows to avoid deadlocks and non-determinism with little care and to reason on program correctness [START_REF] Gava | Formal Proofs of Functional bsp Programs[END_REF][START_REF] Gesbert | Systematic Development of Correct Bulk Synchronous Parallel Programs[END_REF][START_REF] Fortin | BSP-Why: A tool for deductive verification of bsp algorithms with subgroup synchronisation[END_REF] and cost, it is general enough to express many algorithms [START_REF] Bisseling | Parallel Scientific Computation. A structured approach using bsp and mpi[END_REF]. However, modern parallel architecture have now multiple layers of parallelism. For example, supercomputers are made of thousands of interconnected nodes, each one carrying several multi-cores processors. Communications between distant nodes cannot be as fast as communications among the cores of a given processor; Communications between cores, by accessing shared processor cache are faster than communications between processors through RAM.

Contribution of this paper. Those architectures specifics led to a new bridging model, multi-bsp [START_REF] Valiant | A bridging model for multi-core computing[END_REF], where the hierarchical nature of parallel architectures is reflected by a tree-shaped model describing the dependencies between memories. The multi-bsp model gives a more precise picture of the cost of computations on modern architectures. While the model is more complex to grasp than the bsp one, it keeps structured characteristics that prevents deadlock and non-determinism. We propose a language, multi-ml, which aims at providing a way to program multi-bsp algorithms so as bsml [START_REF] Gesbert | Bulk Synchronous Parallel ml with Exceptions[END_REF] is a way to program bsp ones. multi-ml combines the high degree of abstraction of ml (without poor performances because often, ml programs are as efficient as c ones) with the scalable and predictable performances of multi-bsp.

Outline. The remainder of this paper is structured as follows. We first give in Section 2 an overview of previous works: the bsp model at Section 2.1 and then the bsml language at Section 2.2 following with the multi-bsp model at Section 2.3. Our language multi-ml is presented at Section 3. Its formal semantics and implementation, together with examples and benchmarks are given at Section 4. Section 5 discusses some related works and finally, Section 6 concludes the paper and gives a brief outlook on future work.

Previous Works

In this section, we briefly present the bsp and multi-bsp models and how to program bsp algorithms using the bsml language. We assume the reader is familiar with ml programming. We also give an informal semantics of the bsml primitives and some simple examples of bsml programs.

The BSP Model of Computation

In the bsp model [START_REF] Bisseling | Parallel Scientific Computation. A structured approach using bsp and mpi[END_REF][START_REF] Valiant | A Bridging Model for Parallel Computation[END_REF], a computer is a set of p uniform processor-memory pairs and a communication network. A bsp program is executed as a sequence of super-steps (Fig. 1), each one divided into three successive disjoint phases:

(1) each processor only uses its local data to perform sequential computations and to request data transfers to other nodes; [START_REF] Bisseling | Parallel Scientific Computation. A structured approach using bsp and mpi[END_REF] the network delivers the requested data; (3) a global synchronisation barrier occurs, making the transferred data available for the next super-step. This structured model enforces a strict separation of communication and computation: during a super-step, no communication between the processors is allowed, only requests of transfer; information exchanges only occur at the barrier. Note that a bsp library can send data during the computation phase of a super-step, but this is hidden to the programmers.

The performance of a bsp computer is characterised by 4 parameters: (1) the local processing speed r; (2) the number of processors p; (3) the time L required for a barrier; (4) and the time g for collectively delivering a 1-relation, i.e. every processor receives/sends at most one word. The network can deliver an h-relation in time g × h. To accurately estimate the execution time of a bsp program, these 4 parameters can be easily benchmarked [START_REF] Bisseling | Parallel Scientific Computation. A structured approach using bsp and mpi[END_REF]. The execution time (cost) of a super-step s is the sum of the maximal local processing time, the data delivery and the global synchronisation times. The total cost (execution time) of a bsp program is the sum of its super-steps' costs.

BSP Programming in ML

bsml [START_REF] Gesbert | Bulk Synchronous Parallel ml with Exceptions[END_REF] uses a small set of primitives and is currently implemented as a library (http://traclifo.univ-orleans.fr/BSML/) for the ml programming language ocaml (http://caml.org). An important feature of bsml is its confluent semantics: whatever the order of execution of the processes, the final value will be the same. Confluence is convenient for debugging since it allows to get an interactive loop (toplevel); It also eases programming since the parallelisation can be done incrementally from an ml program. Last but not least, it is possible to reason about bsml programs using the coq (https://coq.inria.fr/) proof assistant [START_REF] Gava | Formal Proofs of Functional bsp Programs[END_REF][START_REF] Gesbert | Systematic Development of Correct Bulk Synchronous Parallel Programs[END_REF] and to extract actual bsp programs from proofs.

A bsml program is built as an ml one but using a specific data structure called parallel vector. Its ml type is 'a par. A vector expresses that each of the p processors embeds a value of any type 'a. The processors are labelled with ids from 0 to p -1. The nesting of vectors is not allowed. We use the following notation to describe a vector: v 0 , v 1 , . . . , v p-1 . We distinguish a vector from a usual array because the different values, that will be called local, are blind from each other; it is only possible to access the local value v i in two cases: locally, on processor i (using a specific syntax), or after some communications.

Since a bsml program deals with a whole parallel machine and individual processors at the same time, a distinction between the 3 levels of execution that take place will be needed: (1) Replicated execution r is the default; Code that does not involve bsml primitive is run by the parallel machine as it would be by a single processor; Replicated code is executed at the same time

i $v$ l 'a (if v: 'a par) v i on processor i, assumes v ≡ v 0 , . . . , v p-1 proj g 'a par→ (int→ 'a) x 0 , . . . , x p-1 → (fun i → x i ) put g (int→ 'a)par→ (int→ 'a)par f 0 , . . . , f p-1 → fun i → f i 0, . . . , fun i → f i (p-1)
Table 1 Summary of the bsml primitives.

by every processor, and leads to the same result everywhere; (2) Local execution l is what happens inside parallel vectors, on each of their components; Each processor uses its local data to do their own computations; (3) Global execution g concerns the set of all processors together as for bsml communication primitives. The distinction between local and replicated is strict: the replicated code cannot depend on local information. If it were to happen, it would lead to replicated inconsistency. Parallel vectors are handled through the use of different communication primitives. Table 1 shows their use. Informally, they work as follows: let e be the vector holding e everywhere (on each processor), the indicates that we enter a vector and switch to the local level. Replicated values are available inside the vectors. To access to local information within a vector, we add the syntax $x$ to read the vector x and get the local value it contains. The ids can be accessed with the predefined vector pid. For example, using the toplevel for a simulated bsp machine with 3 processors:

# let vec1 = "HLPP" in $vec1$ˆ", proc "ˆ(string of int $pid$)
;; -: string par = <"HLPP, proc 0", "HLPP, proc 1", "HLPP, proc 2"> The # symbol is the prompt that invites the user to enter an expression to be evaluated. Then, the toplevel gives the evaluated value with its type. Thanks to bsml confluence, it is ensured that the results of the toplevel or of the distributed implementation are identical.

The proj primitive is the only way to extract local values from a vector. Given a vector, it returns a function such that, applied to the pid of a processor, the function returns the value of the vector at this processor. proj performs communications to make local values available globally and it ends the current super-step. For example, if we want to convert a vector into a list, we write: # let list of par vec = List.map (proj vec) procs;; -: val list of par : 'a par → 'a list = <fun> # list of par $pid$ ;; -: int list = [0; 1; 2] where procs is the list of ids [0; 1;

• • • ;p-1].
The put primitive is another communication primitive. It allows any local value to be transferred to any other processor. It is also synchronous, and ends the current super-step. The parameter of put is a vector that, at each processor, holds a function of type (int→ 'a) returning the data to be sent to processor j when applied to j. The result of put is a new vector of functions: at a processor j the function, when applied to i, yields the value received from processor i by processor j. For example, a total exchange could be written:

# let total exchange vec = let msg = put fun dst → $vec$ in List.map $msg$ procs ;; -: val total exchange : 'a par → 'a list par = <fun> # total exchange $pid$ ;; -: int list par = <[0;1;2], [0;1;2], [0;1;2]> where the bsp cost is (p-1)×s×g+L where s is the size of the biggest sent value. Fig. 2 The difference between the multi-bsp and bsp models for a multi-core architecture.

The multi-bsp Model for Hierarchical Architectures

The multi-bsp model [START_REF] Valiant | A bridging model for multi-core computing[END_REF] is another bridging model as the original bsp, but adapted to clusters of multi-cores. The multi-bsp model introduces a vision where a hierarchical architecture is a tree structure of nested components (submachines) where the lowest stage (leaf) are processors and every other stage (node) contains memory. Fig. 2 illustrates the difference between both models for multi-cores. There exist other hierarchical models [START_REF] Li | SGL: Towards a Bridging Model for Heterogeneous Hierarchical Platforms[END_REF], such as d-bsp [START_REF] Beran | Decomposable bulk synchronous parallel computers[END_REF] or h-bsp [START_REF] Cha | h-bsp: A hierarchical bsp computation model[END_REF], but multi-bsp describes them in a simpler way. An instance of multi-bsp is defined by d the depth of a tree and 4 parameters for each stage i: -p i is the number of components inside the i stage. We consider p 1 as a basic computing unit where a step on a word is considered as the unit of time.

Level i

Level i -1 n n.1 . . . . . . n.p i g i g i-1 m i L i
Fig. 3 multi-bsp parameters.

-g i is the bandwidth between stages i and i + 1: the ratio of the number of operations to the number of words that can be transmitted in a second (illustrated in Fig. 3). -L i is the synchronisation cost of all components of i-1 stage, but no synchronisation across above branches in the tree. Every components can execute codes but they have to synchronise in favour of data exchange. Thus, multi-bsp does not allow subgroup synchronisation as the d-bsp does: at a stage i there is only a synchronisation of the sub-components, a synchronisation of each of the computational units that manage the stage i-1. -m i is the amount of memory available at stage i. A node executes some code on its nested components (children), then waits for results, does the communications and synchronises the children. Considering C i j = h i × g j + L j , the communication cost of a super-step i at stage j with h i the size of the exchanged messages at step i, g j the communication bandwidth with stage j and L j the synchronisation cost. We can recursively express the cost of a multi-bsp algorithm as follows: N-1 i=0 w i + d-1 j=0 M j -1 i=0 C i j where N is the number of computational super-steps, w i is the cost of a single computation step and M j is the number of communication phases at stage j. As a more evolved program, we can find an implementation of the standard direct scan in Fig. 4. This code builds the values to be communicated to all processes with a greater pid and it exchanges the values using the put primitive. Then every processes maps the received values on their own data.

3 Design of the Multi-ML Language multi-ml is based on the idea of executing a bsml-like code on every stage of the multi-bsp architecture, that is on every sub-machine. Hence, we add a specific syntax to ml in order to code special functions, called multi-functions, that recursively go through the multi-bsp tree. At each stage, a multi-function allows the execution of any bsml code. We first present the execution model that follows this idea; we then present the specific syntax and we finally give the limitations when using some advanced ocaml features.

Execution Model

A multi-ml tree is formed by nodes and leaves as proposed in multi-bsp with the difference that a node is not only a memory but has the ability to manage (coordinate) the values exchanged by its sub-machines. However, as common architectures do not have dedicated processors for each memory, one (or more, implementation dependent) selected computation unit has the responsibility to perform this management task, which is limited in practice. Because leaves are their own computing units, our approach coincides with multi-bsp if we consider that all the computations and memory accesses, at every nodes, are performed by one (or more) leaf: replicated codes (outside vectors) that takes place in nodes will be costlier than in leaves. This is why computations on nodes are reserved to the simple task of coordination. The multi-ml approach is also a bit more relaxed than multi-bsp regarding synchronisation. Unlike multi-bsp, we allow asynchronous codes in the sub-machines when only lower memories accesses are used. Of course, we do synchronise if a communication primitive is used. As suggested in [START_REF] Valiant | A bridging model for multi-core computing[END_REF], we also allow flat communications between nodes and leaves without using an upper level. In a multi-ml tree, of type a tree, every node and leaf contains a value of type a in its own memory. It is important to notice that the Multi-ML: Programming Multi-BSP Algorithms in ML Primitive Level Type Informal semantics §e § m 'a tree Build a tree of e at(v) b,l,s 'a vn on node n of tree a v (if v: 'a tree) gid m id tree The predefined tree of nodes and leaves ids ...f... l 'a In a vector, recursive call of the multi-function

#x# l 'a
In a vector, reading the value x at upper stage mkpar f b 'a par v 0 , . . . , vp n , where ∀i, f i = v i , at id n of the tree finally v 1 v 2 b,s 'a Return value v 1 to upper stage and keep v 2 in the tree this b,l,s 'a Current value of the tree The main idea of multi-ml is to structure the codes to control all the stage of a tree: we generate the parallelism by allowing a node to call recursively a code on each of its sub-machines (children). When leaves are reached, they will execute their own codes and produce values, accessible by the top node using a vector. As shown in Fig. 6, the data are distributed on the stages (toward leaves) and results are gathered on nodes toward the root node. Let us consider a code where, on a node, the following code is executed: e . As shown in Fig. 5, the node creates a vector containing e for each children i. As the code is run asynchronously, the execution of the node code will continue until reaching a barrier. Table 2 shows the multi-ml primitives (without recall the bsml ones); their authorised level of execution and their informal semantics. n denotes the id of a node/leaf, i.e. its position in the tree encoded by the top-down path of positions in node's vectors. For example, 0 stands for the root, 0.0 for its first child, etc. For the ith component of a vector at node n, the id is n.i. Fig. 7 illustrates this naming. We now describe in details these primitives and multi-functions.

The let-multi Construction. The goal is to define a multi-function, i.e. a recursive function over the multi-bsp tree. Except for the tree's root, when the code ends on a stage i, the computed value is made available to the upper stage i -1 in a vector. The let-multi construction offers a syntax to declare codes for two levels, one for the nodes (level b) and one for the leaves (level s): [args] are the arguments of the newly define multi-function f. In the leaf block (i.e. level s), we find usual ml computations and most of the calculations should take place here. In the node block (i.e. level b), we find the code that will be executed at every stage of the tree but on the leaves. Typically, a node is charged to propagate the computations and the data using vectors (level l); to manage the sub-machine computations; and finally, gather the results using the proj (extraction of values from a vector). To go one step deeper in the tree, the node code must recursively call the multi-function inside a vector. This call must be done inside a vector in order to spread the computation all over the tree in the deeper stages. It is also to notice that a multi-function can only be called at m level of the code and values at this level are available throughout the multifunction execution. Fig. 8 shows, as an example of how data moves through the multi-bsp tree, a simple program summing of the elements of a list. It works as follows: We define the multifunction (line 1); lines 2 -5 give the code for the nodes and lines 6-7 give the code for the leaves; the list is scattered across each component i of the vector (line 3); on line 4, we recursively call the multi-function on the sub-lists (i.e. call in the contexts of the sub-nodes); we finally gather the results in line 5 (sum is a bsml code that performs a proj to sum the p n projected integers).

Tree Construction. It is similar to the above multi-functions: instead of generating a single usual ml value, functions defined with let multi tree build a tree of type a tree. For this, a new constructor determines the values that are stored (keep) at each id and those that are ascended (up) to the upper stage -until now, the value returned by nodes and leaves was implicitly considered as the value given to the upper stage. This is the role of finally which works as follows: finally ˜up:v1 ˜keep:v2 sends up the value v1 and stores in the tree the value v2 (thus replacing the previously stored value). The primitive this returns the last value stored using finally or the default value initialised thanks to a where default construction. It is useful to update the tree. Fig. 9 (next page) shows the modifications that have to be added to sum list in order to obtain a tree containing the list of partial sums on every leaves and the maximal sub-sums on each node -Thus, the root node contains the final sum. The code works as follows: We use a generic operator op with an identity element e and a list li to be distributed (line 1); Then we traverse the tree two times (phases distinguished by a boolean flag): First to split the list and then to compute the partial sums. On the nodes, we split the list (line 6) and then we do a recursive call over the scattered lists to continue the splitting at lower levels and then recover the partial sums of children nodes (line 7), a bsp scan is used to transfer and compose these partial results from sibling nodes left to right (scan direct could be replaced by any scan); Finally, we recall the multi-function (lines 8 -10) to complete the partial sums with the communicated values and for this, we transmit down a list containing only the last value from each branch, keep it in the tree and give it to the upper level (line 11). When reaching the leaves the first time, we compute the partial sums (line 16) and, each time a value (communicated by other branches) comes down to a leaf, we add it to its own partial sums (line 17). Note that using two multifunctions, one to first split the list and another one to compute the partial sums, is surely easier, but using a one-shot multi-function, we exhibit more features of multi-ml.

Variables Accesses. There are three different ways to access to variables in addition to the usual ml access. First, $v$ stands for reading the local value of a vector "v" inside a vector (l level, as in bsml).

The second way is to read a value inside a vector which had been declared outside. As explained above, the values available on a node are not implicitly available on the child nodes. It is thus necessary to copy them from a node to its sub-machines. For example, the code let x=1 in let vect= x+1 is incorrect because "x" is not available on children. It is imperative to use #x#+1 to copy the value of x from the b level into the vector (l level).

The last way is for reading the value of a tree. Within the tree construction §e § (syntax explained below), at(t) stands for reading the value of "t" at id n. Outside a vector (b level), accessing to a tree t is done in the same way. Finally, gid is the predefined tree of nodes/leaves ids. When executed inside a vector (l level) at a level n, at(gid) stands for the id n.i. However, inside a §e § code, it stands for the id of the current level. As expected, in a node (b level) or a leaf (s level), at(gid) is the identifier at the corresponding level. However, at level m, it is the tree of level identifiers.

A Convenient Tree Construction. For building a tree without using a multifunction (which induce communications), we add the §e § syntax. It allows to execute e on every nodes and leaves. One can read the values of a previously defined tree t using the $t$ access in the code of e. In this way, using the predefined tree gid, we can execute different codes on each components of a tree without any need (and possibility) of communication between the stages.

A New Primitive. For performances reason, we chose to add the new primitive mkpar. Indeed, in bsml a replicated code is duplicated on every processors, so it is not necessary to take care of data transfer in code like: let lst=[...] in split $pid$ lst where lst is a large list and split a splitting function. With the multi-ml model, data are not distributed everywhere and we have to transfer data explicitly. One can write split $pid$ #lst# but it is not useful to copy the whole list on every children in order to extract a sub list and throw the rest. This is the reason why mkpar computes, first, p n values and then distributes them to the sub-machines, thus building a vector. This method is more expensive for the node n in terms of computation time, but it reduces drastically the amount of data transfers.

Current Limitations

Exceptions and Partially Evaluated Trees. Exceptional situations are handled in ocaml with a system of exceptions. In parallel, this is at least as relevant: if one processor triggers an exception during a computation, bsml [START_REF] Gesbert | Bulk Synchronous Parallel ml with Exceptions[END_REF] as well as multi-ml have to deal with it, like ocaml would, and prevent a crash.

The problem is when an exception is raised locally (l level) on (at least) one processor whereas other processors continue to follow the execution stream, until they are stopped by the need of synchronisation. This happens when an exception escapes the scope of a parallel vector. Then, a crash can occur: a processor misses the global barrier. To prevent this situation, in [START_REF] Gesbert | Bulk Synchronous Parallel ml with Exceptions[END_REF], we introduce a specific handler of local exceptions that have not been caught locally. The structure trypar...withpar catches any exception and handles it as usual in ocaml. To do this, when a barrier occurs, all exceptions are communicated to all processors in order to allow a global decision to be taken. Furthermore, any access to a vector that is in an incoherent state will raise, again, the exception.

For multi-ml, if an exception is not correctly handled in a stage, it must be propagated to the upper stage at the next barrier -as in bsml. If an exception is no handled in a multi-function, it must be thrown at the global level m as a standard ocaml exception. An exception thrown in a node of a tree leads this node in an incoherent state until the exception has been caught in a upper level. Any access to this tree must raise again the exception. This handling has not been implemented yet for multi-ml but the first author works on it.

An application case is partially evaluated trees. Take for example the following code: if random() then raise Error else 0 where f is a multi-function. A part of the tree will never be instantiated. If a partially evaluated tree is accessed during a code execution an exception could be immediately thrown.

Type System. The main limitation of our prototype is the lack of a type system. Currently, nesting of bsml vectors/trees are not checked. A type system for bsml exists [START_REF] Gesbert | Bulk Synchronous Parallel ml with Exceptions[END_REF] but has not been implemented yet. We are convinced that adding multi-functions will not fundamentally change the type system: it's mainly a matter of adding just a new level of execution.

Other ml Features. We have not yet studied all the interactions of all the ocaml features with the multi-function (as well in bsml). Objects, first-order modules and gadt are left as future works.

We present a formal semantics of multi-ml as well as two implementations. A semantics is useful as a specification of the language so as to simplify the design of the implementations. To get the assurance that both implementations are coherent, using the semantics, we first prove that multi-ml is confluent. We also give some examples and benchmarks to illustrates the usefulness of multiml. Our prototype is freely available at http://www.lacl.fr/vallombert/Multi-ML.

Operational Semantics

We give a big-step semantics of a core-language without tree creation to simplify the presentation. The syntax (Fig. 10) extends the popular core-ml. Programs contain variables, constants (integers, etc.), operators (≤, +, etc.), pairing, let, if, fun statements as usual in ml, rec for recursive calls, the bsml primitives (<e>, put, proj), mkpar, access $x$ to the local value of a vector x, local copy #x# of a parent's variable x, the vector of pid component and gid the tree of ids. Finally, we define let-multi as particular functions with codes for nodes and leaves.

The semantics is a big-step one with environments that represent the memories. We have a tree of memories (one per node and leaf) and we note them E. E n denotes the memory of E at n where n is the id of a node/leaf. {x → v} denotes a binding of a variable x to a value v in the memory; ∈ denotes a membership test and ⊕ denotes an update. Those operators have the subscript n that denotes the application in a specific memory.

E e ⇓ v denotes the evaluation of e in the environment E to the value v. A value is a constant, an operator or a functional closure ( a function with its own environment of execution, denoted (fun x → e)[E]). The rules of evaluation are defined by induction and given in Fig. 11. To simplify the reading of the rules, we count vector pids from 1 to p n and not from 0 to p n -1. For core-ml the semantics are as usual.

Even if the semantics contains many rules, there is no surprise and it has to be read naturally. As explained before, there are 4 different levels of execution: level m for the execution on all computation units; bsp level b for bsml codes; Local level l for the codes inside a vector; and finally level s on the leaves. In this way, the evaluation ⇓ is upscripted by the level and can be subscripted by the id of the sub-machine.

The rules for the bsml primitives (Fig. 11) work as follows: (1) creating a new vector for the machine of id n is triggering p n local evaluations, each with n.i as subscript since we are going one step deeper, in the ith component; proj (2) and put (3) rules build the functions of exchanges; $pid$ rule (4) returns i on child n.i; $x$ rule (5) read at n.i the ith value of the vector x available on node n; #x# rule (6) read the value x at the node n from its child; the rule

§ ¦ ¤ ¥ bsml-like primitives inductive rules ⇓ b n (1) ∀i ∈ {1, . . . , p n } E e ⇓ l n.i v i E < e >⇓ b n v 1 , . . . , vp n (2) E e ⇓ b n v 1 , . . . , vp n E proj e ⇓ b n (fun i → v i )[] (3) E e ⇓ b n f 1 , . . . , fp n E put e ⇓ b n f 1 , . . . , f p n where f i j = f j i (4) E $pid$ ⇓ l n.i i (5) {x → v 1 , . . . , v i , . . . , vp n } ∈ E n E $x$ ⇓ l n.i v i (6) {x → v} ∈ E n E #x# ⇓ l n.i v (7) E n e ⇓ δ v E e ⇓ b,l n v (8) E e ⇓ b n f ∀i ∈ {1, . . . , p n } E (f i) ⇓ b n v i with f ≡ (fun x → e )[E ] E mkpar e ⇓ b n v 1 , . . . , vp n £ ¢ ¡ Multi functions inductive rules ⇓ m (9) E (multi f x → e 1 † e 2 ) ⇓ m (multi f x → e 1 † e 2 )[E] (10) E gid ⇓ b,l n n
In what follows g ≡ (multi

f x → e 1 † e 2 )[E ] (11) E e ⇓ δ v E e ⇓ m v (12) E e 1 ⇓ m g E e 2 ⇓ m v E ⊕ 0 {x → v}⊕ 0 {f → g} e 1 ⇓ b 0 v E e 1 e 2 ⇓ m v (13) E e 1 ⇓ l n.i g E e 2 ⇓ l n.i v E ⊕ n.i {x → v}⊕ n.i {f → g} e 1 ⇓ b n.i v E e 1 e 2 ⇓ l n.i v (14) E e 1 ⇓ l n.i g E e 2 ⇓ l n.i v E ⊕ n.i {x → v}⊕ n.i {f → g} e 2 ⇓ s n.i v E e 1 e 2 ⇓ l
n.i v Fig. 11 Operational big-step semantics rules of a core multi-ml. [START_REF] Cha | h-bsp: A hierarchical bsp computation model[END_REF] is the evaluation of the core ml part (sequential); mkpar rule (8) creates the vector but first the node creates the values to be sent down.

For the multi-functions, we have a rule to create them ( 9) and a rule (12) to initialise the recursion through the architecture from the root node. Then, inside the component i of a vector of sub-machine n, the recursive call of the multi-function generates an evaluation on n.i (rule 13), except if we reach a leaf, then the rule [START_REF] Fortin | BSP-Why: A tool for deductive verification of bsp algorithms with subgroup synchronisation[END_REF] says that the code is evaluated on leaf n.i with level s. The rule [START_REF] Chakravarty | Data Parallel Haskell: A Status Report[END_REF] is for the tree of ids. By induction, we can prove:

Lemma 1 (Confluence) ∀E if E e ⇓ m v 1 and E e ⇓ m v 2 then v 1 ≡ v 2
Co-inductive rules [START_REF] Leroy | Coinductive Big-step Operational Semantics[END_REF] ⇓ ∞ (for diverging programs) can be easily infered from the above rules. For sake of conciseness, we only present some typical examples:

E e 1 ⇓ δ true E e 2 ⇓∞ E if e 1 then e 2 else e 3 ⇓∞ ∃i ∈ {1, . . . , p t } E e ⇓∞ E < e >⇓∞ E e ⇓∞ E proj e ⇓∞
We can then prove by co-induction the following lemma:

Lemma 2 (Mutually exclusive) ∀E if E e ⇓ m v then ¬(E e ⇓ m ∞ )
The result does not depend of the order of evaluation of the processes nor of the bsp sub-machines. All strategy work and return the same value, especially a sequential simulation and a distributed implementation. The former is fine for debugging whereas the latter is for benchmarking. We now present both.

Sequential Simulation and Distributed Implementation

Sequential Simulation. We propose a sequential simulator that works as the ocaml toplevel. Given an architecture as a configuration file, the toplevel allows simulating multi-ml codes on a single core machine and printing the results. Currently, all the basic features of ocaml are available, without typing. To be executed, the multi-ml code is converted into a sequential code using a modified ocaml parser. The simulator creates a tree structure to represent the whole multi-bsp machine. Vectors are represented as arrays of data. A global hash table is used to simulate the memory available at each stage as suggested by the semantics. Fig. 12 shows the result when using the toplevel for a simulated multi-bsp machine composed of 2 processors with respectively 2 cores.

#let multi tree f n = where default = "" where node = let = f ($pid$ + #n# + 1) in finally ˜up:() ˜keep:(gidˆ"=>"ˆn) where leaf=finally ˜up:() ˜keep:(gidˆ"=>"ˆn);; -: val f : int→string tree = <multi-fun>

#(f 0) o "0→ 0" o "0.0→ 1" → "0.0.0→ 2" → "0.0.1→ 3" o "0.1→ 2" → "0.1.0→ 3" → "0.1.1→ 4"
Fig. 12 Example of the Toplevel.

Distributed Implementation. To be portable, our implementation is written to use various communication libraries. We have thus a modular approach and our implementation depends on a generic functor that requires the architecture configuration and some particular communication routines: asynchronous broadcasting and gathering for a group of processors, total exchange and building groups of processes. Our implementation of this module is currently based on mpi. We create one mpi process for every nodes and leaves of the architecture. Those processes are distributed over the physical cores and threads in order to balance the charge. As the code executed by nodes is, most of the time, a simple task of parallel management, this extra job is thus distributed over the leaves to reduce its impact.

Our implementation is based on a daemon running on each mpi process. Each daemon has 3 mpi communicators to communicate with its parent (upper node), its children (leafs) and its siblings (processes at the same sub-level). Each daemon is waiting for a task given by its parent. When a task is received, it is executed by the daemon, then the daemon returns to the waiting state until it receives a "kill" signal, corresponding to the end of the program.

As the code is an spmd one, every processes know the entire code and they just need to receive a signal to execute a task. To do so, and to avoid serialising codes that are inside functional values (the closures) and known by all the nodes due to an spmd execution, when transmitting down values and thus creating parallel vectors, we identify the vectors by two kinds of identifiers: (1) a static identifier is generated globally for every vectors and references their computations through the execution; (2) when a node needs to create a parallel vector, it generates a dynamic identifier that represents the data on its children. Then, when a node executes some code using parallel values inside a vector, it just sends the static identifier (that references the code to execute) with the dynamic identifier (to substitute the distributed value) to its children which can then execute the correct tasks. The main advantage of this method is to avoid serialising unnecessary codes when creating vectors, and thus to reduce the size of the data exchanged by the processes. However, associating a value to a dynamic identifier can lead to a memory over-consumption, for example in loops. When the life cycle of a vector is terminated, we manually clean the memory by removing all the obsolete identifier and calling the garbage collector.

Shared memory. We propose an implementation to avoid some unnecessary copies of the transmitted data. Indeed, the ocaml memory is garbage collected and, to be safe, only a copy of the data can be transmitted. Using the standard posix "mmap" routine and some ipc functionalities (to synchronise the processes), the child (as daemons) can read asynchronously the transmitted serialised value in the mapping of the virtual address space of the father and synchronise with the father only, as the multi-bsp model suggest. As architectures can have different types of memory (distributed or shared), it is possible to mix executions schemes. Since the ocaml memory is garbage collected (currently with a global thread lock), we sadly cannot use pthreads as done in [START_REF] Yzelman | An Object-oriented Bulk Synchronous Parallel Library for Multicore Programming[END_REF] to share values without performing first a copy. We are currently working on using some tricks to overcome this limitation but we leave it as future work.

Benchmarks

In this section we present the benchmarks of a simple scan with integer addition and a naive implementation of the sieve of Eratosthenes. A scan can be used to perform the sieve of Eratosthenes using a particular operator which implies more computations and communications than a simple list summing. The multi-bsp cost of the scan algorithm (Fig. 9) is as follows: The cost C i at level i is the cost of a bsp scan, of the diffusion of the computed values toward the leaves, in addition to the sequential cost of a map on list held by leaves. Let s be the size of the partial sum, the cost of bsp scan at level i is s * p i * g i-1 + L i , the diffusion cost is j∈]i...d] g j * s + l j and the final map cost is O(s d ). The size s may be difficult to evaluate: for a sum of integers it will simply be the size of an integer, but for Eratosthenes sieve, the size of exchanged lists varies depending on which data are held by the node. The sieve of Eratosthenes generates a list of prime numbers below a given integer n. From the list of all elements less than n, it iteratively removes elements that are a multiple of the smaller element of the list that has not been yet considered. We generate only the integers that are not multiple of the 4 first prime numbers, then we iterate √ n time (as it is known to be the maximum number of needed iterations). On our architectures Mirev2 and Mirev3 presented below, the direct and logarithmic scans are equally efficient.

p 0 = 4 g 0 = ∞ L 0 = 149000 m 0 = 0 p 1 = 2 g 1 = 89 L 1 = 1100 m 1 = 64Gb p 2 = 16 g 2 = 6 L 2 = 1800 m 2 = 20M b p 3 = 0 g 3 = 3 L 3 = 0 m 3 = 0 p 0 = 8 g 0 = ∞ L 0 = 195400 m 0 = 0 p 1 = 2 g 1 = 14 L 1 = 472 m 1 = 16Gb p 2 = 4 g 2 = 6 L 2 = 800 m 2 = 6M b p 3 = 0 g 3 = 5 L 3 = 0 m 3 = 0
Fig. 4 gives the bsml code of the direct scan. We used the following functions: elim:int list→ int→ int list which deletes from a list all the integers multiple of the given parameter; final elim:int list→ int list→ int list iterates elim using elements from the first list to delete elements in the second; seq generate:int → int→ int list which returns the list of integers between 2 bounds; and select:int → int list→ int list which gives the √ n first prime numbers of a list. For this naive example, we use a generic scan computation with final elim as the ⊕ operator. In our computation, we also did extend the scan so that the sent values are first modified by a given function (select) to just send the √ n first prime numbers. The bsp methods is thus simple: each processor i holds the integers between i × n p + 1 and (i + 1) × n p . Each processor computes a local sieve (the processor 0 contains thus the first prime numbers) and then our scan is applied. We then eliminate on processor i the integers that are multiple of integers received from processors of lower identifier.

Benchmark were done on two parallel architectures named Mirev2 and Mirev3. Here are the main specifications of these machines:

-Mirev2: 8 nodes with 2 quad-core (AMD 2376) at 2.3Ghz with 16Gb of memory per node and a 1Gb/s network. -Mirev3: 4 nodes with 2 hyper-threaded octo-core (16 threads) (Intel XEON E5-2650) at 2.6Ghz with 64Gb of memory per node and a 10Gb/s network.

The multi-bsp and bsp model can be used to estimate the cost of an algorithm. We estimated the cost of transferring values and the sequential cost of summing lists of integers, then we used the multi-bsp parameters given in Table 3 in order to predict and compare the execution time of scan.

We measured the time to compute the sieve without the time to generate the initial list of values. The experiments have been done on Mirev2 and Mirev3 using bsml (mpi version) and multi-ml over lists of increasing size on an increasing number of processors. The processes have been assigned to machines in order to scatter as much as possible the computation among the machines, i.e. a 16 process run will use one core on each processor of the 8 machines of Mirev3. Tables 4 and5 shows the results of our experimentations. We can see that the efficiency of multi-ml on small list is poor but as the list grows, multi-ml exceeds bsml. This difference is due to the fact that bsml communicates through the network at every super steps; while multi-ml is 500 000 1 000 000 3 000 000 multi-ml bsml multi-ml bsml multi-ml bsml multi-ml bsml 8 0. focusing on communications through local memories and finally communicates through the distributed level. Table 6 gives the computation time of the simple scan using a summing operator. On the sum of integers, we can see that multi-ml introduces a small overhead due to the level management. However it is as efficient as bsml and concord to the estimated execution times. As the experiment shows, multi-ml out-performs bsml with communication intensive algorithms. The bsml program tends to saturate the network when all the processors start to communicate. On the contrary, the multi-ml algorithm avoid this bandwidth over consumption and takes advantage of the shared memory.

Related Work

There are a lot parallel languages or parallel extensions of sequential languages (functional, iterative, object-oriented, etc.). It would be too long to list all of them. We chose to point out those that were the most important to our mind. Notice that, except in [START_REF] Loidl | Comparing Parallel Functional Languages: Programming and Performance[END_REF], there is a lack of comparisons between parallel languages. It is difficult to compare them since many parameters have to be taken into account: efficiency, scalability, expressiveness, etc.

Programming Languages and Libraries for BSP like Computing

Historically, the first library for bsp computing was the bsplib [START_REF] Hill | bsplib: The bsp Programming Library[END_REF] for the c language; it has been extended in the pub library [START_REF] Bonorden | The Paderborn University bsp (pub) library[END_REF] by adding subgroup synchronisations, high performance operations and migration of threads. For the gpu architectures, a bsp library was provided in [START_REF] Hou | BSGP: Bulk-Synchronous gpu Programming[END_REF] with mainly drma primitives close to the bsplib's ones. There is also MulticoreBSP [START_REF] Yzelman | An Object-oriented Bulk Synchronous Parallel Library for Multicore Programming[END_REF] which proposes multi-bsp style programming features. For java, different libraries exist: the first one was [START_REF] Gu | JBSP: A bsp programming library in java[END_REF], then in [START_REF] Da Rosa Righi | MigBSP: A Novel Migration Model for Bulk-Synchronous Parallel Processes Rescheduling[END_REF] a library has been designed with scheduling and migration of bsp threads -the scheduling is implicit but the migration can be explicit. The library hama [START_REF] Seo | hama: An Efficient Matrix Computation with the MapReduce Framework[END_REF] is implemented using a "mapreduce-like" framework. We can also highlight the work of neststep [START_REF] Keßler | NestStep: Nested Parallelism and Virtual Shared Memory for the bsp Model[END_REF] which is c/java library for bsp computing, which brings nested computations capabilities in case of a cluster of multi-core but without any safety.

The bsml primitives were adapted for c++ [START_REF] Hamidouche | A Framework for an Automatic Hybrid mpi +open-mp Code Generation[END_REF]: the bsp++ library provides nested computation in the case of a cluster of multi-cores (mpi+openmp). But it is the responsibility of the programmer to avoid harmful nested parallelism. bsml also inspired bsp-python [START_REF] Hinsen | Using bsp and python to Simplify Parallel Programming[END_REF] and bsp-haskell [START_REF] Miller | bsp in a Lazy Functional Context[END_REF].

Functional Parallel Programming

A survey on parallel functional programming can be found in [START_REF] Hammond | Research Directions in Parallel Functional Programming[END_REF]. It has been used as a basis for the following classification with some updates.

Data-parallel Languages. The first functional one was nesl [START_REF] Blelloch | NESL[END_REF]. This language allows to create particular arrays and nested computations within these arrays. The abstract machine is responsible for the distribution of the data over the available processors. For ml, there is manticore [START_REF] Fluet | Implicitly-threaded Parallelism in Manticore[END_REF], an extension of nesl with the dynamic creation of asynchronous threads and send/received primitives. For gpu architectures, an extension of ocaml, using a special syntax for the kernels has been developed in [START_REF] Bourgoin | Spoc: GPGPU programming through stream processing with ocaml[END_REF].

sac (Single Assignment c) [START_REF] Grelck | SAC-A Functional Array Language for Efficient Multithreaded Execution[END_REF] is a lazy language (with a syntax close to c) for array processing. Some higher-order operations on multi-dimensional arrays are provided and the compiler is responsible for generating an efficient parallel code. A data-parallel extension of haskell has been done in [START_REF] Chakravarty | Data Parallel Haskell: A Status Report[END_REF] where the language allows to create data arrays that are distributed across the processors. And some specific operations permit to manipulate them.

The main drawback of all these languages is that cost analysis is hard to do since the system is responsible for the data distribution.

Explicit process creation. We found two extensions of haskell in this category: eden [START_REF] Loogen | Parallel functional programming in eden[END_REF] and gph [START_REF] Scaife | Empirical Parallel Performance Prediction From Semantics-Based Profiling[END_REF]. Both use a small set of syntactic constructs for explicit process creation. Their fine-grain parallelism, while providing enough control to implement parallel algorithms efficiently, frees the programmer from the tedious task of managing low-level details of communications -which uses lazy shared data. Processes are automatically managed by sophisticated runtime systems for shared memory machines or distributed ones.

As above, cost analysis is hard to do and, sometimes, the runtime fails to distribute correctly the data [START_REF] Scaife | Empirical Parallel Performance Prediction From Semantics-Based Profiling[END_REF]; it introduces too much communications and thus a lack of scalability. Another distributed language is hume [START_REF] Hammond | The dynamic properties of Hume: A functionally-based concurrent language with bounded time and space behaviour[END_REF]. The main advantage of this language is that it is provided with a cost analysis of the programs for real-time purpose but with limitations of the expressiveness.

Algorithmic skeletons. Skeletons are patterns of parallel computations [START_REF] González-Vélez | A Survey of Algorithmic Skeleton Frameworks: Highlevel Structured Parallel Programming Enablers[END_REF]. They can be seen as high-order functions that provide parallelism. They thus fall into the category of functional extensions. They are many skeleton libraries [START_REF] González-Vélez | A Survey of Algorithmic Skeleton Frameworks: Highlevel Structured Parallel Programming Enablers[END_REF]. For ocaml, the most known work is the one of [START_REF] Cosmo | Skeletal Parallel Programming with ocaml P3l 2.0[END_REF].

Distributed functional languages. In front of parallel functional languages, there are many concurrent extensions of functional languages such as erlang, clean or jocaml [START_REF] Mandel | Programming in jocaml[END_REF]. The latter is a concurrent extension of ocaml, which add explicit synchronisations of processes using specific patterns. alice-ml [START_REF] Rossberg | Typed Open Programming -A higher-order, typed approach to dynamic modularity and distribution[END_REF] adds what is called a "future" for communicating values. A future is a placeholder for an undetermined result of a concurrent computation. When the computation delivers a result, the associated future is eliminated by globally replacing it by the result value. The language also contains "promises" that are explicit handles of futures. scala is a functional extension of java which provides concurrency, using the actor model: mostly, creation of agents that can migrate across resources. Two others extensions of ocaml are [START_REF] Chailloux | A Portable Implementation for Objective Caml Flight[END_REF] and [START_REF] Chailloux | HirondML: Fair threads migrations for Objective Caml[END_REF]. The former uses spmd primitives with a kind of futures. The latter allows migration of threads that communicate using particular shared data.

All these languages have the same drawbacks: they are not deadlock and race condition free; furthermore, they do not provide any cost model.

Conclusion and Future Work

Summary of the Contribution

The paper presents a language call multi-ml to program multi-bsp algorithms. It extends our previous bsml that has been designed for programming bsp algorithms. They both have the following advantages: confluent operational semantics; equivalence of the results for both toplevel and distributed implementation; cost model and efficiency.

The multi-bsp model extends the bsp one as a hierarchical tree of nested bsp machines. multi-ml extends bsml with a special syntax to define special recursive functions over this tree of nested machines, each of them programmed using bsml. In a tree, nodes contain codes to manage the submachines whereas leaves perform the largest part of the computation. In this work, we focus on the informal presentation of multi-ml, an operational semantics of a core-language and benchmarks of simple examples with a comparison with predicted performances associated with the multi-bsp cost model. We also compare multi-ml codes with bsml ones as well as the performances of both languages on a typical cluster of hyper-threaded multi-cores. As predicted, multi-ml codes run faster than bsml when the cores share the network: there is no bottleneck; And the multi-core synchronisations are cheaper.

Fig. 1 A

 1 Fig.1A bsp super-step.

1 let scan direct op e vv = 2 let mkmsg pid v dst = 3 if 4 let procs lists = 5 fun pid → from to 0 pid in 6 let receivedmsgs = 7 put mkmsg $vv$ in 8 let values lists = 9 List.map ((compose noSome) 10 $ 11 ( 12 (Fig. 4

 234567891011124 Fig.4bsml direct scan code.

Fig. 5

 5 Fig. 5 Vector distribution.

Fig. 6

 6 Fig. 6 Code propagation.

3. 2 1 Fig. 7

 217 Fig. 7 Node identifiers.

  let multi f [args] = where node = ... ( * bsml code * ) where leaf = ... ( * ocaml code * )

1Fig. 8

 8 Fig. 8 Sum multi-ml example.

1 4 where node = 5 if flag then 6 let 13 let 25 ⇒Fig. 9

 45613259 Fig. 9 Scan multi-ml example.

eFig. 10

 10 Fig.10Syntax of core-multi-ml.

1 p

 1 i∈[0...d[ V sp (i) + O(|l d |) + i∈[0...d[ C i . Where i∈[0...d[ V sp (i) is the total cost of splitting the list toward the leaves (at depth d-1); O(|l d |) is the time needed to compute the local sums in the leaves; and i∈[0...d[ C i corresponds to the cost of diffusing partial sum back to leaves and to add these values to the values held by leaves. This diffusion is done once per node. V sp (i) is the work done at level i to split the locally held chunk l i and scatter it among children nodes. Splitting l i in p i chunks costs O(|l i |) where |l i |, the size of l i , is n * j∈[0...i[ j where n is the size of the initial list holds by the root node. Scattering it among children nodes costs p i * g i-1 + ni p i + L i . The sequential list scan cost at leaves is O(|l d |) = O(n * i∈[0...d[ 1 p i ).

Table 2

 2 Summary of the multi-ml primitives.values contained in a tree are accessed by the corresponding node (or leaf) only. It is impossible to access the values of another component without using explicit communications. In multi-ml codes, we discern four strictly separated execution levels: (1) the level m (multi-bsp) is the upper one (outside trees) and is appropriate to call multi-functions and managing the trees; codes at this level are executed by all the computation units in a spmd fashion; (2) the level b (bsp) is used inside multi-functions and is dedicated to execute bsml

	1)Data	Parent
		3)Result
	Child	. . .	Child
	2)Computations

codes on nodes; (3) level l (local) corresponds to the codes that are run inside vectors; (4) level s stands for standard ocaml codes finally executed by the leaves. It is to notice that it is impossible to communicate vectors or trees and, like in bsml, the nesting of parallelism (of vectors/trees) is forbidden.

Table 3

 3 Multi-BSP parameters of Mirev3 (left) and Mirev2 (right).

Table 4

 4 Execution time of Eratosthenes using multi-ml and bsml on Mirev3.

		7	1.8	22.4	105.0	125.3 430.7	...	...
	16	0.5	0.8	13.3	50.3	68.1	331.5	1200.0	...
	32	0.3	0.5	2.6	18.9	11.3	122.2	173.2	...
	48	0.5	0.4	1.75	14.5	5.5	88.4	69.3	...
	64	0.3	0.3	1.3	8.7	4.1	56.1	51.1	749.9
	96	0.3	0.38	1.6	6.3	3.9	30.8	38.1	576.1
	128	0.5	0.45	2.1	5.2	4.7	24.3	30.6	443.7
			100 000	500 000	1 000 000
			multi-ml bsml	multi-ml bsml	multi-ml bsml
	8		1.5	1.7	64.5	106.1	402.9 1538.1
	16	0.45	0.93	16.0	49.3	91.4	631.7
	32	0.14	0.45	4.1	18.7	21.1	219.7
	48	0.13	0.40	2.6	11.0	10.8	123.5
	64	0.11	0.34	1.89	7.5	8.2	80.5

Table 5

 5 Execution time of Eratosthenes using multi-ml and bsml on Mirev2.

				5 000 000
		multi-ml bsml	P red multi-ml P red bsml
	8	2.91	2.8	3.44	1.83
	16	1.42	1.4	1.72	0.92
	32	0.92	0.73	0.43	0.46
	48	0.84	0.75	0.28	0.31
	64	0.83	0.74	0.21	0.23

Table 6

 6 Execution time and predictions of scan (sum of integers) on Mirev3.

Compared to bsml, multi-ml has several drawbacks. First, the codes, the semantics and the implementation are a bit more complex. Second, the cost model associated to the program is more difficult to grasp: designing multibsp algorithms and programming them in multi-ml is more difficult than using bsml only. However, from our experience, we can say that it is not so hard.

Future Work

In a close future, we plan to axiomatise the multi-ml primitives inside coq, as we did for bsml in [START_REF] Gava | Formal Proofs of Functional bsp Programs[END_REF][START_REF] Gesbert | Systematic Development of Correct Bulk Synchronous Parallel Programs[END_REF], in order to prove the correctness of multi-bsp algorithms. We also consider to formally prove that the implementations follow the formal semantics. We also plan to benchmark bigger examples, we think of model-checking problems and algebraic computations that better follow highlevel languages than intensive float operations can do.

The most important work to do is the implementation of a type system for multi-ml to ensure safety of the codes: forbid nesting of vectors, forbid dataraces when imperatives features such as exceptions handling [START_REF] Gesbert | Bulk Synchronous Parallel ml with Exceptions[END_REF] are used. In the long term, the type system could be used to optimise the compiler. Indeed, currently, even in the case of a share-memory architecture, only serialised values are exchanged between nodes. We consider implementing a dedicated concurrent garbage collector.


Bassem Ouni

Pierre Gaufillet

Eric Jenn

Jérôme Hugues

Model Driven Engineering with Capella and AADL

Keywords: Real time, Embedded systems, Model transformations, Performance evaluation, Constraints verification, Capella, AADL. I

The development of real time embedded equipments is a challenging task that requires the elaboration of multiple models in several domains, notably system, electronics and software, spanning a large spectrum of multiple abstraction levels and viewpoints: structural, behavioral, dependability, etc. These models serve various purposes: specification, design, evaluation or verification and validation. Today, no single modeling language and environment covers all these aspects. While Capella -an open source modeling language and environment for system engineering developed by Thales -fits well to the most early stages of the development process, AADL -the Architecture Analysis and Design Language defined by the Society of Automotive Engineers -provides powerful capabilities to describe and analyze the design artifacts of the software point of view that appear during the latest phase of the design. This is why they have both been selected in the project INGEQUIP of IRT Saint Exupéry. While using different modeling languages for different purpose is perfectly acceptable in a development process, it is important to guarantee that information remain consistent across all models. This is why building a formalized bridge between Capella and AADL is an essential piece of INGEQUIP process. In this paper, after an introduction to the context of INGEQUIP, the high level semantics of Capella and AADL are compared. The mapping used in INGEQUIP between Capella physical models and AADL abstract models is then described. The whole approach is illustrated by some elements coming from the design of TwIRTee -the robotic demonstrator of INGEQUIP -before concluding.

INTRODUCTION

This work is achieved under the INGEQUIP project at the Toulouse Institut de Recherche Technologique (IRT) Saint-Exupéry. IRTs are new research structures established under the auspices of the French Agence Nationale de la Recherche (ANR). IRTs are aimed at favouring the transfer of innovation from laboratories to industries. Towards this goal, IRTs gather engineers coming from small to large companies from various industrial domains, and researchers from public universities and national research agencies. As an example, INGEQUIP covers the space, aeronautics and automotive systems domains. The goal of INGEQUIP is to study and propose solutions for supporting closely integrated development of the main technical domains involved in embedded equipment engineering -system, eleectronics and software engineering. A key element for reaching such goal is to ensure the continuity and consistency of information in the whole chain of activities. In INGEQUIP, the choice has been to obtain this property by relying on models and model transformations. The set of requirements regarding an equipment is usually divided into two categories: functional requirements and non functional requirements. Functional requirements include the system's behavior, capabilities and characteristics as specified by stakeholders whereas non-functional properties or requirements define criteria that can be used to evaluate the operations of the system. In order to design the system and associate to the design elements the realized functional and non functional requirements, several modeling languages are available among which AADL a Seconded from Airbus, 316 route de Bayonne, 31000 Toulouse, France. b Seconded from Thales Avionics, 105 avenue du Général Eisenhower, 31100 Toulouse, France.

[1] -Architecture and Analysis Design Language, AUTOSAR [START_REF]AUTOSAR[END_REF], Capella [START_REF]Capella tool environement and Arcadia methodology[END_REF], EAST-ADL [START_REF]EAST-ADL[END_REF], SysM [START_REF]SysML[END_REF] and UML [START_REF]UML[END_REF] have been considered. While Capella, EAST-ADL and SysML fit system engineering, AADL, AUTOSAR and UML are focused on software engineering. Finally the couple Capella/AADL has been chosen in INGEQUIP because they provide most viewpoints commonly used by designers of embedded equipment at system and software levels: functional breakdown, logical and physical architecture, software dynamic and static architecture, formal behavioral descriptions; they are supported by a number of tools widely available: Capella and OSATE for edition, formal behavioral analysis tools like FIACRE and Tina [START_REF] Berthomieu | Formal Verification of AADL models with Fiacre and Tina[END_REF], Cheddar [8] and code generations like OCARINA [START_REF] Ocarina | Ocarina[END_REF]). They are also based on open technologies like the Eclipse Modeling Framework which allows to develop easily tools extensions. Consistently with the orientation of INGEQUIP, a transformation has then been defined and developed for ensuring a seamless transition from system engineering stage to software engineering stage.

In this paper, we therefore begin in section 2 by introducing the state of the art of engineering models transformation. Then, section 3 presents a first comparison between the semantics of Capella and AADL. The mapping of the transformation between Capella physical model and AADL abstract model is then described in section 4. The whole approach is illustrated by some elements coming from the design of TwIRTee -the robotic demonstrator of INGEQUIP -in section 5 before concluding in section 6.

II. RELATED WORKS

In order to achieve an early analysis of the specification, the verification of functional and non-functional properties of the system, and even code generation for the targeted hardware platform, several studies have proposed comparable transformations to AADL models. In [START_REF] Brun | From UML to AADL: an Explicit Execution Semantics Modelling with MARTE[END_REF], Brun et al. introduce an approach for translating UML/MARTE detailed design into AADL design. The proposed work focuses on the transformation of the thread execution and communication semantics and does not cover transformation of embedded system components, such as equipment parts. Turki et al. [START_REF] Turki | Mapping the MARTE UML Profile to AADL[END_REF] propose a methodology for mapping MARTE model elements to AADL components. They focus on the issues related to modelling architectures. This transformation flow does not consider issues related to the mapping of MARTE properties to AADL property. The syntactic differences between MARTE and AADL are well handled by the transformation rules provided by ATL tool. In [START_REF] Ouni | Accurate energy characterization of OS services in embedded systems[END_REF], AADL is used for modelling the properties of embedded system architecture, including the application's tasks, the hardware platform and the operating system services in order to characterize the energy overhead of embedded operating system . The authors propose an AADL model transformation in order to be exploited by a multiprocessor simulation tool named STORM (Simulation TOol for Real-time Multiprocessor scheduling). AADL provides hardware and software architectures together with the scheduling policy; STORM simulates the system behaviour using all the characteristics (task execution time, processor functioning conditions, etc.) in order to obtain the chronological track of all the scheduling events that occurred at run time, and compute various real-time metrics in order to analyse the system behaviour and performances from various point of views. Then, this work has been extended in [START_REF] Ouni | Thesis dissertation: High-level energy characterization, modeling and estimation for OS-based platforms[END_REF] and a system design exploration methodology has been proposed to verify system requirements when allocating applicative tasks to the processors using a set of tools: RDALTE for the definition and analysis of system requirements and QAML for quantitative analysis. In this paper, the proposed approach for transformation of Capella to AADL models target to cover the various levels of abstraction when modeling systems. We take into account the system behavior and the hardware/software mapping. Next section will detail the transformation flow and how it exploits the complementarity of Capella and AADL in order to cover various embedded system aspects at high level modeling step.

III. PROPOSED METHOD

As Capella and AADL partially overlap, as shown in the diagram (Figure 1) below, the first question that has to be answered before defining the transformations from Capella to AADL is the level at which this transformation should be performed. Capella is clearly positioned on the most abstract part of the system development process with the Operational Analysis, focusing on the capture of stakeholders' needs, and the System analysis, focusing on the functional definition of the system. As for AADL, it doesn't offer support for such kind of analysis. As they deal with the system's architecture, Capella's logical and physical models share lots of concepts with AADL, in particular the capability to express structural refinement. AADL however goes further by providing not only system-oriented abstract components, but also explicit hardware components -device, processor, memory, bus -and explicit software components -process, thread, subprogram.

Moreover, AADL proposes a formal models of communication and execution semantics that is a prerequisite for any low-level behavioral analysis (e.g., schedulability analysis).

Capella provides system modeling capabilities at several layers of abstraction:  At operational level, the customer needs, the actors, the missions and the activities are described.  At system level, a Capella model defines how system can satisfy the former operational need.  Capella logical level modeling starts from functional and non-functional analysis and builds one or several decompositions of the system into logical components.  The building of logical components is performed at physical level: the "final" architecture of the system introducing architectural patterns, services and components, and it makes the logical architecture evolve according to implementation, constraints and choices.

Figure 2 summarizes the relationship between functional, logical and physical architecture in a Capella model. In this work, we interest to parse the physical architecture of the Capella model as it includes functional, logical and physical components.

Whatever the abstraction level of the considered components is, AADL also brings the capability to specify additional information compared to Capella, like functional or non-functional properties. Consequently, the simplest articulation between the two languages is at the levels of the logical or physical architectures. Considering that Capella is well adapted to describing the logical architecture and a first abstract level of physical architecture, and that it is a good practice to limit the risk of data duplication and inconsistency between Capella and AADL models, the best solution is to delay as far as possible the transfer of information. As shown in figure 3, the model transformation will therefore take as input the most detailed physical architecture in Capella, and the design process will go on in AADL.

Operational Analysis

A. Transformation definition

To transform Capella to AADL models, we explore the contents of a Capella model and generate the appropriate AADL code following the Capella/AADL concepts analogy proposed in Table 1. The equivalent of an AADL processor, device are Capella node physical components with respectively a software execution unit and hardware kinds. A physical component with behavior nature and software application kind is considered as process in AADL. Physical buses components are not modeled in Capella meta-models. For this reason, using Capella ecore meta-models, we generate Capella EMF [START_REF]Eclipse Modeling Framework[END_REF] code and exploit it using Java to extract physical buses from Capella model and map them to AADL buses. The determination of buses is elaborated by exploring the Capella physical components, the physical links which are the communication/transportation means linking node Physical components, and physical ports. As depicted in figure 4, the physical links connected by physical ports are gathered in "AllconnectedLinks" list. For each element of the list, a physical bus component, with a bus port, will be generated to bind the physical links. Then, as showed in Figure 5, buses are connected to external ports (tip ports) which are ports of physical components having no subcomponents. This established link is called BusLink. BusLinks are divided into segments that don't cross physical component boundaries. These segments represent synthetic links. Synthetic ports includes the tipports and new ports which are generated at each intersection between BusLinks and physical components. The algorithm describing buses extraction is detailed in algorithm 1. The output of this algorithm is the list of synthetic ports and links that will be mapped to AADL elements.

In Capella, logical components are not stored in the physical components they are deployed on, but, in the physical system root, , For rebuilding the AADL connection path, and as depicted in figure, a virtual physical component is created instead of each logical component, a connection is established between these virtual components, then as for the buses, we split this connection into parts and we generate new Capella ports with a new property: the direction. To transform Capella to AADL models, Accelo plugin [START_REF]Acceleo Project[END_REF] is used, it allows the generation of AADL code from input Capella graphic models. We exploit this plugin to explore the contents of a Capella model and generate the appropriate AADL code following the Capella/AADL concepts analogy proposed in Table 1. TwIRTee is a three-wheeled autonomous rover developed within the INGEQUIP project. Its operational role is very simple: move itself on some predefined tracks from a point A to a point B (a "mission") while avoiding other rovers. To achieve this mission, it is fitted with several sensors (camera, odometry sensors, global positioning,…) and two main actuators (motors).

The development of the rover is not an objective per se. Indeed, TwIRTee is designed so as to cover the major topics addressed in the project namely: early validation, architecture exploration, performance prediction, and formal verification. Furthermore, it is aimed at covering issues, and functional and architectural elements specific to the three industrial domains. Accordingly, missions, functions and the architectural elements are determined so as to tackle or exercise one or several issues: for instance, "the localization" function relies partially on imaging so as to exercise hardware / software space exploration and co-design; the highly redundant architecture provides the experimental setup to perform early performance evaluations (including dependability), etc.

The computing platform of TwIRTee is composed of 2 COM/MON channels that host the main "mission" functions and one channel dedicated to power supply generation and motor control. In order to cover issues related to the development of safety-critical Man Machine Interfaces, the system also contains a remote operator station. Figure 3 and Figure 4 show respectively elements of TwIRTee design in Capella and their corresponding elements in AADL. In this paper, we introduced a transformation from Capella physical architecture to a preliminary software architecture in AADL. The goal of this approach is to implement a seamless development process from system definition and design to software design and implementation. The approach has been applied and validated during the design of the TwIRTee rover demonstrator. The resulting physical model has been used to verify structural, performance (power and energy consumption), timeliness and dependability properties.

Figure 3 -

 3 Figure 1-Capella and AADL positioning

Figure 6 -Capella component exchanges transformation Algorithm 1 -Capella Bus generation algorithm 1 .

 611 Figure 4 -Determination of connected physical links

Figure 7 -Figure 8 -

 78 Figure 7 -Elements of TwIRTee design in Capella

Table 1 -Mapping of Capella -AADL concepts

 1 3. Determinate the list allConnectedLinks including the sets of pls connected by pps. 4. for each element of allConnectedLinks a. Get the category of the link b. Create the list of external ports tipports c. Create a bus instance having the same name of category d. Associate the bus instances with tipports in a BiMap structure bus2TipPorts (key=bus instance, value=tipports). 5. end for 6. Initialize the list of synthetic ports with the tip ports and synthetic links. 7. for each element of bus2TipPorts a. Search the closest common physical component ancestor PcCommonAncestor of tipPorts b. Create the Physical component that will model physically the bus instance: PCBus c. Add new properties to PCBus: isBus and Bustype property d. Add a port BusPort to the PCBus

	e. Add PCbus to PcCommonAncestor
	f. for each port p of bus2TipPorts
	i. Create a link from tip port p to BusPort
	ii. Divide this link into segments that don't cross Physical Component boundaries
	iii. Update the list of synthetic ports and links
	g. end for
	8. end for

ACKNOWLEDGEMENT

The authors thank all people and industrial partners involved in the Ingequip project. This work is supported by the French Research Agency (ANR) and by the industrial partners of IRT Saint-Exupéry Scientific Cooperation Foundation (FCS): Actia Automotive, Airbus (a), Airbus Defense and Space, Continental Automotive, SAGEM, Systerel, Thales Avionics (b), ASTC Design Partners, Space Codesign Systems.