Hagit Attiya

Sebastian Burckhardt

Alexey Gotsman

Adam Morrison

Hongseok Yang

Marek Zawirski

Specification and Complexity of Collaborative Text Editing

Collaborative text editing systems allow users to concurrently edit a shared document, inserting and deleting elements (e.g., characters or lines). There are a number of protocols for collaborative text editing, but so far there has been no precise specification of their desired behavior, and several of these protocols have been shown not to satisfy even basic expectations. This paper provides a precise specification of a replicated list object, which models the core functionality of replicated systems for collaborative text editing. We define a strong list specification, which we prove is implemented by an existing protocol, as well as a weak list specification, which admits additional protocol behaviors.

A major factor determining the efficiency and practical feasibility of a collaborative text editing protocol is the space overhead of the metadata that the protocol must maintain to ensure correctness. We show that for a large class of list protocols, implementing either the strong or the weak list specification requires a metadata overhead that is at least linear in the number of elements deleted from the list. The class of protocols to which this lower bound applies includes all list protocols that we are aware of, and we show that one of these protocols almost matches the bound.

INTRODUCTION

Collaborative text editing systems, like Google Docs [START_REF] Day-Richter | What's different about the new Google Docs: Conflict resolution[END_REF][START_REF] Day-Richter | What's different about the new Google Docs: Making collaboration fast[END_REF], Apache Wave [START_REF]Apache Wave[END_REF], or wikis [START_REF] Leuf | The Wiki Way: Quick Collaboration on the Web[END_REF], allow users at multiple sites to concurrently edit the same document. To achieve high responsiveness and availability, such systems often replicate the document in geographically distributed sites or on user devices. A user can modify the document at a nearby replica, which propagates the modifications to other replicas asynchronously. This propagation can be done either via a centralized server or peer-to-peer. An essential feature of a collaborative editing system is that all changes eventually propagate to all replicas and get incorporated into the docu- Figure 1: Example scenarios of collaborative text editing. Events are presented in format "operation : return value". An arrow from an event e to an event e expresses that the effects of e get incorporated at e's replica before e executes.

