Sreeja S Nair

Filipe Meirim

Mário Pereira

Carla Ferreira

Marc Shapiro

A coordination-free, convergent, and safe replicated tree

Keywords: Distributed data structures, Conflict-free Replicated Data Type, Formal verification

The tree is an essential data structure in many applications. In a distributed application, such as a distributed file system, the tree is replicated. To improve performance and availability, different clients should be able to update their replicas concurrently and without coordination. Such concurrent updates converge if the effects commute, but nonetheless, concurrent moves can lead to incorrect states and even data loss. Such a severe issue cannot be ignored; ultimately, only one of the conflicting moves may be allowed to take effect. However, as it is rare, a solution should be lightweight. Previous approaches would require preventative cross-replica coordination, or totally order all operations after-the-fact, requiring roll-back and compensation operations.

In this paper, we present a novel replicated tree that supports coordination-free concurrent atomic moves, and provably maintains the tree invariant. Our analysis identifies cases where concurrent moves are inherently safe, and we devise a lightweight, coordination-free, rollback-free algorithm for the remaining cases, such that a maximal safe subset of moves takes effect. We present a detailed analysis of the concurrency issues with trees, justifying our replicated tree data structure. We provide mechanized proof that the data structure is convergent and maintains the tree invariant. Finally, we compare the response time and availability of our design against the literature.

Un arbre répliqué, convergent et sûr sans coordination

Résumé : L'arbre est une structure de données essentielle. Quand l'application est distribuée, par exemple dans un système de fichiers distribué, l'arbre est répliqué. Pour améliorer les performances et la disponibilité, les différents clients doivent pouvoir mettre à jour leurs répliques simultanément et sans coordination. Celles-ci convergent si les mises à jour commutent entre elles ; néanmoins, même dans ce cas, des opérations "move" concurrentes peuvent conduire à des états incorrects, et même à la perte de données. Au bout du compte, entre deux opérations "move" en conflit, seul l'une des deux peut être autorisée à prendre effet. Cependant, comme ce cas est rare, la solution doit être légère. Les approches précédentes nécessitaient une coordination préventive des répliques, ou des retours en arrière à posteriori.

Dans cet article, nous présentons un nouvel arbre répliqué, qui met en oeuvre une opération "move" atomique sans coordination, et dont nous prouvons qu'il maintient l'invariant d'arbre. Notre analyse identifie les cas oú les "move" concurrents sont intrinsèquement sûrs, et proposons un algorithme léger, sans coordination et sans retour-arrière, pour les autres cas, de sorte qu'un sous-ensemble maximal et sûr de "move" prenne effet.

Nous présentons une analyse détaillée des problèmes de cohérence dans les arbres. Nous fournissons une preuve mécanisée que la structure des données est convergente et maintient l'invariant d'arbre. Enfin, nous comparons le temps de réponse et la disponibilité de notre concept à la littérature.

Mots-clés : Structures de données distribuées, CRDT, Vérification formelle 1 Introduction

Concurrent data structures are an important programming abstraction; designing concurrent data structures with non-trivial properties is complex. The tree data structure is used in many applications. For instance, a file system is a tree of directories and files. A move (or rename) operation transfers a subtree atomically by changing its parent. Similarly, a rich text editor maintains a DOM tree of blocks with attributes. Text editing modifies the tree structure; in particular a drag and drop can move a subtree from one parent to another.

A tree has a strong structural invariant: nodes are unique, there is a single root, each node has a single parent and has a path to the root, and the child-parent graph is acyclic. Much current work in concurrent data structure design focuses on lock-free or wait-free coordination using primitives such as compare-and-swap (CAS). However, in a distributed and replicated setting, even CAS is too strong. Consider a file system replicated to several locations over the globe, or through a mobile network. Network latency between continents can be between 0.1 and 0.5 seconds; the mobile network may disconnect completely. To ensure availability, a user of the file system must be able to update a replica locally, and update without coordinating at all with other replicas. Replicas converge eventually by exchanging their updates asynchronously.

It is a major challenge to maintain safety in this context; specifically, in this case, to maintain the tree structure. Concurrent atomic moves (also called renames in a file system) are especially problematic [START_REF] Bjørner | Models and software model checking of a distributed file replication system[END_REF]. Consider for instance a tree composed of the root and children a and b. One replica moves a underneath b, while concurrently (without coordination) the other replica moves b under a. Naïvely replaying one replica's updates at the other produces an a-b cycle disconnected from the root. This is a widespread issue; indeed, many replicated file systems have serious anomalies, including incorrect or diverged states [START_REF] Tao | Merging semantics for conflict updates in geo-distributed file systems[END_REF]Section 6 for some examples], violating the tree invariant [START_REF] Bjørner | Models and software model checking of a distributed file replication system[END_REF]. However, concurrent moves are relatively rare in these systems 1 and it is important that we design a solution that has minimal overhead. Solutions in the literature include non-atomic moves [START_REF] Tao | Merging semantics for conflict updates in geo-distributed file systems[END_REF] (resulting in duplicate copies), re-introducing coordination [START_REF] Najafzadeh | Co-design and verification of an available file system[END_REF] (first one to acquire lock proceeds; others abort), or requiring roll-backs [START_REF] Kleppmann | Opsets: Sequential specifications for replicated datatypes (extended version)[END_REF] (the move operation ordered first proceeds, all concurrent operations are rolled back). Najafzadeh et al. [START_REF] Najafzadeh | Co-design and verification of an available file system[END_REF] shows that there can be no coordination-free solution to this problem that is not anomalous.

To support low latency, high availability, and safety, this paper introduces a new light-weight, coordination-free, safe, replicated CRDT [START_REF] Shapiro | Conflict-free replicated data types[END_REF] tree data structure, called Maram. Maram supports the usual operations to query the state, to add or to remove a node, and also supports an atomic move operation. The price to pay is that some move operations "lose", i.e., have no effect; achieving the same end result as previous correct approaches but at a lower cost. Query and add are unremarkable. Remove marks the corresponding node as a "tombstone," but leaves it in the data structure, as is common in replicated data structures [START_REF] Attiya | Specification and complexity of collaborative text editing[END_REF]. We show that moves can be divided into two cases: two concurrent up-moves are always safe. We devise a deterministic arbitration rule for conflicts of down-move: against a concurrent up-move, the up-move wins, and the down-move loses; against a concurrent down-move, the down-move with the highest priority (as defined in Section 4.2) wins and the other loses.

We prove Maram to be safe, even in the presence of concurrent updates (including moves), despite being coordination-free and without any roll-backs. Using the Why3 proof assistant, we apply the CISE proof methodology [START_REF] Gotsman | Cause I'm Strong Enough: Reasoning about consistency choices in distributed systems[END_REF], with the following steps:

1. Sequential safety: We show that the initial state satisfies the tree invariant, and that every individual update operation has a precondition strong enough to maintain the invariant.

Convergence:

We show that any two operations that may execute concurrently commute.

Precondition stability:

We show that for any two operations u, v that may execute concurrently, u preserves the precondition of v, and vice-versa. It follows that every state reachable from the initial state, sequentially or concurrently, satisfies the tree invariant. 2 Maram satisfies an additional desirable property, monotonic reads [START_REF] Terry | Session guarantees for weakly consistent replicated data[END_REF]. This requires that a replica that has delivered some update will not roll it back.

Losing an operation might have impacts on the causally dependent future operations. We devise a independence analysis to capture this effect. The move operations lose if it is dependent on another move operation that loses.

This paper presents the principles of Maram, proves its correctness, and compares the performance of Maram to competing solutions in a simulated geo-replicated environment. The response time of Maram is 1.35 times of the safe rollback-based design, and 1.36 times of the unsafe uncoordinated design (both due to overhead of computing the metadata required for conflict resolution), and up to 11 times faster than (safe) lock-based designs. Furthermore, Maram stabilises (updates become definitive) three orders of magnitude faster than a safe rollback-based design.

This paper proceeds as follows. Section 2 formalises our system model, explains our proof methodology, and defines the tree invariant. In Section 3 we discuss the sequential correctness of a replicated tree. Section 4 proceeds with the proof of convergence, precondition stability and independence, resulting in concurrent safety. In Section 5 we compare the performance of Maram with competing designs. Section 6 overviews the related literature. Finally, in Section 7 we discuss lessons learned and their significance.

Preliminaries

System Model

A distributed system is modelled as a set of processes, distributed over a (high-latency, failureprone) communication network. The processes have disjoint memory and processing capabilities, and they communicate through message passing. A process does not fail. Every message is eventually delivered to its destination. Message delivery is consistent with happens-before (causal consistency).

State and invariant:

The data structure (in this case, a tree) is replicated at a number of processes, called its replicas. The information managed by a replica on behalf of the data structure is called its local state. The union of local states is called the global state. 3A data structure is associated with an invariant, a predicate that must always be satisfied in every local state of a replica. Although evaluated locally, an invariant describes a global property, in the sense that it must be true at all replicas.

Operations:

An unspecified client application submits an operation at some replica of its choice, which we call the origin replica of that operation. For availability, the origin replica should carry out the operation without waiting to coordinate with other replicas.

An update operation has a postcondition that specifies the state after the operation executes, and a precondition that indicates the domain of the operation. As discussed in more detail later, when the operation executes with no concurrency, its precondition guarantees that the operation terminates with the postcondition satisfied.

Updates:

When a client submits an operation, the origin replica generates an effector (a side-effecting lambda), atomically applies the effector to the origin state, and sends the effector to all the other replicas. Every replica eventually receives and delivers the effector, atomically applying it to its own local state. 4 The effector eventually executes at every replica.

We assume that effectors are delivered in causal order. This means that, if some replica that observed an effector u later generates an effector v, then any replica that observes v has previously observed u. 5In what follows, we ignore queries, and identify an update operation with executing its effector at all replicas.

Properties and associated Proof Rules

Consider some data structure (in this case a tree) characterized by a safety invariant (in this case, the tree invariant). We say that a state is local-safe if it satisfies the data structure's invariant. An update is op-safe if, starting from a local-safe state, it leaves it a local-safe state. The distributed data structure is safe if every update is op-safe. According to the CISE logic [START_REF] Gotsman | Cause I'm Strong Enough: Reasoning about consistency choices in distributed systems[END_REF], a distributed data structure is safe if the following properties hold:

1. Sequential safety: Consider an environment restricted to sequential execution (operations execute one after another; there is no concurrency). If the initial state is local-safe at every replica, and each update is op-safe, it follows that the data structure is safe under sequential execution. Classically, sequential op-safety implies that each operation's precondition satisfies the weakest-precondition of the invariant with respect to the operation [START_REF] Edsger | Guarded commands, nondeterminacy and formal derivation of programs[END_REF]. 2. Convergence: Strong Eventual Consistency (SEC) [START_REF] Shapiro | Conflict-free replicated data types[END_REF] states that two replicas that have delivered the same set of operations must be in the same state, i.e., the system converges. If operations commute (as defined later), then SEC is guaranteed [START_REF] Shapiro | Conflict-free replicated data types[END_REF]. 3. Precondition stability: In addition to sequential safety, updates must remain op-safe in the presence of concurrent (uncoordinated) updates. To ensure this, we apply the CISE precondition stability rule [START_REF] Gotsman | Cause I'm Strong Enough: Reasoning about consistency choices in distributed systems[END_REF]: consider two updates u and v; if the execution of u does not make the precondition of v false, nor vice-versa (precondition stability), then executing u and v concurrently is op-safe. This must be true for all concurrent pairs of operations. CISE logic helps us identify the conditions under which concurrent operations conflict. When conflicting, CISE requires the operations to acquire tokens, that bring in a global synchronization point. Hence all updates in CISE are assumed to be definitive.

In order to augment the CISE analysis for handling tentative updates, we add a condition for independence to check whether skipping a move affects a move that already observed the effect of the skipped one. The independency analysis is inspired from Houshmand and Lesani [START_REF] Houshmand | Hamsaz: Replication coordination analysis and synthesis[END_REF], even though they also, like CISE, do not consider tentative updates.

Independence analysis: Consider two updates u and v that are safe, u executed before v. If moving v before u still maintains the safety of v, v is said to be independent of u. Otherwise, if v is unsafe before executing u, v is dependent on the effect of u.

Sequential safety

Let us refine the proof obligations of the first step, sequential safety, i.e., local-safety under sequential execution.

The set of reachable states comprises the initial state, and all states transitively reachable as a result of executing updates sequentially. The set of reachable states is a subset of the set of all possible states. Formally, we note the set of states Σ, a state σ, the initial state σ init , an update u, its precondition Pre u , and the set of updates U . When execution is sequential:

σinit ∈ Σ (1)
and

∀u ∈ U, σ ∈ Σ σ |= Preu =⇒ u(σ) ∈ Σ (2)
Σ is the smallest set satisfying (1) and ( 2) through a sequence of legal updates from the initial state.

The data structure must satisfy its invariant in every sequentially reachable state: this property is called sequential safety. Formally, if Inv denotes the invariant, then

∀σ ∈ Σ σ |= Inv (3)
If the initial state is safe and all sequential updates preserve the invariant, by induction, the data structure is sequentially safe. Formally, if the initial state, σ init , satisfies the invariant, Inv ,

σinit |= Inv (4)
and each update u executing on a state σ preserves the invariant,

∀u ∈ U, σ, σ ∈ Σ σ |= (Inv ∧ Preu) ∧ u(σ) = σ =⇒ σ |= Inv (5)
then the invariant holds true for all reachable states. P re u is the weakest precondition required to maintain the safety of update u. Weakest precondition for an update can be calculated by predicate transformer semantics as described by Dijkstra [START_REF] Edsger | Guarded commands, nondeterminacy and formal derivation of programs[END_REF].

Concurrency

Let us now turn to concurrent execution, and consider the proof obligations for convergence and safety.

Convergence If a replica initiates an update u, while concurrently another replica initiates v, the first replica executes their effectors in the order u; v and the second one in the order v; u. Without precaution, it is likely that their states diverge.

To prevent this, the Strong Eventual Consistency (SEC) property [START_REF] Shapiro | Conflict-free replicated data types[END_REF] requires that any two replicas that delivered the same updates are in equivalent states. To satisfy SEC, effector functions are designed to commute, i.e., both orders above leave the data in the same state. We define commutativity as follows:

∀u1, u2 ∈ U, σ, σ1, σ2 ∈ Σ u1(σ) = σ1 ∧ u2(σ) = σ2 =⇒ u2(σ1) = u1(σ2) (6)

Inria

Precondition stability The main proof obligation, for concurrent execution, is that the precondition of any effector is stable against (i.e., not negated by) an effector that may execute concurrently [START_REF] Gotsman | Cause I'm Strong Enough: Reasoning about consistency choices in distributed systems[END_REF]. This CISE rule is a variant of rely-guarantee reasoning, adapted to a replicated system where effectors execute atomically and definitively. The precondition stability condition can be formally specified as follows:

∀u1, u2 ∈ U, σ, σ ∈ Σ σ |= (Inv ∧ Preu 1 ∧ Preu 2 ) ∧ u1(σ) = σ =⇒ σ |= Preu 2 (7)
Gotsman et al. [START_REF] Gotsman | Cause I'm Strong Enough: Reasoning about consistency choices in distributed systems[END_REF] uses Tokens to formalize concurrency control. Two operations that share the same token do not execute concurrently. Since we are designing a coordination-free data structure, we consider the set of tokens to be an empty set, and hence absent from the formalisation.

Independence In order to ensure that the safety of an operation, is not impacted by skipping any previous operations, we augment the precondition stability analysis with an independence analysis as presented by Houshmand and Lesani [START_REF] Houshmand | Hamsaz: Replication coordination analysis and synthesis[END_REF]. An operation u 2 is said to be independent of operation u 1 if the precondition of u 2 , Pre u2 , is enabled even without executing u 1 . The condition for independency can be formally specified as follows:

∀u1, u2 ∈ U, σ, σ , σ , σ ∈ Σ σ |= (Inv ∧ Preu 1 ) ∧ σ |= (Inv ∧ Preu 2 ) ∧σ |= Inv ∧ u1(σ) = σ ∧ u2(σ ) = σ ∧ u2(σ) = σ =⇒ σ |= Preu 2 ∧ σ |= Inv (8)
In short, u 2 is independent of u 1 if, irrespective of whether u 1 executed before u 2 , the execution of u 2 is safe. This condition is required for safety only if the effect of u 1 is tentative, i.e., if u 1 has conflict resolution policies while applying the update on the state.

Mechanized verification

In order to mechanically discharge the proof obligations listed above, we the use Why3 system [START_REF] Filliâtre | Why3 -Where Programs Meet Provers[END_REF], augmented with the CISE3 plug-in [START_REF] Meirim | CISE3: Verifying weakly consistent applications with why3[END_REF]. Why3 is a framework used for the deductive verification of programs, i.e., "the process of turning the correctness of a program into a mathematical statement and then proving it" [START_REF] Filliâtre | Deductive software verification[END_REF]. The CISE3 plug-in automates the CISE proof rules described above, and generates the required sequential-safety, commutativity and stability checks. Why3 then computes a set of proof obligations, that are discharged via external theorem provers.

3 Sequential specification of a tree

State

The state of a tree data structure consists of a set of nodes, Nodes, and a relation from a child node to its parent, indicated by →. The ancestor relation, → * is defined as

∀a, n ∈ Nodes n → * a =⇒ n → a ∨ ∃p ∈ Nodes n → p ∧ p → * a (9)
At initialization, the set of nodes consists of a single root node. The parent of the root is root itself. The initial state of the tree is thus Nodes = {root} where root → root. A crucial aspect of the abstract representation of the tree is how to express the relation between nodes. Three choices are possible, either maintain a child-to-parent relation, a parent-to-child relation, or both. In particular, when implementing a tree, traversal efficiency depends on keeping both up and down pointers [START_REF] Vinh | Ensuring Availability and Managing Consistency in Geo-Replicated File Systems[END_REF]. Considering that child-to-parent and parent-to-child relations describe a dual view of a tree (i.e., node p is the parent of node n iff node n is a descendent of node p) we selected the one that leads to a simpler specification. An advantage of using a child-to-parent relation is that it can be maintained as a function, as the tree properties ensure that each node has a unique parent. The alternative parent-to-child relation would need a more complex representation, e.g. a function that maps each node to its set of direct descendants, which would impact the simplicity of the specification and the proof effort.

Invariant

The invariant of the tree data structure is as follows:

