Victor Allombert
email: victor.allombert@univ-orleans.fr

Frédéric Gava
email: gava@u-pec.fr

Julien Tesson
email: julien.tesson@lacl.fr

A formal semantics of the MULTI-ML language

Keywords: Semantics, MULTI-BSP, ML let multi mf [args]= | where node = ... in v

In the context of high performance computing, it is important to avoid indeterminism and dead-locks. MULTI-ML is a functional parallel programming language "à la ML", designed to program hierarchical architectures in a structured way. It is based of the MULTI-BSP bridging model. To ensure that a program "cannot go wrong", we first need to define how a program "goes". To do so, we propose a formal operational semantics of the MULTI-ML language to ensure the properties of the MULTI-BSP model. We first describe a core-language and then introduce the big step's semantics evaluation rules. Then, we propose a set of evaluation rules that describe the behaviour of the MULTI-ML language. The memory model is also precisely defined, as the MULTI-BSP model deals with multiple level of nested memories.

I. INTRODUCTION

A. Context

Our previous work aimed at designing a parallel functional language based on the Bulk Synchronous Parallelism (BSP) bridging model called BSML [START_REF] Gesbert | Bulk synchronous parallel ML with exceptions[END_REF]. BSP is a model of parallelism which offers a high level of abstraction and takes into account real communications and synchronisation costs [START_REF] Skillicorn | Questions and Answers about BSP[END_REF]. BSP has been used successfully for a broad variety of applications. To be compliant to a bridging model eases the way of writing codes that ensures efficiency and portability from one architecture to another. Thanks to a cost model it is also possible to reason on the algorithmic costs.

As modern HPC (High Performance Computing) architectures are hierarchical and have multiple layers of parallelism, communication between distant nodes cannot be as fast as among the cores of a given processor. As BSP was designed for flat architectures, we now consider the MULTI-BSP model [START_REF] Valiant | A Bridging Model for Multi-core Computing[END_REF], an extension of BSP which is dedicated to hierarchical architectures. MULTI-ML [START_REF] Allombert | Multi-ML: Programming Multi-BSP Algorithms in ML[END_REF] is an extension of OCAML for programming MULTI-BSP algorithms. MULTI-ML uses a small set of primitives similarly to BSML for BSP algorithms.

To ensure that a language is properly implemented, it is important to provide a semantics that describes precisely the behaviour and the memory model of a language. Natural semantics (also called big-step semantics) aims to describe, in a formal way, how the overall result of the evaluation of an expression is obtained. In the context of MULTI-ML programming, it is thus possible to describe precisely the evaluations steps leading to a valid evaluation of a hierarchical computation. Using a set of inductive and co-inductive rules, we define both terminating and diverging terms evaluation. Thus, we are able to express formally how a MULTI-ML program "goes".

B. Outlines

In this article we introduce the formal (operational) semantics of the MULTI-ML language. First, we introduce MULTI-ML, the MULTI-BSP model and the previous models and languages, in section II. In (section III) we propose a core language that describes the syntax of the language, and the MULTI-ML execution model. Then, in section IV, we give and describe the terminating rules of the MULTI-ML semantics; followed be the diverging one. The formal properties of the semantics are discussed in section V. After the description of related works (in section VI) we conclude in section VII.

II. PREVIOUS WORK A. The BSP bridging model

In the BSP model [START_REF] Valiant | A Bridging Model for Parallel Computation[END_REF], a computer is a set of p uniform pairs of processor-memory with a communication network. A BSP program is executed as a sequence of super-steps (Fig. 1), each one divided into three successive disjointed phases: [START_REF] Gesbert | Bulk synchronous parallel ML with exceptions[END_REF] each processor only uses its local data to perform sequential computations and to request data transfers to other nodes; [START_REF] Skillicorn | Questions and Answers about BSP[END_REF] the network delivers the requested data; (3) a global synchronisation barrier occurs, making the transferred data available for the next super-step. Thanks to this structured execution scheme, deadlocks are avoided and determinism is preserved. As BSP architecture can be easily mapped on any general purpose parallel architecture, it is possible to accurately estimate the execution time of a BSP program with the BSP parameters (not detail in this article). The execution time (cost) of a super-step is the sum of the maximal of the local processing time, the data delivery and the global synchronisation times. The total cost of a BSP program is thus the sum of its supersteps's costs.

B. The BSML language.

BSML [START_REF] Gesbert | Bulk synchronous parallel ML with exceptions[END_REF] is a functional parallel programming language designed to program BSP algorithms. It uses a small set of primitives and is currently implemented as a library for the ML (Meta Language) programming language OCAML.

A BSML program is built as a ML one but using a specific data structure called parallel vector. Its generic ML type is α par. A vector expresses that each of the p processors embeds a value of any type α. Informally, they work as follows: Let e be the vector holding e everywhere (on each processor), the indicates that we enter into the scope of a vector. The informal semantics of this construction is e, . . . , e , assuming that ... denotes a parallel vector.

Within a vector, the syntax $x$ can be used to read the vector x and get the local value it contains. Informally, we have v i on processor i, assuming that v ≡ v 0 , . . . , v p-1 . The ids can be accessed with the predefined vector pid.

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, returns the value of the vector at this processor. The proj primitive is typed α par→(int→α). proj performs communication to make local results available globally and ends the current super-step. Informally, we have proj x 0 , . . . , x p-1 → (fun i → x i ).

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. put is typed (int→α)par→(int→α)par. The parameter of put is a vector that, at each processor, holds a function returning the data to be sent to processor j when applied to j. The result of put is another vector of functions: at a processor j the function, when applied to i, yields the value received from processor i by processor j. Informally, we have put f 0 , . . . , f p-1 → fun i → f i 0, . . . , fun i → f i (p-1) .

C. The Multi-BSP bridging model.

MULTI-BSP is a bridging model [START_REF] Valiant | A Bridging Model for Multi-core Computing[END_REF] which is adapted to hierarchical architectures, mainly clusters of multi-cores. It is an extension of the BSP bridging model. The structure and abstraction brought by MULTI-BSP allows to have portable programs with scalable performance predictions, without dealing with low-level details of the architectures. This model brings a tree-based view of nested components (sub-machines) of hierarchical architectures where the lowest stages (leaves) are processors and every other stage (nodes) contains memory.

Every component can execute code but they have to synchronise in favour of data exchange. Thus, MULTI-BSP does not allow subgroup synchronisation of any group of processors: at a stage i there is only a synchronisation of the subcomponents, a synchronisation of each of the computational units that manage the stage i-1. So, a node executes some code on its nested components (aka "children"), then waits for results, does the communication and synchronises the submachine. A MULTI-BSP algorithm is thus composed by several super-steps, each step is synchronised for each sub-machine. Mainly, an instance of MULTI-BSP is defined by d, the fixed depth of the (balanced and homogeneous) tree architecture, and by 4 parameters for each stage i of the tree : (p i , g i , L i , m i ); described in Fig 2 : p i is the number of subcomponents inside the i-1 stage; 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; L i is the synchronisation cost of all sub-components of a component of i -1 stage; m i is the amount of memory available at stage i for each component of this stage. Thanks to those parameters, the cost of a MULTI-BSP algorithm can be computed as the sum of the costs of the super-steps of the root node, where the cost of each of these super-steps is the maximal cost of the super-steps of the sub-components (plus communication and synchronisation); And so on.

