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.

翻译：我们首次提出了针对协作文本编辑器并发控制算法在标准一致性模型下正确性证明的完整解决方案。该方法的核心在于采用全面的字符串级操作变换——这一方法此前似乎一直缺乏形式化处理。由于这些变换在操作转换过程中可能导致操作数量增加，我们无法使用归纳方法，转而采用了递减图这一创新思路。此外，我们基于客户端-服务器模型而非点对点模型构建算法，从而能够正确将操作变换应用于新生成操作和待处理操作。最后我们解决了延迟问题，使算法在实践中完美运行。这些创新成果带来了协作文本编辑器领域首个形式化正确的并发控制算法，同时实现了快速、容错且高度可扩展的系统实现。