R 1 R 2 R 3 R 1 R 2 R 3 ins(x,
ment in a consistent way. In particular, such systems aim to guarantee eventual consistency: if users stop modifying the document, then the replicas will eventually converge to the same state [START_REF] Terry | Managing Update Conflicts in Bayou, a Weakly Connected Replicated Storage System[END_REF][START_REF] Vogels | Eventually Consistent[END_REF]. Figure 1(a) gives an example scenario of a document edited at several replicas. First, replica R2 inserts x at the first position (zero-indexed) into the empty list. This insertion then propagates to replica R1, which inserts a to the left of x, and to R3, which inserts b to the right of x. Later the modifications made by R1 and R3 propagate to all other replicas, including R2; when the latter reads the list, it observes axb. In this scenario, the desired system behavior is straightforward, but sometimes this is not the case. To illustrate, consider the scenario in Figure 1(b), where R2 deletes x from the list before the insertions of a and b propagate to it. One might expect the read by R2 to return ab, given the orderings ax and xb established at other replicas. However, some implementations allow ba as a response; e.g., this is the case in a Jupiter protocol [START_REF] Nichols | High-latency, low-bandwidth windowing in the Jupiter collaboration system[END_REF], used in public collaboration systems [START_REF] Wang | Google Wave Operational Transformation[END_REF].

There have been a number of proposals of highly available collaborative editing protocols, using techniques such as operation transformations [START_REF] Ellis | Concurrency Control in Groupware Systems[END_REF][START_REF] Ressel | An integrating, transformation-oriented approach to concurrency control and undo in group editors[END_REF][START_REF] Sun | Operational transformation in real-time group editors: issues, algorithms, and achievements[END_REF][START_REF] Sun | Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems[END_REF] and replicated data types (aka CRDTs) [START_REF] Preguiça | A commutative replicated data type for cooperative editing[END_REF][START_REF] Roh | Replicated abstract data types: Building blocks for collaborative applications[END_REF][START_REF] Weiss | Logoot: A Scalable Optimistic Replication Algorithm for Collaborative Editing on P2P Networks[END_REF]. However, specifications of their desired behavior [START_REF] Li | Preserving Operation Effects Relation in Group Editors[END_REF][START_REF] Sun | Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems[END_REF] have so far been informal and imprecise, and several of the protocols have been shown not to satisfy even the basic expectation of eventual consistency [START_REF] Imine | Formal Design and Verification of Operational Transformation Algorithms for Copies Convergence[END_REF]. To address this problem, we introduce a precise specification of a replicated list object, which allows its clients to insert and delete elements into the list at different replicas and thereby captures the core aspects of collaborative text editing [START_REF] Ellis | Concurrency Control in Groupware Systems[END_REF] (Section 3). Our specification has two flavors. The strong specification ensures that orderings relative to deleted elements hold even after the deletion, thereby disallowing the response ba for the read in Figure 1(b). The weak specification provides no such guarantee, while still requiring the ordering between elements that are not deleted to be consistent across the system. We show that both of these specifications ensure eventual consistency.

We prove that the strong specification is correctly implemented by a variant of an existing RGA (Replicated Growable Array) protocol [START_REF] Roh | Replicated abstract data types: Building blocks for collaborative applications[END_REF], which is in the style of replicated data types [START_REF] Preguiça | A commutative replicated data type for cooperative editing[END_REF] (Section 4). The protocol represents the list as a tree, with read operations traversing the tree in a deterministic order. Inserting an element a right after an element x (as in Figure 1(b)) adds a as a child of x in the tree. Deleting an element x just marks it as such; the node of x is left in the tree, creating a so-called tombstone. Keeping the tombstone enables the protocol to correctly incorporate insertions of elements received from other replicas that are ordered right after x (e.g., that of b in Figure 1(b)).

The simplicity of handling deletions via tombstones in the RGA protocol comes with a high space overhead. More precisely, the metadata overhead [START_REF] Burckhardt | Replicated Data Types: Specification, Verification, Optimality[END_REF] of a list implementation is the ratio between the size of a replica's state (in bits) and the size of the userobservable content of the state, i.e., the list that will be read in this state. As we show, the metadata overhead of the RGA protocol is O(D lg k), where D is the number of deletions issued by clients and k is the total number of operations (Section 4). The number of deletions can be high. For example a 2009 study [START_REF] Weiss | Logoot: A Scalable Optimistic Replication Algorithm for Collaborative Editing on P2P Networks[END_REF] indicates that the "George W. Bush" Wikipedia page has about 500 lines. However, since modifications are usually handled as deleting the original line and then inserting the revised line, the page had accumulated about 1.6 million deletions. 1Our main result is that this overhead is, in some sense, inherent. We prove that any protocol from a certain class which implements the list specification for n ≥ 3 replicas incurs a metadata overhead of Ω(D), where D is the number of deletions. This result holds even for the weak list specification and even if the network guarantees causal atomic broadcast [START_REF] Défago | Total Order Broadcast and Multicast Algorithms: Taxonomy And Survey[END_REF]. The result holds for all pushbased protocols, where each replica propagates list updates to its peers as soon as possible, and merges remote updates into its state as soon as they arrive (we give a precise definition in Section 5). This assumption captures the operation of all highly available protocols that we are aware of.

We establish our lower bound for the peer-to-peer model. However, using the fact that it holds for a network with causal atomic broadcast, we extend it to show that, in a push-based client/server list protocol, the metadata overhead at the clients is still Ω(D).

We prove our lower bound using an information-theoretic argument. For every d ≈ D/2-bit string w, we construct a particular execution αw of the protocol such that, at its end, the user-observable state σw of some replica is a list of size O(1) bits. We then show that, given σw, we can decode w by exercising the protocol in a black-box manner. This implies that all states σw must be distinct and, since there are 2 d of them, one of these states must take at least d bits. The procedure that decodes w from σw is nontrivial and represents the key insight of our proof. It recovers w one bit at a time using a "feedback loop" between two processes: one performs a black-box experiment on the protocol to recover the next bit of w, and the other reconstructs the corresponding steps of the execution αw; the messages sent in the reconstructed part of αw then form the basis for the experiment to decode the next bit of w.

SYSTEM MODEL

We are concerned with highly available implementations of a replicated object [START_REF] Attiya | Limitations of Highly-Available Eventually-Consistent Data Stores[END_REF][START_REF] Burckhardt | Replicated Data Types: Specification, Verification, Optimality[END_REF], which supports a set of operations Op. Such an implementation consists of replicas that receive and re-spond to user operations on the object and use message passing to communicate changes to the object's state. The high availability property sets this model apart from standard message-passing models: we require that replicas respond to user operations immediately-without performing any communication-so that user operations complete regardless of network latency and network partitions (e.g., device disconnection). Replicas. We model a replica as a state machine R = (Q, M, Σ, σ0, E, ∆), where Q is a set of internal states, M is a set of possible messages, Σ = Q × (M ∪ {⊥}) is a set of replica states, σ0 = (q0, ⊥) ∈ Σ is the initial state, E is a set of possible events, and ∆ : Σ × E Σ is a (partial) transition function. Note that a replica state explicitly includes a send buffer, containing the message pending transmission or ⊥, which indicates that no message is pending. If ∆(σ, e) is defined, we say that event e is enabled in state σ. Transitions determined by ∆ describe local steps of a replica in which it interacts with users and other replicas. These interactions are modeled by three kinds of events:

• do(op, v): a user invokes an operation op ∈ Op on the replicated object and immediately receives a response v from the replica;

• send (m): the replica broadcasts a message m ∈ M ; and

• receive(m): the replica receives a message m ∈ M .

A protocol is a collection R of replicas. We require that a send (m) event is enabled in state σ if and only if σ = (q, m) for m = ⊥, and in this case ∆((q, m), send (m)) = (q , ⊥) for some q . We further require that a replica can execute any operation with its return values computed deterministically: for any operation op ∈ Op, exactly one do(op, v) event is enabled in σ. We also require that a replica can accept any message: for any message m, receive(m) is enabled in σ. We assume that messages are unique and that a message's sender is uniquely identifiable (e.g., messages are tagged with the sender id and a sequence number). We also assume that a replica broadcasts messages to all replicas, including itself2 ; replicas can implement point-to-point communication by ignoring messages for which they are not the intended recipient.

Executions. An execution of a protocol R is a (possibly infinite) sequence of events occurring at the replicas in R. 3 For each event e, we let repl(e) ∈ R be the replica at which it occurs, and for each do event e = do(op, v) we let op(e) = op and rval(e) = v. A (finite or infinite) sequence of events e1, e2, . . . occurring at a replica R = (Q, M, Σ, σ0, E, ∆) is well-formed if there is a sequence of states σ1, σ2, . . . such that σi = ∆(σi-1, ei) for all i. If the sequence is of length n, we refer to σn as the state of R at the end of the sequence.

We consider only well-formed executions, in which for every replica R ∈ R: (1) the subsequence of events at R, denoted α|R, is well-formed; and (2) every receive(m) event at R is preceded by a send (m) event in α.

Let α be an execution. Event e ∈ α happens before event e ∈ α [START_REF] Lamport | Time, Clocks, and the Ordering of Events in a Distributed System[END_REF] (written e There is an event f ∈ α such that e hb -→ f and f hb Network model. To ensure that every operation eventually propagates to all the replicas, we require that the network does not remain partitioned indefinitely. A replica R has a message pending in event e of execution α if R's has a send (m) event enabled in the state at the end of α |R, where α is the prefix of α ending with e. DEFINITION 1. The network is sufficiently connected in an infinite well-formed execution α of a protocol R if the following conditions hold for all replicas R ∈ R: (1) Eventual transmission: if R has a message pending infinitely often in α, then R also sends a message infinitely often in α, and (2) Eventual delivery: if R sends a message m, then every replica R = R eventually receives m.

Collaborative editing protocols generally assume causal message delivery [START_REF] Roh | Replicated abstract data types: Building blocks for collaborative applications[END_REF][START_REF] Sun | Operational transformation in real-time group editors: issues, algorithms, and achievements[END_REF]. We model this by considering only executions that satisfy causal broadcast [START_REF] Cachin | Introduction to Reliable and Secure Distributed Programming[END_REF]: DEFINITION 2. An execution α of a protocol R satisfies causal broadcast if for any messages m, m , whenever send (m) hb -→ send (m ), any replica R can receive m only after it receives m.

In fact, our results hold even under a more powerful atomic broadcast [START_REF] Défago | Total Order Broadcast and Multicast Algorithms: Taxonomy And Survey[END_REF] model, which delivers all messages to all replicas in the exact same order. DEFINITION 3. An execution α of protocol R satisfies causal atomic broadcast if the following conditions hold: (1) Causal broadcast: α satisfies causal broadcast. (2) No duplicate delivery: each send (m) event in α is followed by at most one receive(m) event per replica R ∈ R. (3) Consistent order: if R receives m before m , then any other replica R receives m before m .

These broadcast primitives can be implemented when not provided by the network [START_REF] Cachin | Introduction to Reliable and Secure Distributed Programming[END_REF]; by providing them "for free," we strengthen our lower bounds and ensure their independence from the complexity of implementing the broadcast primitive.

COLLABORATIVE TEXT EDITING

Following Ellis and Gibbs [START_REF] Ellis | Concurrency Control in Groupware Systems[END_REF], we model the collaborative text editing problem (henceforth, simply collaborative editing) as the problem of implementing a highly available replicated list object whose elements are from some universe U . Users can insert elements, remove elements and read the list using the following operations, which form Op:

• ins(a, k) for a ∈ U and k ∈ N: inserts a at position k in the list (starting from 0) and returns the updated list. For k exceeding the list size, we assume an insertion at the end. We assume that users pass identifiers a that are globally unique.

• del(a) for a ∈ U : deletes the element a and returns the updated list. We assume that users pass only identifiers a that appear in the return value of the preceding operation on the same replica.

• read: returns the contents of the list.

The definition above restricts user behavior to simplify our technical development. Note that these restrictions are insignificant from a practical viewpoint, because they can be easily enforced: [START_REF]Apache Wave[END_REF] identifiers can be made unique by attaching replica identifiers and sequence numbers; and (2) before each deletion, we can read the state of the list and skip the deletion if the deleted element does not appear in it.

Preliminaries: Replicated Data Types

We cannot specify the list object with a standard sequential specification, since replicas may observe only subsets of operations executed in the system, as a result of remote updates being delayed by the network. We address this difficulty by specifying the response of a list operation based on operations that are visible to it. Intuitively, these are the prior operations executed at the same replica and remote operations whose effects have propagated to the replica through the network. Formally, we use a variant of a framework by Burckhardt et al. [START_REF] Burckhardt | Replicated Data Types: Specification, Verification, Optimality[END_REF] for specifying replicated data types [START_REF] Shapiro | Conflict-free Replicated Data Types[END_REF]. We specify the list object by a set of abstract executions, which record the operations performed by users (represented by do events) and visibility relationships between them. Since collaborative editing systems generally preserve causality between operations [START_REF] Sun | Operational transformation in real-time group editors: issues, algorithms, and achievements[END_REF], here we consider only causal abstract executions, where the visibility relation is transitive.

= (H , vis ) is a prefix of abstract execution A if: (1) H is a prefix of H; and (2) vis = vis ∩ (H × H ).
A specification of an object is a prefixclosed set of abstract executions. A protocol correctly implements a specification when the outcomes of operations that it produces in any (concrete) execution can be justified by some abstract execution allowed by the specification. DEFINITION 5. An execution α of a protocol R complies with an abstract execution A = (H, vis) if for every replica R ∈ R, H|R = α| do R , where α| do R denotes the subsequence of do events by replica R in α. DEFINITION 6. A protocol R satisfies a specification S if every execution α of R complies with some abstract execution A ∈ S.

Specifying the List Object

We present two list specifications: strong and weak. Conceptually, the strong specification ensures that orderings relative to deleted elements hold even after the deletion, thereby disallowing the response ba for the read in Figure 1(b). The weak specification does not guarantee this property, allowing both ba and ab as responses.

We denote by elems(A) the set of all elements inserted into the list in an abstract execution A = (H, vis):

elems(A) = {a | do(ins(a, _), _) ∈ H}.
Recall that we assume all inserted elements to be unique, and so there is a one-to-one correspondence between inserted elements and insert operations. For brevity, we write e1 ≤ vis e2 for e1 = e2 ∨ e1 vis -→ e2. (b) The order of the elements is consistent with the list order: ∀i, j. (i < j) =⇒ (ai, aj) ∈ lo.

(c) Elements are inserted at the specified position: if op = ins(a, k), then a = a min{k,n-1} .

2. The list order lo is transitive, irreflexive and total, and thus determines the order of all insert operations in the execution.

x

& & a 8 8 b o o
For example, the strong list specification is satisfied by the abstract execution in Figure 1(a) and the one in Figure 1(b) with the read returning ab; this is justified by the list order a → x → b. On the other hand, the specification is not satisfied by the execution in Figure 1(b) with the read returning ba: for the outcomes of operations in this execution to be consistent with item 1 of Definition 7, the list order would have to be as shown above; but this order contains a cycle, contradicting item 2. In Section 4 we prove that the strong specification is implemented by an existing protocol, RGA [START_REF] Roh | Replicated abstract data types: Building blocks for collaborative applications[END_REF]. However, some protocols, such as Jupiter [START_REF] Nichols | High-latency, low-bandwidth windowing in the Jupiter collaboration system[END_REF], provide weaker guarantees and, in particular, allow the outcome ba in Figure 1(b). We therefore introduce the following weak list specification, to which our lower bound result applies (Section 6) 5 . DEFINITION 8. An abstract execution A = (H, vis) belongs to the weak list specification A weak if and only if there exists a relation lo ⊆ elems(A) × elems(A) such that:

1. Condition 1 in Definition 7 is satisfied.

2. lo is irreflexive and, for all events e = do(op, w) ∈ H, it is transitive and total on {a | a ∈ w}.

Unlike the strong specification, the weak one allows the list order lo to have cycles; the order is required to be acyclic only on the elements returned by some operation. In particular, the weak specification allows the execution in Figure 1(b) with the read returning ba, which is justified using the above cyclic list order. Since at the time of the read, x is deleted from the list, the specification permits us to decide how to order a and b without taking into account the orderings involving x: a → x and x → b. Eventual consistency. A desirable property of highly available replicated objects is eventual consistency. Informally, this guarantees that, if users stop issuing update requests, then the replicas will eventually converge to the same state [START_REF] Terry | Managing Update Conflicts in Bayou, a Weakly Connected Replicated Storage System[END_REF][START_REF] Vogels | Eventually Consistent[END_REF]. Our specifications imply a related convergence property: in an abstract execution satisfying Astrong or A weak , two read operations that see the same sets of list updates return the same response. This is because such operations will return the same elements (Definition 7, item 1a) and in the same order (Definition 7, item 1b). From the convergence property we can establish that our specifications imply eventual consistency for a class of protocols that guarantee the following property of eventual visibility. DEFINITION 9. An abstract execution A = (H, vis) satisfies eventual visibility if for every event e ∈ H, there are only finitely many events e ∈ H such that ¬(e vis -→ e ). 5 We conjecture that Jupiter satisfies the weak specification. DEFINITION 10. A protocol R satisfying the weak (resp., strong) list specification guarantees eventual visibility if every execution α of R complies with some abstract execution A ∈ A weak (respectively, A ∈ Astrong) that satisfies eventual visibility.

Informally, eventual consistency holds for a protocol guaranteeing eventual visibility because: in an abstract execution with finitely many list updates, eventual visibility ensures that all but finitely many reads will see all the updates; then convergence ensures that they will return the same list. To guarantee eventual visibility, a protocol would rely on the network being sufficiently connected (Definition 1).

Metadata Overhead

In addition to the user-observable list contents, the replica state in a list protocol typically contains user-unobservable metadata that is used internally to provide correct behavior. The metadata overhead is the proportion of metadata relative to the user-observable list content.

Formally, let the size of an internal replica state q or a list w ∈ U * be the number of bits required to represent it in a standard encoding; we denote the size of x by |x|. The metadata overhead [START_REF] Burckhardt | Replicated Data Types: Specification, Verification, Optimality[END_REF] of a state σ = (q, m) is |q|/|w| for the unique w such that do(read, w) is enabled in σ; here w represents the user-observable contents of σ. Note that the contents of the send buffer is not part of the metadata. DEFINITION 11 ([5]). The worst-case metadata overhead of a protocol over a given subset of its executions is the largest metadata overhead of the state of any replica in any of these executions.

AN IMPLEMENTATION OF THE STRONG LIST SPECIFICATION

We now present an implementation of the list object, which is a reformulation of the RGA (Replicated Growable Array) protocol [START_REF] Roh | Replicated abstract data types: Building blocks for collaborative applications[END_REF], and prove that it implements the strong list specification.

Timestamped Insertion Trees

Our representation of the list at a replica uses a timestamped insertion (TI) tree data structure. It stores both the list content and timestamp metadata used for deterministically resolving the order between elements concurrently inserted at the same position.

Formally, a tree is a finite set N of nodes, each corresponding to an element inserted into the list. A node is a tuple n = (a, t, p), where a ∈ U is the element, t ∈ C is a timestamp for the insertion, and p ∈ (C ∪ {•}) is either the parent node (identified by its timestamp) or the symbol • representing the tree root. We define the set C of timestamps and a total order on them later (Section 4.2). For a node n = (a, t, p) we let n.a = a, n.t = t, and n.p = p. For two nodes n, n with n .p = n.t, we say n is the parent of n and write n Read. To read the list, we traverse the tree N by depth-first search, starting at the root. We assemble the visited elements into a sequence s(N ) using prefix order (the parent precedes its children) and visit the children in decreasing timestamp order.

(a,t 3 ) o (x,t 1 ) s(N 1 ) = a x c (c,t 2 ) N 1 = {(x,t 1 ,o),(c,t 2 ,x),(a,t 3 ,o)} (a,t 3 ) o (x,t 1 ) (b,t 4 ) s(N 2 ) = a x b c (c,t 2 ) N 2 =N 1 ∪ {(b,t 4 ,x)} ins(b,2)
Figure 2: Illustration of TI trees. Each box shows a tree, with the set of nodes that define it, its graphical representation, and the sequence of elements it denotes. The tree on the right results from an insert operation for element b at position 2. The order on the timestamps is t1 < t2 < t3 < t4.

Insert. To insert a new element a at position k into the list, let s(N ) = a0 . . . an-1 and pick a new timestamp t that is larger than any of the timestamps appearing in N . Then let p be the element to the left of the insertion position:

p = a k-1 (if k > 0) or p = • (if k = 0)
. We now add a new node (a, t, p) to N . Note that a newly inserted node is the child of the immediately preceding element with the highest timestamp. Thus, it is visited immediately after that element during a read, which makes it appear at the correct position in the list.

The RGA Protocol

We now define the RGA protocol R n rga for n replicas. Each replica stores a TI tree, as well as a set of elements that represent tombstones, used to handle deletions (Section 1). Insertions and deletions are recorded in a send buffer, which is periodically transmitted to other replicas by causal broadcast. State and messages. Timestamps are pairs (x, i), where x ∈ N and i ∈ {1, . . . , n} is a replica identifier. They are ordered lexicographically:

(x, i) < (x , i ) ⇐⇒ (x < x ) ∨ ((x = x ) ∧ (i < i )).
Messages are of the form (A, K), where A is a set of nodes (representing insert operations) and K is a set of elements (representing delete operations), and either A or K is non-empty. The state of a replica is (N, T, (A, K)), where: N is a TI tree, representing the replica-local view of the list; T ⊆ U is the set of tombstones; and (A, K) is a send buffer, containing the message to send next. A pair (∅, ∅) indicates that no message is pending (thus corresponding to ⊥ in Section 2). The initial state is (∅, ∅, (∅, ∅)). do transitions. To execute an insert operation at a replica i in a state (N, T, (A, K)), we construct a node as described in the "Insert" procedure of Section 4.1 and add it to both N and A. As the timestamp of the node we take ((1 + (the largest timestamp in N )), i), or (1, i) if N = ∅. This timestamp is guaranteed to be globally unique. To execute a delete operation, we add the deleted element to both T and K. All operations return the local view of the list, which is obtained by traversing N as described in the "Read" procedure of Section 4.1, and then removing all elements belonging to T . send transition is enabled whenever either A or K is nonempty. It sends (A, K) as the message and sets both A and K to empty. receive transition for a message (Am, Km) adds Am to N and Km to T . The protocol relies on causal delivery of messages, which ensures that no parents can be missing from N . In particular, N stays well-formed after adding Am. We show an example execution in Figure 3, which matches the example in Figure 1(b) and complies with the strong list specification.

Guarantees

The following theorems state the correctness and asymptotic complexity bounds of RGA. We provide full proofs in [2, §A] and discuss the key insights (convergence and stability) below. THEOREM 1. The protocol R n rga satisfies the strong list specification.

THEOREM 2. The worst-case metadata overhead of R n rga over executions with k operations and D deletions is O(D lg k).

Convergence. Each replica maintains a TI tree that grows over time, meaning that nodes are added to the set, but never modified or removed. Because set union is associative and commutative, the order in which nodes are added does not matter. For example, changing the order of message delivery to R2 in Figure 3 does not change the final tree. As a consequence, if the same set of nodes is delivered to any two replicas in any order, their trees are guaranteed to match, which ensures convergence. Stability. The following lemma (proved in [2, §A]) shows that when we add more elements to a TI tree, the order of existing elements remains stable. This implies the strong list specification, because all replicas order all insertions the same way at all times. LEMMA 3. Let A, B be two TI trees such that A ⊆ B. Then s(A) is a subsequence of s(B).

Trees vs. Lists. In the standard RGA implementation [START_REF] Shapiro | A Comprehensive study of Convergent and Commutative Replicated Data Types[END_REF], TI trees are represented as lists (corresponding to the tree traversal). We show in [2, §A] that these representations are functionally equivalent. Lists are convenient to implement, but offer little insight as to why the algorithm guarantees convergence. Not surprisingly, the reason why RGA actually works has been a bit of a mystery, and we are not aware of any prior correctness proofs.

PUSH-BASED PROTOCOLS

Our lower bound results hold for push-based protocols, a class of protocols that contains the protocols of several collaborative editing systems [START_REF] Nichols | High-latency, low-bandwidth windowing in the Jupiter collaboration system[END_REF][START_REF] Preguiça | A commutative replicated data type for cooperative editing[END_REF][START_REF] Roh | Replicated abstract data types: Building blocks for collaborative applications[END_REF][START_REF] Sun | Operational transformation in real-time group editors: issues, algorithms, and achievements[END_REF], including the RGA protocol of Section 4. Informally, a replica in a push-based protocol propagates list updates to its peers as soon as possible and merges remote updates into its state as soon as they arrive (as opposed to using a more sophisticated mechanism, such as a consensus protocol). We define this class of protocols assuming that the network provides causal broadcast; when this is not the case, a protocol may need to delay merging arriving updates to enforce casuality. Formally, we require that in a push-based protocol, every operation observe all operations that happen before it, that list insertions always generate a message, and that a deletion-which, unlike an insertion, may not be unique-generates a message if it does not already observe another deletion of the same element. DEFINITION 13. A protocol R satisfying the weak (strong) list specification is push-based if the following hold:

• For any execution α of R and e = do(ins(a, _), _) ∈ α, replica repl(e) has a message pending after e.

• For any execution α of R and e = do(del(a), _) ∈ α, if there does not exist event e = do(del(a), _) ∈ α that happens before e, then replica repl(e) has a message pending after e.

• For every execution α of R there exists an abstract execution A = (H, vis) ∈ A weak (A ∈ Astrong) that α complies with, such that ∀e , e ∈ H. e vis -→ e ⇐⇒ e hb -→ e.

The class of push-based protocols contains both op-based protocols [START_REF] Burckhardt | Replicated Data Types: Specification, Verification, Optimality[END_REF], in which a message carries a description of the latest operations that the sender has performed (e.g., RGA), and statebased [START_REF] Burckhardt | Replicated Data Types: Specification, Verification, Optimality[END_REF] protocols, in which a message describes all operations the sender knows about (i.e., its state). We also show ([2, §B]) that the class of push-based protocols contains eventually consistent writepropagating protocols [START_REF] Attiya | Limitations of Highly-Available Eventually-Consistent Data Stores[END_REF]-which model many deployed highly available eventually consistent protocols [START_REF] Bailis | Bolt-on Causal Consistency[END_REF][START_REF] Burckhardt | Replicated Data Types: Specification, Verification, Optimality[END_REF][START_REF] Decandia | Dynamo: Amazon's Highly Available Key-value Store[END_REF][START_REF] Du | Orbe: Scalable Causal Consistency Using Dependency Matrices and Physical Clocks[END_REF][START_REF] Du | Closing The Performance Gap between Causal Consistency and Eventual Consistency[END_REF][START_REF] Lloyd | Don't Settle for Eventual Consistency[END_REF][START_REF] Shapiro | Conflict-free Replicated Data Types[END_REF][START_REF] Zawirski | Write fast, read in the past: Causal consistency for client-side applications[END_REF]under the natural assumption that sending a message does not affect the state of the list at the sending replica.

LOWER BOUNDS ON METADATA OVERHEAD

Here we show a lower bound on the worst-case metadata overhead (Definition 11) of a push-based protocol satisfying the weak or strong list specification. THEOREM 4. Let R be a push-based protocol that satisfies the weak or strong list specification for n ≥ 3 replicas. Then the worstcase metadata overhead of R over executions with D deletions is Ω(D).

This follows from the following theorem, because any execution consistent with the strong list specification is also consistent with the weak one. THEOREM 5. Let R be a push-based protocol that satisfies the weak list specification for n ≥ 3 replicas. Then for every integer D ≥ 4, there exists an execution αD of R with D deletions such that: (1) the metadata overhead of some state σ of some replica R in αD is Ω(D); (2) αD satisfies causal atomic broadcast; and (3) R does not receive any message before σ in αD.

PROOF. Let d = (D -2)/2 . We show that there exists an execution of R with D deletions that satisfies the desired conditions, in which the user-observable contents of some internal state is a list with a single element, and yet the size of this state is at least d bits. It follows that the metadata overhead of this state is Ω(D).

We show the existence of this execution using an informationtheoretic argument. Namely, for every d-bit string w we construct an execution αw that satisfies causal atomic broadcast and in which: (1) replica R1 performs D deletions and receives no messages; (2) at the end of αw, the user-observable list at R1 contains the single element " * " and R1 has no messages pending; and yet (3) we can decode w given only σw, the state of R1 at the end of αw (this decoding process exercises the protocol R in a black-box manner). Hence, all states σw must be distinct. Since there are 2 d of them, one of these states σw 0 must take at least d bits. Since this state has no messages pending, its metadata overhead is Ω(D), and thus, αw 0 is the desired execution. Encoding w. Given a d-bit string w = w1 . . . w d , we construct an execution αw of R that builds a list encoding the path from the root of a binary tree of height d to the w-th leaf (when w is interpreted as the binary representation of an integer). Figure 4(a) details the construction: it shows pseudocode which, as it executes, constructs the execution; instructions of the form ei correspond to a state transition e at replica Ri. We abuse notation by writing op instead of do(op, _), by specifying inserts of whole strings instead of element by element, and by specifying positions relative to prior insertions rather than with integers. Figure 5(a) depicts αw for w = 10.

Only replica R1 participates in the encoding execution αw. We start by inserting the string [0 ]0 (i.e., the root). Because R is a pushbased protocol, R1 has a message m1 pending following these insertions. We then proceed with a series of steps, for i = 1, . . . , d. Each step i begins with R1 in state σi having a message mi pending. R1 first broadcasts mi. We then insert the string [i ]i immediately to the left or to the right of [i-1 ]i-1, depending on whether the i-th bit of w is set. Because R is a push-based protocol, R1 has a message pending following these insertions, and we proceed to step i+1. When we are done, we broadcast the current pending message and insert the element * between [ d and ] d , and broadcast the message m d+2 that is pending following this insertion. For example, if w = 10, the state of the list at R1 at this point is [0 ]0 [2 * ]2 [START_REF]Apache Wave[END_REF]1. We then delete all the [i and ]i elements, for i = 0, . . . , d, and if D is odd, we insert and delete an additional element, so that the number of deletions in αw is exactly D. Because R is a push-based protocol, R1 has a message pending following these deletions, which we broadcast to empty R1's send buffer. Finally, we read the list at R1, observing that it is * . This follows because for any abstract execution A = (H, vis) that the encoding execution αw complies with, all ins and del events are visible to the read, due to Condition (1) of Definition 4. The read's response must thus be * , since by assumption one of such executions A is consistent with the weak list specification.

The output of the encoding procedure is σw, the state of R1 at the end of the encoding execution αw. It is easy to check that αw is well-formed; furthermore, it vacuously satisfies causal atomic broadcast. Decoding w from σw. We reconstruct w one bit at a time by "replaying" the execution αw. To replay iteration i of αw, we rely on a procedure Recover() that recovers wi from σw and m1, . . . , mi. (We describe Recover() in the next paragraph; for now, assume it is an oracle.) Knowing wi, in turn, determines the next event of R1 in αw, and hence provides us with mi+1. The decoding process thus only uses messages from R1 that it reconstructs with the bits of w already known. Figure 4(b) shows the pseudocode which, as it executes, decodes w. We start with R1 in its initial state and recon-

Input: w = w 1 , . . . , w d // R 1 starts in its initial state σ 0 . ins 1 ([ 0 ] 0 , 0) for i = 1, . . . , d // The state of R 1 here is σ i . send 1 (m i ) if w i = 1 then ins 1 ([ i ] i just after ] i-1 ) else ins 1 ([ i ] i just before [ i-1 ) // The state of R 1 here is σ i+1 . send 1 (m d+1 ) ins 1 ( * between [ d and ] d ) send 1 (m d+2 ) for i = 0, . . . , d del 1 ([ i ) del 1 (] i ) if D = 2(d + 1) + 1 then ins 1 (b, 0) del 1 (b) send 1 (m d+3 ) read 1 = * //
(m j ) receive 1 (m j ) read 2 = . . . [ i-1 ] i-1 . . . ins 2 (x between [ i-1 and ] i-1 ) send 2 (mx) receive 2 (mx) receive 1 (mx) if read 1 = x * return 1 else // read 1 = * x return 0
(c) Recover(σw, m1, . . . , mi)

Figure 4: Encoding and decoding procedures. Events are subscripted with the id of their replica.

struct m1, which does not depend on w. We then proceed in steps, for i = 1, . . . , d. In step i we know m1, . . . , mi, and we recover bit wi from σw and m1, . . . , mi. Having recovered wi, we replay the insertion that R1 performs at step i of the encoding and reconstruct mi+1.

Recovering wi from σw and m1, . . . , mi. The Recover() procedure determines wi by performing state transitions on fresh copies of R1 and R2; the transitions that an execution of Recover() performs have no effect on the state of the replicas in the "replayed" execution constructed by the decoding process, or on other Recover() executions. Figure 4(c) shows these state transitions, and Figures 5(b)-5(c) illustrate the overall decoding of w = 10 (the use of the replica R3 is explained below). We start off with R2 in its initial state and R1 in state σw. We deliver the messages m1, . . . , mi to both replicas in the same order. We then read at R2 and receive response v i w ; we will show that [i-1 ]i-1 ∈ v i w . Next, R2 inserts element x between [i-1 and ]i-1 and broadcasts a message mx, which we deliver to both replicas. Finally, we read at R1 and observe the list in state y i w . We will show that y i w contains only x and * , and if x precedes * then wi = 1; otherwise, wi = 0. Validity of Recover(σw, m1, . . . , mi) state transitions. Assuming that m1, . . . , mi are the first i messages sent by R1 in αw, we show that the state transitions performed by an execution of Recover(σw, m1, . . . , mi) in Figure 4(c) occur in an extension β i w of αw of the form:

β i w = αw receive2(m1) receive1(m1) . . . receive2(mi) receive1(mi) do2(read2, v i w ) do2(ins2(x, k i w ), _) send 2(mx) receive2(mx) receive1(mx) do1(read1, y i w ),
where k i w is the position at which R2 inserts x into the list. In the following, we prove that the execution β i w is well-formed (Claim 6), that it satisfies causal atomic broadcast (Claim 7), that [START_REF] Day-Richter | What's different about the new Google Docs: Making collaboration fast[END_REF], and that y i w = x * or y i w = * x (Claim 9). To this end, we exploit the fact that σw is R1's state at the end of αw, which allows Recover() to perform the same state transitions at R1 that occur in β i w , without having access to the entire execution αw that leads R1 to state σw. CLAIM 6. Execution β i w is well-formed.

[i-1 ]i-1 ∈ v i w (Claim
PROOF. By assumption, Recover() is passed the first i messages sent by R1 in αw. The claim thus follows from the following: (1) αw is well-formed; (2) at the end of αw, R1 is in state σw; (3) because R2 does not participate in αw, the state of R2 at the end of αw is its initial state; (4) a replica always accepts any sent message (by definition); and (5) R is push-based, and so R2 has a message pending following its ins operation. CLAIM 7. Execution β i w satisfies causal atomic broadcast.

PROOF. Immediate from inspection of the message delivery order in

β i w . CLAIM 8. [i-1 ]i-1 ∈ v i w .
PROOF. For j = 1, . . . , d + 1, let ej, fj ∈ αw be the do events in which R1 inserts [j-1 and ]j-1 into the list. Let r ∈ β i w be the do event at which R2 reads v i w . Because R is a correct push-based protocol and β i w satisfies causal atomic broadcast, by Definition 13, β i w complies with some abstract execution A = (H, vis) ∈ A weak such that ej vis -→ r and fj vis -→ r if and only if j ≤ i, and no del operation is visible to r. This holds because in β i w , R2 receives only the messages m1, . . . , mi before r, and each mj is the first message sent by R1 after ej and fj. It thus follows from the definition of the weak list specification (Definition 8) that

v i w = . . . [i-1 ]i-1 . . . . CLAIM 9. y i w = x * or y i w = * x.
PROOF. Let f ∈ β i w be the do event at which R2 inserts x into the list, and r ∈ β i w be the do event at which R1 reads y i w . Because

[ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 0 ] 0 [ 2 ] 2 [ 1 ] 1 [ 0 ] 0 [ 2 *] 2 [ 1 ] 1 R 1 σ w (deletes) * m 4 m 3 m 2 m 1 [ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 0 ] 0 [ 2 ] 2 [ 1 ] 1 [ 0 ] 0 [ 2 *] 2 [ 1 ] 1 R 1 * m 1 R 2 m 4 m 2 x* R 3 m x m 3 [ 0 ] 0 [ 0 x] 0 m x [ 0 x] 0 [ 2 *] 2 [ 1 ] 1 [ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 0 ] 0 [ 2 ] 2 [ 1 ] 1 [ 0 ] 0 [ 2 *] 2 [ 1 ] 1 R 1 * m 1 R 2 m 4 m 2 *x R 3 m x m x [ 0 ] 0 [ 2 *] 2 [ 1 x] 1 m 3 [ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 1 x] 1 m 5 m 5 m 5
(a) Encoding w = 10: execution αw, at the end of which the state of R1 is σw.

[ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 0 ] 0 [ 2 ] 2 [ 1 ] 1 [ 0 ] 0 [ 2 *] 2 [ 1 ] 1 R 1 σ w (deletes) * m 4 m 3 m 2 m 1 [ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 0 ] 0 [ 2 ] 2 [ 1 ] 1 [ 0 ] 0 [ 2 *] 2 [ 1 ] 1 R 1 * m 1 R 2 m 4 m 2 x* R 3 m x m 3 [ 0 ] 0 [ 0 x] 0 m x [ 0 x] 0 [ 2 *] 2 [ 1 ] 1 [ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 0 ] 0 [ 2 ] 2 [ 1 ] 1 [ 0 ] 0 [ 2 *] 2 [ 1 ] 1 R 1 * m 1 R 2 m 4 m 2 *x R 3 m x m x [ 0 ] 0 [ 2 *] 2 [ 1 x] 1 m 3 [ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 1 x] 1 m 5 m 5 m 5
(b) Decoding w1 = 1 given σw and m1. (We do not show replicas receiving their own messages.)

[ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 0 ] 0 [ 2 ] 2 [ 1 ] 1 [ 0 ] 0 [ 2 *] 2 [ 1 ] 1 R 1 σ w (deletes) * m 4 m 3 m 2 m 1 [ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 0 ] 0 [ 2 ] 2 [ 1 ] 1 [ 0 ] 0 [ 2 *] 2 [ 1 ] 1 R 1 * m 1 R 2 m 4 m 2 x* R 3 m x m 3 [ 0 ] 0 [ 0 x] 0 m x [ 0 x] 0 [ 2 *] 2 [ 1 ] 1 [ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 0 ] 0 [ 2 ] 2 [ 1 ] 1 [ 0 ] 0 [ 2 *] 2 [ 1 ] 1 R 1 * m 1 R 2 m 4 m 2 *x R 3 m x m x [ 0 ] 0 [ 2 *] 2 [ 1 x] 1 m 3 [ 0 ] 0 [ 1 ] 1 [ 0 ] 0 [ 1 x] 1 m 5 m 5 m 5
(c) Decoding w2 = 0 given σw, m1 and m2. (We do not show replicas receiving their own messages.)

Figure 5: Examples of the encoding and decoding procedures from Theorem 5 applied to w = 10. Figure 5(a) shows the execution αw constructed by the encoding procedure, whose output is σw, the state of R1 at the end of αw. Figure 5(b) shows the first step of decoding w from σw. The decoding procedure performs the state transitions of the events at R1 that are outside of the dashed rectangle and of the events at R2; these transitions are valid because they occur in the depicted execution, in which the events inside the dashed rectangle lead R1 to state σw. The relative order of x and * read at R1 therefore recovers bit w1 = 1. Figure 5(c) shows the second step of decoding w: Recovering w1 = 1 allows the decoding procedure to perform the state transitions by R1 in αw that depend on w1.

R is a correct push-based protocol, β i w compiles with some abstract execution A = (H, vis) ∈ A weak such that f vis -→ r. Now, let e ∈ β i w be the do event at which R1 inserts * into the list. Then e vis -→ r by definition of an abstract execution (Definition 4). Because all other elements inserted in β i w are deleted by R1 before r, but x and * are not deleted in β i w , the claim follows.

Correctness of recovering wi. Having shown that the state transitions performed by Recover() yield the lists y i w = x * or y i w = * x, it remains to show that we correctly recover wi from y i w : (y i w = x * ) ⇐⇒ (wi = 1).

In principle, the weak list specification allows R1's read to order x and * arbitrarily, since [i-1 and ]i-1 are deleted from the list by the time the read occurs. We show, however, that R1 cannot do this, because it cannot rule out the possibility that another replica has already observed [i-1 x ]i-1 and * together, and therefore their order is fixed. Consider the following extension of β i w , in which R3 receives the messages generated after each insertion and then reads the list (it is easy to see that this execution satisfies causal atomic broadcast):

γ i w = β i w receive3(m1) . . . receive3(mi) receive3(mx) receive3(mi+1) . . . receive3(m d+2 ) do3(read3, z i w ).
We show that the list z i w contains * after x if and only wi = 1. Informally, this follows because every element inserted from iteration i onwards in the encoding procedure (and hence in γ i w ), including * , goes after ]i-1 if and only if wi = 1, and no del events are visible to R3, so its read response must order x before ]i-1 before * .

Formally, consider the following events in γ i w : w * , the ins of * by R1; wx, the ins of x by R2; and rz, the read by R3, whose response is z i w . Because R is a correct push-based protocol and γ i w satisfies causal broadcast, by Definition 13, γ i w complies with some abstract execution A = (H, vis) ∈ A weak such that for any e, e ∈ H, e vis -→ e if and only if e hb -→ e. Therefore, no del event is visible to w * , wx or rz. Let lo be a list order that A is consistent with (Definition 8). We proceed to show that (x, * ) ∈ lo if and only if wi = 1. Observe that if wi = 1, every element inserted from iteration i onwards of the encoding process is inserted after ]i-1, and if wi = 0, every element inserted from iteration i onwards is inserted before [i-1. Therefore, the response of w * establishes that (]i-1, * ) ∈ lo if and only if wi = 1. The response of wx establishes that ([i-1, x) ∈ lo and (x, ]i-1) ∈ lo. It follows that (x, * ) ∈ lo if and only if wi = 1, since [i-1, x, ]i-1, * ∈ z i w and lo is total and transitive on {a | a ∈ rval(rz) = z i w }. We conclude by noting that y i w = x * or y i w = * x (Claim 9); recall that y i w is the response to the read at R1 performed by Recover(). Since (x, * ) ∈ lo if and only if wi = 1, then y i w = x * if and only if wi = 1.

