Davide Frey
email: davide.frey@irisa.fr

Roy Friedman

Achour Mostfaoui
email: achour.mostefaoui@univ-nantes.fr

Matthieu Perrin
email: matthieu.perrin@etu.univ-nantes.fr

Michel Raynal
email: michel.raynal@irisa.fr

Franois Taiani
email: francois.taiani@irisa.fr

D.1.2 -Modular quasi-causal data structures

Keywords: Causal consistency, Sequential Consistency, Eventual Consistency, Scalability, Distributed Computer Systems

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 errorprone distributed specification techniques. In addition existing consistency conditions are usually defined independently from the computing entities (nodes) that manipulate the replicated data; i.e., they do not take into account how computing entities might be linked to one another, or geographically distributed. In this deliverable, we address these issues with two novel contributions. The first contribution proposes a notion of proximity graph between computing nodes. If two nodes are connected in this graph, their operations must satisfy a strong consistency condition, while the operations invoked by other nodes are allowed to satisfy a weaker condition. We use this graph to provide a generic approach to the hybridization of data consistency conditions into the same system. Based on this, we design a distributed algorithm based on this proximity graph, which combines sequential consistency and causal consistency (the resulting condition is called fisheye consistency). The second contribution of this deliverable focuses on improving the limitations of eventual consistency. To this end, we formalize 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.

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 faulttolerance. 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 † . 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] Richard | 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] Richard | PRAM: A scalable shared memory[END_REF] or causality [ANB + 95]. 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.

These weaker consistency models are not a desirable goal in themselves [START_REF] Attiya | A correctness condition for high-performance multiprocessors (extended abstract)[END_REF], but rather an unavoidable compromise to obtain acceptable performance and availability [AW94, Bre00, XSK + 14]. These works try in general to minimize the violations of strong consistency, as these create anomalies for programmers and users. They further emphasize the low probability of such violations in their real deployments [DHJ + 07].

In this deliverable we therefore present two contributions that aim to improve the state of the art of consistency criteria for large-scale geo-replicated systems. The first contribution, published in [START_REF] Friedman | Fisheye consistency: keeping data in synchr in a georeplicated world[END_REF], consists of a hybrid consistency criterion that links the strength of data consistency with the proximity of the participating nodes. The second, published in [START_REF] Perrin | Update consistency for waitfree concurrent objects[END_REF], addresses the limitations of eventual consistency by precisely defining the nature of the converged state.

Motivation and problem statement

Roadmap This deliverable consists of 7 sections. Section 2 introduces the definition of our first contribution, fisheye consistency. Then, Section 3 builds on top of this communication abstraction a distributed algorithm implementing this hybrid proximity-based data consistency condition. Section 4 introduces preliminary notions towards the definition of our second contribution. Section 5 defines the new update-consistency criterion. Section 6 presents a generic construction for any UQ-ADT object with a sequential specification. Finally, Section 7 concludes the document. † We use indifferently participant or process to designate the computing entities that invoke the distributed object.

Fisheye Consistency

In spite of their benefits, the above consistency conditions generally ignore the relative "distance" between nodes in the underlying "infrastructure", where the notions of "distance" and "infrastructure" may be logical or physical, depending on the application. This is unfortunate as distributed systems must scale out and geo-replication is becoming more common. In a georeplicated system, the network latency and bandwidth connecting nearby servers is usually at least an order of magnitude better than what is obtained between remote servers. This means that the cost of maintaining strong consistency among nearby nodes becomes affordable compared to the overall network costs and latencies in the system. Some production-grade systems acknowledge the importance of distance when enforcing consistency, and do propose consistency mechanisms based on node locations in a distributed system (e.g. whether nodes are located in the same or in different data-centers). Unfortunately these production-grade systems usually do not distinguish between semantics and implementation. Rather, their consistency model is defined in operational terms, whose full implications can be difficult to grasp. In Cassandra [START_REF] Lakshman | Cassandra: A decentralized structured storage system[END_REF], for instance, the application can specify for each operation the type of consistency guarantee it desires. For example, the constraints QUO-RUM and ALL require the involvement of a quorum of replicas and of all replicas, respectively; while LOCAL QUORUM is satisfied when a quorum of the local data center is contacted, and EACH QUORUM requires a quorum in each data center. These guarantees are defined by their implementation, but do not provide the programmer with a precise image of the consistency they deliver.

The need to take into account "distance" into consistency models, and the current lack of any formal underpinning to do so are exactly what motivates the hybridization of consistency conditions that we propose in our work (which we call fisheye consistency). Fisheye consistency conditions provide strong guarantees only for operations issued at nearby servers. In particular, there are many applications where one can expect that concurrent operations on the same objects are likely to be generated by geographically nearby nodes, e.g., due to business hours in different time zones, or because these objects represent localized information, etc. In such situations, a fisheye consistency condition would in fact provide global strong consistency at the cost of maintaining only locally strong consistency.

Consider for instance a node A that is "close" to a node B, but "far" from a node C, a causally consistent read/write register will offer the same (weak) guarantees to A on the operations of B, as on the operations of C. This may be suboptimal, as many applications could benefit from varying levels of consistency conditioned on "how far" nodes are from each other. Stated differently: a node can accept that "remote" changes only reach it with weak guarantees (e.g., because information takes time to travel), but it wants changes "close" to it to come with strong guarantees (as "local" changes might impact it more directly).

In this work, we propose to address this problem by integrating a notion of node proximity in the definition of data consistency. To that end, we formally define a new family of hybrid consistency models that links the strength of data consistency with the proximity of the participating nodes. In our approach, a particular hybrid model takes as input a proximity graph, and two consistency conditions, taken from a set of totally ordered consistency conditions, namely a strong one and a weaker one. A classical set of totally ordered conditions is the following one: linearizability, sequential consistency, causal consistency, and PRAM-consistency [START_REF] Richard | PRAM: A scalable shared memory[END_REF]. Moreover, as already said, the notion of proximity can be geographical (cluster-based physical distribution of the nodes), or purely logical (as in some peer-to-peer systems).

The philosophy we advocate is related to that of Parallel Snapshot Isolation (PSI) proposed in [START_REF] Sovran | Transactional storage for geo-replicated systems[END_REF]. PSI combines strong consistency (Snapshot Isolation) for transactions started at nodes in the same site of a geo-replicated system, but only ensures causality among transactions started at different sites. In addition, PSI prevents write-write conflicts by preventing concurrent transactions with conflicting write sets, with the exception of commutable objects.

Although PSI and our work operate at different granularities (fisheye-consistency is expressed on individual operations, each accessing a single object, while PSI addresses general transactions), they both show the interest of consistency conditions in which nearby nodes enjoy stronger semantics than remote ones. In spite of this similitude, however, the family of consistency conditions we propose distinguishes itself from PSI in a number of key dimensions. First, PSI is a specific condition while fisheye-consistency offers a general framework for defining multiple such conditions. PSI only distinguished between nodes at the same physical site and remote nodes, whereas fisheye-consistency accepts arbitrary proximity graphs, which can be physical or logical. Finally, the definition of PSI is given in [START_REF] Sovran | Transactional storage for geo-replicated systems[END_REF] by a reference implementation, whereas fisheyeconsistency is defined in functional terms as restrictions on the ordering of operations that can be seen by applications, independently of the implementation we propose. As a result, we believe that our formalism makes it easier for users to express and understand the semantics of a given consistency condition and to prove the correctness of a program written w.r.t. such a condition.