root ∈ Nodes ∧ root → root ∧ ∀ ∈ Nodes n = root =⇒ root → n (Root) ∧ ∀n ∈ Nodes ∃p ∈ Nodes n → p (Parent) ∧ ∀n, p, p ∈ Nodes n → p ∧ n → p =⇒ p = p (Unique) ∧ ∀n ∈ Nodes n → * root (Reachable) Inv Root ∧ Parent ∧ Unique ∧ Reachable (10)
Clause Root states that the root node is present in Nodes, and is the only node to be its own parent. Clause Parent asserts that every node in the tree has a parent in the tree. Clause Unique requires the parent of a node to be unique. Clause Reachable imposes that the root is an ancestor of all nodes. We call this conjunction, Equation ( 10), the tree invariant.

A further invariant which forbids cycles can be derived:

∀n ∈ Nodes n = root =⇒ n → * n (Acyclic)
Since the parent relation inductively defines the ancestor relation, by Unique there is a unique path to a given ancestor of a node. By Reachable, the root node is an ancestor of every node in the tree. In this scenario, a cycle would require a node to have multiple parents, which is prevented by Unique.

Operations

Add An add operation has two arguments: the node to be added, n, and its prospective parent, p. The add effector adds node n to Nodes and the mapping n → p to the parent relation. The postcondition of the add effector indicates this:

6 Post add(n,p) n ∈ Nodes ∧ n → p (11)
To ensure the tree invariant, we derive the precondition that n is a new node and p is already in the tree, i.e.,

Pre add(n,p) n / ∈ Nodes ∧ p ∈ Nodes (12)
Let us see how this precondition is derived. If the add operation is updating a safe state, i.e., the starting state respects the invariant, and if the precondition is satisfied, then the update should maintain the invariant. Hereafter, we highlight the precondition clauses needed to ensure each part of the invariant.7

Precondition Invariant clause

Root Parent Unique Reachable add(n, p) n / ∈ Nodes p ∈ Nodes n / ∈ Nodes p ∈ Nodes rem(n) n = root ∀n ∈ Nodes n → n true ∀n ∈ Nodes n → n move(n, p ) n = root p ∈ Nodes true p ∈ Nodes ∧ p = n ∧ p → * n
Table 1: Precondition required by each operation to uphold specific clauses of the invariant

Inv ∧ n / ∈ Nodes add(n, p) Post add(n,p) ∧ Root ∧ Unique Inv ∧ p ∈ Nodes add(n, p) Post add(n,p) ∧ Parent ∧ Reachable
Table 1 lists the preconditions required by operations to preserve each invariant clause. With the derived preconditions, the add operation can be specified as follows:

(Add-Operation) Inv ∧ n / ∈ Nodes ∧ p ∈ Nodes add(n, p) Inv ∧ n ∈ Nodes ∧ n → p
If the add operation is issued on a state that is safe and contains p but not n, then n is added to the tree with parent p.

Remove operation Remove receives as argument a node n to be deleted. Its effector removes node n from the set of nodes. The postcondition of remove indicates this effect:

Post rem(n) n / ∈ Nodes (13)
Similarly to add, we list the predicates needed to preserve each clause of the invariant in Table 1.

In the case of the remove operation, we need to ensure that n is not the root, and n is a leaf node, i.e., there are no child nodes for n. The remove can be specified as follows:

(Remove-Operation)

Inv ∧ n = root ∧ ∀ n ∈ Nodes n → n rem(n) Inv ∧ n / ∈ Nodes
If a remove operation is issued on a safe state where n is not root and has no children, then n is removed from the tree.

Move operation

The move operation takes two arguments: the node to be moved n, and the new parent p . Its effector changes the parent of node n to p as follows:

Post move(n,p ) n → p (14)
To preserve the expected behaviour we require that the node to be moved is already present in the tree. We derive the safety clauses as shown in Table 1. Formally, the move operation can be specified as follows:

(Move-Operation) Inv ∧ n ∈ Nodes ∧ n = root ∧ p ∈ Nodes ∧ p = n ∧ p → * n move(n, p ) Inv ∧ n → p RR n°9395
For the move operation to be safe, n is not the root, p is in the tree, n and p are different, and p is not a descendant of n. These last two conditions are needed to prevent move from creating a cycle of unreachable nodes, as we show with the following counterexample. Consider a tree composed of nodes a and b. Root node R is the parent of node a, i.e., a → R and node a is the parent of node b, b → a, and hence R is the ancestor of b, b → * R. Moving a under b will make both a and b unreachable from the root, and also form a cycle. This violates the invariant by invalidating the tree structure. To avoid this scenario, a precondition is needed that prevents moving a node underneath itself. When moving node n from its current parent to the new parent p , p should not be a descendant of n, p → * n.

Mechanized verification of the sequential specification

Following the formalization of the tree data structure above, we use Why3 to mechanically prove its sequential safety. The mechanical proof requires some extra definitions and axioms.

We need a predicate for reachability. For this, we first define a path, a sequence of nodes related by the parent relation. We use s[n] to indicate the nth element in the sequence s. We denote the set of possible sequences of nodes by S. The path predicate determines the validity conditions for a path s between nodes x and y in state σ. If x = y, the path has length zero. Otherwise, the length of the path is greater than zero, where the first path element must be x, all contiguous path elements are related by the parent relation, and node y is the parent of the last path element. We say y is reachable from x if there exists a path from x to y. Formally,

path(σ, x, y, s) length(s) = 0 ∧ x = y (15)
∨ (length(s) > 0 ∧ s[0] = x ∧ s[length(s) -1] → y ∧ ∀ 0 ≤ i < length(s) -1 s[i] → s[i + 1])
reachability(σ, x, y) ∃s ∈ S path(σ, x, y, s)

To formalize the properties of the path predicate, we define a set of axioms as follows:

path to parent ∀σ ∈ Σ ∀x, y ∈ Nodes x → y =⇒ ∃s ∈ S path(σ, x, y, s) ∧ s = [x] ( 17
)
path composition ∀σ ∈ Σ ∀x, y, z ∈ Nodes ∃s1 ∈ S path(σ, x, y, s1)

∧ y → z =⇒ ∃s2 ∈ S path(σ, x, z, s2) ∧ s2 = s1 + [y] (18)
path transitivity ∀σ ∈ Σ ∀x, y, z ∈ Nodes, s1, s2 ∈ S path(σ, x, y, s1)

∧ path(σ, y, z, s2) =⇒ ∃s3 ∈ S path(σ, x, z, s3)

∧ s3 = s1 + s2 path uniqueness ∀σ ∈ Σ ∀x, y ∈ Nodes, s1, s2 ∈ S path(σ, x, y, s1) (20) ∧ path(σ, x, y, s2) =⇒ s1 = s2 path exclusion ∀σ ∈ Σ ∀x, y, z ∈ Nodes, s ∈ S x → * y ∧ path(σ, z, y, s) =⇒ x / ∈ s (21) path separation ∀σ ∈ Σ ∀x, y, z ∈ Nodes, s1, s2 ∈ S path(σ, x, y, s1) (22) ∧ path(σ, y, z, s2) ∧ x = y ∧ x = z ∧ y = z =⇒ s1 ∩ s2 = ∅
Axiom path to parent defines the singleton path of a node to its parent. The recursive composition of paths is axiomatized in path composition. The transitivity property is defined in path transitivity. Axiom path uniqueness asserts there is a single path between two nodes. The path exclusion expresses the conditions for excluding nodes from a path. Lastly, path separation defines a convergence criterion essential for Why3's SMT solvers, asserting that the direction of the path is converging towards the root.

We also require extra axioms to express the properties of the unaffected nodes in the case of Inria add and move operations. They are as follows:

σ add = add(n, p)(σ) σmove = move(n, p)(σ) remaining nodes add ∀σ ∈ Σ ∀n ∈ Nodes, s1, s2 ∈ seq(Nodes) n = n (23) ∧ path(σ, n , root, s1) ∧ path(σ add , n , root, s2) =⇒ s1 = s2 descendants move ∀σ ∈ Σ ∀n ∈ Nodes, s1, s2 path(σ, n , c, s1) (24)
∧ path(σmove, n , c, s2

) =⇒ s1 = s2 remaining nodes move σ ∈ Σ ∀n ∈ Nodes, s1, s2 n → * n (25) ∧ path(σ, n , root, s1) ∧ path(σmove, n , root, s2) =⇒ s1 = s2
The state σ add is obtained by applying add(n, p) operation to σ. The axiom remaining nodes add asserts that the paths already present in the tree remain in the tree after executing the add operation. Given that the move operation updates σ to σ move , axiom descendants move asserts that the descendants of the node being moved continue to be its descendants, and remaining nodes move asserts that other paths are not affected. These axioms are defined to ensure that the paths to the root, from nodes unaffected by move or add operations, remain unchanged. The specification proven using Why3 is available in Meirim et al. [START_REF] Meirim | Maram proof files[END_REF].

Concurrent tree specification

In this section, we discuss the convergence and concurrent safety of the tree. In a sequential execution environment, as seen in Section 3, if the initial state and each individual update are safe, then all reachable states are safe. This is not true when executing concurrently on multiple replicas. In this case, there are three extra proof obligations (Subsection 2.2.2, Subsection 2.2.2, Subsection 2.2.2):

• Ensuring that different replicas converge, despite effectors being executed concurrently in different orders.

• Ensuring that safety of an update is not violated by a concurrent update.