D. The Multi-ML language.

MULTI-ML [START_REF] Allombert | Functional Abstraction for Programming Multi-Level Architectures: Formalisation and Implementation[END_REF], [START_REF] Allombert | Multi-ML: Programming Multi-BSP Algorithms in ML[END_REF] (https://git.lacl.fr/vallombert/Multi-ML) is based on the idea of executing BSML-like codes on every stage of a MULTI-BSP architecture. This approach facilitates incremental development from BSML codes to MULTI-ML ones. MULTI-ML follows the MULTI-BSP approach where the hierarchical architecture is composed by nodes and leaves. On nodes, it is possible to build parallel vectors, as in BSML. This parallel data structure aims to manage values that are stored on the sub-nodes: at stage i, the code let v= e evaluates the expression e on each i-1 stages. Inside a parallel vector, we note #x# to copy the value x stored at stage i to the memory i -1.

MULTI-ML also introduce the concept of multi-function to recursively go through a MULTI-BSP architecture. A multifunction is a particular recursive function, defined by the keyword let multi, which is composed by two codes: the node and the leaf codes. The recursion is initiated by calling the multi-function (recursively) inside the scope of a parallel vector, that is to say, on the sub-nodes. The evaluation of a multi-function starts (and ends) on the root node. The Fig. 3 shows how a multi-function is defined.

After the definition of the multi-function mf on line 1 where [args] symbolises a set of arguments, we define the node code (from line 2 to 6). The recursive call of the multi-function is done on line 5, within the scope of a parallel vector. The node code ends with a value v, which is available as a result of the recursive call from the upper node. The leaf code, from lines 7 to 9 consists of sequential computations. As expected, the synchronous communication primitives of BSML are also available to communicate values from/to parallel vectors. We also propose another parallel data structure called tree. A tree is a distributed structure where a value is stored in every nodes and leaves memories. A tree can be built using a multi-tree-function, with the let multi tree keyword and can be handled by several primitives of the language.

::= Values | op Operator | cst Constant | (fun x → e )[E] Closure | (rec f x → e )[E] Recursive closure | (multi f x → e † e)[E] Multi-function closure | (v, v) Pair | < v, . . . , v

III. A CORE LANGUAGE

To ease the understanding and avoid to be overwhelmed by the details of a complete language, we choose to select a subset of MULTI-ML to form a core-language called µMULTI-ML. It relies on a minimal set of ML constructions and a set MULTI-ML primitives. This set is sufficient enough to express all the parallel behaviour that are used in MULTI-ML. Thus, features such as records, modules, pattern matching, sum types are excluded from µMULTI-ML. The grammar of the µMULTI-ML is defined in Figure 4.

In this grammar, x and f range over an infinite set of identifiers. We also find the typical ML-like language constructors such as let for bindings and also fun and rec for, respectively, function and recursive functions. As expected, the application is denoted (e e). For the sake of readability, we take the liberty to use the familiar infix notation for binary and ternary operators, as well as the usual precedence and associativity rules. When the context is clear, we can avoid the usage of parentheses. The multi-function definition is written with the keyword multi. It takes one arguments and two expressions separated by the † symbol; the first one is used to control the parallelism on the node and the second is for leaf code. Then, we have the parallel primitive mkpar which aims to build parallel vectors; followed by the synchronous parallel primitives used for communications: proj and put.

The distinction made between the syntactic sugar (the , # and $ notations), used when programming MULTI-ML algorithms, and the core parallel primitives (replicate, down and apply), available in the semantics only, simplifies the semantics. Indeed, the syntactic sugar eases the way of programming but it is not suitable for the semantics as it introduces implicit assumptions. Thus, we must transform and abstract the syntactic sugar using the core parallel primitives. The transformation applied to switch from the syntactic sugar to the core parallel primitives is straightforward and produce and equivalent expression. The parallel vector scope, denoted << e >>, is transformed using the replicate core primitive. Thus, << e >> is simply transformed into replicate (fun _ → e ). The $ syntax is transformed using the apply primitive. Like in BSML, the transformation is simple and does not require a complicated expression analysis. To do so, we build a vector of functions that takes, as argument, the dollar's annotated value. Using the apply primitive, we can apply this vector of functions on the vector of values. For example, the expression << e $x$ >> is transformed into apply (replicate (fun _ x → e x )) x. The # syntax stands for a communication of a value to the sub-nodes. The primitive down is used to perform such a transfer. As the down primitive aims to distribute a value to all the sub-nodes, the transformation is obvious. For example, the expression << e #x# >> is transformed into apply (replicate (fun _ x → e x ))(down x). As the sharp annotated value is given as argument of the vector of functions, there are no redundant copies. The expression << #x# + #x# >> is transformed into a code that copy x to the sub-nodes, only once.

Then, the evaluation of an expression leads to a value v. Variables stands for the standard operators, such as common computations on integers or the fst and snd projections, and also constants (which might refer to integer values, booleans, characters, strings, etc.), functional, recursive and multi-function closures (that is to say a value which stores both a function and its environment), pairs and also parallel vectors.

An environment E is interpreted as a partial mapping (informally called "finite mapping") with finite domain from identifiers to values. The extension of E by v in x, written E ⊕ {x → v}.

A. The multi-level execution model

As MULTI-ML deals with MULTI-BSP architectures, we can distinguish several levels of execution. An expression is thus evaluated at a specific stage of the MULTI-BSP architecture, depending on the level of parallelism expressed. Those levels are useful to identify where the computations take place, but also where a data is stored. Furthermore, the notion of locality is embedded in the MULTI-ML type system to guarantee safe communications through the MULTI-BSP levels (the MULTI-ML type system is not discussed in this article). The memory localities (see Fig. 5) of MULTI-ML are the following: m: The multi, or global, memory of the multi-level architecture. At this level, all the nodes and leaves of the MULTI-BSP architecture are concerned by any execution. A value defined at level m is accessible "anywhere" on the machine. b: The BSP memory of a node. At this level, a BSML code can be executed in order to manage communications and parallel computations. It is possible to point toward the underlying memory via the parallel vectors. A value defined at level b is only accessible in the concerned node and can be communicated with the respect of certain limitations. l: The local memory of a sub-node (inside a parallel vector). This is the underlying memory that can be managed inside a parallel vector from the upper node . This memory can contain pointers to the upper memory via the # syntax. Expressions of this level cannot be communicated because they are specific to a node and may have no sense anywhere else. c: Like l, this memory is managed inside vectors but it is free of references to the upper level. It is possible to transfer such communicable values through the MULTI-BSP levels. s: The sequential memory of a leaf. It can contain specific values such as non-deterministic expressions. At this level, there is only sequential (ML) code and the execution takes place in the lower level of the memory. A value defined at level s can be communicated under certain constraints.

IV. BIG-STEP SEMANTICS

In this section we give the big-step semantics (also called natural semantics) to describe the evaluation of an expression to its final value using inductive rules. Here, we consider both a terminating semantics for terms where rules leads to a finite derivation tree; and diverging rules (leading to infinite evaluation). In the context of ML programming, we only consider an eager (or call-by-value) evaluation strategy.

We choose to describe a subset of the MULTI-ML semantics rules for conciseness reasons; all the rules can be found in [START_REF] Allombert | Functional Abstraction for Programming Multi-Level Architectures: Formalisation and Implementation[END_REF].

A. Syntax definition

We denote the inference rules as following:

P M e ⇓ L p v and P M e ⇓ L p ∞
On the left-hand side, we have the inductive inference rule (leading to a finite derivation tree). It can be read: under the premises (or antecedents) P, the inference rule concludes that, on the component p of locality L, within a multi-environment M, the expression e is evaluated into a value v. On the righthand side, the co-inductive inference rule is written similarly, but using a double-bar. It stands for a case where e diverges: ∞. Otherwise, it is an error: no applicable rules are defined.

The environment of evaluation is denoted by M and is called a multi-environment. It is composed by two elements:

(1) a MULTI-BSP environment and (2) a tree of environments. The first element represents the MULTI-BSP global memory. This memory contains values that are accessible by any processes. Thus every execution taking place outside the scope of a multi-function is global; otherwise, it is executed on nodes or leaves. Depending on the implementation and the architecture, it can be simulated by a virtual unified memory (each processor have a local copy) or by a physical global memory, for example, when simulating an execution in the toplevel. In practice, the memory is replicated on each component of the MULTI-BSP architecture. But for the semantics, we choose to create a single environment that is used during MULTI-BSP evaluations. An evaluation taking place at the MULTI-BSP level, denoted by multi, is then evaluated within the environment ||M||@multi. The notation ||M|| denotes the extraction of an environment from the memory M and the @ refers to the targeted memory. As expected, every unit of the architecture can access this MULTI-BSP environment. It is possible to lookup in it at any time, from any level p, that is to say, from each component of the MULTI-BSP architecture. Nevertheless, the modifications of this environment are possible at the MULTI-BSP level only.

The second element represents all the environments of the architecture. It takes the shape of a tree which maps all the environments of the different levels of the architecture, that is to say all the nodes and leaves. To refer to the environment of a particular component p of this tree is denoted ||M||@p. The components are identified using a regular tree numbering where 0 stands for the root node, and 0.0 to 0.n identify its n sub-components. Thus, it contains its own environment only, deprived of the MULTI-BSP memory. As the MULTI-BSP memory is always available, the notation ||M|| p stands for the environment composed by ||M||@multi∪||M||@p, where the subscript p stands for the targeted memory.

Comm((fun x → e )[E]) = Comm_expr E (e) Comm((rec f x → e )[E]) = Comm_expr E (e) Comm_expr E (x) = , if x / ∈ E Comm(v), if {x → v} ∈ E
Fig. 6. The communication predicates. Now, we introduce the symbol of rule evaluation. The piece of notation ⇓ L p denotes an evaluation taking place at a specific level L, also parametrised by the position p. The evaluation level L can take the values m, b, l or s, to specify on which level the evaluation must occur. m is used when evaluation level is MULTI-BSP; b when it a BSP evaluation; l when the evaluation takes place within the scope of a parallel vector; and s for sequential evaluations.

In the semantics, we do not make any distinctions between l and c. It is not useful, as we propose a predicate to check if a value is communicable: Comm(v) (in Fig. 6), for rules performing communications. By abuse of the notation, this predicate is if the value v is communicable, ⊥ otherwise.

When communicating closures, we check if the expression e contained in the closure is communicable within the enclosed environment. To do so, we use the Comm_expr predicate which is pretty straightforward: given an environment E, on mkpar, proj, put, apply, down, replicate and multi-functions it is ⊥; otherwise it calls, recursively, the predicate on sub-expression.

The subtlety of this notation comes with the communicability of x. We assume that, if x / ∈ E, then the value x is communicable. Indeed, if x does not belong to E, it means that x is a free variable which comes from the application of a closure, as the environment used for a closure is ε, which is the environment of the closed term. Thus, during the evaluation of an application (e 1 e 2 ), we assume that x is communicable in e 1 as its communicability will be checked with e 2 . As expected, the communication of cst and op is and on multi-function closures it is ⊥.

The position p stands for the identifier of the component where an evaluation takes place. We use the notation p.i to refer to the ith sub-unit of a component that is accessible through a parallel vector. The identifier alias root stands for the root node and, as explained previously, multi is used when the whole architecture is concerned by an evaluation.

B. Terminating evaluation rules

As the MULTI-ML language proposes different levels associated with different behaviours, we propose several rules that are either generic or specific to m, b, l.

1) Generic rules: The generic rules that can be evaluated regardless to the evaluation level can be found in Fig. 7.

The VALUES and OP_EVAL rules a straightforward. The VAR rule introduces the predicate lookup(x, M, p, L) (defined in Fig. 8). As the VAR rule gives the value corresponding to a binding, we must lookup for it in a particular way. The value x must be seek, first, in ||M||@p, which is the memory of the evaluation at level p. Then,

VALUES M cst ⇓ L p cst VAR {x → v} ∈ lookup(x, M, p, L) M x ⇓ L p v CLS E = select(M, F (fun x → v ), p, L) v ≡ (fun x → e )[E] M fun x → e ⇓ L p v APP M e 1 ⇓ L p (fun x → e )[E] M e 2 ⇓ L p v M ⊕p E ⊕p {x → v} e ⇓ L p v M (e 1 e 2 ) ⇓ L p v LET_IN M e 1 ⇓ L p v 1 M ⊕p {x → v 1 } e 2 ⇓ L p v 2 M let x = e 1 in e 2 ⇓ L p v 2 Fig. 7. Generic evaluation rules. lookup(x, M, p, L) = if {x → v} ∈ ||M||@p then v Value at p if {x → v} ∈ ||M||@multi then if L ≡ l then ⊥ Out of reach else v
Value at multi else ⊥ Unbound value if the value is not found there, we must look for it in the MULTI-BSP environment: ||M|| multi . If the value is not found anyway, the identifier is unbound in the current expression, which is an impossible (or ⊥) evaluation ("unbound value").

As expected, if the evaluation takes place at the MULTI-BSP level (multi), the variable x is only searched for in the environment ||M|| multi . Furthermore, we add the locality of the evaluation as an input of the lookup predicate to ensure that the values defined in the m memory will not be accessed within the scope of a parallel vector (of locality l).

The CLS (or CLOSURE) rule is used to enclose all the needed variables that are available in M. To do so, we use the predicate select(M, V, p, L) (Fig. 9) to select all the variables of the set of variables V from the multi-environment M. As the predicate uses lookup, we must provide the current level p and its locality L. The set of variables V is determined using F(e), which stands for the set of free variables of the expression. The set of free variables F(e) is defined as usual, and available in Fig. 10.

The APP rule is used to evaluate functional constructions on values. The rule introduces the notation ⊕ p , which is a

select(M, V, p, L) = let E = ∅ ∀α ∈ V, lookup(α, M, p, L) ⊕ E
where V ≡ α0, . . . , αn return E Fig. 9. The select predicate.

F(e) ::= 11. BSP evaluation rules. concatenation operator allowing to enrich the environment of p with bindings. Here, we add the closure environment E and the binding {x → v} to ||M|| p to the environment of p.

F(op) = ∅ F(cst) = ∅ F(x) = x F(fun x → e ) = F(e)\{x} F(rec f x → e ) = F(e)\{x} F(multi f x → e1 † e2) = F(e1) ∪ F (e2)\{x} F(let x = e1 in e2) = F(e1) ∪ F (e2)\{x} F(e1 e2) = F(e1) ∪ F (e2) F((e1, e2)) = F(e1) ∪ F (e2)
REPLICATE ∀i ∈ p M ⊕p i {f → (fun _ → e [ ])} f () ⇓ l p i v i Comm((fun _ → e [ ])) M replicate (fun _ → e ) ⇓ b p < v 0 , . . . , vn > DOWN M x ⇓ b p v Comm(v) M down x ⇓ b p < v > MKPAR M e ⇓ b p (e )[E ] ∀i ∈ p M ⊕p E e i ⇓ b p v i Comm(v i ) M mkpar e ⇓ b p < v 0 , . . . , vn > APPLY M e 1 ⇓ b p < (e i )[E i ] > M e 2 ⇓ b p < v 0 , . . . , vn > ∀i ∈ p M ⊕ p.i {f i → (e i )[E i ], x i → v i } f i x i ⇓ l p.i v i M apply e 1 e 2 ⇓ b p < v 0 , . . . , v n > PROJ M e ⇓ b p < v 0 , . . . , vn > ∀i ∈ p M ⊕ p.i {f → (e )[E ]} f i ⇓ b p.i v i Comm(v i ) M proj e ⇓ b p (e )[E ] PUT M e ⇓ b p < (e 0 )[E 0 ], . . . , (en)[En] > ∀i, j ∈ p M ⊕ p.i {f i → (e i )[E i ]} f i j ⇓ l p.i v ij M ⊕ p.j {f j → (e j )[E j ]} f j i ⇓ l p.j v ij M put e ⇓ b p < (e 0 )[E 0 ], . . . , (e n )[E n ] > f Fig.
The LET_IN rule is necessary to bind values within a context. The rule is straightforward as it only adds {x → v 1 } to the environment of p.

2) BSP rules: In Fig. 11 we describe the BSP rules that can be executed at level b (that is to say on nodes).