Extension to a Client/Server Model

In a client/server protocol, replicas communicate only with a central server and not directly with each other. (The motivation is to maintain state on the server instead of on the replicas, and so the server usually does more than merely relay messages between replicas [START_REF] Nichols | High-latency, low-bandwidth windowing in the Jupiter collaboration system[END_REF].) To model such protocols in our framework, which assumes a broadcast transport, we require replicas to process only messages to/from the server: DEFINITION 14. A protocol R = {R1, . . . , Rn, S} is a client/server protocol if for every replica Ri = (Q i , M, Σ i , σ i 0 , E, ∆ i ), and σ ∈ Σ i , if ∆ i (σ, receive(m)) = σ, then m was sent by S. We call S the server.

In practice, users do not interact directly with the server, and so we consider only executions in which do events do not occur at the server.

Assuming atomic broadcast, a broadcast protocol can simulate a client/server protocol using state machine replication [START_REF] Lamport | Time, Clocks, and the Ordering of Events in a Distributed System[END_REF].

R i ∈ R simulating replica Ri = (Q i , M, Σ i , σ i 0 , E, Σ i ) ∈ R.
The initial internal state is (q i 0 , q S 0 ), where q i 0 and q S 0 are the initial internal states of Ri and of S, respectively. that simulates R in the following sense: (1) for any execution α of R that satisfies causal atomic broadcast, there exists an execution

