Matthieu Perrin

Achour Mostefaoui

Claude Jard

Update Consistency for Wait-free Concurrent Objects

Keywords: Abstract Data Types, Consistency Criteria, Eventual Consistency, Replicated Object, Sequential Consistency, Shared Set, Update Consistency

In large scale systems such as the Internet, replicating data is an essential feature in order to provide availability and fault-tolerance. Attiya and Welch proved that using strong consistency criteria such as atomicity is costly as each operation may need an execution time linear with the latency of the communication network. Weaker consistency criteria like causal consistency and PRAM consistency do not ensure convergence. The different replicas are not guaranteed to converge towards a unique state. Eventual consistency guarantees that all replicas eventually converge when the participants stop updating. However, it fails to fully specify the semantics of the operations on shared objects and requires additional non-intuitive and error-prone distributed specification techniques.

This paper introduces and formalizes a new consistency criterion, called update consistency, that requires the state of a replicated object to be consistent with a linearization of all the updates. In other words, whereas atomicity imposes a linearization of all of the operations, this criterion imposes this only on updates. Consequently some read operations may return out-dated values. Update consistency is stronger than eventual consistency, so we can replace eventually consistent objects with update consistent ones in any program. Finally, we prove that update consistency is universal, in the sense that any object can be implemented under this criterion in a distributed system where any number of nodes may crash.

I. INTRODUCTION

Reliability of large scale systems is a big challenge when building massive distributed applications over the Internet. At this scale, data replication is essential to ensure availability and fault-tolerance. In a perfect world, distributed objects should behave as if there is a unique physical shared object that evolves following the atomic operations issued by the participants 1 . This is the aim of strong consistency criteria such as linearizability and sequential consistency. These criteria serialize all the operations so that they look as if they happened sequentially, but they are costly to implement in message-passing systems. If one considers a distributed implementation of a shared register, the worst-case response time must be proportional to the latency of the network either for the reads or for the writes to be sequentially consistent [START_REF] Lipton | PRAM: A scalable shared memory[END_REF] and for all the operations for linearizability [START_REF] Attiya | Sequential consistency versus linearizability[END_REF]. This generalizes to many objects [START_REF] Attiya | Sequential consistency versus linearizability[END_REF]. Moreover, the availability of the shared object cannot be ensured in asynchronous systems where more than a minority of the processes of a system may crash [START_REF] Attiya | Sharing memory robustly in message-passing systems[END_REF]. In large modern distributed systems such as Amazon's cloud, partitions do occur between data centers, as well as inside data centers [START_REF] Vogels | Eventually consistent[END_REF]. Moreover, it is economically unacceptable to sacrifice availability. The only solution is then to provide weaker consistency criteria. Several weak consistency criteria have been considered for modeling shared memory such as PRAM [START_REF] Lipton | PRAM: A scalable shared memory[END_REF] or causality [START_REF] Ahamad | Causal memory: Definitions, implementation, and programming[END_REF]. They expect the local histories observed by each process to be plausible, regardless of the other processes. However, these criteria do not impose that the data eventually converges to a consistent state. Eventual consistency [START_REF] Vogels | Eventually consistent[END_REF] is another weak consistency criterion which requires that when all the processes stop updating then all replicas eventually converge to the same state. This paper follows the long quest of the (a) strongest consistency criterion (there may exist several incomparable criteria) implementable for different types of objects in an asynchronous system where all but one process may crash (wait-free systems [START_REF] Herlihy | Wait-free synchronization[END_REF]). A contribution of this paper consists in proving that weak consistency criteria such as eventual consistency and causal consistency cannot be combined is such systems. This paper chooses to explore the enforcement of eventual consistency. The relevance of eventual consistency has been illustrated many times. It is used in practice in many large scale applications such as Amazon's Dynamo highly available key-value store [START_REF] Decandia | Dynamo: amazon's highly available key-value store[END_REF]. It has been widely studied and many algorithms have been proposed to implement eventually consistent shared object. Conflict-free replicated data types (CRDT) [START_REF] Shapiro | Conflict-free replicated data types[END_REF] give sufficient conditions on the specification of objects so that they can be implemented. More specifically, if all the updates made on the object commute or if the reachable states of the object form a semi-lattice then the object has an eventually consistent implementation [START_REF] Shapiro | Conflict-free replicated data types[END_REF]. Unfortunately, many useful objects are not CRDTs.

The limitations of eventual consistency led to the study of stronger criteria such as strong eventual consistency [START_REF] Shapiro | A comprehensive study of convergent and commutative replicated data types[END_REF]. Indeed, eventual consistency requires the convergence towards a common state without specifying which states are legal. In order to prove the correctness of a program, it is necessary to fully specify which behaviors are accepted for an object. The meaning of an operation often depends on the context in which it is executed. The notion of intention is widely used to specify collaborative editing [START_REF] Sun | Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems[END_REF], [START_REF] Li | A new paradigm of user intention preservation in realtime collaborative editing systems[END_REF]. The intention of an operation not only depends on the operation and the state on which it is done, but also on the intentions of the concurrent operations. In another solution [START_REF] Bieniusa | An optimized conflict-free replicated set[END_REF], it is claimed that, it is sufficient to specify what the concurrent execution of all pairs of non-commutative operations should give (e.g. an error state). This result, acceptable for the shared set, cannot be extended to other more complicated objects. In this case, any partial order of updates can lead to a different result. This approach was formalized in [START_REF] Burckhardt | Replicated data types: specification, verification, optimality[END_REF], where the concurrent specification of an object is defined as a function of partially ordered sets of updates to a consistent state leading to specifications as complicated as the implementations themselves. Moreover, a concurrent specification of an object uses the notion of concurrent events. In message-passing systems, two events are concurrent if they are produced by different processes and each process produced its event before it received the notification message from the other process. In other words, the notion of concurrency depends on the implementation of an object not on its specification. Consequently, the final user may not know if two events are concurrent without explicitly tracking the underlying messages. A specification should be independent of the system on which it is implemented.

Contributions of the paper:

for not restricting this work to a given data structure, this paper first defines a class of data types called UQ-ADT for updatequery abstract data type. This class encompasses all data structures where an operation either modifies the state of the object (update) or returns a function on the current state of the object (query). This class excludes data types such as a stack where the pop operation removes the top of the stack and returns it (update and query at the same time). However, such operations can always be separated into a query and an update (lookup top and delete top in the case of the stack) which is not a problem as, in weak consistency models, it is impossible to ensure atomicity anyway. This paper has three main contributions.

• It proves that in a wait-free asynchronous system, it is not possible to implement eventual and causal consistency for all UQ-ADTs.

• It introduces update consistency, a new consistency criterion stronger than eventual consistency and for which the converging state must be consistent with a linearization of the updates. • Finally, it proves that for any UQ-ADT object with a sequential specification there exists an update consistent implementation by providing a generic construction. The remainder of this paper is organized as follows. Section II formalizes the notion of consistency criteria and the type of objects we target in this paper. Section III recalls the definition of (strong) eventual consistency. Section IV proves that eventual consistency cannot be combined with causal consistency in wait-free systems. Section V introduces (strong) update consistency and compares it with (strong) eventual consistency. Section VI compares, through the example of the set, the expressiveness of strong update consistency and strong eventual consistency. Section VII presents a generic construction for any UQ-ADT object with a sequential specification. Finally, Section VIII concludes the paper.

II. ABSTRACT DATA TYPES AND CONSISTENCY

CRITERIA Before introducing the new consistency criterion, this section formalizes the notion of object and how a consistency criterion is defined. In distributed systems, sharing objects is a way to abstract message-passing communication between processes. The abstract type of these objects has a sequential specification, defined in this paper by a transition system that characterizes the sequential histories allowed for this object. However, shared objects are implemented in a distributed system using replication and the events of the distributed history generated by the execution of a distributed program is a partial order [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]. The consistency criterion makes the link between the sequential specification of an object and a distributed execution that invokes it. This is done by characterizing the partially ordered histories of the distributed program that are acceptable. The formalization used in this paper is explained with more details in [START_REF] Perrin | Consistent shared data types: Beyond memory[END_REF].

An abstract data type is specified using a transition system very close to Mealy machines [START_REF] Mealy | A method for synthesizing sequential circuits[END_REF] except that infinite transition systems are allowed as many objects have an unbounded specification. As stated in the Introduction, this paper focuses on "update-query" objects. On the one hand, the updates have a sideeffect that usually affects the state of the object (hence all processes), but return no value. They correspond to transitions between abstract states in the transition system. On the other hand, the queries are read-only operations. They produce an output that depends on the state of the object. Consequently, the input alphabet of the transition system is separated into two classes of operations (updates and queries).

Definition 1 (Update-query abstract data type). An update-query abstract data type (UQ-ADT) is a tuple O = (U, Q i , Q o , S, s 0 , T, G) such that:

• U is a countable set of update operations;

• Q i and Q o are countable sets called input and output alphabets;

Q = Q i × Q o is the set of query operations. A query operation (q i , q o ) ∈ Q is denoted q i /q o (query q i returns value q o ). • S is a countable set of states; • s 0 ∈ S is the initial state; • T : S × U → S is the transition function; • G : S × Q i → Q o is the output function.
A sequential history is a sequence of operations. An infinite sequence of operations (w i ) i∈N ∈ (U ∪ Q) ω is recognized by O if there exists an infinite sequence of states (s i ) i≥1 ∈ S ω (note that s 0 is the initial state) such that for all i ∈ N, T (s i , w

i ) = s i+1 if w i ∈ U or s i = s i+1 and G(s i , q i ) = q o if w i = q i /q o ∈ Q.
The set of all infinite sequences recognized by O and their finite prefixes is denoted by L(O). Said differently, L(O) is the set of all the sequential histories allowed for O.