• Ensuring that a tentative update does not effect the safety of the dependent update.

For ease of exposition, first we discuss concurrent safety; convergence is deferred to Subsection 4.3, since the conflicts occurring in the latter can be addressed using the policies discussed in the former, and independence is discussed in Subsection 4.4.

Precondition stability

We use the precondition stability rule of CISE logic (Subsection 2.2.2) to analyze the concurrent safety of our tree data structure. For each operation, we analyze whether it violates the precondition of any other concurrent operation. Formally, operation op 1 is stable under operation op 2 if,

Inv ∧ Preop 1 ∧ Preop 2 op2 Inv ∧ Postop 2 ∧ Preop 1 (26)
We check the sequential specification for stability. If this fails, then it will be necessary to modify the specification, so that it does satisfy stability.

Stability of add operation

Concurrent adds: First we check the stability of the precondition of add against itself. Let us consider two operations add(n 1 , p 1 ) and add(n 2 , p 2 ). Using Equation (26), we get

Pre add(n 1 ,p 1 ) n1 / ∈ Nodes ∧ p1 ∈ Nodes Pre add(n 2 ,p 2 ) n2 / ∈ Nodes ∧ p2 ∈ Nodes Post add(n 2 ,p 2 ) n2 ∈ Nodes ∧ n2 → p2 Inv ∧ Pre add(n 1 ,p 1 ) ∧ Pre add(n 2 ,p 2 ) ∧ n1 = n2 add(n2, p2) Inv ∧ Post add(n 2 ,p 2 ) ∧ Pre add(n 1 ,p 1 ) (27)
The highlighted clause n 1 = n 2 is required for the stability condition. Indeed, the sequential specification does not disallow adding the same node at different replicas, and the clause n / ∈ Nodes is unstable therein. Thus the analysis highlights a subtlety.

Concurrent remove: Let us check the stability of the precondition of add(n 1 , p 1 ) against a concurrent remove(n 2 ). Using (26), we get:

Pre add(n 1 ,p 1 ) n1 / ∈ Nodes ∧ p1 ∈ Nodes Pre remove(n 2 ) n2 = root ∧ ∀ n ∈ Nodes n → n2 Post remove(n 2 ) n2 / ∈ Nodes Inv ∧ Pre add(n 1 ,p 1 ) ∧ Pre remove(n 2 ) ∧ n2 = p1 remove(n2) Inv ∧ Post remove(n 2 ) ∧ Pre add(n 1 ,p 1 ) (28)
In the sequential specification, clause p 1 ∈ Nodes in the precondition of add is unstable against a remove of its parent; performing those operations concurrently would be unsafe.

To fix this, we see two possible approaches. The classical way is to strengthen the precondition with coordination, for instance locking to avoid concurrency. We reject this, as it conflicts with our objective of availability under partition. Our alternative is to weaken the specification thanks to coordination-free conflict resolution. We apply a common approach, to mark a node as deleted, as a so-called tombstone, without actually removing it from the data structure. 8We now distinguish a concrete state and its abstract view. We modify the specification to include a set of tombstones, TS (initially empty), in the concrete state. The abstract state is the resolved state as seen by some application using Maram. An abstraction function maps the concrete state to the abstract state.

The concrete and abstract states of a tree are the same if either there are no nodes in the set of tombstones or for each node in the set of tombstones, all its descendants are also present in the set of tombstones. In other cases, the abstraction function need to provide guidance on the presence of the descendants of a node that appears in the set of tombstones.

We present two abstraction functions -skipping abstraction and keeping abstraction. The skipping abstraction skips the descendants of the node that is marked as a tombstone. The keeping abstraction, on the other hand, preserves the tombstoned node if it observes the node has a descendant not in the set of tombstones. Both the abstraction functions satisfy the required safety properties since they only change the view of the tree for an application. Therefore the choice is application-specific. To illustrate the difference, consider the tree consisting of the root and a single child, as shown in Figure 1. One replica performs a remove of node p, while concurrently another replica adds n under p. In the first replica, node p is marked as a tombstone in the concrete state (the shaded box). Thus, the abstract state shows node p removed. When the replicas exchange their updates, they converge to the concrete state (the state in the shaded box). Figure 1a and Figure 1b show the result of a skipping abstraction and keeping abstraction respectively. In both the cases, node p is marked as a tombstone. In the case of the skipping abstraction, node p and the descendants are "skipped". Meanwhile for keeping abstraction, since its descendant n is not a tombstone, p is "revived" in the abstract view. With tombstones, let us update the postcondition for remove:

Post remove(n) n ∈ TS (31)
Let us now derive the predicates needed to preserve each clause of the invariant in this refined case.

Inv ∧ n = root remove(n) Post remove(n) ∧ Root Inv ∧ true remove(n) Post remove(n) ∧ Parent Inv ∧ true remove(n) Post remove(n) ∧ Unique Inv ∧ true remove(n) Post remove(n) ∧ Reachable
To maintain sequential safety in the modified remove specification, the precondition forbids only removing the root node. As the remove operation does not alter the tree structure, reachability is not impacted. The refined specification of the remove operation is as follows:

(Remove-Operation)

Inv ∧ n = root remove(n) Inv ∧ n ∈ TS
The application could strengthen this precondition with an added clause to delete only the leaf nodes visible in the abstract view. This helps prevent accident loss of a sub-tree. Since this is not necessary for safety, we are not considering that condition.

Concurrent move: Next we check the stability of the precondition of add under a concurrent move operation. Let us consider two operations add(n 1 , p 1 ) and move(n 2 , p 2 ). Using (26), we get

Pre add(n 1 ,p 1 ) n1 / ∈ Nodes ∧ p1 ∈ Nodes Pre move(n 2 ,p 2 ) n2 ∈ Nodes ∧ n2 = root ∧ p 2 ∈ Nodes ∧ p 2 = n2 ∧ p 2 → * n2 Post move(n 2 ,p 2 ) n2 → p 2 Inv ∧ Pre add(n 1 ,p 1 ) ∧ Pre move(n 2 ,p 2 ) ∧ true move(n2, p 2 ) Inv ∧ Post move(n 2 ,p 2 ) ∧ Pre add(n 1 ,p 1 ) (32)
We see that the precondition of add is stable against a concurrent move operation.

Stability of remove operation

Concurrent add: Consider the sequential specification of two operations remove(n 1 ) and add(n 2 , p 2 ). Using (26), we get

Pre remove(n 1 ) n1 = root ∧ ∀ n ∈ Nodes n → n1 Pre add(n 2 ,p 2 ) n2 / ∈ Nodes ∧ p2 ∈ Nodes Post add(n 2 ,p 2 ) n2 ∈ Nodes ∧ n2 → p2 Inv ∧ Pre remove(n 1 ) ∧ Pre add(n 2 ,p 2 ) ∧ n1 = p2 add(n2, p2) Inv ∧ Post add(n 2 ,p 2 ) ∧ Pre remove(n 1 ) (33)

Inria

We see that the clause that node n 1 has to be a leaf node is not satisfied if n 1 = p 2 since add operation introduces a child node under p 2 . However, the refined specification of tombstones as described above does not require the node n 1 to be a leaf node. So that solution fixes this conflict as well.

Concurrent remove: Consider the sequential specification of two remove operations remove(n 1 ) and remove(n 2 ). Using (26), we get

Pre remove(n 1 ) n1 = root ∧ ∀ n ∈ Nodes n → n1 Pre remove(n 2 ) n2 = root ∧ ∀ n ∈ Nodes n → n2 Post remove(n 2 ) n2 / ∈ Nodes Inv ∧ Pre remove(n 1 ) ∧ Pre remove(n 2 ) ∧ true remove(n2) Inv ∧ Post remove(n 2 ) ∧ Pre remove(n 1 ) (34)
We see that the remove operation is stable under a concurrent remove. Furthermore, the refined specification is also stable since it adds n 1 and n 2 to TS .

Concurrent move: Consider the sequential specification of two operations remove(n 1 ) and move(n 2 , p 2 ). Using (26), we get

Pre remove(n 1 ) n1 = root ∧ ∀ n ∈ Nodes n → n1 Pre move(n 2 ,p 2 ) n2 ∈ Nodes ∧ n2 = root ∧ p 2 ∈ Nodes ∧ p 2 = n2 ∧ p 2 → * n2 Post move(n 2 ,p 2 ) n2 → p 2 Inv ∧ Pre remove(n 1 ) ∧ Pre move(n 2 ,p 2 ) ∧ n1 = p 2 move(n2, p 2 ) Inv ∧ Post move(n 2 ,p 2 ) ∧ Pre remove(n 1 ) (35)
We see that the clause for the remove operation that n 1 should be a leaf node is violated if a node is moved under it. Again, we can observe that the refined specification of remove eliminates this issue due to the absence of the violation-causing clause.

Stability of move operation

Concurrent add: Consider the sequential specification of two operations move(n 1 , p 1 ) and add(n 2 , p 2 ). Using (26), we get

Pre move(n 1 ,p 1 ) n1 ∈ Nodes ∧ n1 = root ∧ p 1 ∈ Nodes ∧ p 1 = n1 ∧ p 1 → * n1 Pre add(n 2 ,p 2 ) n2 / ∈ Nodes ∧ p2 ∈ Nodes Post add(n 2 ,p 2 ) n2 ∈ Nodes ∧ n2 → p2
Inv ∧ Pre move(n 1 ,p 1 ) ∧ Pre add(n 2 ,p 2 ) ∧ true add(n2, p2)