α of R such that α| do R i = α | do R i for i = 1..n; (2) the set of internal states of each R i is Q i × Q S ,
where Q i and Q S are respective sets of Ri and S; and (3) until R i receives a message, its state is _, q S 0 , where (q S 0 , ⊥) is the initial state of S. PROOF. For 1 = 1..n, replica R i ∈ R maintains two state machines, of Ri and of S. R i broadcasts exactly the messages broadcast by the replica Ri it is simulating. We use the fact that messages are delivered to all replicas in R in the same order to simulate the server S using state machine replication.

Figure 6 shows the state machine of replica R i ∈ R . Upon a do event, R i performs the corresponding transition on Ri's state machine and broadcasts any message m that Ri would send to S. Upon receiving a message m, R i delivers m to the two state machines it maintains. (However, because m corresponds to a message sent by some Rj, the Ri state machine ignores it, by Definition 14.) If, as a result of receiving m, S broadcasts a message m * , then R i (locally) delivers m * to Ri's state machine and broadcasts any message m that Ri sends as a result of receiving m * .

In any execution α of R that satisfies causal atomic broadcast, all messages are delivered to all replicas in the same order. Therefore, each replica R i performs the same state transitions at S, and (locally) delivers the same messages from S to its Ri state machine. The claim follows.

