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