System Model

The system consists of n processes denoted p 1 , ..., p n . We note Π the set of all processes. Each process is sequential and asynchronous. "Asynchronous" means that each process proceeds at its own speed, which is arbitrary, may vary with time, and remains always unknown to the other processes. Said differently, there is no notion of a global time that could be used by the processes.

Processes communicate by sending and receiving messages through channels. Each channel is reliable (no message loss, duplication, creation, or corruption), and asynchronous (transit times are arbitrary but finite, and remain unknown to the processes). Each pair of processes is connected by a bi-directional channel.

Basic notions and definitions

This section is a short reminder of the fundamental notions typically used to define the consistency guarantees of distributed objects, namely, operation, history, partial order on operations, and history equivalence. Interested readers will find in-depth presentations of these notions in textbooks such as [START_REF] Attiya | Distributed Computing: Fundamentals, Simulations and Advanced Topics[END_REF][START_REF] Herlihy | The Art of Multiprocessor Programming[END_REF][START_REF] Lynch | Distributed Algorithms[END_REF][START_REF] Raynal | Concurrent Programming: Algorithms, Principles, and Foundations[END_REF].

Concurrent objects with sequential specification

A concurrent object is an object that can be simultaneously accessed by different processes. At the application level the processes interact through concurrent objects [START_REF] Herlihy | The Art of Multiprocessor Programming[END_REF][START_REF] Raynal | Concurrent Programming: Algorithms, Principles, and Foundations[END_REF]. Each object is defined by a sequential specification, which is a set including all the correct sequences of operations and their results that can be applied to and obtained from the object. These sequences are called legal sequences.

Execution history

The execution of a set of processes interacting through objects is captured by a history Ĥ = (H,→ H ), where → H is a partial order on the set H of the object operations invoked by the processes.

Concurrency and sequential history

If two operations are not ordered in a history, they are said to be concurrent. A history is said to be sequential if it does not include any concurrent operations. In this case, the partial order → H is a total order.

Equivalent history

Let Ĥ p represent the projection of Ĥ onto the process p, i.e., the restriction of Ĥ to operations occurring at process p. Two histories Ĥ1 and Ĥ2 are equivalent if no process can distinguish them, i.e., ∀p ∈ Π ∶ Ĥ1 p = Ĥ2 p.

Legal history Ĥ being a sequential history, let Ĥ X represent the projection of Ĥ onto the object X. A history Ĥ is legal if, for any object X, the sequence Ĥ X belongs to the specification of X.

Process Order Notice that since we assumed that processes are sequential, in the following, we restrict the discussion to execution histories Ĥ for which for every process p, Ĥ p is sequential. This total order is also called the process order for p.

The Family of Fisheye Consistency Conditions

This section introduces a hybrid consistency model based on (a) two consistency conditions and (b) the notion of a proximity graph defined on the computing nodes (processes). The two consistency conditions must be totally ordered in the sense that any execution satisfying the stronger one also satisfies the weaker one. Linearizability and SC define such a pair of consistency conditions, and similarly SC and CC are such a pair.

The notion of a proximity graph

Let us assume that for physical or logical reasons linked to the application, each process (node) can be considered either close to or remote from other processes. This notion of "closeness" can be captured trough a proximity graph denoted G = (Π,E G ⊆ Π × Π), whose vertices are the n processes of the system (Π). The edges are undirected. N G (p i ) denotes the neighbors of p i in G.

The aim of G is to state the level of consistency imposed on processes in the following sense: the existence of an edge between two processes in G imposes a stronger data consistency level than between processes not connected in G.

Example

To illustrate the semantic of G, we extend the original scenario that Ahamad, Niger et al use to motivate causal consistency in [ANB + 95]. Consider the three processes of Figure 1, paris, berlin, and new-york. Processes paris and berlin interact closely with one another and behave symmetrically : they concurrently write the shared variable X, then set the flags R and S respectively to 1, and finally read X. By contrast, process new-york behaves sequentially w.r.t. paris and berlin: new-york waits for paris and berlin to write on X, using the flags R and S, and then writes X.

process paris is X ← 1 R ← 1 a ← X end process process berlin is X ← 2 S ← 1 b ← X end process process new-york is repeat c ← R until c = 1 repeat d ← S until d = 1 X ← 3 end process
Figure 1: new-york does not need to be closely synchronized with paris and berlin, calling for a hybrid form of consistency If we assume a model that provides causal consistency at a minimum, the write of X by new-york is guaranteed to be seen after the writes of paris and berlin by all processes (because new-york waits on R and S to be set to 1). Causal consistency however does not impose any consistent order on the writes of paris and berlin on X. In the execution shown on Figure 2, this means that although paris reads 2 in X (and thus sees the write of berlin after its own write), berlin might still read 1 in b (thus perceiving 'X.write(1)' and 'X.write(2)' in the opposite order to that of paris).

Sequential consistency removes this ambiguity: in this case, in Figure 2, berlin can only read 2 (the value it wrote) or 3 (written by new-york), but not 1. Sequential consistency is however too strong here: because the write operation of new-york is already causally ordered with those of paris and berlin, this operation does not need any additional synchronization effort. This situation can be seen as an extension of the write concurrency freedom condition introduced in [ANB + 95]: new-york is here free of concurrent write w.r.t. paris and berlin, making causal consistency equivalent to sequential consistency for new-york. paris and berlin however write to X concurrently, in which case causal consistency is not enough to ensure strongly consistent results.

If we assume paris and berlin execute in the same data center, while new-york is located on a distant site, this example illustrates a more general case in which, because of a program's logic or activity patterns, no operations at one site ever conflict with those at another. In such a situation, rather than enforce a strong (and costly) consistency in the whole system, we propose a form of consistency that is strong for processes within the same site (here paris and berlin), but weak between sites (here between paris,berlin on one hand and new-york on the other).

In our model, the synchronization needs of individual processes are captured by the proximity graph G introduced at the start of this section and shown in Figure 3: paris and berlin are connected, meaning the operations they execute should be perceived as strongly consistent w.r.t. one another ; new-york is neither connected to paris nor berlin, meaning a weaker consistency is allowed between the operations executed at new-york and those of paris and berlin.

Fisheye consistency for the pair (sequential consistency, causal consistency)

When applied to the scenario of Figure 2, fisheye consistency combines two consistency conditions (a strong and a weaker one, here causal and sequential consistency) and a proximity graph to form an hybrid distance-based consistency condition, which we call G-fisheye (SC,CC)-consistency.

The intuition in combining SC and CC is to require that (write) operations be observed in the same order by all processes if:

• They are causally related (as in causal consistency),

• Or they occur on "close" nodes (as defined by G).

Formal definition Formally, we say that a history Ĥ is G-fisheye (SC,CC)-consistent if:

• There is a causal order ↝ H induced by Ĥ (as in causal consistency); and p op 1 p : X.write(2) op 2 p : Y .write(4) q op 1 q : X.write(3) op 2 q : Y .read→4 op 3 q : Y .read→5