Client/server lower bound. Since the executions constructed in the proof of Theorem 5 satisfy causal atomic broadcast, they can also be viewed as executions of a protocol simulating a push-based client/server protocol (Proposition 10). We therefore obtain COROLLARY 11. Let R be a push-based client/server protocol that satisfies the weak or strong list specification for n ≥ 3 replicas. Then the worst-case metadata overhead of R on the clients over executions with D deletions is Ω(D).

PROOF. Let R be a push-based client/server protocol that satisfies the weak or strong list specification. Let R be the protocol simulating R from Proposition 10. Take D ≥ 4. By Theorem 5, there exists an execution αD of R with D deletions such that: (1) the metadata overhead of some state σ of some replica R ∈ R is Ω(D); (2) αD satisfies causal atomic broadcast; and

(3) R does not any message before σ. Because R simulates R, we have that σ = ((q R , q S ), _), where q R and q S are, respectively, internal states of the replica R ∈ R that R is simulating and of the server. Moreover, it follows from Proposition 10 that q S is the initial internal state of the server. Therefore, |(q R , q S )| = O(|q R | + |q S |) = O(|q R |), because |q S | is a constant. Since the user-observable content at R and R is the same, it follows that the metadata overhead at R is Ω(D).

RELATED WORK

Previous attempts at specifying the behavior of replicated list objects [START_REF] Li | Preserving Operation Effects Relation in Group Editors[END_REF][START_REF] Sun | Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems[END_REF] have been informal and imprecise: they typically required the execution of an operation at a remote replica to preserve the effect of the operation at its original replica, but they have not formally defined the notions of the effect and its preservation.