Along the paper, replicated sets are used as the key example. Three kinds of operations are possible: two update operation by element, namely insertion (I) and deletion (D) and a query operation read (R) that returns the values that belong to the set. Let Val be the support of the replicated set (it contains the values that can be inserted/deleted). At the beginning, the set is empty and when an element is inserted, it becomes present until it is deleted. More formally, it corresponds to the UQ-ADT given in Example 1.

Example 1 (Specification of the set). Let Val be a countable set, called support. The set object S Val is the UQ-ADT (U, Q i , Q o , S, ∅, T, G) with:

• U = {I(v), D(v) : v ∈ Val}; • Q i = {R}, and Q o = S = P <∞ (Val ) contain all the finite subsets of Val ; • for all s ∈ S and v ∈ Val , G(s, R) = s, T (s, I(v)) = s ∪ {v} and T (s, D(v)) = s \ {v}.
The set U of updates is the set of all insertions and deletions of any value of Val . The set of queries Q i contains a unique operation R, a read operation with no parameter. A read operation may return any value in Q o , the set of all finite subsets of Val. The set S of the possible states is the same as the set of possible returned values Q o as the read query returns the content of the set object. I(v) (resp. D(v)) with v ∈ Val denotes an insertion (resp. a deletion) operation of the value v into the set object. R/s denotes a read operation that returns the set s representing the content of the set.

During an execution, the participants invoke an object instance of an abstract data type using the associated operations (queries and updates). This execution produces a set of partially ordered events labelled by the operations of the abstract data type. This representation of a distributed history is generic enough to model a large number of distributed systems. For example, in the case of communicating sequential processes, an event a precedes an event b in the program order if they are executed by the same process in that sequential order. It is also possible to model more complex modern systems in which new threads are created and destroyed dynamically, or peer-to-peer systems where peers may join and leave.

Definition 2 (Distributed History). A distributed history is a tuple

H = (U, Q, E, Λ, →):
• U and Q are disjoint countable sets of update and query operations, and all queries q ∈ Q are in the form q = q i /q o ; • E is a countable set of events;

• Λ : E → U ∪ Q is a labelling function; • →⊂ E × E is a partial order called program order,
such that for all e ∈ E, {e ′ ∈ E : e ′ → e} is finite.

Let H = (U, Q, E, Λ, →) be a history. The sets U H = {e ∈ E : Λ(e) ∈ U } and Q H = {e ∈ E : Λ(e) ∈ Q} denote its sets of update and query events respectively. We also define some projections on the histories. The first one allows to withdraw some events: for

F ⊂ E, H F = (U, Q, F, Λ| F , → ∩(F × F ))
is the history that contains only the events of F . The second one allows to substitute the order relation: if → is a partial order that respects the definition of a program order ( →),

H → = (U, Q, E, Λ, → ∩(E × E))
is the history in which the events are ordered by →. Note that the projections commute, which allows the notation H → F . Definition 3 (Linearizations). Let H = (U, Q, E, Λ, →) be a distributed history. A linearization of H corresponds to a sequential history that contains the same events as H in an order consistent with the program order. More precisely, it is a word Λ(e 0 ) . . . Λ(e n ) . . . such that {e 0 , . . . , e n , . . .} = E and for all i and j, if i < j, e j → e i . We denote by lin(H) the set of all linearizations of H.

Definition 4 (Consistency criterion). A consistency criterion

III. EVENTUAL CONSISTENCY

In this section, we recall the definitions of eventual consistency [START_REF] Vogels | Eventually consistent[END_REF] and strong eventual consistency [START_REF] Shapiro | A comprehensive study of convergent and commutative replicated data types[END_REF]. Fig. 1 illustrates these two consistency criteria on small examples. In the remaining of this article, we consider an UQ

-ADT O = (U, Q i , Q o , S, s 0 , T, G) and a history H = (U, Q, E, Λ, →).
Eventual consistency: eventual consistency requires that, if all the participants stop updating, all the replicas eventually converge to the same state. In other word, H is eventually consistent if it contains an infinite number of updates (i.e. the participants never stop writing) or if there exists a state (the consistent state) compatible with all but a finite number of queries.

Definition 5 (Eventual consistency).

A history H is eventually consistent (EC) if U H is infinite or there exists a state s ∈ S such that the set of queries that return non consistent values while in the state s,

{q i /q o ∈ Q H : G(s, q i ) = q o }, is finite.
All the histories presented in Fig. 1 are eventually consistent. The executions represent two processes sharing a set of integers. In Fig. 1a, the first process inserts value 1 and then reads twice the set and gets respectively {2} and {1}; afterwards, it executes an infinity of read operations that return the empty set (ω in superscript denotes the operation is executed an infinity of times). In the meantime, the second process inserts a 2 then reads the set an infinity of times. It gets respectively {1} and {2} the two first times, and empty set an infinity of times. Both processes converge to the same state (∅), so the history is eventually consistent. However, before converging, the processes can read anything a finite but unbounded number of times.

Strong eventual consistency: strong eventual consistency requires that two replicas of the same object converge as soon as they have received the same updates. The problem with that definition is that the notions of replica and message reception are inherent to the implementation, and are hidden from the programmer that uses the object, so they should not be used in its specification. A visibility relation is introduced to model the notion of message delivery. This relation is not an order since it is not required to be transitive.