The REPLICATE rule is used to create parallel vectors. This primitive is introduced by the code transformation and is not available in the syntax of the MULTI-ML language. The REPLI-CATE primitive requires, syntactically, a function definition as an argument. This function takes any argument, denoted with _ (similarly to the OCAML syntax), which is unbound in the enclosed term. Such function definition allows to delay the evaluation of the expression e when REPLICATE is evaluated.

As the expression e is generated (by the transformation from syntactic sugar to core primitives), there are no free variables in e. Indeed, a variable appears within the scope of a parallel vector, it was necessarily annotated by # or $, and thus bound by the apply primitive. Otherwise, the expression is illformed. This is necessary for the MULTI-ML runtime system. The notation ∀i ∈ p allows to reference the i sub-components of the current node p, from 0 to n. Thus, the closure is added to the environment of each leaf of the current node, identified by p i , if the term is communicable. Then, the function is evaluated on the unit value (), on each sub-components. As the evaluation takes place within the scope of a parallel vector, its evaluation locality is l. The resulting value is, as expected, a parallel vector which contains the results of the evaluation of e on each sub-component.

The DOWN rule is used to distribute data to the sub-nodes. From a variable x, it builds a parallel vector containing the corresponding value v, if v is communicable. The distributed values are identical on the sub-nodes, thus the resulting parallel vector is < v >.