Burckhardt et al. [START_REF] Burckhardt | Replicated Data Types: Specification, Verification, Optimality[END_REF] have previously proposed a framework for specifying replicated data types (on which we base our list specifications) and proved lower bounds on the metadata overhead of several data types. In contrast to us, they handle much simpler data types than a list. Thus, our specifications have to extend theirs with an additional relation, defining the order of elements in the list. Similarly, their proof strategy (and its extension in [START_REF] Attiya | Limitations of Highly-Available Eventually-Consistent Data Stores[END_REF]) for establishing lower bounds would not be applicable to lists; obtaining a lower bound in this case requires a more delicate decoding argument, recovering information incrementally.

There are more protocols implementing a highly available replicated list than the RGA protocol we considered. Treedoc [START_REF] Preguiça | A commutative replicated data type for cooperative editing[END_REF] and Logoot [START_REF] Weiss | Logoot: A Scalable Optimistic Replication Algorithm for Collaborative Editing on P2P Networks[END_REF] are other implementations of the strong list specification using the approach of replicated data types [START_REF] Shapiro | Conflict-free Replicated Data Types[END_REF]. As in RGA, the state of a replica can be viewed as a tree, where a deterministic traversal defines the order of the list. The replication protocol represents position of a node in the tree as a sequence of edge labels on the path from the root of the tree (in RGA, it is a relative position to an existing node). Like RGA, these protocols have worst-case metadata overhead linear in the number of deletions. WOOT [START_REF] Oster | Data consistency for P2P collaborative editing[END_REF] is a graph-based list implementation: its main component is a representation of a partial list order, i.e., ordering restrictions inferred at the time user performs operations. The total list order is computed as a view of the graph based on a non-declarative specification of intended ordering.