Definition 6 (Strong eventual consistency

∀V ⊂ U H , ∃s ∈ S, ∀q i /q o ∈ Q H , V = {u ∈ U H : u vis --→ q i /q o } ⇒ G(s, q i ) = q o .
The history of Fig. 1a is not strong eventually consistent because the I(1) must be visible by all the queries of the first process (by reflexivity and growth), so there are only two possible sets of visible updates ({I(1)} and{I(1), I(2)}) for these events, but the queries are done in three different states ({1}, {2} and ∅); consequently, at least two of these queries see the same set of updates and thus need to return the same value. Fig. 1c, on the contrary, is strong eventually consistent: the replicas that see {I(1)} are in state ∅ and those that see {I(1), I(2)} are in state {1, 2}.

IV. PIPELINED CONVERGENCE

A straightforward way to strengthen eventual consistency is to compose it with another consistency criterion that imposes restrictions on the values that can be returned by a read operation. Causality is often cited as a possible candidate to play this role [START_REF] Sun | Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems[END_REF]. As causal consistency is well formalized only for memory, we will instead consider Pipelined Random Access Memory (PRAM) [START_REF] Lipton | PRAM: A scalable shared memory[END_REF], a weaker consistency criterion. As the name suggests, PRAM was initially defined for memory. However, it can be easily extended to all UQ-ADTs. Let's call this new consistency criterion pipelined consistency (PC). In a pipelined consistent computation, each process must have a consistent view of its local history with all the updates of the computation. More formally, it corresponds to Def. 7. Pipelined consistency is local to each process, as different processes can see concurrent updates in a different order.

Definition 7.

A history H is pipelined consistent (PC) if, for all maximal chains (i.e. sets of totally ordered events) p of H, lin (

H UH ∪p ) ∩ L(O) = ∅.
Pipelined consistency can be implemented at a very low cost in wait-free systems. Indeed, it only requires FIFO reception. However, it does not imply convergence. For example, the history given in Figure 2 is pipelined consistent but not eventually consistent. In this history, two processes p 1 and p 2 share a set of integers. Process p 1 first inserts 1 and then 3 in the set and then reads the set forever. Meanwhile, process p 2 inserts 2, deletes 3 and reads the set forever. The words w 1 and w 2 are correct linearizations for both processes, with regard to Definition 7 so the history is pipelined consistent, but after stabilization, p 2 sees the element 3 whereas p 1 does not.

• I(1) • R/{2} • R/{1} • R/∅ ω • I(2) • R/{1} • R/{2} • R/∅ ω (a) EC but not SEC nor UC • I(1) • D(2) • R/{1, 2} ω • I(2) • D(1) • R/{1, 2} ω (b) SEC but not UC • I(1) • R/∅ • R/{1, 2} ω • I(2) • R/{1, 2} ω (c) SEC and UC but not SUC • I(1) • R/{1} • I(2) • R/{1, 2} ω • R/{2} • R/{1, 2} ω (d) SUC but not PC
Figure 1: Four histories for an instance of S N (cf. example 1), with different consistency criteria. The arrows represent the program order, and an event labeled ω is repeated an infinite number of times. . Pipelined convergence, that imposes both pipelined consistency and eventual consistency, cannot be implemented in a wait-free system.

• a I(1) • b I(3) • c R/{1, 3} • d R/{1, 2, 3} • e R/{1, 2} ω • f I(2) • g D(3) • h R/{2} • i R/{1, 2} • j R/{1, 2, 3} ω w 1 = I(1)•I(3)•R/{1, 3}•I(2)•R/{1, 2, 3}•D(3)•R/{1, 2} ω w 2 = I(2) • D(3) • R/{2} • I(1) • R/{1, 2} • I(3) • R/{1, 2, 3} ω
Proof: We consider the same program as in Figure 2, and we suppose the shared set is pipelined convergent. By the same argument as developed in [START_REF] Attiya | Sequential consistency versus linearizability[END_REF], it is not possible to prevent the processes from not seeing each other's first update at their first reads. Indeed, if p 1 did not receive any message from process p 2 , it is impossible for p 1 to make the difference between the case where p 2 crashed before sending any message and the case where all its messages were delayed. To achieve availability, p 1 must compute the return value based solely on its local knowledge, so it returns {1, 3}. Similarly, p 2 returns {2}. To circumvent this impossibility, it is necessary to make synchrony assumption on the system (e.g. bounds on transmission delays) or to assume the correctness of a majority of processes.

If the first read of p 1 returns {1, 3}, as the set is pipelined consistent, there must exist a linearization for p 1 that contains all the updates, R/{1, 3} and an infinity of queries. As 2 ∈ {1, 3}, the possible linearizations are defined by the ω-regular language I(1)

•I(3)•R/{1, 3} + •I(2)•R/{1, 2, 3} ⋆ •D(3)•R/{1, 2} ω
, so any history must contain an infinity of events labelled R/{1, 2} ω . Similarly, if p 2 starts by reading {2}, it will eventually read {1, 2, 3} an infinity of times. This implies that pipelined convergence cannot be provided in wait-free systems.

Consequently causal consistency, that is stronger than pipelined consistency, cannot be satisfied together with eventual consistency in a wait-free system.

V. UPDATE CONSISTENCY

In this section, we introduce two new consistency criteria: update consistency and strong update consistency 2 , and we compare them to eventual consistency and strong eventual consistency. Fig. 1 illustrates these four consistency criteria on four small examples.

Update consistency: eventual consistency and strong eventual consistency are not interested in defining the states that are reached during the histories (the same updates have to lead to the same state whatever is the state). They do not depend on the sequential specification of the object, so they give very little constraints on the histories. For example, an implementation that ignores all the updates is strong eventually consistent, as all the queries return the initial state. In update consistency, we impose the existence of a total order on the updates, that contains the program order and that leads to the consistent state according to the abstract data type. Another equivalent way to approach update consistency is that, if the number of updates is finite, it is possible to remove a finite number of queries such that the history is sequentially consistent.

Definition 8 (Update consistency). A history

H is update consistent (UC) if U H is infinite or if there exists a finite set of queries Q ′ ⊂ Q H such that lin H E\Q ′ ∩ L(O) = ∅.
The history of Fig. 1c is update consistent because the sequence of operations I(1)I( 2) is a possible explanation for the state {1, 2}. The history of Fig. 1b is not update consistent because any linearization of the updates would position a deletion as the last event.

∀q ∈ Q H , lin H ≤ V (q)∪{q} ∩ L(O) = ∅ where V (q) = {u ∈ U H : u vis --→ q}.
Fig. 1d shows an example of strong update consistent history: nothing prevents the second process from seeing the insertion of 2 before that of 1. Strong eventual consistency and update consistency does not imply strong update consistency: in the history of Fig. 1c, after executing event I(1), the only three possible update linearizations are I(1), I(1) • I(2) and I(2) • I(1) and none of them can lead to the state ∅ according to the sequential specification of a set object. So the history of Fig. 1c is not strong update consistent, while it is update consistent and strong eventually consistent.

Proposition 2 (Comparison of consistency criteria). If a history H is update consistent, then it is eventually consistent. If H is strong update consistent, then it is both strong eventually consistent and update consistent.

Proof: Suppose H is update consistent. If H contains an infinite number of updates, then it is eventually consistent. Otherwise, there exists a finite set

Q ′ ⊂ Q H and a word w ∈ lin H EH \Q ′ ∩ L(O).
As the number of updates is finite, there is a finite prefix v of w that contains them all. v ∈ L(O), so it labels a path between s 0 and a state s in the UQ-ADT. All the queries that are in w but not in v return the same state s, and the number of queries in Q ′ and v is finite. Hence, H is eventually consistent.

Suppose

H is strong update consistent with a finite number of updates.

Q ′ = u∈UH {q ∈ Q H , q ≤ u}
is finite, and lin (E H \ Q ′ ) contains only one word that is also contained into L(O). Obviously, H is update consistent Now, suppose H is strong update consistent. Strong update consistency respects both eventual delivery and growth properties. Let V ⊂ U H . As the relation ≤ is a total order, there is a unique word w in lin H ≤ V ∩ L(O). Let us denote s the state obtained after the execution of w. For all q ∈ Q H such that V = {u ∈ U H : u vis --→ q}, lin H ≤ Eq∪{q} ∩ L(O) = {w • Λ(q)}, so q = q i /q o with G(s, q i ) = q o . Consequently, H is strong eventually consistent.

VI. EXPRESSIVENESS OF UPDATE CONSISTENCY: A CASE STUDY

The set is one of the most studied eventually consistent data structures. Different types of sets have been proposed as extensions to CRDTs to implement eventually consistent sets even though the insert and delete operations do not commute. The simplest set is the Grow-Only Set (G-Set) [START_REF] Shapiro | A comprehensive study of convergent and commutative replicated data types[END_REF], in which it is only possible to insert elements. As the insertion of two elements commute, G-Set is a CRDT. Using two G-Set, a white list for inserted elements and a black list for the deleted ones, it is possible to build a Two-Phases Set (2P-Set, a.k.a. U-Set, for Unique Set) [START_REF] Wuu | Efficient solutions to the replicated log and dictionary problems[END_REF], in which it is possible to insert and remove elements, but never insert again an element that has already been deleted. Other implementations such as C-Set [START_REF] Aslan | C-set: a commutative replicated data type for semantic stores[END_REF] and PN-Set, add counters on the elements to determine if they should be present or not. The Observe-Remove Set (OR-Set) [START_REF] Shapiro | A comprehensive study of convergent and commutative replicated data types[END_REF], [START_REF] Mukund | Optimized orsets without ordering constraints[END_REF] is the best documented algorithm for the set. It is very close to the 2P-Set in its principles, but each insertion is timestamped with a unique identifier, and the deletion only black-lists the identifiers that it observes. It guaranties that, if an insertion and a deletion of the same element are concurrent, the insertion will win and the element will be added to the set. Finally, the last-writer-wins element set (LWW-element-Set) [START_REF] Shapiro | A comprehensive study of convergent and commutative replicated data types[END_REF] attaches a timestamp to each element to decide which operation should win in case of conflict. All these sets, and the eventually consistent objects in general, have a different behavior when they are used in distributed programs.

The above mentioned implementations are eventually consistent. However, as eventual consistency does not impose a semantic link between updates and queries, it is hazardous to say anything on the conformance to the specification of the object. Burckhardt et al. [START_REF] Burckhardt | Replicated data types: specification, verification, optimality[END_REF] propose to specify the semantics of a query by a function on its concurrent history, called visibility, that corresponds to the visibility relation in strong eventual consistency, and a linearization of this history, called arbitration. In comparison, sequential specifications are restricted to the arbitration relation. It implies that fewer update consistent objects than eventually consistent objects can be specified. Although the variety of objects with a distributed specification seems to be a chance that compensates the lower level of abstraction it allows, an important bias must be taken into account: from the point of view of the user, the visibility of an operation is not an a priori property of the system, but an a posteriori way to explain what happened. If one only focuses on the final state, an update consistent object is appropriate to be used instead of an eventually consistent object, since the final state is the same as if no operations were concurrent.

By adding further constraints on the histories, concurrent specifications strengthen the consistency criteria. Even if strong update consistency is stronger than strong eventual consistency, we cannot say in general that a strong update consistent object can always be used instead of its strong eventually consistent counterpart. We claim that this is true in practice for reasonable objects, and we prove this in the case of the Insert-wins set (the concurrent specification of the OR-set). The arbitration relation is not used for the OR-set, and the visibility relation has already been defined for strong eventual consistency. The concurrent specification only adds one more constraint on this relation: an element is present in the set if and only if it was inserted and is not yet deleted. Definition 10 (Strong eventual consistency for the Insert-wins set). A history H is strong eventually consistent for the Insert-wins set on a support Val if it is strong eventually consistent for the set S Val and the visibility relation vis --→ verifies the following additional property. For all x ∈ Val and q ∈ Q H , with Λ(q) = R/s, x ∈ s ⇔ ∃u ∈ vis(q, I(x)), ∀u ′ ∈ vis(q, D(x)), u vis --→ u ′ , where

for all o ∈ U , vis(q, o) = {u ∈ U H : u vis --→ q ∧ Λ(u) = o}.
The OR-Set implementation of a set is not update consistent. The history on Fig. 1b is not update consistent, as the last operation must be a deletion. However, if the updates made by a process are not viewed by the other process before it makes its own updates, the insertions will win and the OR-set will converge to {1, 2}. On the contrary, a strong update consistent implementation of a set can always be used instead of an Insert-wins set, as it only forbids more histories.

Proposition 3 (Comparison with Insert-wins set)

. Let H = (U, Q, E, Λ, →) be a history that is strong update consistent for S Val . Then H is strong eventually consistent for the Insert-wins set.

Proof: Suppose H is strong update consistent for S Val . We define the new relation IW --→ such that for all e, e ′ ∈ E, e IW --→ e ′ if one of the following conditions holds:

• e vis --→ e ′ ; • e and e ′ are two updates on the same element and e ≤ e ′ ; • e ′ is a query, and there is an update e ′′ such that e IW --→ e ′′ and e ′′ IW --→ e ′ .

The relation IW --→ is acyclic because it is included in ≤, its growth and eventual delivery properties are ensured by the fact that it contains vis --→. Moreover, no two updates for the same element are concurrent according to IW --→ and the last updates are also the last for the ≤ relation, consequently H is strong eventually consistent for the Insert-wins set. This result implies that an OR-set can always be replaced by an update consistent set, because the guaranties it ensures are weaker than those of the update consistent set. It does not mean that the OR-set is worthless. It can be seen as a cache consistent set [START_REF] Goodman | Cache consistency and sequential consistency[END_REF] that, in some cases may have a better space complexity than update consistency.

VII. GENERIC CONSTRUCTION OF STRONG UPDATE CONSISTENT OBJECTS

In this section, we give a generic construction of strong update consistent objects in crash-prone asynchronous message-passing systems. This construction is not the most efficient ever as it is intended to work for any UQ-ADT object in order to prove the universality of update consistency. For a specific object an ad hoc implementation on a specific system may be more suitable.

A. System Model

We consider a message-passing system composed of finite set of sequential processes that may fail by halting. A faulty process simply stops operating. A process that does not crash during an execution is correct. We make no assumption on the number of failures that can occur during an execution. Processes communicate by exchanging messages using a communication network complete and reliable. A message sent by a correct process to another correct process is eventually received. The system is asynchronous; there is no bound on the relative speed of processes nor on the message transfer delays. In such a situation a process cannot wait for the participation of any a priori known number of processes as they can fail. Consequently, when an operation on a replicated object is invoked Algorithm 1: a generic UQ-ADT (code for p i ) locally at some process, it needs to be completed based solely on the local knowledge of the process. We call this kind of systems wait-free asynchronous messagepassing system.

1 object (U, Q i , Q o , S, s 0 , T, G) 2 var clock i ∈ N ← 0; 3 var update i ⊂ (N × N × U ) ← ∅;
We model executions as histories made up of the sequences of events generated by the different processes. As we focus on shared objects and their implementation, only two kinds of actions are considered: the operations on shared objects, that are seen as events in the distributed history, and message receptions.

B. A universal implementation

Now, we prove that strong update consistency is universal, in the sense that every UQ-ADT has a strong update consistent implementation in a waitfree asynchronous system. Algorithm 1 presents an implementation of a generic UQ-ADT. The principle is to build a total order on the updates on which all the participants agree, and then to rewrite the history a posteriori so that every replica of the object eventually reaches the state corresponding to the common sequential history. Any strategy to build the total order on the updates would work. In Algorithm 1, this order is built from a Lamport's clock [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] that contains the happened-before precedence relation. Process order is hence respected. A logical Lamport's clock is a pretotal order as some events may be associated with the same logical time. In order to have a total order, the events are timestamped with a pair composed of the logical time and the id of the process that produced it (process ids are assumed unique and totally ordered). The algorithm actions performed by a process p i are atomic and totally ordered by an order → i . The union of these orders for all processes is the program order →.

At the application level, a history is composed of update and query operations. In order to allow only strong update consistent histories, Algorithm 1 proposes a procedure update() and a function query().

A history H is allowed by the algorithm if update(u) is called each time a process performs an update u, and query(q i ) is called and returns q o when the event q i /q o appears in the history. The code of Algorithm 1 is given for process p i . Each process p i manages its view clock i of the logical clock and a list updates i of all timestamped update events process p i is aware of. The list updates i contains triplets (cl, j, u) where u is an update event and (cl, j) the associated timestamp. This list is sorted according to the timestamps of the updates:

(cl, j) < (cl ′ , j ′ ) if (cl < cl ′ ) or (cl = cl ′ and j < j ′ ).
The algorithm timestamps all events (updates and queries). When an update is issued locally, process p i informs all the other processes by reliably broadcasting a message to all other processes (including itself). Hence, all processes will eventually be aware of all updates. When a message(cl, j, u) is received, p i updates its clock and inserts the event to the list updates i . When a query is issued, the function query() replays locally the whole list of update events p i is aware of starting from the initial state then it executes the query on the state it obtains.

Whenever an operation is issued, its is completed without waiting for any other process. This corresponds to wait-free executions in shared memory distributed systems and implies fault-tolerance.

Proposition 4 (Strong update consistency). All histories allowed by Algorithm 1 are strong update consistent.

Proof: Let H = (U, Q, E, Λ, →) be a distributed history allowed by Algorithm 1. Let e, e ′ ∈ E H be two operations invoked by processes p i and p i ′ , on the states (update, clock) and (update ′ , clock ′ ), respectively. We pose:

• e vis --→ e ′ if e ∈ U H and p i ′ received the message sent during the execution of e before it starts executing e ′ , or e ∈ Q H and e → e ′ . As the messages are received instantaneously by the sender, vis --→ contains →. It is growing because the set of messages received by a process is growing with time.

• e ≤ e ′ if c < c ′ or c = c ′ and i < i ′ . This lexical order is total because two operations on the same process have a different clock. Moreover it contains vis --→ because when p i ′ received the message sent by e, it executed line 9 and when it executed e ′ , it executed line 5, so c ′ ≥ c + 1. Moreover, the history of e contains at most c×n+i events, where n is the number of processes, so it is finite. Let q ∈ Q H and E q = {u ∈ U H : u

C. Complexity

Algorithm 1 is very efficient in terms of network communication. A unique message is broadcast for each update and each message only contains the information to identify the update and a timestamp composed of two integer values, that only grow logarithmically with the number of processes and the number of operations. Moreover, this algorithm is wait-free and its execution does not depend on the latency of the network.

This algorithm re-executes all past updates each time a new query is issued. In an effective implementation, a process can keep intermediate states. These intermediate states are re-computed only if very late message arrive. The algorithm does not look space efficient also as the whole history must be kept in order to rebuild a sequential history. Because data space is cheap and fast nowadays, compared to bandwidth, many applications can afford this complexity and would keep this information anyway. For example, banks keep track of all the operations made on an account for years for legal reasons. In databases systems, it is usual to record all the events in log files. Moreover, asynchrony is used as a convenient abstraction for systems in which transmission delays are actually bounded, but the bound is too large to be used in practice. This means that after some time old messages can be garbage collected.

The proposed algorithm is a theoretical work whose goal is to prove that any update-query object has a strong update consistent implementation. This genericity prevents an effective implementation that may take benefit from the nature and the specificity of the actual object. The best example of this are pure CRDTs like the counter and the grow-only set. If all the update operations commute in the sequential specification, all linearizations would lead to the same state so a naive implementation, that applies the updates on a replica as soon as the notification is received, achieves update consistency. In [START_REF] Karsenty | An algorithm for distributed groupware applications[END_REF], Karsenty and Algorithm 2: the shared memory (code for p i ) 1 object UC mem(X, V, v 0 ) 2 var clock i ∈ N ← 0; 3 var mem i ∈ mem(X, (N 2 × V ), (0, 0, v 0 )); Beaudouin-Lafon propose an algorithm to implement objects such that each update operation u contains an undo u -1 such that for all s, T (T (s, u), u -1 ) = s. This algorithm is very close to ours as it builds the convergent state from a linearization of the updates stored by each replica. They use the undo operations to position newly known updates at their correct place, which saves computation time. As it is a very frequent example in distributed systems, we now focus on the shared memory object.

Algorithm 2 shows an update consistent implementation of the shared memory object. A shared memory offers a set X of registers that contain values taken from a set V . The query operation read(x), where x ∈ X, returns the last value v ∈ V written by the update operation write(x, v), or the initial value v 0 ∈ V if x was never written. Algorithm 2 orders the updates exactly like Algorithm 1. As the old values can never be read again, it is not necessary to store them forever, so the algorithm only keeps in memory the last known value of each register and its timestamp in a local memory mem i , implemented with an associative array. When a process receives a notification for a write, it updates its local state if the value is newer that the current one, and the read operations just return the current value. This implementation only needs constant computation time for both the reads and the writes, and the complexity in memory only grows logarithmically with time and the number of participants.

VIII. CONCLUSION

This paper proposes a new consistency criterion, update consistency, that is stronger than eventual consistency and weaker than sequential consistency. Our approach formalizes the intuitive notions of sequential specification for an abstract data type and distributed history. This formalization first allowed to prove that eventual consistency when associated with causal consistency or PRAM consistency can no more be implemented in an asynchronous distributed system where all but one process may crash. This paper formalizes the new consistency criterion and proves that (1) it is strictly stronger than eventual consistency and (2) that it is universal in the sense that allowed any update consistent object can be implemented in wait-free systems. The latter has been proved through a generic construction that implement all considered data types.

  C characterizes which histories are allowed for a given data type. It is a function C that associates with any UQ-ADT O, a set of distributed histories C(O). A shared object (instance of an UQ-ADT O) is C-consistent if all the histories it allows are in C(O).

Figure 2 :

 2 Figure 2: PC but not EC

  Only three consistent states are actually possible: state ∅, e.g. for the linearization I(1) • I(2) • D(1) • D(2), state {1} for the linearization I(2) • D(1) • I(1) • D(2) and state {2} for the linearization I(1) • D(2) • I(2) • D(1

  vis --→ q}. Lines 15 to 18 build an explicit sequential execution, that is in lin H ≤ Eq∪{q} by definition of ≤ and in L(O) by definition of O.

4 fun 6 broadcast

 46 write (x ∈ X, v ∈ V ) 5 clock i ← clock i + 1; msg (clock i , i, x, v); msg (cl ∈ N, j ∈ N, x ∈ X, v ∈ V ) 9 clock i ← max(clock i , cl); 10 var (cl ′ , j ′ , v ′ ) ∈ N 2 × V ← mem i .read(x); 11 if (cl ′ , j ′ ) < (cl, j) then 12 mem i .write(x, (cl, j, v)) (x ∈ X) ∈ V 16 var (cl, j, v) ∈ N 2 × V ← mem i .read(x);

  Strong convergence: if two query operations view the same past of updates V , they can be issued in the same state s:

		). A history
	H is strong eventually consistent (SEC) if there exists
	an acyclic and reflexive relation	vis --→ (called visibility
	relation) that contains → and such that:

• Eventual delivery: when an update is viewed by a replica, it is eventually viewed by all replicas, so there can be at most a finite number of operations that do not view it: ∀u ∈ U H , {e ∈ E, u vis --→ e} is finite;

• Growth: if an event has been viewed once by a process, it will remain visible forever: ∀e, e ′ , e ′′ ∈ E, (e vis --→ e ′ ∧ e ′ → e ′′ ) ⇒ (e vis --→ e ′′ ); •

  Each query is the result of the ordered execution, according to ≤, of the updates it views:

	Strong update consistency: strong update consis-
	tency is a strengthening of both update consistency and
	strong eventual consistency. The relationship between
	update consistency and strong update consistency is
	analogous to the relation between eventual consistency
	and strong eventual consistency.
	Definition 9 (Strong update consistency). A history H
	is strong update consistent (SUC) if there exists (1) an
	acyclic and reflexive relation	vis --→ that contains → and
	(2) a total order ≤ that contains	vis --→ such that:
			). Update
			consistency is incomparable with strong eventual con-
			sistency.

