面对任意规模与延迟的操作并发控制

我们首次提出了一个完整的解决方案，以证明协同文本编辑器的并发控制算法针对标准一致性模型的正确性。我们方法成功的关键在于使用了全面的逐串操作变换（stringwise operational transformations），这似乎至今尚未得到过形式化处理。由于这些变换在操作被变换时有时会导致操作数量增加，我们无法使用归纳方法，而是采用了递减图（decreasing diagrams）这一新颖思想。我们还将算法建立在客户端-服务器模型而非对等模型之上，这使得操作变换能够正确地应用于新生成的操作和待处理操作。最后，我们解决了延迟问题，使得我们的算法在实践中完美运行。这些创新的结果是首个针对协同文本编辑器的形式化正确的并发控制算法，以及一个快速、容错且高度可扩展的实现。