Operational Concurrency Control in the Face of Arbitrary Scale and Latency

TL;DR

This paper introduces a formally verified, scalable concurrency control algorithm for collaborative text editing that handles arbitrary scale and latency, ensuring correctness and practical efficiency.

Contribution

It provides the first formal correctness proof for a stringwise operational transformation-based concurrency control algorithm in collaborative editing.

Findings

First formal correctness proof for operational transformations

Algorithm works effectively under high latency and scale

Implementation is fast, fault-tolerant, and highly scalable

Abstract

We present for the first time a complete solution to the problem of proving the correctness of a concurrency control algorithm for collaborative text editors against the standard consistency model. The success of our approach stems from the use of comprehensive stringwise operational transformations, which appear to have escaped a formal treatment until now. Because these transformations sometimes lead to an increase in the number of operations as they are transformed, we cannot use inductive methods and adopt the novel idea of decreasing diagrams instead. We also base our algorithm on a client-server model rather than a peer-to-peer one, which leads to the correct application of operational transformations to both newly generated and pending operations. And lastly we solve the problem of latency, so that our algorithm works perfectly in practice. The result of these innovations is the first ever formally correct concurrency control algorithm for collaborative text editors together with a fast, fault tolerant and highly scalable implementation.