Inv ∧ Post add(n 2 ,p 2 ) ∧ Pre move(n 1 ,p 1 ) (36)
The precondition of move is stable against a concurrent add operation.

Stability

Pre move(n 1 ,p 1 ) n1 ∈ Nodes ∧ n1 = root ∧ p 1 ∈ Nodes ∧ p 1 = n1 ∧ p 1 → * n1 Pre remove(n 2 ) n2 = root ∧ ∀ n ∈ Nodes n → n2 Post remove(n 2 ) n2 / ∈ Nodes Inv ∧ Pre move(n 1 ,p 1 ) ∧ Pre remove(n 2 ) ∧ n2 = p 1 remove(n2) Inv ∧ Post remove(n 2 ) ∧Pre move(n 1 ,p 1 ) (37)
Observe here that removing n 2 violates the clause p 1 ∈ Nodes if n 2 and p 1 are the same. However, in our refined specification, the postcondition of remove is n 2 ∈ TS , keeping the clause p 1 ∈ Nodes stable.

Concurrent move: Consider the sequential specification of two operations move(n 1 , p 1 ) and move(n 2 , p 2 ). Using (26), we get

Pre move(n 1 ,p 1 ) n1 ∈ Nodes ∧ n1 = root ∧ p 1 ∈ Nodes ∧ p 1 = n1 ∧ p 1 → * n1 Pre move(n 2 ,p 2 ) n2 ∈ Nodes ∧ n2 = root ∧ p 2 ∈ Nodes ∧ p 2 = n2 ∧ p 2 → * n2 Post move(n 2 ,p 2 ) n2 → p 2 Inv ∧ Pre move(n 1 ,p 1 ) ∧ Pre move(n 2 ,p 2 ) ∧ p 1 → * n2 move(n2, p 2 ) Inv ∧ Post move(n 2 ,p 2 ) ∧ Pre move(n 1 ,p 1 ) (38)
We see here that a concurrent move of p 1 or an ancestor of p 1 invalidates the precondition clause p 1 → * n 1 that prevents a cycle from forming. This is a subtle condition missed in many previous works [START_REF] Kleppmann | Opsets: Sequential specifications for replicated datatypes (extended version)[END_REF][START_REF] Najafzadeh | Co-design and verification of an available file system[END_REF][START_REF] Tao | Merging semantics for conflict updates in geo-distributed file systems[END_REF]; hence it highlights the value of a formal analysis. We discuss this condition in more detail in Subsection 4.2 and explain how we refine the specification for stability. Table 2 shows the summary of the stability analysis on the sequential specification discussed in Section 3. A condition indicates that the precondition of the operation in that row is stable under the operation in the column under the condition.

Safety of concurrent moves

We closely examine how a move operation on a remote replica might affect the precondition of a concurrent move in the local replica. Consider an operation move(n, p ). In a sequential execution, precondition clause p → * n forbids moving a node under itself (which would cause a cycle). However a concurrent move of p under n will not preserve the precondition of the operation, p → * n, resulting in a cycle. This issue generalizes to p or its ancestor concurrently moving under n or a descendant of n. For easy reference, we call this move as a cycle-causing-concurrent-move. Observe that the precondition prevents an ancestor of n moving under itself in sequential execution. Therefore, only the ancestors of p that are not ancestors of n would lead to a cycle. We call this set of ancestors critical ancestors, and the set of n and its descendants critical descendants as defined in Table 3.

Consider two concurrent move operations move(n, p ) and move(p , n). Figure 2 shows the critical ancestors and critical descendants of both move operations. The node l is common ancestor of both n and p farthest from the root. The critical ancestors and critical descendants of move(n, p ) are grouped together in the dark gray region with and without a border respectively, and that of move(p , n) are grouped together in the light gray region.

Note that the set of critical descendants of a move overlaps with the critical ancestors set of its corresponding cycle-causing-concurrent-move. Hence, we consider only the critical ancestors of move operations.

Let us take a step back and analyze the types of move operations. Some move operations result in a node moving farther away from the root, called down-moves, and another set of move operations result in the node moving nearer to the root, or to remain at the same distance from the root, called up-moves. We define rank as the distance of a node from the root node, as follows:

rank (root) = 0 (39) rank (n) = rank (p) + 1 | ∀n, p ∈ Nodes n → p (40) up-move(n, p ) =⇒ rank(n) > rank(p ) (41) down-move(n, p ) =⇒ rank(n) ≤ rank(p ) (42) Commutativity Operations add (n 2 , p 2 ) rem(n 2 ) move(n 2 , p 2 ) add (n 1 , p 1 ) rem(n 1 ) move(n 1 , p 1 ) ¬(n 1 = n 2 ∧ p 1 = p 2 )
Table 4: Result of commutativity analysis of the sequential specification discussed in Section 3

Consider a move operation, move(n, p ), moving node n at the same level or towards the root, i.e., an up-move. This gives us that rank (n) > rank (p ). In this case, the rank of a critical descendant will be always greater than the rank of a critical ancestor. Formally,

∀n, p, p , d, a ∈ Nodes n → p ∧ rank (n) > rank (p ) ∧d → * n ∧ p → * a =⇒ rank (d) > rank (a) ( 43
)
This implies that a cycle-causing-concurrent-move can only be a down-move. Hence, we have that concurrent up-moves are safe; stability issues can occur only between two concurrent downmoves, or between an up-move and a down-move. Our next step is to design a coordination-free conflict resolution policy for the moves that conflict. The conflict resolution policy is required if both the concurrent move operations move a node in the set of critical ancestors of the other. If we have up-moves, we apply the effect of the operation. In case of a concurrent down-move and up-move, up-move wins and the down-move is skipped. In case of concurrent down-moves, we apply a deterministic conflict resolution policy; the operation with highest priority number wins. The priority number of a move operation is specific to each application, with a condition that it must be unique for each move.

Contrast our approach with the alternative that uses shared-exclusive locks for concurrent moves [START_REF] Najafzadeh | Co-design and verification of an available file system[END_REF]. Consider concurrent operations move(n, p ), moving node n under p , and move(p , n), moving node p under n. These operations compete for a lock. The one that succeeds first will apply its move, blocking the other. When it releases the lock, this releases the second one, but its precondition is no longer valid and it cannot execute. Thereby, safety is preserved, at the cost of aborting the second move. This work essentially achieves the same end result, but without the overhead of locking. Our experiments in Section 5 show the performance difference.

Convergence

As discussed in Section 2.2, to ensure convergence, we design the data structure such that concurrent updates commute [START_REF] Shapiro | Conflict-free replicated data types[END_REF]. Add and remove operations result in adding the added and removed node to Nodes and TS respectively. Since set union is commutative, each of these two operations commutes with itself and with the other.

The move operation changes the parent pointer of a node. It commutes with add and remove, since it doesn't have an effect on set membership.

However, observe that in the sequential specification two moves do not commute, if the same node is moved to two different places. This issue is fixed by the conflict resolution policy discussed earlier. The results of the commutativity analysis is show in Table 4.

Inria

Independence

We use the independence conditions from Subsection 2.2.2 to check for safety violations due to tentative moves. We check whether each operation is independent of up-move and down-move since they are the only operations that have tentative effects. For the dependent operations, we compute the condition under which it is dependent and use it to devise dependency resolution policies. In order to compute dependency conditions, we use the dependency analysis proposed by Houshmand and Lesani [START_REF] Houshmand | Hamsaz: Replication coordination analysis and synthesis[END_REF]. An operation op 2 is dependent on op 1 if the execution of op 1 enabled Pre op2 that was not enabled before its execution, i.e.,

Inv ∧ Preop 1 op1 Inv ∧ Postop 1 ∧ Preop 2 (44)
If the dependency condition evaluates to true, then op 2 is independent of op 1 . We use this analysis to check the independence of add, remove, up-move and down-move with respect to a historical tentative operation, i.e., an up-move or down-move performed before the operation under observation.

Independence of add operation

Historical up-move: We use Equation 4.4 as follows:

Pre up-move(n 1 ,p 1 ) n1 ∈ Nodes ∧ n1 = root ∧ p 1 ∈ Nodes ∧ n1 = p 1 ∧ p 1 → * n1 ∧ rank (n1) > rank (p 1 ) Post up-move(n 1 ,p 1 ) skip ∨ n1 → p 1 Pre add(n 2 ,p 2 ) p2 ∈ Nodes ∧ n2 / ∈ Nodes
Since the historical up-move doesn't change the membership of Nodes, we can see that add is independent of up-move.

Historical down-move: An add operation is independent of a historical down-move in the same manner because it does not change the membership of Nodes either.

Independence of remove operation

Historical up-move: For checking the independence of remove, Equation 4.4 becomes:

Pre up-move(n 1 ,p 1 ) n1 ∈ Nodes ∧ n1 = root ∧ p 1 ∈ Nodes ∧ n1 = p 1 ∧ p 1 → * n1 ∧ rank (n1) > rank (p 1 ) Post up-move(n 1 ,p 1 ) skip ∨ n1 → p 1 Pre remove(n 2 ) n2 = root
Since n 2 = root is unaffected by a historical up-move, remove is independent of up-move.

Historical down-move: Similarly to historical up-move, a historical down-move also has no impact of the precondition of a remove operation. Hence remove is independent of a historical down-move.