-(c) respects ★ ↝ H,G , i.e., ( ★ ↝ H,G ) (p i +W ) ⊆ (→ S i ).
If we apply this definition to the example of Figure 2 with the proximity graph proposed in Figure 3 we obtain the following: because paris and berlin are connected in G, X.write(1) by paris and X.write(2) by berlin must be totally ordered in ★ ↝ H,G (and hence in any sequential history Ŝi perceived by any process p i ). X.write(3) by new-york must be ordered after the writes on X by paris and berlin because of the causality imposed by ↝ H . As a result, if the system is G-fisheye (SC,CC)-consistent, b? can be equal to 2 or 3, but not to 1. This set of possible values is as in sequential consistency, with the difference that G-fisheye (SC,CC)-consistency does not impose any total order on the operation of new-york.

Given a system of n processes, let ∅ denote the graph G with no edges, and K denote the graph G with an edge connecting each pair of distinct processes. It is easy to see that CC is ∅-fisheye (SC,CC)-consistency. Similarly SC is K-fisheye (SC,CC)-consistency.

A larger example Figure 4 and Table 1 illustrate the semantic of G-fisheye (SC,CC) consistency on a second, larger, example. In this example, the processes p and q on one hand, and r and s on the other hand, are neighbors in the proximity graph G (shown on the left). There are two pairs of write operations: op 1 p and op 1 q on the register X, and op 2 p and op 3 r on the register Y . In a sequentially consistency history, both pairs of writes must be seen in the same order by all processes. As a consequence, if r sees the value 2 first (op 1 r ) and then the value 3 (op 2 r ) for X, s must do the same, and only the value 3 can be returned by x?. For the same reason, only the value 3 can be returned by y?, as shown in the first line of Table 1.

In a causally consistent history, however, both pairs of writes ({op 1 p ,op 1 q } and {op 2 p ,op 3 r }) are causally independent. As a result, any two processes can see each pair in different orders. x? may return 2 or 3, and y? 4 or 5 (second line of Table 1).

G-fisheye (SC,CC)-consistency provides intermediate guarantees: because p and q are neighbors in G, op 1 p and op 1 q must be observed in the same order by all processes. x? must return 3, as in a sequentially consistent history. However, because p and r are not connected in G, op 2 p and op

Implementing Fisheye Consistency

Our implementation of G-fisheye (SC,CC)-consistency relies on a broadcast operation with hybrid ordering guarantees. In this section, we present this hybrid broadcast abstraction, before moving on the actual implementation of of G-fisheye (SC,CC)-consistency in Section 3.3.

G-fisheye (SC,CC)-broadcast: definition

The hybrid broadcast we proposed, denoted G-(SC,CC)-broadcast, is parametrized by a proximity graph G which determines which kind of delivery order should be applied to which messages, according to the position of the sender in the graph G. Messages (SC,CC)-broadcast by processes which are neighbors in G must be delivered in the same order at all the processes, while the delivery of the other messages only need to respect causal order.

The (SC,CC)-broadcast abstraction provides the processes with two operations, denoted TOCO broadcast() and TOCO deliver(). We say that messages are toco-broadcast and tocodelivered.

Causal message order. Let M be the set of messages that are toco-broadcast. The causal message delivery order, denoted ↝ M , is defined as follows [START_REF] Birman | Reliable communication in the presence of failures[END_REF][START_REF] Raynal | The causal ordering abstraction and a simple way to implement it[END_REF]. Let m 1 ,m 2 ∈ M; m 1 ↝ M m 2 , iff one of the following conditions holds:

• m 1 and m 2 have been toco-broadcast by the same process, with m 1 first;

• m 1 was toco-delivered by a process p i before this process toco-broadcast m 2 ;

• There exists a message m such that

(m 1 ↝ M m) ∧ (m ↝ M m 2 ).
Definition of the G-fisheye (SC,CC)-broadcast. The (SC,CC)-broadcast abstraction is defined by the following properties.

• Validity. If a process toco-delivers a message m, this message was toco-broadcast by some process. (No spurious message.)

• Integrity. A message is toco-delivered at most once. (No duplication.)

• G-delivery order. For all the processes p and q such that (p,q) is an edge of G, and for all the messages m p and m q such that m p was toco-broadcast by p and m q was toco-broadcast by q, if a process toco-delivers m p before m q , no process toco-delivers m q before m p .

• Causal order. If m 1 ↝ M m 2 , no process toco-delivers m 2 before m 1 .

• Termination. If a process toco-broadcasts a message m, this message is toco-delivered by all processes.

It is easy to see that if G has no edges, this definition boils down to causal delivery, and if G is fully connected (clique), this definition specifies total order delivery respecting causal order. Finally, if G is fully connected and we suppress the "causal order" property, the definition boils to total order delivery.

3.2 G-fisheye (SC,CC)-broadcast: algorithm

Local variables.

To implement the G-fisheye (SC,CC)-broadcast abstraction, each process p i manages three local variables.

• causal i [1.

.n] is a local vector clock used to ensure a causal delivery order of the messages; causal i [ j] is the sequence number of the next message that p i will toco-deliver from p j .