• Eventual delivery: ∀u ∈ U H , {e ∈ E, u vis --→ e} is finite; • Growth: ∀e, e ′ , e ′′ ∈ E, e vis --→ e ′ ∧ e ′ → e ′′ ⇒ e vis --→ e ′′ ; • Strong sequential convergence: A query views an update if this update precedes it according to vis --→.

We use indifferently participant or process to designate the computing entities that invoke the distributed object.

These consistency criteria were previously presented as a brief announcement in DISC 2014[START_REF] Perrin | Brief announcement: Update consistency in partitionable systems[END_REF].

ACKNOWLEDGMENT

This work has been partially supported by a French government support granted to the CominLabs excellence laboratory (Project DeSceNt: Plug-based Decentralized Social Network) and managed by the French National Agency for Research (ANR) in the "Investing for the Future" program under reference Nb. ANR-10-LABX-07-01. This work was partially funded by the French ANR project SocioPlug (ANR-13-INFR-0003).


Caifang Cai

Marc Lambert

Thomas Rodet

A parameter inversion approach based on a MCMC sampling method in Eddy-Current Testing

Keywords: Markov Chain Monte Carlo (MCMC), inverse problem, metamodeling and Eddy-Current Testing (ECT)

come

A parameter inversion approach based on a MCMC