MKPAR also aims to build a parallel vector. Nevertheless, the evaluation of the ith elements of the resulting vector takes place at level p, sequentially. This evaluation is done within a single environment that is common to every evaluation. Thus, one evaluation could impact the environment of another one with a code using side effects, even if there is no way of doing any side effects in the current semantics. It is important to note that the big-step semantics does not allow to describe precisely the evaluation order of the i evaluations. We arbitrarily choose to do it in accordance to the ascending order: from 0 to n. Thus, the expression e is applied on i, which corresponds to the processor identifier (pid) of the i st component. It is important to check that every value v i is communicable. Indeed, we need to communicate the values v 0 , .., v n to the sub-nodes of the level p and we must check the validity of such a transfer.

As expected, the APPLY rule applies a parallel vector of functions (e i ) on a parallel vector of data (v i ) and returns a parallel vector of values. Here, we compute, in parallel, the evaluations of f i v i within the environment of each sub-component i.

The PROJ rule must be applied on a parallel vector available at the current level p. The resulting value is a closure which contains the content of the given vector. As expected, the values are accessible via their original identifiers. It is also necessary to check whether or not the values of the given vector are communicable in order to build a communicable closure.

The PUT rule works as expected. It takes a parallel vector of communication functions, referenced as f i within environment p i . Then, the received values are accessible via f j . Here, both i and j stand for the sub-components of the current node p. They are denoted as distinct variables to show the all-to-all exchange.

3) Local rules: Rules that can be executed within the scope of a parallel vector (of locality l) can be found in Fig. 13.

The MULTI_NODE and MULTI_LEAF rules are relative to the recursive multi-function calls, which corresponds to the