Independence of down-move operation

Historical up-move: The pre and postconditions required to analyse the dependence of a down-move operation under a historical up-move is as follows:

Pre up-move(n 1 ,p 1 ) n1 ∈ Nodes ∧ n1 = root ∧ p 1 ∈ Nodes ∧ n1 = p 1 ∧ p 1 → * n1 ∧ rank (n1) > rank (p 1 ) Post up-move(n 1 ,p 1 ) skip ∨ n1 → p 1 Pre down-move(n 2 ,p 2 ) n2 ∈ Nodes ∧ n2 = root ∧ p 2 ∈ Nodes ∧ n2 = p 2 ∧ p 2 → * n2 ∧ rank (n2) ≤ rank (p 2 )
Note that the reasoning for the up-move operation also remains valid here since the effect of both moves are the same, only their preconditions differ, only the clause comparing the ranks of the node and the new parent differs. The first part of the dependency condition remains, (n

1 = n 2 ∨ n 1 → * n 2 ) ∧ (p 2 = n 1 ∨ p 2 → * n 1 ).
The condition rank (n 2 ) ≤ rank (p 2 ) will be effected only if the historical up-move decreased the rank of n 2 . Hence we have the condition

n 2 = n 1 ∨ n 2 → * n 1 .
Combining the clauses, we have ((

n 1 = n 2 ∨ n 1 → * n 2 ) ∧ (p 2 = n 1 ∨ p 2 → * n 1 )) ∨ (n 2 = n 1 ∨ n 2 → * n 1 )
, the condition under which a down-move is dependent on a historical up-move.

Historical down-move: We consider the following pre and postconditions:

Pre down-move(n 1 ,p 1 ) n1 ∈ Nodes ∧ n1 = root ∧ p 1 ∈ Nodes ∧ n1 = p 1 ∧ p 1 → * n1 ∧ rank (n1) ≤ rank (p 1 ) Post down-move(n 1 ,p 1 ) skip ∨ n1 → p 1 Pre down-move(n 2 ,p 2 ) n2 ∈ Nodes ∧ n2 = root ∧ p 2 ∈ Nodes ∧ n2 = p 2 ∧ p 2 → * n2 ∧ rank (n2) ≤ rank (p 2 )
We use the reasoning as in the previous cases on these ang get p 2 = n 1 ∨ p 2 → * n 1 , the condition under which a down-move, down-move(n 2 , p 2 ), is dependent on a historial down-move, down-move(n 1 , p 1 ).

We see that up-move and down-move operations are dependent on each other and add and remove are independent of up-move and down-move. We also derived the conditions under which up-moves and down-moves are dependent on each other. We use this information to design dependence resolution policies.

Safe specification of a replicated tree

We incorporate the stability, commutativity, and independence analysis results and the design refinements, resulting in the coordination-free, safe and convergent replicated tree data structure specified in Specification 3. The state now consists of a set of nodes, Nodes, and tombstones, TS . Since the tombstones also form part of the tree, they also have to maintain the tree structure. The invariants refer to the set of nodes which includes tombstones.

We also introduce some definitions to help define the coordination-free and conflict-free upmove and down-move operations. We define an operation as a tuple consisting of its type (add, remove, up-move or down-move), its parameters, and its priority. The priority is arbitrary (e.g. supplied by the application); the only condition being that priorities are totally ordered. We define C as the set of operations concurrent with the operation under consideration. H is the set of operations seen by the current operation. We also define operations on critical ancestors as crit-anc-overlap, where the node being moved is a member of the set of critical ancestors of the other operation. self -or -under indicates the node itself and its descendants.

With the help of these definitions, we define the up-move and down-move operations in three parts: the actual precondition needed to ensure sequential safety, the conflict resolution condition (highlighted in light blue), the dependency condition (highlighted in dark blue), and

State: Nodes × TS Invariant: root → root ∧ ∀n ∈ Nodes root → n ∧ root / ∈ TS (Root) ∧ ∀n ∈ Nodes n = root ∧ ∃p ∈ Nodes n → p (Parent) ∧ ∀n, p, p ∈ Nodes n → p ∧ n → p =⇒ p = p (Unique) ∧ ∀n ∈ Nodes n = root =⇒ n → * root (Reachable) Add operation: (Add-Operation) Inv ∧ p ∈ Nodes ∧ n / ∈ Nodes add(n, p) Inv ∧ n ∈ Nodes ∧ n → p
Remove operation:

(Remove-Operation) Inv ∧ n = root remove(n) Inv ∧ n ∈ TS Definitions: operation (type, params, priority)
C set of concurrent operations H history of operations available at the origin replica crit-anc-overlap(op1, op2) op1.params.n ∈ critical ancestor (op2) ∧ op2.params.n ∈ critical ancestor (op1)

self -or -under (n) {n |n = n ∨ (n ∈ Nodes ∧ n → * n)}
Move operation:

(Up-move-Operation) Inv ∧ n ∈ Nodes ∧ n = root ∧ p ∈ Nodes ∧ n = p ∧ p → * n ∧ rank (n) > rank (p ) up-move(n, p ) op ∈ C op.type = up-move ∧ op.params.n = n ∧ op.priority > priority op ∈ H (op.type = up-move ∧ p ∈ self -or -under (op.params.n))
∨(op.type = down-move ∧ (n ∈ self -or -under (op.params.n) Inria the update on the state. Note that the conflict resolution and dependency checks are performed while applying the effect of the operation on the local and remote replicas, while the precondition is checked only at the local replica.

∨ (op.params.n ∈ self -or -under (n) ∧ p ∈ self -or -under (op.params.n)))) =⇒ Inv ∧ n → p (Down-move-Operation) Inv ∧ n ∈ Nodes ∧ n = root ∧ p ∈ Nodes ∧ n = p ∧ p → * n ∧ rank (n) ≤ rank (p ) down-move(n,

Mechanized verification of the concurrent specification

We use the CISE3 plug-in, presented in Section 2.2.3, to identify conflicts as shown in Tables 2 and4. Given the sequential specification from Section 3, CISE3 automatically generates a set of meta-operations to check stability and commutativity of executing pairs of operations.

Provable concurrent execution

We update the Why3 specification according to the conflict resolution policies from Section 4.5.

For example, for the add operation we place the new precondition that nodes must be uniquely identified:

assume { ... ∧ n1 = n2 }
Next, we refine the definition of type state to include tombstones, as follows:

type state = { mutable nodes: fset elt; ...; mutable tombstones: fset elt; }

We update the specification of the rem accordingly:

val rem (n : elt) (s : state) : unit ensures { s.tombstones = add n (old s).tombstones }

where add stands for the logical adding operation on sets. Finally, the implementation of the conflict resolution policy for a pair of move operations requires us to be a bit more creative. We update the state type definition to include ranking and critical ancestors information. We implement a custom analysis move refined operation since concurrent operations are not available off-the-shelf in Why3, a framework for verification of sequential specifications. We encode the arguments of two move operations as arguments of the move refined operation: n1 (n2), np1 (np2), and pr1 (pr2) stand for the node to be moved, the new parent, and the unique priority levels respectively, of the first (second) move.

All analysis functions, except move refined, are automatically generated by the CISE3 plugin of Why3. Finally, 55 verification conditions are generated for the implementation and given specification of move refined. All of these are automatically verified, using a combination of SMT solvers. The specification and the proof results are available at [START_REF] Meirim | Maram proof files[END_REF].

Evaluation

This paper presents the design of a coordination-free, safe, convergent, and highly available replicated tree. The specification of Maram doesn't require any synchronization to execute an operation; this implies that the design is coordination-free. Sections 3 and 4 provide a mechanized proof that our design is safe and convergent. In this section, we conduct an evaluation to showcase the high availability of our design.

We measure availability in two parts -response time and stabilization time. The first metric, response time, is the time taken to log and acknowledge a client request. Recall that the effect of a move operation in our specification consists of either updating the state, or a skip. The effect of the update will be definitive only after being aware of all its concurrent operations. In order We run the experiments10 with three replicas connected in a mesh with a FIFO connection and simulate different network latencies, zero latency, real world latency as shown in Table 5 and 10 times real world latency. Our warm-up workload, a mix of add, remove and move operations, creates a tree with 997 nodes including the root. We then have concurrent workloads 11 on the three replicas, varying conflict rates at 0%, 2%, 10%, and 20%.

We compare Maram with three solutions from the literature: (i) UDR tree (short for Undo-Do-Redo tree) [START_REF] Kleppmann | Opsets: Sequential specifications for replicated datatypes (extended version)[END_REF]; (ii) all move operations acquiring a global lock (Global l); and, (iii) move operations acquiring read locks on critical ancestors and write lock on the moving node (Subtree l) [START_REF] Najafzadeh | Co-design and verification of an available file system[END_REF].

The average response time for each design for different conflict rates with latency configuration 2 (Table 5) are shown in Figure 4a. Observe that Maram and UDR tree show similar average response time across different conflict rates; owing to the synchronization-free design. Maram has a slightly higher response time than UDR tree due to the overhead of metadata calculation. The response time for Subtree l [START_REF] Najafzadeh | Co-design and verification of an available file system[END_REF] increases with an increase in the conflict rate due to lock contention, whereas that of Global l is the same across all conflict rates since the proportion of lock-acquiring-moves remains the same.

Figure 4c shows the average stabilization time for our design and the UDR tree design [START_REF] Kleppmann | Opsets: Sequential specifications for replicated datatypes (extended version)[END_REF] on a logarithmic scale, for different latency configurations. Our solution gives lower stabilization time, since only down-moves and a very few up-moves have transient state in the case of Maram whereas for a UDR tree [START_REF] Kleppmann | Opsets: Sequential specifications for replicated datatypes (extended version)[END_REF] all operations are in transient state until a local replica asserts that there are no more concurrent operations. 12 Next, we run an experiment to measure the overhead introduced by the conflict resolution policy. As a lower bound, we compare the response time of Maram with a naïve unsafe implementation, that uses a simple eventual consistency approach, and thus is not safe. Figure 4b shows the response time of both the designs. For Maram metadata calculation implies slightly higher response time.

Related work

Several works have addressed the problem of designing a replicated tree. Martin et al. [START_REF] Martin | Abstract unordered and ordered trees CRDT[END_REF] introduce some designs for conflict-free replicated tree data types.

n 1 = n 2 ∨ p 1 = n 2 true n 2 / ∈ self -or-under(n 1 ) ∨p 1 / ∈ self -or-under(n 2 )
Table 6: Result of dependency analysis. The cell shows the condition under which the operation in the row is independent of the operation in the column.

construct replicated trees with different semantics. Add and remove operations are supported in their design. However they do not consider move operations. Kleppmann et al. [START_REF] Kleppmann | Opsets: Sequential specifications for replicated datatypes (extended version)[END_REF] propose the UDR tree, which supports atomic move operations, using the notion of opsets. Opsets totally order all operations eventually. This is more expensive than our solution based on partial order. When a new operation is performed, all the later operations are redone. Thus all operations pay a heavy price, and not just the conflicting moves. But UDR requires eventually consistent delivery layer, whereas Maram requires a more expensive causal delivery layer.

Compared to the work of Kleppmann et al. [START_REF] Kleppmann | Opsets: Sequential specifications for replicated datatypes (extended version)[END_REF], we also show under what conditions a move operation might skip.

Najafzadeh et al. [START_REF] Najafzadeh | Co-design and verification of an available file system[END_REF] designs the replicated tree called Subtree l in Section 5. Their solution introduces coordination; acquires read locks on the critical ancestors, and a write lock on the node being moved. This approach is not available under partition, but only move operations pay an overhead.

Tao et al. [START_REF] Tao | Merging semantics for conflict updates in geo-distributed file systems[END_REF] propose a replicated tree with a move operation that does not require any coordination between replicas, replacing each move with non-atomic copy and delete operations. This might lead to having multiple copies of the same node.

Compared to all the above solutions, our design supports atomic move operation that depends on partial ordering without acquiring any locks. An atomic update provides all or no guarantee, i.e., either the update is applied or it is not. Ensuring atomicity avoids partial execution of updates.

Kaki et al. [START_REF] Kaki | Mergeable replicated data types[END_REF] introduce the concept of Mergeable Replicated Data Types (MRDTs) inspired by three-way-merge. The safety of an MRDT binary tree depends on the labeling of the childparent relations (whether it belongs to the right or left of the ancestor). It also requires to keep track of all the ancestor relations apart from the parent-child relations. A generic MRDT tree can be considered as an extension to the MRDT binary tree, but requires tracking all ancestor relations and a complex lexicographical ordering when concretizing the merged result.

Discussion

Moving from causal consistency to eventual consistency

Houshmand and Lesani [START_REF] Houshmand | Hamsaz: Replication coordination analysis and synthesis[END_REF] propose dependency analysis to help relax the requirement of causal delivery. We run this analysis for all operations, irrespective of whether the update is tentative or definitive.

Inria

Table 6 shows the results of the dependency analysis of Maram. We can observe that no operations are dependent on remove, and add and remove are not dependent on move. As there is no fully independent operation, relaxing causal delivery is not helpful to Maram.

Message overhead for conflict resolution

In order to use Maram in a real-world application, we need to understand the overhead of conflict resolution. Conflict resolution requires some meta information that is sent along with the update message from the origin replica. This may have an impact on the bandwidth lost, hence understanding the components is important.

The conflict resolution policy of Maram needs information to compute a set of concurrent operations. Assuming a replica works as a single threaded process, we use vector clocks. The size of vector clocks is linear with the number of replicas. This poses an additional overhead.

Conflict resolution also takes as input the set of critical ancestors, descendants, and the priority.The size of the set of critical ancestors depends on the depth of the subtree comprising the least common ancestor of the node being moved and the destination parent. The size of the set of critical ancestors is linear to the difference in the rank of the new parent and the least common ancestor. The size of the set of descendants might be large for the nodes nearer to the root. This poses an overhead on the metadata. The priority can be a single number or a string and is independent of other factors. Hence using the conflict resolution of Maram will cause a considerable overhead on message delivery.

The time taken to compute this metadata is the difference between the response time of a naïve unsafe replicated tree and Maram in Figure 4b.

Computing the set of concurrent moves

Maram requires a set of concurrent operations to apply the conflict resolution. For this, the Maram system layer does not busy-wait. Every replica makes progress locally, without waiting to receive remote logs (availability under partition). Conflict resolution applies only after a replica receives a concurrent conflicting operation.

To conclude, Maram is a safe, coordination-free replicated tree, designed using conflict resolution policies.

Conclusion

This paper presents the design of a light-weight, coordination-free, safe, convergent and highly available replicated tree data structure, Maram. We provide mechanized proof of safety and convergence of Maram, and experimentally demonstrate the efficiency of the design by comparing it with the existing solutions. operations, whose names appear in the head of the table. For each verification condition, we run the available SMTs until one of them is able to discharge it, or else every one fails to complete the proof. Finally, each verification condition is identified with a name of the form lemma P, where P for the nature of the condition, i.e., it is either a precondition or a postcondition. For instance, on the first table, pre move1 stands for the first precondition of the move operation, and so on. Times are given in seconds.

Proof obligations

Figure 1 :

 1 Figure 1: Resolving conflict of concurrent remove and add

Figure 2 :

 2 Figure 2: Critical ancestors and critical descendants

  p ) op ∈ C op.type = up-move ∧ (crit-anc-overlap(down-move(n, p ), op) ∨ op.params.n = n) ∧ op ∈ C op.type = down-move ∧ (crit-anc-overlap(down-move(n, p ), op) ∨ op.params.n = n) ∧ op.priority > priority op ∈ H (op.type = up-move ∧ (n ∈ self -or -under (op.params.n) ∨ (op.params.n ∈ self -or -under (n) ∧ p ∈ self -or -under (op.params.n)))) ∨(op.type = down-move ∧ p ∈ self -or -under (op.params.n)) =⇒ Inv ∧ n → p

Figure 3 :

 3 Figure 3: Concurrent specification of Maram

Figure 4 :

 4 Figure 4: Experimental results. Each bar is the average of 15 runs, the error bars show standard deviation

[

  until] then there is a path from [from] to [until] *) axiom path_transitivity: forall from middle until f pth1 pth2.path f from middle pth1 → path f middle until pth2 → disjoint_seq pth1 pth2 → from = until → (forall j. 0 ≤ j < length pth1 → pth1[j] = until) → path f from until (pth1 ++ pth2)(*Recursive path composition *) axiom path_composition: forall n x y: elt, f : elt → elt, pth : seq elt. n = y → not (mem y pth) → distinct (snoc pth x) → path f n x pth → edge x y f → path f n y (snoc pth x) (* If there is a path between two nodes, that path is unique *) axiom path_uniqueness: forall x y: elt, f: elt → elt, pth1 pth2: seq elt. path f x y pth1 → path f x y pth2 → pth1 == pth2 (* If node np is not reachable to node c, then np will not belong to any path that contains node c *) axiom path_exclusion: forall f x c np p. not (reachability f np c) → path f x c p → not (mem np p) (* Given a path between two nodes, there is no overlap between any two consecutive subpaths *) axiom path_separation: forall final initial middle : elt, f : elt → elt, p1 p2 : seq elt. path f middle final p2 → path f initial middle p1 → final = initial → middle = initial → middle = final → disjoint_seq p1 p2 constant n: elt (* constant used for defining a state witness *) type state [@state] = { (* parent relation: up-pointers to direct ancestor *) mutable parent : elt → elt; (* parent root *) mutable root : elt; (* nodes in the parent *) mutable nodes : fset elt; } invariant { F.mem root nodes } invariant { parent root = root } invariant { forall x. F.mem x nodes → F.mem (parent x) nodes } invariant { forall x. F.mem x nodes → reachability parent x root } invariant { forall x. F.mem x nodes → reachability parent root x → x = root } by { parent = (fun _ → n); root = n; nodes = F.singleton n } (* Paths already present in the tree remain in the tree after executing the add operation *) axiom remaining_nodes_add: forall n w p: elt, s: state, l: seq elt. path s.parent w s.root l → not (mem n l) → F.mem w s.nodes → F.mem p s.nodes → not (F.mem n s.nodes) →

Table 2 :

 2 Stability analysis of sequential specificationConcurrent remove: Consider the sequential specification of two remove operations move(n 1 , p 1 ) and remove(n 2 ). Using (26), we get

			Stable against concurrent operation
			add (n 2 , p 2 )	remove(n 2 )	move(n 2 , p 2 )
	Operations	add (n 1 , p 1 ) remove(n 1 ) move(n 1 , p 1 )	n 1 = n 2 n 1 = p 2 true	p 1 = n 2 true p 1 = n 2	true n 1 = p 2 p 1 → * n 2