• total i [1.

.n] is a vector of logical clock values such that total i [i] is the local logical clock of p i (Lamport's clock), and total i [ j] is the value of total j [ j] as known by p i .

• pending i is a set containing the messages received and not yet toco-delivered by p i .

Description of the algorithm.

Let us remind that for simplicity, we assume that the channels are FIFO. Algorithm 1 describes the behavior of a process p i . This behavior is decomposed into four parts.

The first part (lines 1-6) is the code of the operation TOCO broadcast(m). Process p i first increases its local clock total i [i] and sends the protocol message TOCOBC(m, ⟨causal i [⋅],total i [i],i⟩) to each other process. In addition to the application message m, this protocol message carries the control information needed to ensure the correct toco-delivery of m, namely, the local causality vector (causal i [1..n]), and the value of the local clock (total i [i]). Then, this protocol message is added to the set pending i and causal i [i] is increased by 1 (this captures the fact that the future application messages toco-broadcast by p i will causally depend on m).

The second part (lines 7-14) is the code executed by p i when it receives a protocol message TOCOBC(m,⟨s caus m j [⋅], s tot m j , j⟩) from p j . When this occurs p i adds first this protocol message to pending i , and updates its view of the local clock of p j (total i [ j]) to the sending date of the protocol message (namely, s tot m j ). Then, if the local clock of p i is late (total i [i] ≤ s tot m j ), p i catches up (line 11), and informs the other processes of it (line 12).

The third part (lines 15-17) is the processing of a catch up message from a process p j . In this case, p i updates its view of p j 's local clock to the date carried by the catch up message. Let us notice that, as channels are FIFO, a view stotal i [ j] can only increase.

The final part (lines 18-31) is a background task executed by p i , where the application messages are toco-delivered. The set C contains the protocol messages that were received, have not yet been toco-delivered, and are "minimal" with respect to the causality relation ↝ M . This minimality is determined from the vector clock s caus m j [1.

.n], and the current value of p i 's vector clock (causal i [1..n]). If only causal consistency was considered, the messages in C could be delivered.

Then, p i extracts from C the messages that can be toco-delivered. Those are usually called stable messages. The notion of stability refers here to the delivery constraint imposed by the proximity graph G. More precisely, a set T 1 is first computed, which contains the messages of C that (thanks Algorithm 1 The G-fisheye (SC,CC)-broadcast algorithm executed by p i

1: operation TOCO broadcast(m) 2: total i [i] ← total i [i] + 1 3: for all p j ∈ Π ∖ {p i } do send TOCOBC(m, ⟨causal i [⋅],total i [i],i⟩) to p j 4: pending i ← pending i ∪ ⟨m,⟨causal i [⋅],total i [i],i⟩⟩ 5: causal i [i] ← causal i [i] +
for all p k ∈ Π ∖ {p i } do send CATCH UP(total i [i],i) to p k 13:
end if 14: end on receiving 15: on receiving CATCH UP(last date j , j) wait until T 1 ≠ ∅ where 23:

T 1 ≡ ⟨m,⟨s caus m j [⋅],s tot m j , j⟩⟩ ∈ C ∀p k ∈ N G (p j ) ∶ ⟨total i [k],k⟩ > ⟨s tot m j , j⟩ 24:
wait until T 2 ≠ ∅ where 25:

T 2 ≡ ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ⟨m,⟨s caus m j [⋅],s tot m j , j⟩⟩ ∈ T 1 ∀p k ∈ N G (p j ), ∀⟨m k ,⟨s caus m k k [⋅],s tot m k k ,k⟩⟩ ∈ pending i ∶ ⟨s tot m k k ,k⟩ > ⟨s tot m j , j⟩ ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ 26: ⟨m 0 ,⟨s caus m 0 j 0 [⋅],s tot m 0 j 0 , j 0 ⟩⟩ ← argmin ⟨m,⟨s caus m j [⋅],s tot m j , j⟩⟩∈T 2
⟨s tot m j , j⟩ 27:

pending i ← pending i ∖ ⟨m 0 ,⟨s caus m 0 j 0 [⋅],s tot m j , j 0 ⟩⟩ 28:
TOCO deliver(m 0 ) to application layer 29:

if j 0 ≠ i then causal i [ j 0 ] ← causal i [ j 0 ] + 1 end if ▷ for causal i [i] see line 5 30:
end loop forever 31: end background task to the FIFO channels and the catch up messages) cannot be made unstable (with respect to the total delivery order defined by G) by messages that p i will receive in the future. Then the set T 2 is computed, which is the subset of T 1 such that no message received, and not yet toco-delivered, could make incorrect -w.r.t. G -the toco-delivery of a message of T 2 .

Once a non-empty set T 2 has been computed, p i extracts the message m whose timestamp ⟨s tot m j [ j], j⟩ is "minimal" with respect to the timestamp-based total order (p j is the sender of m). This message is then removed from pending i and toco-delivered. Finally, if j ≠ i, causal i [ j] is increased to take into account this toco-delivery (all the messages m ′ toco-broadcast by p i in the future will be such that m ↝ m ′ , and this is encoded in causal i [ j]). If j = i, this causality update was done at line 5.

Theorem 1. Algorithm 1 implements a G-fisheye (SC,CC)-broadcast.

Proof of Theorem 1

The proof combines elements of the proofs of the traditional causal-order [BSS91, RST91] and total-order broadcast algorithms [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF][START_REF] Attiya | Sequential consistency versus linearizability[END_REF] on which Algorithm 1 is based. It relies in particular on the monoticity of the clocks causal i [1..n] and total i [1..n], and the reliability and FIFO properties of the underlying communication channels. We first prove some useful lemmata, before proving termination, causal order, and G-delivery order in intermediate theorems. We finally combine these intermediate results to prove Theorem 1.

We use the usual partial order on vector clocks:

C 1 [⋅] ≤ C 2 [⋅] iff ∀p i ∈ Π ∶ C 1 [i] ≤ C 2 [i]
with its accompanying strict partial order:

C 1 [⋅] < C 2 [⋅] iff C 1 [⋅] ≤ C 2 [⋅] ∧C 1 [⋅] ≠ C 2 [⋅]
We use the lexicographic order on the scalar clocks ⟨s tot j , j⟩:

⟨s tot j , j⟩ < ⟨s tot i ,i⟩ iff (s tot j < s tot i ) ∨ (s tot j = s tot i ∧ i < j)
We start by three useful lemmata on causal i [⋅] and total i [⋅]. These lemmata establish the traditional properties expected of logical and vector clocks.

Lemma 1. The following holds on the clock values taken by causal i [⋅]:

1. The successive values taken by causal i [⋅] in Process p i are monotonically increasing.

The sequence of causal i [⋅]

values attached to TOCOBC messages sent out by Process p i are strictly increasing.

Proof Proposition 1 is derived from the fact that the two lines that modify causal i [⋅] (lines 5, and 29) only increase its value. Proposition 2 follows from Proposition 1 and the fact that line 5 insures successive TOCOBC messages cannot include identical causal i

[i] values. ◻ Lemma 1
Lemma 2. The following holds on the clock values taken by total i [⋅]:

1. The successive values taken by total i [i] in Process p i are monotonically increasing.

2. The sequence of total i [i] values included in TOCOBC and CATCH UP messages sent out by Process p i are strictly increasing.

The successive values taken by total i [⋅]

in Process p i are monotonically increasing.

Proof Proposition 1 is derived from the fact that the lines that modify total i [i] (lines 2 and 11) only increase its value (in the case of line 11 because of the condition at line 10). Proposition 2 follows from Proposition 1, and the fact that lines 2 and 11 insures successive TOBOBC and CATCH UP messages cannot include identical total i [i] values.

To prove Proposition 3, we first show that:

∀ j ≠ i ∶ the successive values taken by total i [ j] in p i are monotonically increasing.

(1)

For j ≠ i, total i [ j] can only be modified at lines 9 and 16, by values included in TOBOBC and CATCH UP messages, when these messages are received. Because the underlying channels are FIFO and reliable, Proposition 2 implies that the sequence of last date j and s tot m j values received by p i from p j is also strictly increasing, which shows equation (1).

From equation (1) and Proposition 1, we conclude that the successive values taken by the vector total i [⋅] in p i are monotonically increasing (Proposition 3).

◻ Lemma 2 Lemma 3. Consider an execution of the protocol. The following invariant holds: for i ≠ j, if m is a message sent from p j to p i , then at any point of p i 's execution outside of lines 28-29, s caus m j [ j] < causal i [ j] iff that m has been toco-delivered by p i .

Proof

We first show that if m has been toco-delivered by p i , then s caus m j [ j] < causal i [ j], outside of lines 28-29. This implication follows from the condition s caus m j [⋅] ≤ causal i [⋅] at line 21, and the increment at line 29.

We prove the reverse implication by induction on the protocol's execution by process p i . When

p i is initialized causal i [⋅] is null: causal 0 i [⋅] = [0⋯0] (2)
because the above is true of any process, with Lemma 2, we also have

s caus m j [⋅] ≥ [0⋯0] (3)
for all message m that is toco-broadcast by Process p j .

(2) and (3) imply that there are no messages sent by p j so that s caus m j [ j] < causal 0 i [ j], and the Lemma is thus true when p i starts.

Let us now assume that the invariant holds at some point of the execution of p i . The only step at which the invariant might become violated in when causal i [ j 0 ] is modified for j 0 ≠ i at line 29. When this increment occurs, the condition s caus m j 0 [ j 0 ] < causal i [ j 0 ] of the lemma potentially becomes true for additional messages. We want to show that there is only one single additional message, and that this message is m 0 , the message that has just been delivered at line 28, thus completing the induction, and proving the lemma. For clarity's sake, let us denote causal ○ i [ j 0 ] the value of causal i [ j 0 ] just before line 29, and causal • i [ j 0 ] the value just after. We have causal

• i [ j 0 ] = causal ○ i [ j 0 ] + 1. We show that s caus m 0 j 0 [ j o ] = causal ○ i [ j 0 ], where s caus m 0 j 0 [⋅]
is the causal timestamp of the message m 0 delivered at line 28. Because m 0 is selected at line 26, this implies that

m 0 ∈ T 2 ⊆ T 1 ⊆ C. Because m 0 ∈ C, we have s caus m 0 j 0 [⋅] ≤ causal ○ i [⋅] (4)
at line 21, and hence s caus

m 0 j 0 [ j 0 ] ≤ causal ○ i [ j 0 ] (5)
At line 21, m 0 has not been yet delivered (otherwise it would not be in pending i ). Using the contrapositive of our induction hypothesis, we have

s caus m 0 j 0 [ j 0 ] ≥ causal ○ i [ j 0 ] (6)
(5) and ( 6) yield s caus

m 0 j 0 [ j 0 ] = causal ○ i [ j 0 ] (7)
Because of line 5, m 0 is the only message tobo broadcast by P j 0 whose causal timestamp verifies (7). From this unicity and (7), we conclude that after causal i [ j 0 ] has been incremented at line 29, if a message m sent by

P j 0 verifies s caus m j 0 [ j 0 ] < causal • i [ j 0 ], then • either s caus m j 0 [ j 0 ] < causal • i [ j 0 ] -1 = causal ○ i [ j 0 ],
and by induction assumption, m has already been delivered;

• or s caus m j 0 [ j 0 ] = causal • i [ j 0 ] -1 < causal ○ i [ j 0 ]
, and m = m 0 , and m has just been delivered at line 28.

◻ Lemma 3

Termination

Theorem 2. All messages toco-broadcast using Algorithm 1 are eventually toco-delivered by all processes in the system. Proof We show Termination by contradiction. Assume a process p i toco-broadcasts a message m i with timestamp ⟨s caus m i i [⋅],s tot m i i ,i⟩, and that m i is never toco-delivered by p j . If i ≠ j, because the underlying communication channels are reliable, p j receives at some point the TOCOBC message containing m i (line 7), after which we have

⟨m i ,⟨s caus m i i [⋅],s tot m i i ,i⟩⟩ ∈ pending j (8)
If i = j, m i is inserted into pending i immediately after being toco-broadcast (line 4), and (8) also holds.

m i might never be toco-delivered by p j because it never meets the condition to be selected into the set C of p j (noted C j below) at line 21. We show by contradiction that this is not the case. First, and without loss of generality, we can choose m i so that it has a minimal causal timestamp s caus m i i [⋅] among all the messages that j never toco-delivers (be it from p i or from any other process). Minimality means here that

∀m x , p j never delivers m x ⇒ ¬(s caus m x x < s caus m i i ) (9)
Let us now assume m i is never selected into C j , i.e., we always have

¬(s caus m i i [⋅] ≤ causal j [⋅]) (10)
This means there is a process p k so that

s caus m i i [k] > causal j [k] (11)
If i = k, we can consider the message m ′ i sent by i just before m i (which exists since the above implies s caus m i i [i] > 0). We have s caus

m ′ i i [i] = s caus m i i [i]
-1, and hence from (11) we have

s caus m ′ i i [i] ≥ causal j [k] (12)
Applying Lemma 3 to [START_REF]BZP +[END_REF] implies that p j never toco-delivers m ′ i either, with s caus

m ′ i i [i] < s caus m i i [i]
(by way of Proposition 2 of Lemma 1), which contradicts (9). If i ≠ k, applying Lemma 3 to causal i [⋅] when p i toco-broadcasts m i at line 3, we find a message m k sent by p k with s caus

m k k [k] = s caus m i i [k]
-1 such that m k was received by p i before p i toco-broadcast m i . In other words, m k belongs to the causal past of m i , and because of the condition on C (line 21) and the increment at line 29, we have

s caus m k k [⋅] < s caus m i i [⋅] (13)
As for the case i = k, (11) also implies

s caus m k k [k] ≥ causal j [k] (14)
which with Lemma 3 implies that that p j never delivers the message m k from p k , and with (13) contradicts m i 's minimality (9).

We conclude that if a message m i from p i is never toco-delivered by p j , after some point m i remains indefinitely in C j m i ∈ C j (15)

Without loss of generality, we can now choose m i with the smallest total order timestamp ⟨s tot m i i ,i⟩ among all the messages never delivered by p j . Since these timestamps are totally ordered, and no timestamp is allocated twice, there is only one unique such message.

We first note that because channels are reliable, all processes p k ∈ N G (p i ) eventually receive the TOCOBC protocol message of p i that contains m i (line 7 and following). Lines 10-11 together with the monotonicity of total k [k] (Proposition 1 of Lemma 2), insure that at some point all processes p k have a timestamp total k [k] strictly larger than s tot m i i :

∀p k ∈ N G (p i ) ∶ total k [k] > s tot m i i ( 16
)
Since all changes to total k [k] are systematically rebroadcast to the rest of the system using TO-COBC or CATCHUP protocol messages (lines 2 and 11), p j will eventually update total j [k] with a value strictly higher than s tot m i i . This update, together with the monotonicity of total j [⋅] (Proposition 3 of Lemma 2), implies that after some point:

∀p k ∈ N G (p i ) ∶ total j [k] > s tot m i i (17)
and that m i is selected in T j 1 . We now show by contradiction that m i eventually progresses to T j 2 . Let us assume m i never meets T j 2 's condition. This means that every time T j 2 is evaluated we have:

∃p k ∈ N G (p i ),∃⟨m k ,⟨s caus m k k [⋅],s tot m k k ,k⟩⟩ ∈ pending j ∶ ⟨s tot m k k ,k⟩ ≤ ⟨s tot m i ,i⟩ (18)
Note that there could be different p k and m k satisfying (18) in each loop of Task T . However, because N G (p i ) is finite, the number of timestamps ⟨s tot m k k ,k⟩ such that ⟨s tot m k k ,k⟩ ≤ ⟨s tot m i ,i⟩ is also finite. There is therefore one process p k 0 and one message m k 0 that appear infinitely often in the sequence of (p k ,m k ) that satisfy (18). Since m k 0 can only be inserted once into pending j , this means m k 0 remains indefinitely into T j 2 , and hence pending j , and is never delivered. (18) and the fact that i ≠ k 0 (because

p i ∈ N G (p i )) yields ⟨s tot m k 0 k ,k 0 ⟩ < ⟨s tot m i ,i⟩ (19)
which contradicts our assumption that m i has the smallest total order timestamps ⟨s tot m i i ,i⟩ among all messages never delivered to p j . We conclude that after some point m i remains indefinitely into T j 2 .

m i ∈ T j 2 (20)
If we now assume m i is never returned by argmin at line 26, we can repeat a similar argument on the finite number of timestamps smaller than ⟨s tot m i ,i⟩, and the fact that once they have been removed form pending j (line 27), messages are never inserted back, and find another message m k with a strictly smaller time-stamp that p j that is never delivered. The existence of m k contradicts again our assumption on the minimality of m i 's timestamp ⟨s tot m i ,i⟩ among undelivered messages.

This shows that m i is eventually delivered, and ends our proof by contradiction.

◻ T heorem 2

Causal Order We prove the causal order property by induction on the causal order relation ↝ M .

Lemma 4. Consider m 1 and m 2 , two messages toco-broadcast by Process p i , with m 1 tocobroadcast before m 2 . If a process p j toco-delivers m 2 , then it must have toco-delivered m 1 before m 2 .

Proof We first consider the order in which the messages were inserted into pending j (along with their causal timestamps s caus m 1 2 i

). For i = j, m 1 was inserted before m 2 at line 4 by assumption. For i ≠ j, we note that if p j delivers m 2 at line 28, then m 2 was received from p i at line 7 at some earlier point. Because channels are FIFO, this also means m 1 was received and added to pending j before m 2 was.

(

) 21
We now want to show that when m 2 is delivered by p j , m 1 is no longer in pending j , which will show that m 1 has been delivered before m 2 . We use an argument by contradiction. Let us assume that ⟨m 1 ,⟨s caus m 1 i ,s tot m 1 i ,i⟩⟩ ∈ pending j

at the start of the iteration of Task T which delivers m 2 to p j . From Proposition 2 of Lemma 1, we have

s caus m 1 i < s caus m 2 i ( 23
)
which implies that m 1 is selected into C along with m 2 (line 21):

⟨m 1 ,⟨s caus m 1 i ,s tot m 1 i ,i⟩⟩ ∈ C
Similarly, from Proposition 2 of Lemma 2 we have:

s tot m 1 i < s tot m 2 i ( 24
)
which implies that m 1 must also belong to T 1 and T 2 (lines 23 and 25). ( 24) further implies that ⟨s tot m 2 i ,i⟩ is not the minimal s tot timestamp of T 2 , and therefore m 0 ≠ m 2 in this iteration of Task T . This contradicts our assumption that m 2 was delivered in this iteration; shows that (22) must be false; and therefore with (21) that m 1 was delivered before m 2 .

◻ Lemma 4

Lemma 5. Consider m 1 and m 2 so that m 1 was toco-delivered by a process p i before p i tocobroadcasts m 2 . If a process p j toco-delivers m 2 , then it must have toco-delivered m 1 before m 2 .

Proof Let us note p k the process that has toco-broadcast m 1 . Because m 2 is toco-broadcasts by p i after p i toco-delivers m 1 and increments causal i [k] at line 29, we have, using Lemma 3 and Proposition 1 of Lemma 1:

s caus m 1 k [k] < s caus m 2 i [k] (25)
Because of the condition on set C at line 21, when p j toco-delivers m 2 at line 28, we further have

s caus m 2 i [⋅] ≤ causal j [⋅] (26)
and hence using (25)

s caus m 1 k [k] < s caus m 2 i [k] ≤ causal j [k] (27)
Applying Lemma 3 to (27), we conclude that p j must have toco-delivered m 1 when it delivers m 2 .

◻ Lemma 5

Theorem 3. Algorithm 1 respects causal order.

Proof We finish the proof by induction on ↝ M . Let's consider three messages m 1 , m 2 , m 3 such that

m 1 ↝ M m 3 ↝ M m 2 (28)
and such that:

• if a process toco-delivers m 3 , it must have toco-delivered m 1 ;

• if a process toco-delivers m 2 , it must have toco-delivered m 3 ;

We want to show that if a process toco-delivers m 2 , it must have tolo-delivered m 1 . This follows from the transitivity of temporal order. This result together with Lemmas 4 and 5 concludes the proof.

◻ T heorem 3 G-delivery order Theorem 4. Algorithm 1 respects G-delivery order.

Proof Let's consider four processes p l , p h , p i , and p j . p l and p h are connected in G. p l has tocobroadcast a message m l , and p h has toco-broadcast a message m h . p i has toco-delivered m l before m h . p j has toco-delivered m h . We want to show that p j has toco-delivered m l before m h .

We first show that:

⟨s tot m h h ,h⟩ > ⟨s tot m l l ,l⟩ (29)
We do so by considering the iteration of the background task T (lines 18-18) of p i that toco-delivers m l . Because p h ∈ N G (p l ), we have

⟨total i [h],h⟩ > ⟨s tot m l l ,l⟩ (30)
at line 23.

If m h has not been received by p i yet, then because of Lemma 3.2, and because communication channels are FIFO and reliable, we have:

⟨s tot m h h ,l⟩ > ⟨total i [h],h⟩ (31)
which with (30) yields (29).

If m h has already been received by p i , by assumption it has not been toco-delivered yet, and is therefore in pending i . More precisely we have:

⟨m h ,⟨s caus m h h [⋅],s tot m h h ,h⟩⟩ ∈ pending i (32)
which, with p h ∈ N G (p l ), and the fact that m l is selected in T i 2 at line 25 also gives us (29). We now want to show that p j must have toco-delivered m l before m h . The reasoning is somewhat the symmetric of what we have done. We consider the iteration of the background task T of p j that toco-delivers m h . By the same reasoning as above we have

⟨total j [l],l⟩ > ⟨s tot m h h ,h⟩ (33)
at line 23.

Because of Lemma 3.2, and because communication channels are FIFO and reliable, (33) and (29) imply that m l has already been received by p j . Because m h is selected in T j 2 at line 25, (29) implies that m h is no longer in pending j , and so must have been toco-delivered by p j earlier, which concludes the proof.

◻ T heorem 4

Theorem 1. Algorithm 1 implements a G-fisheye (SC,CC)-broadcast.

Proof

• Validity and Integrity follow from the integrity and validity of the underlying communication channels, and from how a message m j is only inserted once into pending i (at line 4 if i = j, at line 8 otherwise) and always removed from pending i at line 27 before it is toco-delivered by p i at line 28;

• G-delivery order follows from Theorem 4;

• Causal order follows from Theorem 3;

• Termination follows from Theorem 2.

◻ T heorem 1 3.3 An Algorithm Implementing G-Fisheye (SC,CC)-Consistency

The high level object operations read and write

Algorithm 2 uses the G-fisheye (SC,CC)-broadcast we have just presented to realized G-fisheye (SC,CC)-consistency using a fast-read strategy. This algorithm is derived from the fast-read algorithm for sequential consistency proposed by Attiya and Welch [START_REF] Attiya | Sequential consistency versus linearizability[END_REF], in which the total order broadcast has been replaced by our G-fisheye (SC,CC)-broadcast.

The write(X,v) operation uses the G-fisheye (SC,CC)-broadcast to propagate the new value of the variable X. To insure any other write operations that must be seen before write(X,v) by p i are Algorithm 2 Implementing G-fisheye (SC,CC)-consistency, executed by p i 1: operation X.write(v)

2:

TOCO broadcast(WRITE(X,v,i)) if (i = j) then delivered i ← true endif 12: end on toco deliver properly processed, p i enters a waiting loop (line 4), which ends after the message WRITE(X ,v,i) that has been toco-broadcast at line 2 is toco-delivered at line 11.

The read(X) operation simply returns the local copy v x of X. These local copies are updated in the background when WRITE(X ,v, j) messages are toco-delivered.

Theorem 5. Algorithm 2 implements G-fisheye (SC,CC)-consistency.

Proof of Theorem 5

The proof uses the causal order on messages ↝ M provided by the G-fisheye (SC,CC)-broadcast to construct the causal order on operations ↝ H . It then gradually extends ↝ H to obtain ★ ↝ H,G . It first uses the property of the broadcast algorithm on messages to-broadcast by processes that are neighbors in G, and then adapts the technique used in [START_REF] Masaaki Mizuno | Sequential consistency in distributed systems : theory and implementation[END_REF][START_REF] Raynal | Distributed Algorithms for Message-Passing Systems[END_REF] to show that WW (writewrite) histories are sequentially consistent. The individual histories Ŝi are obtained by taking a topological sort of (

★ ↝ H,G ) (p i +W ).
For readability, we denote in the following r p (X,v) the read operation invoked by process p on object X that returns a value v (X.read → v), and w p (X,v) the write operation of value v on object X invoked by process p (X.write(v)). We may omit the name of the process when not needed.

Let us consider a history Ĥ = (H, po → H ) that captures an execution of Algorithm 2, i.e., po → H captures the sequence of operations in each process (process order, po for short). We construct the causal order ↝ H required by the definition of Section 2.2.2 in the following, classical, manner:

• We connect each read operation r p (X,v) = X.read → v invoked by process p (with v ≠ , the initial value) to the write operation w(X,v) = X.write(v) that generated the WRITE(X ,v) message carrying the value v to p (line 10 in Algorithm 2). In other words, we add an edge ⟨w(X,v) rf → r p (X,v)⟩ to po → H (with w and r p as described above) for each read operation r p (X,v) ∈ H that does not return the initial value . We connect initial read operations r(X, ) to an element that we add to H.

We call these additional relations read-from links (noted rf →).

• We take ↝ H to be the transitive closure of the resulting relation.

↝ H is acyclic, as assuming otherwise would imply at least one of the WRITE(X ,v) messages was received before it was sent. ↝ H is therefore an order. We now need to show ↝ H is a causal order, i.e., that the result of each read operation r(X,v) is the value of the latest write w(X,v) that occurred before r(X,v) in ↝ H (said differently, that no read returns an overwritten value). Lemma 6. ↝ H is a causal order.

Proof We show this by contradiction. We assume without loss of generality that all values written are distinct. Let us consider w p (X,v) and r q (X,v) so that w p (X,v) rf → r q (X,v), which implies w p (X,v) ↝ H r q (X,v). Let us assume there exists a second write operation w r (X,v ′ ) ≠ w p (X,v) on the same object, so that

w p (X,v) ↝ H w r (X,v ′ ) ↝ H r q (X,v) (34)
(illustrated in Figure 5). w p (X,v) ↝ H w r (X,v ′ ) means we can find a sequence of operations op i ∈ H so that w p (X,v) → 0 op 0 ...

→ i op i → i+1 ... → k w r (X,v ′ ) (35)
with

→ i ∈ { po → H , rf →},∀i ∈ [1,k].
The semantics of po → H and rf → means we can construct a sequence of causally related (SC,CC)-broadcast messages m i ∈ M between the messages that are toco-broadcast by the operations w p (X,v) and w r (X,v ′ ), which we note WRITE p (X,v) and WRITE r (X,v ′ ) respectively:

WRITE p (X,v) = m 0 ↝ M m 1 ... ↝ M m i ↝ M ... ↝ M m k ′ = WRITE r (X,v ′ ) (36)
where ↝ M is the message causal order introduced in Section 3.1. We conclude that WRITE p (X,v) ↝ M WRITE r (X,v ′ ), i.e., that WRITE p (X,v) belongs to the causal past of WRITE r (X,v ′ ), and hence that q in Figure 5 toco-delivers WRITE r (X,v ′ ) after WRITE p (X,v).

p wp(X, v) q rq(X, v) r wr(X, v ′ ) rf → ↝ H ↝ H Figure 5: Proving that ↝ H is

causal by contradiction

We now want to show that WRITE r (X,v ′ ) is toco-delivered by q before q executes r q (X,v). We can apply the same reasoning as above to w r (X,v ′ ) ↝ H r q (X,v), yielding another sequence of operations

op ′ i ∈ H: w r (X,v ′ ) → ′ 0 op ′ 0 ... → ′ i op ′ i → ′ i+1 ... → ′ k ′′ r q (X,v) (37)
with

→ ′ i ∈ { po → H , rf →}.
Because r q (X,v) does not generate any (SC,CC)-broadcast message, we need to distinguish the case where all op ′ i relations correspond to the process order po → H (i.e., op ′ i = po → H ,∀i). In this case, r = q, and the blocking behavior of X.write() (line 4 of Algorithm 2), insures that WRITE r (X,v ′ ) is toco-delivered by q before executing r q (X,v). If at least one op ′ i corresponds to the read-from relation, we can consider the latest one in the sequence, which will denote the tocodelivery of a WRITE z (Y,w) message by q, with WRITE r (X,v ′ ) ↝ M WRITE z (Y,w). From the causality of the (SC,CC)-broadcast, we also conclude that WRITE r (X,v ′ ) is toco-delivered by q before executing r q (X,v).

Because q toco-delivers WRITE p (X,v) before WRITE r (X,v ′ ), and toco-delivers WRITE r (X,v ′ ) before it executes r q (X,v), we conclude that the value v of v x is overwritten by v ′ at line 10 of Algorithm 2, and that r q (X,v) does not return v, contradicting our assumption that w p (X,v) rf → r q (X,v), and concluding our proof that ↝ H is a causal order.

◻ Lemma 6

To construct ★ ↝ H,G , as required by the definition of (SC,CC)-consistency (Section 2.2.2), we need to order the write operations of neighboring processes in the proximity graph G. We do so as follows:

• We add an edge w p (X,v) ww → w q (Y,w) to ↝ H for each pair of write operations w p (X,v) and w q (Y,w) in H such that:

-(p,q) ∈ E G (i.e., p and q are connected in G); w p (X,v) and w q (Y,w) are not ordered in ↝ H ; -The broadcast message WRITE p (X,v) of w p (X,v) has been toco-delivered before the broadcast message WRITE p (Y,w) of w q (Y,w) by all processes.

We call these additional edges ww links (noted ww →).

• We take ★ ↝ H,G to be the recursive closure of the relation we obtain.

★ ↝ H,G is acyclic, as assuming otherwise would imply that the underlying (SC,CC)-broadcast violates causality. Because of the G-delivery order and termination of the toco-broadcast (Section 3.1), we know all pairs of WRITE p (X,v) and WRITE p (Y,w) messages with (p,q) ∈ E G as defined above are toco-delivered in the same order by all processes. This insures that all write operations of neighboring processes in G are ordered in

★ ↝ H,G .
We need to show that ★ ↝ H,G remains a causal order, i.e., that no read in ★ ↝ H,G returns an overwritten value.

Lemma 7.

★ ↝ H,G is a causal order.

Proof We extend the original causal order ↝ M on the messages of an (SC,CC)-broadcast execution with the following order ↝ G M :

m 1 ↝ G M m 2 if • m 1 ↝ M m 2 ; or
• m 1 was sent by p, m 2 by q, (p,q) ∈ E G , and m 1 is toco-delivered before m 2 by all processes; or • there exists a message m 3 so that

m 1 ↝ G M m 3 and m 3 ↝ G M m 2 .
↝ G M captures the order imposed by an execution of an (SC,CC)-broadcast on its messages. The proof is then identical to that of Lemma 6, except that we use the order ↝ G M , instead of ↝ M . ◻ Lemma 7

Theorem 5. Algorithm 2 implements G-fisheye (SC,CC)-consistency.

Proof The order

★ ↝ H,G we have just constructed fulfills the conditions required by the definition of G-fisheye (SC,CC)-consistency (Section 2.2.2):

• by construction

★ ↝ H,G subsumes ↝ H (↝ H ⊆ ★ ↝ H,G );
• also by construction ★ ↝ H,G , any pair of write operations invoked by processes p,q that are neighbors in G are ordered in ★ ↝ H,G ; i.e., ( ★ ↝ H,G ) ({p,q} ∩W ) is a total order.

To finish the proof, we choose, for each process p i , Ŝi as one of the topological sorts of ( ★ ↝ H,G ) (p i +W ), following the approach of [START_REF] Masaaki Mizuno | Sequential consistency in distributed systems : theory and implementation[END_REF][START_REF] Raynal | Distributed Algorithms for Message-Passing Systems[END_REF]. Ŝi is sequential by construction. Be-

cause ★ ↝ H,G is causal, Ŝi is legal. Because ★ ↝ H,G respects po → H , Ŝi is equivalent to Ĥ (p i +W ). Finally, Ŝi respects ( ★ ↝ H,G ) (p i +W ) by construction.
◻ T heorem 5

Towards Update Consistency

We now introduce the second contribution of this deliverable. This contribution 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 line of work consists in proving that weak consistency criteria such as eventual consistency and causal consistency cannot be combined is such systems. In this second part of our work we therefore 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 [DHJ + 07]. 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 [SPB + 11]. 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 [SJZ + 98, LZM00]. 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 [BZP + 12], 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 s et, 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.

To avoid restricting our results to a given data structure, we first define a class of data types called UQ-ADT for update-query 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. Based on this notion, we then present three main contributions.

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

• We introduce 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, we prove that for any UQ-ADT object with a sequential specification there exists an update consistent implementation by providing a generic construction.

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, which we describe by means of 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 deliverable 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] George | A method for synthesizing sequential circuits[END_REF] except that infinite transition systems are allowed as many objects have an unbounded specification. As stated above, this part of our work focuses on "update-query" objects. On the one hand, the updates have a side-effect 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.