isN ode(p) M e 1 ⇓ l p (multi f x → e 1 † e 2 )[M ] M e 2 ⇓ l p v M ⊕p {x → v}⊕p {f → (multi f x → e 1 † e 2 )[M ]} e 1 ⇓ b p v M (e 1 e 2 ) ⇓ l p v MULTI_LEAF isLeaf (p) M e 1 ⇓ l p (multi f x → e 1 † e 2 )[M ] M e 2 ⇓ l p v M ⊕p {x → v} e 2 ⇓ s p v M (e 1 e 2 ) ⇓ l p v Fig. 12. Local evaluation rules. MULTI_DEF M = select(||M|| multi , F (multi f x → e 1 † e 2 )) v ≡ (multi f x → e 1 † e 2 )[M ] M (multi f x → e 1 † e 2 ) ⇓ m multi v MULTI_CALL M e 1 ⇓ m multi (multi f x → e 1 † e 2 )[M ] M e 2 ⇓ m multi v M ⊕root {x → v}⊕root {f → (multi f x → e 1 † e 2 )[M ]} e 1 ⇓ b root v Comm(v )
M (e 1 e 2 ) ⇓ m multi v Fig. 13. MULTI-BSP evaluation rules. application of multi-function function on a value within the scope of a parallel vector. MULTI_NODE and MULTI_LEAF are applied regarding to the type of the current component. The operators isN ode(p) and isLeaf (p) are used to make such a distinction. Informally speaking, isN ode(p) is impossible (returns ⊥) if p has no sub-components. On the contrary, isLeaf (p) is impossible (⊥) if p has sub-components. Concerning the MULTI_NODE rule, the environment of evaluation of e 1 (standing for the node code) is enriched by the argument given to the multi-function and the closure of the multifunction. Indeed, the sub-node must be able to recall the multifunction. We can observe that, after enriching the environment, the evaluation of e 1 goes from l to b (from a vector to a (sub-)node). This locality change is due to the fact that, a recursive of a multi-function (done within the scope of a parallel vector) is evaluated, we must initiate the recursion on the sub-nodes: which corresponds to evaluate e 1 at level b. A level change occurs during the evaluation of this rules. On the contrary, the MULTI_LEAF rule is not concerned by this environment enrichment because of its status of leaf. A similar change of level can be observed in the MULTI_LEAF rule, when we go from l to s (from a vector to a (sub-)leaf).

4) Multi-BSP rules: Finally, the rule used to call a multifunction is defined in Fig. 13.

The MULTI_DEF rule aims to create the closure of a multi-function and make it available in the MULTI-BSP environment. To do so, we simply call the predicates select(||M|| multi , F(multi f x → e 1 † e 2 )) in order to built the environment M from the MULTI-BSP environment and the free variables of the multi-function itself.

The MULTI_CALL rule is used to initiate the multi-function

MKPAR-E M e ⇓ b p ∞ M mkpar e ⇓ b p ∞ MKPAR-V M e ⇓ b p (e )[E ] ∃i ∈ p M ⊕p E e i ⇓ b p ∞
M mkpar e ⇓ b p ∞ Fig. 14. mkpar coinductive evaluation rule.

evaluation. As expected, the multi-function evaluation starts on the root node, with an environment enriched by the given argument and the multi-function closure. Thus, the evaluation of e 1 , corresponding to the node code, is evaluated at level b, on the root node. As the resulting value of the evaluation of the multi-function is going to be transferred to the MULTI-BSP level, we also need to check if v is communicable. Indeed, the final value must be available in the ||M multi || environment.

To do so, in case of a distributed MULTI-BSP memory, we must broadcast v from the root node to all the components of the MULTI-BSP architecture. Thus, we must check that v is communicable.

C. Diverging evaluation rules

Using the co-inductive approach described in [START_REF] Leroy | Coinductive big-step operational semantics[END_REF], we propose a set of rules which describe the diverging rules. The diverging rules are pretty straightforward as they describe the fact that each evaluation of an expression of a rule can lead to infinite evaluation. For conciseness reasons, we only describe (in Fig. 14) the mkpar rule (all the diverging rules can be found in [START_REF] Allombert | Functional Abstraction for Programming Multi-Level Architectures: Formalisation and Implementation[END_REF]). The MKPAR-E rules describes the divergence of the evaluation of e; whereas MKPAR-V describes the divergence of e , which is the expression enclosed in the closure given by the evaluation of e. In both cases, the evaluation of the whole rule diverges.

V. SEMANTICS PROPERTIES

In this section, we give the properties of the semantics rules. We prove that the evaluation of an expression following the proposed rules is deterministic. The lemmas 1 and 2 ensure that, if a value v is obtained from the execution of e and then, the evaluation is deterministic. The lemma 3 ensures that an evaluation produces a value or diverges (evaluation and divergence exclusivity), that is to say, and evaluation "does not go wrong".

Lemma 1 (Evaluation is deterministic). Let e be a program, let M be an environment, L an evaluation locality, p a position and v 1 and v 2 be values.

If M e ⇓ L p v 1 and M e ⇓ L p v 2 then v 1 = v 2 .
Proof. See [START_REF] Allombert | Functional Abstraction for Programming Multi-Level Architectures: Formalisation and Implementation[END_REF] Lemma 2 (Evaluation or not). Let e be a MULTI-ML expression, M be an evaluation environment, L an evaluation locality and p a position. Then:

• It is impossible to obtain a value v such that M e ⇓ L p v • or there exists a value v such that M e ⇓ L p v

Proof. (Using classical logic). The excluded middle holds over M e ⇓ L p v. Lemma 3 (Evaluation does not go wrong). Let e be a MULTI-ML program, let M be an environment, L an evaluation locality, p a position and v a value. If M e ⇓ L p v and M e ⇓ L p ∞ then there is a contradiction. Proof. See [START_REF] Allombert | Functional Abstraction for Programming Multi-Level Architectures: Formalisation and Implementation[END_REF] Note that those lemmas does not prove that any program can be evaluated. For example, the program 0 0 (zero applied on zero) goes wrong since, for any environment E and value v, neither E (0 0) ⇓ v nor E (0 0) ⇓ ∞ holds. To do that, we must provide a typing system which allow to identify such programs.

VI. RELATED WORK

A. Hierarchical programming and Multi-BSP libraries

There are many papers about the gains of mixing shared and distributed memories -e.g. MPI and OPEN-MP [START_REF] Cappello | MPI Versus MPI+OpenMP on IBM SP for the NAS Benchmarks[END_REF]. As intended, the programmer must manage the distribution of the data for these two different models. For example, the work of [START_REF] Hamidouche | A Framework for an Automatic Hybrid MPI+OpenMP Code Generation[END_REF] in which a BSP extension of C++ runs the same code on both a cluster and on multi-cores. But it is the responsibility of the programmer to avoid harmful nested parallelism. This is thus not a dedicated language working for hierarchical architectures. We can also highlight the work of NESTSTEP [START_REF] Kessler | NestStep: Nested Parallelism and Virtual Shared Memory for the BSP Model[END_REF] which is a C/JAVA library for BSP computing, which authorises nested computations in case of a cluster of multi-cores -but without any safety.

B. Distributed functional languages.