sampling method in Eddy-Current Testing


Rafife Nheili

Philippe Langlois

Christophe Denis

Numerical Reproducibility in open TELEMAC: A Case Study within the Tomawac Library

The lack of numerical reproducibility for parallel floatingpoint computations is a stringent problem for HPC numerical simulations. Reproducibility is indeed desirable for code verification, testing, debugging and even for certification authority agreement. We describe and analyse strategies towards numerically reproducible simulations with a well known open source software for computational fluid dynamics.

Introduction

Numerical reproducibility consists in getting the same result when running a parallel HPC software with a varying number of processing units. The lack of numerical reproducibility mainly comes from the non-associativity of the floating-point addition: the non-deterministic parallel reductions lead to different results, as for instance when summing with the MPI reduction.

We present a case study focusing on open TELEMAC-MASCARET, a well known modelling tool developed by EDF and associates since 20 years [4]. It implements the finite element method to approximate the solutions of numerous applications of free surface fluids in both river and maritime hydraulics [START_REF] Hervouet | Hydrodynamics of free surface flows: Modelling with the finite element method[END_REF]. In our scope, the main step of this resolution is the assembly process: i) Quantities are computed for each element and stored in its local nodes. ii) These local quantities are accumulated to the global points of the mesh, via a connectivity table which links local nodes and global points. For the parallel computation, the elements are distributed between the processors thanks to a sub-domain decomposition. So the assembly process is first executed "at the processor level", then the processors that share the interface nodes communicate to exchange and add the missing contributions. This accumulation is order dependant in floating-point arithmetic. As soon as one interface node is shared between more than 2 processors, a different computing order occurs compared to the sequential one. Hence this interface assembly step lacks of numerical reproducibility when varying the number of computing units, i.e. the number of sub-domains. Others sources of non-reproducibility as the dot products and the segment assembly step will not be discussed in the following case study.

We focus on the Tomawac library which is the TELEMAC unit to solve transport equations with the method of characteristics. This method introduces no dot product. So its reproducibility only depends on the previously described parallel summation within the finite element assembly step. In this paper, we improve this computation to provide the numerical reproducibility of Tomawac. ⋆ 1 firstname.lastname@univ-perp.fr, 2 christophe.denis@edf.fr. Authors thank J.-M. Hervouet (EDF R&D, Chatou) for his kind and valuable contribution.

First we exhibit cases of non-reproducibility for Tomawac when we compute the assembly step with the classical floating-point reduction FPSum. Fig. 1(Left) shows the maximum relative errors between the sequential result and the parallel ones for several number of processors p = 2, 4, 8, 16 (x-axis is the simulation time scale). Reproducible results should yield a unique plot at every time step when p is varying. It is not the case. We analyse three approaches to achieve reproducibility.

IntSum converts FPSum to the sum of 8 byte integers [4]. The finite element and the interface node assembly steps are computed with integer recoding and integer sums. This choice is reasonable here because every interface node belongs to less than ten neighbouring elements.

Fig. 1 (

 1 Right) now displays a unique plot that illustrates the expected numerical reproducibility of IntSum. The parallel IntSum accuracy compared to the sequential FPSum one is of the order of 10 -15 . Reproducibility and accuracy are different software quality goals. Indeed IntSum is more accurate than FPSum. CompSum improves FPSum with a twice more accurate compensated sum[START_REF] Ogita | Accurate sum and dot product[END_REF]. It consists in accumulating the round-off errors of intermediate sums to later compensate the computed result. The accumulated errors of each global point are added to its final value. Fig.1(Right) exhibits the CompSum reproducibility and the same good properties already mentioned for IntSum. ReprodSum modifies FPSum with the reproducible sum from[START_REF] Demmel | Fast reproducible floating-point summation[END_REF]. It uses a pre-rounding technique that rounds the input values to a common threshold that depends on the maximum and on the size of the entry vector. It does not depend on the computation order and is almost as accurate as FPSum.

Fig. 1 :

 1 Fig. 1: Reproducibility and accuracy improvement for the mean wave frequency (Nice test case, Tomawac). Left: Parallel vs. sequential FPSum. Right: IntSum, CompSum and their accuracy compared to sequential FPSum (dashed).


Chemseddine Chohra

Philippe Langlois

David Parello

Efficiency of Reproducible Level 1 BLAS

Numerical reproducibility failures appear in massively parallel floating-point computations. One way to guarantee the numerical reproducibility is to extend the IEEE-754 correct rounding to larger computing sequences, as for instance for the BLAS libraries. Is the overcost for numerical reproducibility acceptable in practice? We present solutions and experiments for the level 1 BLAS and we conclude about the efficiency of these reproducible routines.

Introduction

Numerical reproducibility is an open question for current high performance computing platforms. Dynamic scheduling and non-deterministic reduction on multithreaded systems affect the operation order. This leads to non-reproducible results because the floating-point addition is not associative. Numerical reproducibility is important for debugging and for validating results, particularly if legal agreements require the exact reproduction of the execution results. Failures have been reported in numerical simulation for energy science, dynamic weather forecasting, atomic or molecular dynamic, fluid dynamic -see entries in [START_REF] Jézéquel | First steps towards more numerical reproducibility[END_REF].

Solutions provided at the middleware level forbid the dynamic behavior and so impact the performances -see [START_REF] Reinders | Intel Threading Building Blocks[END_REF] for TBB, [START_REF] Story | Numerical reproducibility in the Intel Math Kernel Library[END_REF] for OpenMP or Intel MKL. Note that adding pragmas in the source code avoids memory alignment effects onto reproducibility. A first algorithmic solution has been recently proposed in [START_REF] Demmel | Fast reproducible floating-point summation[END_REF]. Their summation algorithms, ReprodSum and FastReprodSum, guarantee the reproducibility independently from the computation order. They return about the same accuracy as the performance optimized algorithm only running a small constant times slower. Correctly rounded results ensure numerical reproducibility. IEEE754-2008 floating-point arithmetic is correctly rounded in its four rounding modes [START_REF]Standard for Floating-Point Arithmetic[END_REF]. We propose to extend this property to the level 1 routines of the BLAS that depend on the summation order: asum, dot and nrm2, respectively the sum of the absolute values, the dot product and the vectorial Euclidean norm. Recent algorithms that compute the correctly rounded sum of n floating-point values allow us to implement such reproducible parallel computation. The main issue is ⋆ firstname.lastname@univ-perp.fr to investigate whether the running-time overhead of these reproducible routines remains reasonable enough in practice. In this paper we present experimental answers to this question. Our experimental framework is significant of the current computing practice: it consists in a shared memory parallel system with several sockets of multicore x86 processing units. We apply standard optimization techniques to implement efficient sequential and parallel level 1 routines. We show that for large vectors, reproducible and accurate routines introduces almost no overhead compared to their original counterparts in a performance-optimized library (Intel MKL). For shorter ones, reasonable overheads are measured and presented in Table 4.1. Since Level 1 BLAS performance is mainly dominated by the memory transfers, additional computation does not significantly increase the running time, especially for large vectors.

The paper is organized as follows. In Section 2, we briefly present some accurate summation algorithms, their optimizations and an experimental performance analysis to decide how to efficiently implement the level 1 BLAS. The experimental framework used throughout the paper is also described in this part. Section 3 is devoted to the performance analysis of the sequential implementation of the level 1 BLAS routines. Section 4 describes their parallel implementations and the measure of their efficiency. We conclude describing the future developments of this ongoing project towards efficient and reproducible BLAS.

Choice of Optimized Floating-Point Summation

Level 1 BLAS subroutines mainly rely on floating-point sums. It exists several correctly rounded summation algorithms. Our first step aims to derive optimized implementations of such algorithms and to choose the most efficient ones. In the following, we briefly describe these accurate algorithms and then, how to optimize and to compare them.

All floating-point computations satisfy the IEEE754-2008. Let f l( p i ) be the computed sum of a length n floating-point vector p. The relative error of the classical accumulation is of the order of u

• n • cond( p i ), where cond( p i ) = |p i |/| p i |
is the condition number of the sum. u is the machine precision that equals 2 -53 for IEEE754 binary64.

Some Accurate or Reproducible Summation Algorithms

Algorithm SumK [START_REF] Ogita | Accurate sum and dot product[END_REF] reduces the previous relative error bound as if the classical accumulation is performed in K times the working precision:

|SumK(p) -p i | | p i | ≤ (n • u) K 1 -(n • u) K • cond( P i ) + u. (2.1)
SumK replaces the floating-point add by Knuth's TwoSum algorithm that computes both the sum and its rounding error [START_REF] Muller | Handbook of Floating-Point Arithmetic[END_REF]. SumK iteratively accumulates these rounding errors to enhance the final result accuracy. The correct rounding could be achieved by choosing a large enough K to vanish the effect of the condition number in (2.1) -but in practice this latter is usually unknown.

Algorithm iFastSum [START_REF] Zhu | Correct rounding and hybrid approach to exact floatingpoint summation[END_REF] repeats SumK to error-free transform the entry vector. This distillation process terminates returning a correctly rounded result thanks to a dynamic control of the error.