Table 3 :

 3 Critical ancestors and critical descendants of move(n, p )

	Inria

Table 5 :

 5 Real world latency configurations in ms to measure this, we introduce a metric called stabilization time. Stabilization time measures the duration for which an update is in a transient state.

  They use set CRDTs to

		Independent	add (n 2 , p 2 )	Under remove(n 2 )	move(n 2 , p 2 )
	Operation	add (n 1 , p 1 ) remove(n 1 ) move(n 1 , p 1 )	p 1 = n 2 n 1 = n 2	true true	true true

  This section presents the Why3 specification of Maram.

		Proof obligations Proof obligations	Alt-Ergo 2.3.2	CVC4 1.7 Alt-Ergo 2.3.2	Z3 4.8.6 CVC4 1.7	Z3 4.8.6
	lemma VC for remove remove analysis lemma pre remove2 lemma pre remove1 lemma VC for lemma pre add1 add move analysis lemma pre add2 lemma pre remove1 lemma pre move1 lemma pre remove2 lemma pre remove1 lemma pre remove2 lemma pre move2 lemma pre move3 lemma pre move4 lemma pre remove1 lemma pre move5		0.16 0.22 Alt-Ergo 2.3.2 0.20 0.16 0.27 0.21 0.24	0.12 0.11 0.35 CVC4 1.7 0.41 0.11 0.15 0.09	Z3 4.8.6
	lemma VC for	lemma pre move1 lemma pre remove2 lemma pre move1		0.15	0.10 0.10
	move move analysis lemma pre move2 lemma postcondition lemma pre move2		0.10	0.10 0.22
			lemma pre move3 lemma pre move3		0.09	0.07 0.12
			lemma pre move4 lemma pre move4		0.23	0.10 0.11
	lemma VC for		lemma pre move5 lemma pre add1 lemma pre move5		0.11	0.11 0.11
	add add analysis	lemma pre move1 lemma pre add2 lemma pre add1		0.11	0.21 0.31
			lemma pre move2 lemma pre add1 lemma pre add2	0.22 (1s) (1s) FAILURE 0.34
			lemma pre move3 lemma pre add2 lemma postcondition	(1s) (1s) (1s) 0.22 0.35
			lemma pre move4 lemma pre add1		0.10	0.15 0.20
			lemma pre move5 lemma pre add2		0.11	0.09 0.35
	lemma VC for	lemma pre move1 lemma pre add1 lemma pre remove1 (1s) (1s) (1s) 0.11 0.17
	lemma pre move2 lemma pre add2 add remove analysis lemma pre remove2	0.22	0.10 0.16
			lemma pre move3 lemma postcondition 0.51 (1s) FAILURE 0.09 lemma pre add1 0.19
	lemma VC for		lemma pre move4 lemma pre move1 lemma pre add2		0.09 (1s) (1s) FAILURE 0.24
	remove move analysis	lemma pre move5 lemma pre move2 lemma pre add1		0.23	0.11 0.25
			lemma pre move1 lemma pre move3 lemma pre add2		0.93	0.24 0.23
			lemma pre move2 lemma pre move4 lemma pre remove1	0.15	0.22 0.29
			lemma pre move3 lemma pre move5 lemma pre remove2	(1s) (1s) FAILURE 0.11 0.11
			lemma pre move4 lemma pre remove1 lemma postcondition (1s) (1s) FAILURE 0.14 0.27
			lemma pre move5 lemma pre remove2		0.23	0.09 0.19
			lemma postcondition 0.26 (1s) FAILURE lemma pre remove1 0.19 (1s) (1s) (1s)
			lemma pre remove2		0.19
			lemma pre move1		0.32
			lemma pre move2	(1s) (1s) FAILURE
	C Specification of Maram in Why3 lemma pre move3	0.15
			lemma pre move4		0.17
			lemma pre move5		0.11
	lemma postcondition (* parent relation: up-pointers to direct ancestor *) type state = { mutable parent : elt → elt;	0.22 0.16 0.23
	(* parent root *)
	mutable root	: elt;
	(* nodes in the parent *)
	mutable nodes	: fset elt;
	(* rank for each node *)
	mutable rank	: elt → int;
						Inria Inria

For example, a file system trace we analyzed contained 1198823 operations in total,

create operations, 49509 remove operations and just 547 move operations (70939 structural operations altogether).RR n°9395

We furthermore claim (without proof) that Maram is live, in the sense that, if every message sent is eventually delivered to some replica r 1 , then, given some update originating at a replica r 2 , its postcondition eventually takes effect at replica r 1 .

Note that this global view cannot be observed by any single replica and is merely an explanatory device.Inria

Note that, at this point, the system is committed to this operation, and the operation's precondition must be true at the remote replica.

In Section 7 we consider relaxing this requirement to eventual consistency, which states only that all updates are eventually delivered at all replicas. RR n°9395

RR n°9395

For readability, we simplify the postcondition to express only the changes caused by the operation. The part of the state not mentioned remains unaffected.

Denoted in inference style, as in[START_REF] Kaki | Safe replication through bounded concurrency verification[END_REF]. The condition above the line represents the pre-state, an update event is noted . , and the condition below the line indicates the post-state.Inria

Ideally, one will remove the tombstone at some safe time in the future; this is non-trivial[START_REF] Baquero | Making operation-based CRDTs operation-based[END_REF] and out of the scope of this paper.Inria

Note that rank (n 2 ) cannot increase since an up-move does not cause the rank of any move to increase.Inria

On DELL PowerEdge R410 machine with 64 GB RAM, and 24 cores @2.40GHz Intel Xeon E5645 processor.

250 operations per replica -60% add,

12% remove, 14% upmove and 14% downmove.[START_REF] Martin | Abstract unordered and ordered trees CRDT[END_REF] Note here that Maram's stabilisation time does not depend on conflict rate, but only on the proportion of moves in the workload. As this proportion grows towards 100%, the stabilisation time of Maram tends to be the same as that of UDR.RR n°9395

rue Simone Iff -CS 42112

Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

Independence of up-move operation

Historical up-move: Now we analyse whether an up-move is independent of a historical upmove.

Pre up-move(n 1 ,p 1 ) n1 ∈ Nodes ∧ n1 = root ∧ p 1 ∈ Nodes ∧ n1 = p 1 ∧ p 1 → * n1 ∧ rank (n1) > rank (p 1 )

We first divide the postcondition of the historical up-move into two parts: on the one hand, skip, which leaves the state as it was; and on the other hand, n 1 → p 1 , which changes the parent relation. Then we divide the precondition of the second up-move into two parts, n 2 ∈ Nodes ∧ n 2 = root ∧ p 2 ∈ Nodes ∧ n 2 = p 2 , which is unaffected by the historical up-move, and p 2 → * n 2 ∧ rank (n 2 ) > rank (p 2 ), which is potentially effected by the second part of the postcondition of the historical up-move.

Note that Pre up-move(n2,p 2 ) was not enabled before the execution of op 1 , i.e., the execution of op 1 enabled at least one predicate p 2 → * n 2 or rank (n 2 ) > rank (p 2 ). Let us consider them one at a time.

Let us derive the conditions under which moving a node to a different parent introduces an ancestor relation that enables the condition p 2 → * n 2 (it was previously disabled). This means that the historical up-move operation caused a disconnection between p 2 and n 2 . This will happen only if the node being moved by the historical up-move was either n 2 or a descendant of n 2 and the new parent of the current move was either n 1 or a descendant of n 1 (the node moved by the historical up-move). Hence we have (n

The condition rank (n 2 ) > rank (p 2 ) will be enabled after an up-move only if rank (p 2 ) decreased. 9 This will happen only if p 2 was the node moved or its descendant. Hence we have that

The historical up-move either enabled one or both of the conditions. Combining them gives p 2 = n 1 ∨ p 2 → * n 1 , the condition under which an up-move, up-move(n 2 , p 2 ), is dependent on a historial up-move, up-move(n 1 , p 1 ).

Historical down-move:

To check for independence of an up-move with a historical downmove, we have the following condition:

We apply the same reasoning as in the previous case for the condition

as the condition under which an up-move is dependent under a historical down-move.

There is a difference in the second part though; the condition rank (n 2 ) > rank (p 2 ) will be enabled after a down-move only if rank (n 2 ) increases (not possible for a down-move to decrease the rank). This will happen only if n 2 was the node moved or its descendant, i.e., n 2 = n 1 ∨n 2 → * n 1 .

Combining both the conditions, we have ((

as the condition under which an up-move, up -move(n 2 , p 2 ), is dependent on a historial down-move, down-move(n 1 , p 1 ).

A Specification of sequential tree in Why3

This section presents the Why3 specification of a sequentially safe tree.

predicate reachability (f: elt → elt) (x y: elt) = exists p. path f x y p (* If there is an edge between nodes x and y (* the path is defined as the singleton seq with node x *) axiom path_to_parent: forall x y : elt, f : elt → elt. edge x y f → path f x y (cons x empty)

B.1 Why3 proof sessions

This section presents the quantitative results of using Why3 and CISE3 to analyse the sequential operations. Each table presents the set of generated verification conditions for a specific pair of