Except in [START_REF] Loidl | Comparing Parallel Functional Languages: Programming and Performance[END_REF], there is a lack of comparisons between parallel functional languages. It is difficult to compare them since many parameters have to be taken into account: efficiency, scalability, expressiveness, etc. A data-parallel extension of HASKELL called NEPAL has been done in [START_REF] Chakravarty | Nepal -Nested Data Parallelism in Haskell[END_REF], an abstract machine is responsible for the distribution of the data over the available processors. MULTIMLTON [START_REF] Sivaramakrishnan | MultiMLton: A multicore-aware runtime for standard ML[END_REF] is a multi-core aware runtime for standard ML, which is an extension of the MLTON compiler. It manages composable and asynchronous events using, in particular, safe-futures. A description of other bridging models for hierarchical architectures and other parallel languages can be found in [START_REF] Allombert | Functional Abstraction for Programming Multi-Level Architectures: Formalisation and Implementation[END_REF].

Currently, we are not aware of any safe and efficient functional parallel language dedicated to hierarchical architectures.

VII. CONCLUSION

In this paper we have presented the formal semantics of the MULTI-ML language, a parallel functional language dedicated to hierarchical architectures, relying of the MULTI-BSP bridging model. The semantics describes the behaviour of the MULTI-ML language regarding the multiple level of execution of hierarchical architectures. Furthermore, we propose a memory model that ensures consistency with respect to the MULTI-BSP programming model. Using both a terminating semantics leading to a finite derivation tree and a diverging semantics leading to infinite evaluations, we have described how a MULTI-ML expression "goes". Moreover, in accordance to the presented lemmas, we ensure that the evaluation of a valid MULTI-ML expression "does not go wrong".

Fig. 1 .

 1 Fig. 1. A BSP super-step

Fig. 3 .

 3 Fig. 3. A Multi-ML code.

  | let x = e in e Let binding | fun x → e Function | rec f x → e Recursive function | multi f x → e † e Multi-function | (e e) Application | if e then e else e Conditional | (e, e) Pairing | mkpar e Parallel primitives | proj e | put e Synchro. parallel primitives | replicate (fun _ → e ) Core parallel primitives | down x | apply e e Core parallel primitives v

Fig. 4 .

 4 Fig. 4. The µMULTI-ML grammar.

Fig. 5 .

 5 Fig. 5. The Multi-ML localities

Fig. 8 .

 8 Fig. 8. The lookup predicate.

Fig. 10 .

 10 Fig. 10. The free variable predicate.


Jérôme (presenter), LEMIERE, Bruno, BELLENFANT, Gaël Jacob

Geology, Genetic Processes And Their Consequences On Environmental Impacts At The Abandoned W Mine Of Enguialès

Introduction

We investigate here arsenic issues at the Enguialès abandoned tungsten mine, their relationships with the ore genesis model, and the consequences of the hydrogeochemical reactions on the environmental impact of the site, and on the longterm site management plan.

Geological setting and mining history

The former Enguialès mine belonged to the Leucamp -Enguiales regional tungsten district (Cantal -Aveyron region, French Massif Central), hosted in the pre-Hercynian micaschists sequence of "la Chataigneraie". This sequence was intruded during Silesian times [START_REF] Monié | -40Ar/39Ar Laser-Probe Dating of W, Au and/or Sb Deposits and associated granites in the Southern French Massif Central (Cévennes, Châtaigneraie)[END_REF] by several types of granites and microgranites. The Entraygues porphyritic monzogranite batholith occurs nearby the mine and probably under it. It has a distinctive contact metamorphism aureole of hornfels ans spotted micaschists, with abundant cordierite, poekilitic andalusite, biotite, tourmaline and rare sillimanite. It was intruded by a muscovite leucogranite and by microgranitic veins (Figure 1). The mineralisation is hosted in a cross-patterned quartz vein stockwork covering 1,3 km x 0,3 km. The miners designated the veins with "male" names when they occurred along the regional schistosity (NW-SE strike, NE dip, thickness 1 to 50 cm) and "female" names when they crossed the schistosity (NE-SW strike, W dip, thickness 5 to 80 cm) (Figure 2). The recognised extension was 300 m long, with 200 m downwards dip.

The mine is located between 400 and 700 m elevation at the surface, across a steep slope above the Lot river valley.

The ore-bearing veins paragenesis comprises quartz, wolframite, scheelite, fluorapatite, while the hydrothermal alteration selvages paragenesis comprises tourmaline (schorl), sericite ans sulphides in a quartz greisen. Sulphides come as a first phase (pyrite, arsenopyrite) and a second phase (chalcopyrite, molybdenite, bismuthinite, marcasite), followed by a late carbonate phase. Secondary minerals developed through weathering include oxyhydroxides, hydrated sulphates, and arseniates, the most conspicuous being scorodite.

The vein-type, perigranitic nature, and the structural control result in a high arsenopyrite contents in the veins and their host rocks. Late Variscan leucogranitic magmatism and fluid circulation is believed to be the origin of mineralisation [START_REF] Lerouge | Fluids and the W(±As,Au) ore deposits of the Enguialès-Leucamp District, La Châtaigneraie, French Massif Central[END_REF]Goer de Herve et al., 2006).

The deposit was discovered in 1957 by SMMC (Société Minière et Métallurgique du Chatelet) and mined from 1969 to 1978. Irregular distribution, recovery and productivity issues, and W price collapse (1971) led to mine closure in 1979. A total 450,000 t of ore averaging 0,6% WO 3 was mined, yielding 1 300 t of 70% WO 3 concentrates. A final attempt by the BRGM-S.M. d'Anglade-Petrofina-Charter consortium to locate extensions was not successful and the site was abandoned in 1983.

Ore beneficiation, according to the 1978 flow sheet, comprised crushing and staged milling (size fractions 5mm, 2mm and 0,8mm), pulp preparation, classification, and gravity sorting using jig concentrators or shaking tables. A last concentration step was added during the mine lifetime with froth flotation, using mainly gas oil, and then probably specific reagents such as xanthates, though this is not documented.

Processing residues comprised therefore +2-5mm gravel, +0,8-2mm dried sand, <0,8mm thickened sand, and sulphidic decantation sludge. Waste rock was used to build tracks and platforms. Process waste was dumped down the topographic slope out of the galeries.

Waste rock is not observable as large heaps. Due to the selective underground extraction method, and to the steep hillside topography, most of it was discharged near the adits and galleries. Most seems to have been used as engineering material to build platforms and access tracks along the slopes. Some may have been disposed by gravity but is now covered by vegetation.

Environmental impacts (GB, BL, PhB, FC)