Algorithms AccSum [START_REF] Rump | Accurate floating-point summation -part I: Faithful rounding[END_REF] and FastAccSum [START_REF] Rump | Ultimately fast accurate summation[END_REF] also rely on error-free transformations of the entry vector. They split the summands, relatively to max |p i | and n, such that their higher order parts are then exactly accumulated. This split-and-accumulate steps are iterated to enhance the accuracy up to return a faithfully rounded sum. These algorithms return the correctly rounded sum and FastAccSum requires 25% less floating-point operations than AccSum.

HybridSum [START_REF] Zhu | Correct rounding and hybrid approach to exact floatingpoint summation[END_REF] and OnlineExact sum [START_REF] Zhu | Algorithm 908: Online exact summation of floating-point streams[END_REF] exploit the short range of the floatingpoint number exponents. These algorithms accumulate the summands with a same exponent in a specific way to produce a short vector with no rounding error. The length of the output vector of this error-free transform step is the exponent range. HybridSum splits the summands such that floating-point numbers can be used as error-free accumulators. OnlineExact uses two floating-point numbers to simulate a double length accumulator. These algorithms then apply iFastSum to evaluate the correctly rounded sum of the error-free short vector(s).

ReprodSum and FastReprodSum [START_REF] Demmel | Fast reproducible floating-point summation[END_REF] respectively rely on AccSum and FastAcc-Sum to compute not fully accurate but reproducible sums independently of the summation order. So numerical reproducibility of parallel sums is ensured for every number of computing units.

Experimental Framework

Table 2.1 describes our experimental framework. Aggressive compiler options as -ffast-math are disabled to prevent the modification of the sensitive floatingpoint properties of these algorithms. Rounding intermediate results to the bi-nary64 format (53 bit mantissa) and value safe optimizations are provided with -fp-model double and -fp-model strict options. Runtimes are measured in cycles with the hardware counters thanks to the RDTSC assembly instruction. We display the minimum cycle measures over more than fifty runs for each data. Condition dependant data are computed with the dot product generator from [START_REF] Ogita | Accurate sum and dot product[END_REF]. We compare our solutions to the well optimized but non-reproducible MKL BLAS implementation [6].

Implementation, Optimization and Test

For a fair comparison, all algorithms are manually optimized by a best effort process. AVX vectorization, data prefetching and loop unrolling are carefully It is not a surprise that HybridSum and OnlineExact are interesting for larger size vectors. These algorithms produce one or two short vectors (length = 2048 in binary64) whose distillation is of constant time compared to the linear times of the data preprocessing step (exponent extraction) or also, of the successive error free transformations in the other algorithms. Moreover they are very less sensitive to the conditionning of the entry vector. Shorter size vectors benefit from the other algorithms, especially from FastAccSum while their conditionning remains small.

In the following we take advantage of these different behaviors according to the size of the entry vector. We call it a "mixed solution". In practice for the

Sequential Level 1 BLAS

Now we focus on the sum of the absolute value vector (asum), the dot product (dot) and the 2-norm (nrm2). Note that other level 1 BLAS subroutines do not suffer neither of accuracy nor of reproducibility failures. In this section, we start with sequential algorithms detailling our implementations and their efficiency.

Sum of Absolute Values

The condition number of asum equals 1. So SumK is enough to efficiently get a correctly rounded result. According to (2.1), K is chosen such that n ≤ u 1/K-1 .

Figure 3.1a exhibits that the correctly rounded asum costs less than 2× the optimized MKL dasum. Indeed K = 2 applies for the considered sizes. Note that K = 3 is enough until n ≤ 2 35 , i.e. until 256 Terabyte of data.

Dot Product

The dot product of two n-vectors is transformed into a sum of a 2n-vector with Dekker's TwoProd [START_REF] Dekker | A floating-point technique for extending the available precision[END_REF]. This sum is correctly rounded using a "mixed solution". Short vectors are correctly rounded with FastAccSum. For large n, we avoid to build and read this intermediate 2n-vector: the two TwoProd results are directly exponent-driven accumulated into the short vectors of OnlineExact. This explains why this latter is interesting for shorter dot products than what we can expect from Section 2.3.