Another class of protocols is based on operational transformations (OT) [START_REF] Ellis | Concurrency Control in Groupware Systems[END_REF], which apply certain transformation functions to pairs of concurrent updates. If applying the transformation function allows commuting two operations (TP1) and three operations (TP2) then OT ensures that the list state converges, regardless of the order in which the operations are received [START_REF] Ressel | An integrating, transformation-oriented approach to concurrency control and undo in group editors[END_REF]. However, it was shown [START_REF] Imine | Formal Design and Verification of Operational Transformation Algorithms for Copies Convergence[END_REF] that several OT protocols do not satisfy TP1 and TP2 and do not converge. OT protocols store a log of updates at each replica, so their metadata overhead is also at least linear in the number of updates.

CONCLUSION

This paper provides a precise specification of the list replicated object, which models the core functionality of collaborative text editing systems. We define a strong list-and show that it is implemented by an existing system [START_REF] Roh | Replicated abstract data types: Building blocks for collaborative applications[END_REF]-as well as a weak list, which we conjecture describes the behavior of the Jupiter protocol [START_REF] Nichols | High-latency, low-bandwidth windowing in the Jupiter collaboration system[END_REF], underlying public collaboration systems [START_REF] Wang | Google Wave Operational Transformation[END_REF].

We prove a lower bound of Ω(D), where D is the number of deletions, on the metadata overhead of push-based list protocols, which model the implementation of all highly available list protocols that we are aware of. Our lower bound applies for both weak and strong semantics. Exploring client/server systems in future research is therefore of practical interest, as some client/server systems do not implement the strong semantics, and our results suggest that this might not offer a complexity advantage.