The Enguialès mine site is currently managed as abandoned with no responsible party. The first environmental studies were led in connection with EU mining waste inventories [START_REF] Cottard | Audits environnementaux de six mines fermées ou abandonnées de la région Midi-Pyrénées[END_REF]. The widespread occurence of As-bearing phases in waste dumps was recognised by [START_REF] Courtin-Nomade | Arsenic in iron cements developed within tailings of a former metalliferous mine-Enguialès, Aveyron, France[END_REF] and confirmed by subsequent studies (unpublished data, 2017). The structural control still applies to site hydrogeology and the faulted network channelises the As-rich fluids. Pyrite oxidation provided extensive Fe hydroxide coatings. Mining and beneficiation methods determined waste and residues typology. The underground mine opens on a steep topographic slope, on which waste rock and tailings were disposed. A first generation of gravity sorting on coarse mill feed gave moderately reactive quartz tailings, while later finer mill feeds and floatation techniques gave highly reactive and mobile tailings, with much higher As contents. Fast erosion of the latter, accelerated by the steep topography and the intensity of the rainy episodes, contributes to a high As load of surface water in particulate form. Acidic mine runoff is discharged nearby, favoring As and metals solubility, in the absence of any neutralising host rocks. traps. Fe hydroxide fracture coatings behave as natural arsenic retardants through sorption phenomena. This reduces groundwater As migration.

Methods

Geological, depth, air photo and topographic observations on waste

On-site geochemical analyses of waste were performed using portable X-ray fluorescence (pXRF) spectrometers (Niton XLt, XL3t, Olympus Delta 50). Both soil (Compton) and mining/geochem (fundamental parameters) modes were used in order to cover a large range of elements (As, Ba, Ca, Cr, Fe, K, Mn, Ni, Pb, Rb, S, Sn, Sr, Ti, V, W, Zn, Zr). Counting times in the 60-120 s range, and emission voltage in the 15-50kV were used. Relative accuracy was ensured by QA/QC blanks, duplicates and periodic CRMs measurement. Absolute accuracy was evaluated using laboratory analyses, performed by ICP/AES and ICP/MS after acid digestion of alkali sintered samples. Results were also compared with analyses after aqua regia digestion.

Water analyses were performed on site for physicochemical parametres (pH, ORP, EC) and by laboratory methods (ICP/AES, ion chromatography) for the main cations, anions and trace elements Water monitoring on site was performed for 49 days in the (TB 465) runoff using an YSI 6920 multiparametric recording probe intended for environmental monitoring in waters with little or moderate mineralization (conductivity < 4mS/cm). The probe was calibrated offsite using standard solutions and checked onsite with an YSI control solution. The probe was set up to record hourly the following water parameters: pH, temperature, electrical conductivity (and by conversion, estimated salinity and TDS), Eh (redox potential), turbidity and dissolved oxygen. The latter two parameters are measured optically.

The probe was placed in a pipe retained by a dam of stones between the mine drainage spring and a small pond (see Erreur ! Source du renvoi introuvable.). At the end of the monitoring period, the sensors were checked in the laboratory to evaluate their response to clogging by iron precipitate. It was necessary to lightly wipe sensors to carry out the verification (Figure 6), because during a first measurement without cleaning, the precipitates present on the surface of the sensors polluted the standard solutions. The results of this verification are presented in Table 1. The various sensors have a relatively low drift given the important deposits on their surfaces, with the exception of the dissolved oxygen sensor for low concentrations. It can be concluded that if the absolute values provided by the probe require a critical reading, their relative values are representative of the events affecting mine drainage.

In order to compare the variations of the mine drainage physico-chemical parameters with precipitation, rainfall data recorded by the Vieillevie weather station, located 9 km southeast of Enguialès, were used.

Results and discussion

Detailed site investigations by [START_REF] Cottard | Audits environnementaux de six mines fermées ou abandonnées de la région Midi-Pyrénées[END_REF], [START_REF] Courtin-Nomade | Arsenic in iron cements developed within tailings of a former metalliferous mine-Enguialès, Aveyron, France[END_REF] and Baranger (2008) showed that the main environmental impact of the former mine was the emission of arsenic towards surface water, resulting from acid drainage out of the mine galleries and from the meteoric leaching of the waste dumps.

In order to understand better the origin of acid drainage, the mine runoff was continuously monitored. The mine drainage reaction to short but intense rainfall events was studied. These results were cross-referenced with data on the geology and the multiphase genesis of the mineralisation, as well as with the mining and beneficiation methods and their consequences on residues typology. An inventory of the extent of the contamination of the site and the transport modes of the contaminants (both in solute and particulate form) were carried out, taking into account the topography and the weather conditions. A risk classification of residues was made possible by detailed pXRF mapping.

Solid waste

The process waste deposits were mapped and analysed using pXRF in order to delineate source areas and to establish a preliminary ranking of their hazardousness. This was based on total As only, as no As speciation data could be collected. However, the deeply oxidised erosion profile (Figure 7) suggests that, even if the As leachable fraction differs significantly from the total As, the ranking of source areas and the remediation options remain the same. Two types of residues were observed and occur as separate masses along the slope.

A grey to rusty, coarse-grained (millimetric) quartz-rich material occurs on the outer sides of the dump (Figure 8). It is believed to be the residue of mechanical gravity sorting processes, used in the early history of the mine. Their composition is roughly similar to the hydrothermally altered micaschists (Table 2, Table 3) but with anomalously high As and W. They are partly covered by vegetation. A fine-grained (<1mm), white to pale yellow material occurs in the central part of the dump, immediately under the former processing plant. It is believed to be the residue of floatation processes with gas-oil ands xanthates, used in the late history of the mine, just before closure. This is supported by the location and by the observation of strong organic odours. A GC/MS scan for organic molecules confirmed the abundance of heavy petroleum hydrocarbons (C10 to C40), did not identify aromatic hydrocarbons but found S-bearing metabolites, probably from the degradation of xanthates.

Their composition is also roughly similar to the hydrothermally altered micaschists (Table 4) but with anomalously high Zn and Cu, and very high As and W. This part of the dump is severely eroded (Figure 7) and the fine grained material is carried away to the river, especially during rainstorms. Almost no vegetation grows on this material. Significant deviations were observed with ICP/AES analyses after aqua regia digestion for Sn, Ti, W, and Zr. For these elements, pXRF results are often more accurate than aqua regia analyses [START_REF] Lemiere | A review of pXRF (field portable X-ray fluorescence) applications for applied geochemistry[END_REF].

Mine water

Most of the mine drainage is observed as runoff at the TB465 outlet. It is then discharged to the nearby Crozafon creek and then to the Lot river, a little more than 2km downstream. The outlet and the creek have been monitored through sampling programs [START_REF] Cottard | Audits environnementaux de six mines fermées ou abandonnées de la région Midi-Pyrénées[END_REF](Cottard et al., , unpublished data, 2017)).

The probe remained in place for 49 days, but the accumulation of iron hydroxide precipitate heavily clogged its sensors. When the probe was recovered, the pipe in which it was placed was completely clogged. Water was no longer flowing through the pipe, but the probe was still in the pond water. Consequently, the recorded values correspond to the physico-chemical parameters of this pond.

Results of conductivity, pH, temperature, dissolved oxygen concentration and rainfall measurements are presented in Figure 9. The ORP sensor seems to have been particularly affected by precipitates, as it hardly recorded any significant variations.

