Abstract
Collaborative text editing systems allow multiple users to concurrently edit the same document, which can be modeled by a replicated list object. In the literature, there is a family of operational transformation (OT)-based Jupiter protocols for replicated lists, including AJupiter, XJupiter, and CJupiter. They are hard to understand due to the subtle OT technique, and little work has been done on formal verification of complete Jupiter protocols. Worse still, they use quite different data structures. It is unclear about how they are related to each other, and it would be laborious to verify each Jupiter protocol separately. In this work, we make contributions towards a better understanding of Jupiter protocols and the relation among them. We first identify the key OT issue in Jupiter and present a generic solution. We summarize several techniques for carrying out the solution, including the data structures to maintain OT results and to guide OTs. Then, we propose an implementation-independent AbsJupiter protocol. Finally, we establish the (data) refinement relation among these Jupiter protocols (AbsJupiter included). We also formally specify and verify the family of Jupiter protocols and the refinement relation among them using TLA+ (TLA stands for “Temporal Logic of Actions”) and the TLC model checker. To our knowledge, this is the first work to formally specify and verify a family of OT-based Jupiter protocols and the refinement relation among them. It would be helpful to promote a rigorous study of OT-based protocols.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Ellis C A, Gibbs S J. Concurrency control in groupware systems. In Proc. the 1989 ACM SIGMOD International Conference on Management of Data, May 1989, pp.399-407.
Attiya H, Burckhardt S, Gotsman A, Morrison A, Yang H, Zawirski M. Specification and complexity of collaborative text editing. In Proc. the 2016 ACM Symposium on Principles of Distributed Computing, July 2016, pp.259-268.
Nichols D A, Curtis P, Dixon M, Lamping J. High-latency, low-bandwidth windowing in the Jupiter collaboration system. In Proc. the 8th Annual ACM Symposium on User Interface and Software Technology, November 1995, pp.111-120.
Xu Y, Sun C, Li M. Achieving convergence in operational transformation: Conditions, mechanisms and systems. In Proc. the 17th ACM Conference on Computer Supported Cooperative Work, February 2014, pp.505-518.
Shapiro M, Preguiça N, Baquero C, Zawirski M. Conflict-free replicated data types. In Proc. the 13th International Conference on Stabilization, Safety, and Security of Distributed Systems, October 2011, pp.386-400.
Wei H, Huang Y, Lu J. Specification and implementation of replicated list: The Jupiter protocol revisited. In Proc. the 22nd International Conference on Principles of Distributed Systems, December 2018, Article No. 12.
Sun C, Ellis C. Operational transformation in real-time group editors: Issues, algorithms, and achievements. In Proc. the 1998 ACM Conference on Computer Supported Cooperative Work, November 1998, pp.59-68.
Ressel M, Nitsche-Ruhland D, Gunzenhäuser R. An integrating, transformation-oriented approach to concurrency control and undo in group editors. In Proc. the 1996 ACM Conference on Computer Supported Cooperative Work, November 1996, pp.288-297.
Imine A, Rusinowitch M, Oster G, Molli P. Formal design and verification of operational transformation algorithms for copies convergence. Theor. Comput. Sci., 2006, 351(2): 167-183.
Randolph A, Boucheneb H, Imine A, Quintero A. On consistency of operational transformation approach. In Proc. the 14th International Workshop on Verification of Infinite-State Systems, August 2012, pp.45-59.
Randolph A, Boucheneb H, Imine A, Quintero A. On synthesizing a consistent operational transformation approach. IEEE Trans. Computers, 2015, 64(4): 1074-1089.
Hoare C A. Proof of correctness of data representations. Acta Inf., 1972, 1(4): 271-281.
Lamport L, Merz S. Auxiliary variables in TLA+. arXiv:1703.05121, 2017. https://arxiv.org/pdf/1703.051-21.pdf, Sept. 2020.
Lamport L. If you’re not writing a program, don’t use a programming language. Bulletin of the EATCS, 2018, 125: Article No. 7.
Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers (1st edition). Addison-Wesley Professional, 2002.
Yu Y, Manolios P, Lamport L. Model checking TLA+ specifications. In Proc. the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, September 1999, pp.54-66.
Hong W, Chen Z, Yu H, Wang J. Evaluation of model checkers by verifying message passing programs. SCIENCE CHINA Information Sciences, 2019, 62(10): Article No. 200101.
Lamport L. The temporal logic of actions. ACM Trans. Program. Lang. Syst., 1994, 16(3): 872-923.
Abadi M, Lamport L. The existence of refinement mappings. Theor. Comput. Sci., 1991, 82(2): 253-284.
Sun D, Sun C. Context-based operational transformation in distributed collaborative editing systems. IEEE Trans. Parallel Distrib. Syst., 2009, 20(10): 1454-1470.
Yuan D, Luo Y, Zhuang X, Rodrigues G R, Zhao X, Zhang Y, Jain P U, Stumm M. Simple testing can prevent most critical failures: An analysis of production failures in distributed data-intensive systems. In Proc. the 11th USENIX Conference on Operating Systems Design and Implementation, October 2014, pp.249-265.
Li D, Li R. An approach to ensuring consistency in peer-to-peer real-time group editors. Computer Supported Cooperative Work, 2008, 17(5/6): 553-611.
Liu Y, Xu Y, Zhang S J, Sun C. Formal verification of operational transformation. In Proc. the 19th International Symposium on Formal Methods, May 2014, pp.432-448.
Sun C, Xu Y, Agustina A. Exhaustive search of puzzles in operational transformation. In Proc. the 17th ACM Conference on Computer Supported Cooperative Work, February 2014, pp.519-529.
Sinchuk S, Chuprikov P, Solomatov K. Verified operational transformation for trees. In Proc. the 7th International Conference on Interactive Theorem Proving, August 2016, pp.358-373.
Author information
Authors and Affiliations
Corresponding author
Supplementary Information
ESM 1
(PDF 427 kb)
Rights and permissions
About this article
Cite this article
Wei, HF., Tang, RZ., Huang, Y. et al. Jupiter Made Abstract, and Then Refined. J. Comput. Sci. Technol. 35, 1343–1364 (2020). https://doi.org/10.1007/s11390-020-0516-0
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11390-020-0516-0