In the following, we use replicated sets 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: 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.

• U = {I(v),D(v) ∶ v ∈ Val}; • Q i = {R}
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 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).

• 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 6: 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.

Eventual Consistency

In this section, we recall the definitions of eventual consistency [START_REF] Vogels | Eventually consistent[END_REF] and strong eventual consistency [SPB + 11]. Fig. 6 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. 6 are eventually consistent. The executions represent two processes sharing a set of integers. In Fig. 6a, 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). 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 ′′ );

• Strong convergence: if two query operations view the same past of updates V , they can be

• 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} ω Figure 7: PC but not EC issued in the same state s: ∀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. 6a 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. 6c, 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}.

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 [SJZ + 98]. As causal consistency is well formalized only for memory, we will instead consider Pipelined Random Access Memory (PRAM) [START_REF] Richard | 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 U H ∪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 7 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. Proposition 1 (Implementation). Pipelined convergence, that imposes both pipelined consistency and eventual consistency, cannot be implemented in a wait-free system.

Proof. We consider the same program as in Figure 7, 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.

Update Consistency

We now introduce our new consistency criteria: update consistency and strong update consistency. Section 5.1 provides their main definitions, while Section 5.2 discusses their expressive power by means of a case study.

Definitions

We give below the definitions of consistency and strong update consistency. Then, in Figure 6, we compare them to eventual consistency and strong eventual consistency 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. 6c 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. 6b