The recorded data are largely unusable and therefore the results of the ORP measurements are not presented. The monitoring period was marked by a continuous heavy rain event from May 28 th to 31th, and an intense but isolated rain event on May 22 nd . The remainder of the monitoring period was generally dry with a few days of low rainfall.

The conductivity shows a sharp increase between May 28 th and June 1 st , followed by a slow decrease until the end of the monitoring period. This increase is due to the leaching and dissolution of oxidized minerals in the levels of the mine above the water table. These minerals, most of which are soluble, were washed or submerged during the heavy rain event while they are usually out of the water. The period of decrease in conductivity observed from April 27 th to May 15 th could correspond to a seasonal variation, or be the result of a prior rain event.

The pH is globally stable until a brutal acidification episode between May 31 and June 2. This increase in acidity is probably due to the leaching of oxidised sulphide minerals in the mine cavities. Usually, some of these minerals are above the water table where they react with air oxygen and with the seepage of oxygenated water.

During the passage of water during an intense rain event, they are therefore already oxidized and they dissolve very quickly, releasing sulphuric acid and dissolved metals (Fe, Pb, Zn, etc.).

The water temperature varied within a very limited range between 13.0 and 13.6°C. Overall, we observe the usual warming of the weather between April and June. Between May 30th and June 2nd, the temperature drops and then rises sharply. This drop in temperature partly covers and follows the main rain event of the study period.

Besides the influx of colder rain water, it could be due to a decrease in the residence time of the water underground and thus a lower warming of water by the geothermal gradient. This is further supported by the time shift between rainfall and temperature change, which would not be observed if the mine aquifer did not play a role.

Dissolved oxygen concentration is generally stable except for sudden increase between May 31 and June 2 followed by a slower decrease until June 6. This increase is probably due to an intensification of the flowrate of the mine drainage spring at the emergence caused by the increase of the water pressure load under the effect of the important water inflows. These variations in dissolved oxygen concentration would therefore indirectly reflect variations in drainage flow. The decrease in dissolved oxygen would represent the progressive emptying of the mine until it returns to its base flow. The fact that the dissolved oxygen concentration drops to a lower level (70%) than its base level before the intense rainy episode may be attributed to sensor sealing by precipitates.

Heavy rains were followed by strong increases in acidity and conductivity, As, sulphate and metal contents. The increase in As and metal contents being concomitant with the increase in flow rate, this means that despite their short duration, these intense rainfall events can represent a significant proportion of the As and metal discharge to the environment throughout the year.

Conclusions

The main impact of the abandoned Enguialès tungsten mine is the release of arsenic towards surface water, through process waste erosion and leaching, and through mine runoff.

For the former, a detailed geochemical mapping of residues allowed to identify finegrained floatation residues as the main source. The steep slopes and the stormy rainfall regime imply that erosion contributes massively to As particular transport, while solute As release by rainfall leaching could not be precisely located. As leaching is probably active but diffuse.

For the latter, water monitoring showed a slowly mitigating As release from the mine runoff but does not allow to investigate in detail the relationships with meteoric events. Continuous monitoring is more efficient for transfer evaluation and modelling than periodic sampling.

Such data, along with pXRF waste mapping, are essential data for a site management plan to minimise long-term environmental impacts.

Figure 1 :

 1 Figure 1: Geological map (from the 1:50000 map, Goer de Herve et al., 2006)

Figure 2 :

 2 Figure 2: Vein network (from the mine 1:1000 plan)

Figure 3 :

 3 Figure 3: Air view of the site (Google Earth)

Figure 4 :

 4 Figure 4: On-site analysis of residues using pXRF

Figure 5 :Figure 6 :

 56 Figure 5 : Mine drainage spring (left) and pipe hosting the multiparametric probe (right)

Figure 7 :

 7 Figure 7: Eroded As-rich floatation residues in gravity dumps

Figure 9 :

 9 Figure 9: Conductivity, pH, temperature, dissolved oxygen concentration and rainfall during water monitoring period

Table 1 : Results of the verification of the sensors of the probe with standard solutions

 1

	Parameter	Unit	Standard solutions	Measured value
				at 21°C
	Conductivity	µS/cm 1332	1420
	pH		4,01	3,6
	ORP	mV	220	220
	ORP	mV	470	500
	Dissolved oxygen	%	100	101
	Dissolved oxygen	%	0	21

Table 2 : statistics of pXRF measurements on host micaschists and derived soil, in mg/kg<

 2

	Mo < LD

Table 3 : statistics of pXRF measurements on coarse residues, in mg/kg

 3

		Zr	Sr U	Rb Pb As	Zn W	Cu Fe	Mn	Cr V	Ti	Ca K	S	Ba Sb Sn
	nb values		20 20	1 20 15		19 18		5 17	20		19 18 14 20 19	20	4 20 15 15
	mini		42 26	118 14		16 32		49 31 29015 221 47 72 660 307 3929 2723 200 25 32
	maxi	182 204 30 803 282 2034 225 488 370 152090 1659 159 126 5855 5355 29311 4076 1633 110 100
	median	120 63 30 292 28		70 88 112 101 49803 594 85 94 2606 678 18761 3377 1026 56 64
	average	124 72	325 47 325 92 178 118 62831 688 86 94 2906 927 17521 3388 969 59 63
		Mo Zr Sr Rb Pb As Zn W		Cu Fe	Mn Cr V Ti	Ca K	S	Ba Sb Sn
	nb values		6 11 11 11 11	11	8	11 10	11 11	9 10 11	11	11	4	11	3	7
	mini		9 52 35 163 34 432 29	91 37 32914 212 36 56 1886 485 12441 1487 167	25 28
	maxi	18 105 77 375 134 3122 50 1898 168 93991 563 94 137 3477 1091 24926 4811 579	35 56
	median	11 81 52 194 47 598 36 366 49 44522 257 55 84 2531 692 17457 2649 401	33 34
	average	12 77 53 222 60 898 38 464 66 47254 300 58 84 2554 769 18195 2899 398

Table 4 : statistics of pXRF measurements on fine-grained residues, in mg/kg Figure 8: As-bearing coarse gravity sorting residues in dumps Mo Zr Sr Rb Pb As

 4

				Zn W	Cu Fe	Mn Cr V	Ti	Ca K	S	Ba Sb Sn
	nb values 14 46 50 52 51	52	30	52 42	52 50 42 40 52 51	52	22 51	8 35
	mini	10 33 18 162 21	214	31 153 37 13473 128 31 59 461 319 1872 1296 180 25 18
	maxi	35 313 86 400 422 212336 1578 9423 6066 776331 1527 112 144 7592 1823 29131 51361 722 73 87
	median	13 104 55 270 57	830	52 1031 91 41606 362 61 87 2559 699 18357 2246 422 36 30
	average	16 107 55 263 81 11700 118 1479 445 86598 420 63 90 2654 762 17725 8784 426 41 33