Figure 3.1b shows this runtime divided by the input vector size -the condition number is 10 32 . Despite the previous optimizations, the overcost ratio compared to MKL dot is between 3 and 6. This is essentially justified by the additional computations (memory transfers are unchanged). If a fused-multiplyand-add unit (FMA) is available, the 2MultFMA algorithm [START_REF] Muller | Handbook of Floating-Point Arithmetic[END_REF] that only costs 2 FMA (compared to the TwoProd's 17 flop) certainly improves these values.

Euclidean Norm

It is not difficult to implement an efficient and reproducible Euclidean norm. Reproducibility is ensured by the correct rounding of the sum of the squares and then by the correct rounding of the IEEE-754 square root. Of course this reproducible 2-norm is only faithfully rounded. Hence a "mixed solution" is similar to the dot one.

Here the MKL nrm2 is not used as the comparison reference since we measure very desapointing runtimes for it. We implement a non-reproducible simple and efficient 2-norm with the optimized MKL dot (cblas_ddot). We named it nOrm2.

The memory transfer cost dominates the computing one for dot and nOrm2: compared to dot, nOrm2 halves the memory tranfer volume, performs the same number of floating-point operations and runs twice faster, see Figures 3.1b and 3.1c. As previously mentionned, the "mixed solution" dot product is still computation-dominated. This justifies that the previous dot ratios prohibitively double for our sequential nrm2.

Reproducible Parallel Level 1 BLAS

Now we consider the parallel implementations. As in the previous section, parallel asum relies on parallel SumK while parallel dot and nrm2 derive from a parallel version of a "mixed solution" for the dot product. We start introducing these two parallel algorithms. Then we derive the parallel reproducible level 1 BLAS and perform its performance analysis.

From Parallel Sums to Reproducible Level 1 BLAS

Parallel SumK. It derives from the sequential version and has already been introduced in [START_REF] Yamanaka | A parallel algorithm for accurate dot product[END_REF]. It consists in 2 steps. Step 1 applies the SumK algorithm on the local data without the final error compensation for every K iterations. Hence it returns a K-length vector S such that (S j ) j=1,K is the sum of the j th layer in SumK applied to the local subvector. Step 2 gathers these K-length vectors to the master unit and applies the sequential SumK.

Parallel dot "mixed solution". Every n-length entry vector is splitted within P threads (or computing units) and N denotes the length of these local subvectors. The key point is to perform efficient error-free transformations of these N -vectors until the last reduction step. This consists in a 4 step process presented with Fig. 4.1 for P = 2. Steps 1 and 2 are processed by the P threads with local private vectors. Step 1 is similar to the sequential case and produces one vector of size = 2N or 2048 or 4096: TwoProd transforms short N -vectors into a 2None while this latter is not built for larger entries but directly exponent-driven accumulated into the size-length vector as for HybridSum or OnlineExact. Step 2: the size-length vector is distillated (as for iFastSum) into a smaller vector of non overlapping floating-point numbers. Step 3: every thread fuses this small vector into a global shared one. Step 4 is performed by the master thread that computes the correctly rounded result of the global vector with FastAccSum. Let us remark that the small vector issued from Step 2 is at most of length 40 in binary64. Hence the distillation certainly benefits from cache effect. The next fusing step moves accross the computing units these vectors of length 40 in the worst case. This induces a communication over-cost especially for distributed memory environments. Nevertheless it introduces no more reduction step than a classic parallel summation.

The Reproducible Parallel Level 1 BLAS. The reproducible parallel Rasum derives from parallel SumK as in Sect. 3.1. The parallel dot "mixed solution" gives reproducible parallel Rdot and Rnrm2. In practice, the parallel implementation of the Step 1 differs from the sequential one as follows.

For shorter vectors, iFastSum is prefered to FastAccSum to minimize the Step 3 communications. For medium sized vectors, HybridSum is prefered to Online-Exact for Rdot to minimize the Step 2 distillation cost. Otherwise OnlineExact is chosen to minimize the exponent extraction cost.

Test and Results

The experimental framework is unchanged. Each physical core runs at most one thread thanks to the KMP_AFFINITY variable. For every routine, we run from 1 to 16 threads on 16 cores to select the most efficient configurations with respect to the vector size. This optimal number of threads is given in parentheses in Table 4.1 except when it corresponds to the maximum possible ressources [START_REF] Zhu | Correct rounding and hybrid approach to exact floatingpoint summation[END_REF]. Intel MKL's (hidden) choice is denoted with a ⋆. For the next performance comparisons, optimized parallel routines are necessary as references. We use the MKL parallel dot and we implement asum and Our reproducible Rasum compares very well to the optimized asum: the initial 2× overcost tends to 1 for n about 10 6 , see Fig. 4.2a. Compared to the sequential cases and since it operates now on 16× smaller local vectors, our reproducible Rdot and Rnrm2 reach their optimal linear performance for larger entry sizes. Nevertheless the reproducible Rdot runs less than 2× slowler than the MKL reference for vector size up to 10 5 , see Fig. 4.2b. For the same reasons as in the sequential case (Sect. 3.3), our reproducible Rnrm2 is not enough efficient to exhibit the same optimal tendency. Nevertheless the Rnmr2 overhead now reduces to the more convincing ratios compared to nOrm2, see Fig. 4.2c.

Finally our fully accurate reproducible level 1 routines compare quite favourably to those derived from the reproducible FastReprodSum, especially for large vectors: see Fig. 4.2. Those lastest algorithms read twice the entry vector and thus suffer from cache effects for large vectors. It is not the case for our algorithms. On the other hand, the additional computation required by OnlineExact or Hy-bridSum benefit from the floating-point unit availability.

Conclusion and Future Developments

This experimental work illustrates that reproducible level 1 BLAS can be implemented with a reasonable overcost compare to the performance-optimized non-reproducible routines. Moreover our implementations offer full accuracy almost for free compared to the existing reproducible solutions.

Indeed the floating-point peak performance of current machines is far to be exploited by level 1 BLAS. So the additional floating-point operations required by our accuracy enhancement do not significantly increase their execution time.

Of course these results are quantitatively linked to the experimental framework. Nevertheless the same tendencies should be observed in other current computing contexts. Work is ongoing to benefit from FMA within dot and nrm2, to validate an hybrid OpenMP+MPI implementation on larger HPC cluster, to port and optimize this approach to accelerators (as Intel Xeon Phi) and to compare it to the expansions and software long accumulator of [START_REF] Collange | Reproducible and Accurate Matrix Multiplication in ExBLAS for High-Performance Computing[END_REF].

Finally there is alas no reason to be optimistic for the BLAS level 3 where the floating-point units have no space left for extra computation. Reproducible solutions need to be implemented from scratch, for example following [START_REF] Van Zee | BLIS: A Framework for Rapidly Instanciating BLAS Functionality[END_REF].

Fig. 2 . 2 :

 22 Fig. 2.2: Runtime/size for optimized summation algorithms

Fig. 3 . 1 :

 31 Fig. 3.1: Runtime/size for sequential asum, dot and nrm2.

Fig. 4 . 1 :

 41 Fig. 4.1: Parallel dot "mixed solution"

Fig. 4 . 2 :

 42 Fig. 4.2: Runtime/size of parallel level 1 BLAS (up to 16 threads, cond=10 32 )

Table 2 .

 2 1: Experimental framework Figures 2.2a and 2.2b present the runtime measured in cycles divided by the vector size (y-axis). Vector lengths vary between 2 10 and 2 25 (x-axis) and two condition numbers are considered : 10 8 and 10 32 .

	Software
	Compiler	ICC 14.0.2
	Options	-O3 -axCORE-AVX-I -fp-model double -fp-model strict
		-funroll-all-loops
	Parallel library OpenMP 4.0
	BLAS library	Intel MKL 11
	Hardware
	Processor	Xeon E5 2660 (Sandy Bridge) at 2.2 GHz
	Cache	L1: 32KB, L2: 256KB, shared L3 for each socket: 20MB
	Bandwidth	51.2 GB/s
	#cores	2 × 8 cores (hyper-threading disabled)
			1: Declare array C
			2: Declare distance of prefetch
	3: 4: 5: 6: end for exp = exponent(pi) FastTwoSum(C1exp, pi, C1exp, error) C2exp = C2exp + error 7: S = iFastSum(C1 ∪ C2) 8: return S	3: for i in 1:n (Manually unrolled) do 4: prefetch(p i+distance ); 5: exp = exponent(pi) 6: FastTwoSum(C2exp, pi, C2exp, error) 7: C2exp+1 = C2exp+1 + error 8: end for 9: S = iFastSum(C)
		10: return S
	(a) Before optimization	(b) After optimization
	Alg. 2.1: Optimization of algorithm OnlineExact(p, n)

combined to pull out the best implementation of each algorithm. Moreover, some tricks improve the exponent based table access in HybridSum and OnlineExact, see for instance Alg. 2.1 for the latter and

[START_REF] Chohra | Level 1 Parallel RTN-BLAS: Implementation and Efficiency Analysis[END_REF]

for details. 1: Declare arrays C1 and C2 2: for i in 1:n do

Table 4 .

 4 1: Runtime overcost for the reproducibility of parallel level 1 BLAS Our parallel asum runs up to 16 MKL dasum and performs a final reduction. Our parallel nOrm2 derives similarly from the sequential nOrm2 introduced in Sect. 3.3. These implementations exhibit the best performances in Fig.4.2. As in Section 2.3, our implementations of ReprodSum and FastReprodSum are optimized in a fair way using again AVX vectorization, data prefetching and loop unrolling. The latter one is selected for the sequel.We compare our reproducible Rasum, Rdot and Rnrm2, to the optimized but non-reproducible reference implementations, and to the one derived from FastReprodSum. Fig.4.2 and Table4.1 present these results.

	Vector size	10 3	10 4	10 5	10 6	10 7
	Rasum/asum	2.0 (1/1)	1.5 (4/2)	1.3	1.1	1
	Rdot/mkldot	6.4 (8/⋆)	3.8 (8/⋆)	1.6	1.1	1
	Rnrm2/nOrm2	9.1 (8/⋆)	7.1 (8/⋆)	3.4	1.6	1.5
	Rasum/FastReprodasum 0.9 (1/1)	0.9 (4/4)	1.0	0.8	0.5
	Rdot/FastReprodDot	1.5 (8/1)	1.5 (8/8)	0.9	0.7	0.6
	Rnrm2/FastReprodNrm2 1.7 (8/1)	1.5 (8/8)	0.9	0.5	0.4
	nrm2 parallel versions.


χprq ¨Einc prq " Iprq ´iω 0 ´χprq ¨iωµ 0 ż Ḡpr; r 1 q ¨Ipr 1 qdr 1 By MoM

3 ř v "1 χu,v;m,n,pE inc v ;m,n,p " ´1 iω 0 ř m 1 ,n 1 ,p 1 I puq m 1 ,n 1 ,p 1 ψ puq m 1 ,n 1 ,p 1 pr m,n,p q ´3 ř v "1 χu,v;m,n,p 3 ř κ"1 ř p 1 ř m 1 ,n 1 η v κ;p;p 1 ;pm´m 1 q,pn´n 1 q I pκq m 1 ,n 1 ,p 1
By fast Fourier transform (FFT) The techniques for calculating the impedance matrix -1 st method

ξ v κ;p;p 1 " ÿ m 1 ,n 1 η v κ;p;p 1 ;pm´m 1 q,pn´n 1 q I pκq m 1 ,n 1 ,p 1 " IFFT " FFT ! η v κ;p;p 1 ) b FFT " p0q I pκq p 1 ** Ding,
The impedance matrix : η v κ;p;p 1 px , y q " iωµ 0 ş D Gvκ rpx ´x 1 q, py ´y 1 q; zp; z 1 s ψ pκq 0,0,p 1 pr 1 qdr 1 After detouring the integral path to avoid branch cuts or singularites for the integral involving r η v κ;p;p 1 pkx , ky q, the DFT of η 1 v κ;p;p 1 (the windowed version of η v κ;p;p 1 ) can be constructed as

η1 v κ;p;p 1 ;α,β " 1 4π 2 ∆x ∆y exp ´i 2πα Mt∆x xs `i 2πβ Nt∆y ys ť`8 ´8 dσ R x dσ R y r η v κ;p;p 1 " σx pσ R x , σ R y q, σy pσ R x , σ R y q ‰ ˇˇˇˇB pσx , σy q Bpσ R x , σ R y q ˇˇˇˇ# `8 ř l 1 ,l 2 "´8
e i2πrl 1 pxs{∆x q`l 2 pys{∆y qs r w

" 2π ∆x ´α Mt `l1 ¯´σx `σR x , σ R y ˘, 2π ∆y ´β Nt `l2 ¯´σy `σR x , σ R

Padua interpolation-integration technique -calculating fast oscillating integrals

The goal is to compute the I-FT of fast oscillating spectrum in the kx ´ky plane G px , y q " 1 4π 2 8 ij ´8 G0 pkx , ky qe pikx x `iky y q dkx dky Interpolation of the non-oscillating part at the Padua points with Chebyshev's polynomial interpolant Ln G0 pkx , ky q " n ÿ k"0 k ÿ j"0 c j, k´j Tj pkx q Tk´j pky q ´1 2 c n,0 Tn pkx q T 0 pky q with weights c j, k´j computed using 2

Fourier transform of Chebyshev polynomials given by ż 1 ´1 Tnpkx q expp´ikx x q dkx are managed using The Padua points with their generating curve for n " 12 (left, 91 points) and n " 13 (right, 105 points), also as union of two Chebyshev-Lobatto sub-grids (red and blue bullets). Image taken from 5

Fast calculation of EM scattering problems -2 nd method

The Lippman-Schwinger integral formulation E sca prq " iωµ 0 ż Ḡee `r, r 1 ˘¨χ `r1 ˘¨E tot `r1 ˘dr 1

where the contrast function χ prq " ´iω 0 ¨`¯ i ´¯ b ˘ i is the permittivity tensor of an inclusion in the composite medium. ¯ b is the permittivity tensor of the composite medium in the global coordinate system.

The incident field is defined as

E inc prq " iωµ 0 ż Ḡee `r, r 1 ˘¨J 0 `r1 ˘dr 1 " iωµ 0 Ḡee `r, r 1 ˘¨βIl
Asymptotic formulation with polarization tensor -2 nd method

The Lippman-Schwinger integral formulation

When permittivity tensor of the inclusion ¯ i " Ī i and its size is small enough, the scattered field can be derived into the asymptotic formulation.

E sca prq " iωµ 0 Ḡee pr, rmq ¨¯ ¨Einc prmq

The polarization tensor

The polarization tensor in the local coordinate for the inclusion with volume V is :

¯ " ´iω 0 V ¨» - α l 0 0 0 αt 0 0 0 αt fi fl α l " 11 i ´ 11 11 `Ll p i ´ 11 q αt " 22 i ´ 22 22 `Lt p i ´ 22 q
L l and Lt are dependent on the shape of inclusion.

For a cubic inclusion, L l " c arctan `c { ? 1 `2c ˘and Lt " p1 ´Ll q { 2, where c " 11 { 22 6 . The 3 rd case -three scatterers

kxFigure :

 : Figure: Damaged structure with uniaxial dielectric (glass-based) or conductive (graphite-based) multilayers Figure: The transformation between the local and global coordinates by rotation matrix

  .54 `0.46 cos " py ´∆y {2qπ b *

  FIGURE 1. The Padua points with their generating curve for n = 12 (left, 91 points) and n = 13 (right, 105 points), also as union of two Chebyshev-Lobatto subgrids (red and blue bullets).

  Figure:The Padua points with their generating curve for n " 12 (left, 91 points) and n " 13 (right, 105 points), also as union of two Chebyshev-Lobatto sub-grids (red and blue bullets). Image taken from 5

  Figure: The Configuration of the 1 st Case 7

Figure : Formulations1Figure :

 :: Figure: Damaged structure with uniaxial dielectric (glass-based) or conductive (graphite-based) multilayers

FigureFigure :

 : Figure: Influence of the choice of the isosurface

Figure :

 : Figure: Influence of the choice of the isosurface

Figure :

 : Figure: Imaging results by MUSIC for noiseless case (left figure) and 30 dB noisy case (right figure)

FigureFigure :

 : Figure: Influence of the choice of the isosurface

Figure :

 : Figure: Influence of the choice of the isosurface

Ding, Rodeghiero, Zhong, Lambert, Lesselier (L2S) Direct and Inverse Problem in Anisotropic Multilayers ENDE Xi'an June 2014

Configuration of interest

The 1 st case -one scatterer


Julien Heulot
email: jheulot@insa-rennes.fr

Judicaël Menant
email: jmenant@insa-rennes.fr

Maxime Pelcat
email: mpelcat@insa-rennes.fr

Jean-Franc ¸ois Nezan
email: jnezan@insa-rennes.fr

Luce Morin
email: lmorin@insa-rennes.fr

Muriel Pressigout

Slaheddine Aridhi
email: saridhi@ti.com

Demonstrating a Dataflow-based RTOS for Heterogeneous MPSoC by means of a Stereo Matching Application

This demonstration paper presents a multicore Real Time Operating System (RTOS) that schedules a parameterized dataflow Model of Computation (MoC) onto a multicore Digital Signal Processor (DSP) at runtime. This RTOS called Synchronous Parameterized and Interfaced Dataflow Embedded Runtime (SPIDER) exploits the Parameterized and Interfaced Synchronous Dataflow (PiSDF) MoC and its features at runtime to identify locally static regions and to optimize their execution onto multicore platforms. The RTOS is used to dispatch a stereo matching algorithm tasks with a varying range of disparities. The platform used for this demonstration is a Texas Instruments Keystone II Multiprocessor System-on-Chip (MPSoC) device composed of 8 DSP cores, 4 ARM cores, a shared memory subsystem, Multicore Navigator and multiple dedicated accelerators.

I. INTRODUCTION

Limitations in the processing power of each individual Processing Element (PE) caused by size and power consumption considerations is currently leading to the integration of more and more PEs into MPSoC devices such as Texas Instruments' Keystones processors 1 . Concurrently, signal processing applications are becoming increasingly dynamic in terms of hardware resource requirements. This trend is due to the growing complexity of algorithms to meet the target performance required for complex applications. SPIDER runtime presented in this demonstration is an open source project 2 . One of the primary challenges in the design and implementation of multicore signal processing systems is to dispatch computational jobs efficiently onto the available PEs while taking into account dynamic changes in both application functionality and resource requirements. The SPIDER runtime optimizes the multicore scheduling composed of the assignation, the ordering and the timing of the actors on PEs.

To handle these challenges, applications managed by the SPIDER runtime are described using the PiSDF dataflow MoC [START_REF] Desnos | Pimm: Parameterized and interfaced dataflow meta-model for mpsocs runtime reconfiguration[END_REF]. A dataflow MoC decomposes algorithms into pieces of This work is supported by the ANR COMPA project. 1 www.ti.com 2 http://github.com/COMPA-Runtime/COMPA-Runtime computation called actors. These actors exchange data called data tokens through First In, First Out data queues (FIFOs). In embedded systems, one of the most commonly used dataflow MoC is Synchronous DataFlow (SDF) [START_REF] Lee | Synchronous data flow[END_REF]. The PiSDF model is obtained by the utilization of Parameterized and Interfaced dataflow Meta-Model (PiMM) over an SDF graph. The PiMM enhances the SDF by integrating two features: a parameter acyclic graph which transmits control values between actors and an interfaced hierarchical scheme to maintain schedulability over hierarchy exploration [START_REF] Desnos | Pimm: Parameterized and interfaced dataflow meta-model for mpsocs runtime reconfiguration[END_REF]. The SPIDER runtime exploits these features to efficiently extract parallelism, and reduce the overall latency of a dataflow graph execution.

Stereo matching techniques aim to reconstruct depth maps from a pair of images. Embedded vision is becoming very important in many application fields including intelligent vehicle, cartography, civil engineering, medicine or augmented reality applications. The SPIDER runtime enables the reuse of the stereo matching algorithm in MPSoCs irrespective of the nature and the number of computing elements as the algorithm description is independent of the targeted platform. This paper is organized as follows: Section II describes the SPIDER components and Section III details the stereo matching use case. Finally, Section IV presents the demonstrator.

II. SYNCHRONOUS PARAMETERIZED AND INTERFACED DATAFLOW EMBEDDED RUNTIME (SPIDER)

A. Dataflow MoC

The SPIDER runtime is based on a Dataflow MoC. The MoC chosen for this RTOS is the PiSDF due to its good properties on parametrization and hierarchy [START_REF] Desnos | Pimm: Parameterized and interfaced dataflow meta-model for mpsocs runtime reconfiguration[END_REF]. It will demonstrate how the predictability inherited from SDF allows the SPIDER runtime to take relevant and fast scheduling decisions. Parameters are variables integers that influence data production and consumption of actors in the graph. They can be static, constant for the whole execution, or they can be set dynamically by specific actors called configuration actors.

To extract the maximum parallelism from PiSDF, the methodology presented transforms the PiSDF graph into an single rate Synchronous DataFlow (srSDF) graph at runtime once parameters are resolved. An srSDF graph is an SDF graph where production and consumption rates are equal on each edge. This is achieved by replicating the actors which need to be fired more than once, thus ensuring a single execution of each actor of the srSDF graph during a graph iteration. In this way, the scheduler retains a global knowledge of actors dependencies for the entire graph iteration.

Once this srSDF graph has been generated, the scheduler dispatches actors onto the MPSoC. To do so, the process is separated into: ordering and mapping. The ordering task consists of sorting all non-executed actors of the srSDF graph into one list. This list is then used to map actors onto each PE of the MPSoC. Both ordering and mapping tasks may be optimized to reduce different metrics such as: latency, throughput, memory utilization or energy efficiency. The current runtime focuses on execution latency.

B. RTOS Topology

The SPIDER runtime targets heterogeneous platforms. A local decision on actor firing may lead to an inefficient global decision as there may be another PE available for this actor which could have permitted earlier completion of the job. In order to ensure efficient global decisions, a Master/Slave execution scheme is thus preferred for heterogeneous platforms.

The SPIDER runtime uses a PiSDF graph as an input algorithm graph defining parameters that influence algorithm execution. Since configuration actors can be executed on any PE of the MPSoC, it is important to send parameters back to the Master PE. The Master PE then makes scheduling decisions based on these parameter values.

The runtime execution scheme is described in figure 1. A Local RunTime (LRT) is a low footprint operating system that processes actors. A LRT can be implemented over multiple types of PE: general-purpose processor, DSP, accelerator (unsupported for the moment), and so on. The Global RunTime (GRT) is the master of the system. It thus knows the algorithm topology and takes multicore scheduling decisions but can also process actors.

The GRT sends orders to each LRT via a dedicated job queue. A job embeds all data required to execute one instance of an actor. When a parameter is set by a configuration actor, its value is sent to the GRT via a parameter queue. To obtain timing feedbacks on previous and current executions, LRTs sends back actor start and end times through low priority timing FIFOs.

III. STEREO MATCHING USE CASE ALGORITHM

Stereo matching algorithms generate a disparity map from a pair of images by matching pixels from left and right images. This disparity map is representative to a depth map of the scene. For this demonstration, a dense local stereo matching algorithm [START_REF] Mei | On building an accurate stereo matching system on graphics hardware[END_REF] has been selected. For each pixel, an error is computed for all matching possibilities and the disparity with the lowest error is chosen. This algorithm is deterministic, but results in high computational complexity.

The matching error is computed from the correlation of the two pixels (and their neighborhood). This error is then iteratively refined with a bilateral filter. This refinement step has the highest computing cost. It may be noted that since these errors are computed independently, this stereo matching algorithm can be easily parallelized.

As the errors are computed for each matching possibility (each disparity), the total execution time is linear with respect to the disparity range; hence reducing the disparity range significantly decreases the total execution time. In order to optimize the algorithm and reduce its complexity without sacrificing performance, the disparity range can be adjusted in real time using the histogram of the disparity map.

IV. DEMONSTRATOR

The demonstration of the SPIDER runtime will be performed on a Texas Instruments c6636 Keystone II platform. This platform embeds 8 c66x DSP cores and 4 generalpurpose ARM Cortex A-15 cores interconnected by a TeraNet Network-on-Chip. To synchronize the cores, the SPIDER runtime uses the Multicore Navigator. This communication system is composed of 16k hardware queues which send data tokens between LRTs and is also used for the bidirectional GRT LRTs communication for jobs, parameters and timings. To exchange data, the SPIDER runtime allocates memory regions in the 6MB shared L2 (MSMC) memory and DDR memory. One of the 20 shared timers is used for global system monitoring.

A USB stereo camera will be plugged on the board to provide a stereo video source. The resulting disparity map will be sent through the Ethernet port to an assisting computer to be displayed. DIP switches or a web interface will be used to change the disparity range at runtime. Then, the SPIDER runtime will automatically dispatch the computation onto all 12 cores; the schedule being dependent on the disparity range chosen at runtime. The disparity range is an example of PiSDF parameters. One of the 4 ARM PEs will run the GRT while the other cores will run LRTs. A Gantt chart of the current execution will also be displayed on the assisting computer.

Fig. 1 .

 1 Fig. 1. Runtime execution scheme