∀q ∈ Q H ,lin H ≤ V (q)∪{q} ∩ L(O) ≠ ∅ where V (q) = {u ∈ U H ∶ u vis → q}.
Fig. 6d 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. 6c, 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. 6c 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 E H ∖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∈U H {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 ≤ E q ∪{q} ∩ L(O) = {w ⋅ Λ(q)}, so q = q i q o with G(s,q i ) = q o . Consequently, H is strong eventually consistent.

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) [SPB + 11], 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] Gene | 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 [AMSM + 11] and PN-Set, add counters on the elements to determine if they should be present or not. The Observe-Remove Set (OR-Set) [SPB + 11, MSS14] is the best documented alg orithm 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) [SPB + 11] 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. 6b 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 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] James R Goodman | Cache consistency and sequential consistency[END_REF] that, in some cases may have a better space complexity than update consistency.

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.

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 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.

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.

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 wait-free asynchronous system. Algorithm 3 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 3, 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 pre-total 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 ↦.

Algorithm 3 a generic UQ-ADT (code for p i ) At the application level, a history is composed of update and query operations. In order to allow only strong update consistent histories, Algorithm 3 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 3 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 faulttolerance. Proposition 4 (Strong update consistency). All histories allowed by Algorithm 3 are strong update consistent.

Proof. Let H = (U,Q,E,Λ,↦) be a distributed history allowed by Algorithm 3. 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 Algorithm 4 the shared memory (code for p i ) 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 vis → q}. Lines 15 to 18 build an explicit sequential execution, that is in lin H ≤ E q ∪{q} by definition of ≤ and in L(O) by definition of O.