We also show a simple list protocol whose metadata overhead is O(D lg k), where k is the number of operations. Closing the gap between the upper and lower bound is left for future work, as is the question of relaxing the restriction to push-based protocols.

Our work is a first step towards specifying and analyzing general collaborative editing systems, providing more features than those captured by the list object. This includes systems for sharing structured documents, such as XML [START_REF] Martin | Scalable XML collaborative editing with undo[END_REF]. While our lower bound would hold for more general systems, it is possible that the additional features induce additional complexity.

  0) : x ins(x, 0) : x ins(a, 0) ins(b, 1) ins(a, 0) del(x) : ε ins(b, 1) : ax : xb : ax : xb read : axb read : ?

  → e , or simply e hb -→ e if the context is clear) if one of the following conditions holds: (1) Thread of execution: repl(e) = repl(e ) and e precedes e in α. (2) Message delivery: e = send (m) and e = receive(m). (3) Transitivity:

DEFINITION 4 .

 4 A causal abstract execution is a pair (H, vis), where H is a sequence of do events 4 , and vis ⊆ H×H is an acyclic visibility relation (with (e1, e2) ∈ vis denoted by e1 vis -→ e2) such that: (1) if e1 precedes e2 in H and repl(e1) = repl(e2), then e1 vis -→ e2; (2) if e1 vis -→ e2, then e1 precedes e2 in H; and (3) vis is transitive (if e1 vis -→ e2 and e2 vis -→ e3, then e1 vis -→ e3).

Figure 1

 1 Figure1graphically depicts abstract executions, where vis is the transitive closure of arrows in the figure and H is the result of some topological sort of vis. An abstract execution A = (H , vis ) is a prefix of abstract execution A if: (1) H is a prefix of H; and (2) vis = vis ∩ (H × H ). A specification of an object is a prefixclosed set of abstract executions. A protocol correctly implements a specification when the outcomes of operations that it produces in any (concrete) execution can be justified by some abstract execution allowed by the specification.

DEFINITION 7 .

 7 An abstract execution A = (H, vis) belongs to the strong list specification Astrong if and only if there is a relation lo ⊆ elems(A) × elems(A), called the list order, such that: 1. Each event e = do(op, w) ∈ H returns a sequence of elements w = a0 . . . an-1, where ai ∈ elems(A), such that (a) w contains exactly the elements visible to e that have been inserted, but not deleted: ∀a. a ∈ w ⇐⇒ (do(ins(a, _), _) ≤ vis e) ∧ ¬(do(del(a), _) ≤ vis e).

  pa -→ n . DEFINITION 12. A set of nodes N is a TI tree if (1) timestamps uniquely identify nodes: ∀n, n ∈ N : n.t = n .t =⇒ n = n ; (2) all parents are present: if n ∈ N and n.p = •, then n pa -→ n for some n ∈ N ; and (3) parents are older than their children: n pa -→ n =⇒ n.t < n .t.

Figure 2

 2 Figure2shows an example of a TI tree and illustrates the read and insert operations explained below. Read. To read the list, we traverse the tree N by depth-first search, starting at the root. We assemble the visited elements into a sequence s(N ) using prefix order (the parent precedes its children) and visit the children in decreasing timestamp order.

1 )Figure 3 :

 13 Figure 3: Illustration of an RGA execution, with time proceeding from top to bottom. Bullets show the transitions of the replicas R1, R2, and R3, and in some places we indicate the current state of the tree N and the tombstone set T . The order on the timestamps is t1 < t2 < t3.

PROPOSITION 10 .Figure 6 :

 106 Figure 6: State machine of replicaR i ∈ R simulating replica Ri = (Q i , M, Σ i , σ i 0 , E, Σ i ) ∈ R.The initial internal state is (q i 0 , q S 0 ), where q i 0 and q S 0 are the initial internal states of Ri and of S, respectively.

  The state of R 1 here is σw.(a) Execution αw, at the end of which the state of R1 encodes w Input: σw // R 1 starts in its initial state σ 0 , // which does not depend on w.ins 1 ([ 0 ] 0 , 0) for i = 1, . . . , d // We now know σ i , // so can generate m i . send 1 (m i ) w i ← Recover(σw, m 1 , . . . , m i ) if w i = 1 then ins 1 ([ i ] i just after ] i-1 ) else ins 1 ([ i ] i just before [ i-1 ) // We now know σ i+1 . output w (b) Decoding w given σw Input: σw, m 1 , . . . , m i // We perform the state transitions // below on copies of the state // machines, with R 2 starting in its // initial state and R 1 in state σw. // The replica state in the outer // decoding procedure is unaffected . for j = 1, . . . , i receive 2

Wikipedia stores this information also to track the document's edit history.

The latter is used to support atomic broadcast[START_REF] Défago | Total Order Broadcast and Multicast Algorithms: Taxonomy And Survey[END_REF], defined later.

Formally, an execution consists of events instrumented with unique event ids and replicas. In the paper we do not use this more accurate formulation so as to avoid clutter.

Formally, H consists of do events instrumented with unique event ids and replicas, as in the case of an execution α. To avoid clutter, we do not use this more accurate presentation.

Acknowledgments

We would like to thank Marc Shapiro and Pascal Urso for comments that helped improve the paper. Attiya and Morrison were supported by the Israel Science Foundation (grant 1749/14) and by Yad Hanadiv Foundation. Gotsman was supported by an EU project ADVENT. Yang was supported by an Institute for Information & Communication Technology Promotion (IITP) grant funded by the Korea government (MSIP, No. R0190-15-2011). Zawirski was supported by an EU project SyncFree.