Complexity

Algorithm 3 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 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 know n 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 4 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 4 orders the updates exactly like Algorithm 3. 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.

Conclusion

This work was motivated by the increasing popularity of geographically distributed systems. We have presented two contributions that make it possible to formally define and reason about consistency conditions in large-scale systems. The first contribution defines a mixed approach in which the operations invoked by nearby processes obey stronger consistency requirements than operations invoked by remote ones. The second consists of a new consistency criterion, update consistency, that is stronger than eventual consistency and weaker than sequential consistency. Update consistency formalizes the intuitive notions of sequential specification for an abstract data type and distributed history.

Figure 3 :

 3 Figure 2: Executing the program of Figure 1.

C

  ≡ ⟨m,⟨s caus m j [⋅],s tot m j , j⟩⟩ ∈ pending i s caus m j [⋅] ≤ causal i [⋅]22:

  on toco deliver WRITE(X ,v, j)

  , 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}.

  is not update consistent because any linearization of the updates would position a deletion as the last event. 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

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.

3 r Table 1 :

 r1 Possible executions for the history of Figure4

	Consistency	x?	y?
	Sequential Consistency	3	5
	Causal Consistency	{2,3} {4,5}
	G-fisheye (SC,CC)-consistency	3	{4,5}
	may be seen in different orders by different processes (as in a causally consistent history), and y?
	may return 4 or 5 (last line of Table 1).

  ). Update consistency is incomparable with strong eventual consistency.

	• 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 accord-
	ing to	vis →. Each query is the result of the ordered execution, according to ≤, of the updates
	it views:
	Strong update consistency strong update consistency is a strengthening of both update consis-
	tency 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: