×

Strong eventual consistency of the collaborative editing framework WOOT. (English) Zbl 1485.68021

Summary: Commutative Replicated Data Types (CRDTs) are a promising new class of data structures for large-scale shared mutable content in applications that only require eventual consistency. The WithOut Operational Transforms (WOOT) framework is the first CRDT for collaborative text editing introduced by G. Oster et al. [“Data consistency for P2P collaborative editing”, in: Proceedings of the 20th anniversary conference on computer supported cooperative work, CSCW’06. New York, NY: Association for Computing Machinery (ACM). 259–268 (2006; doi:10.1145/1180875.1180916)]. Its eventual consistency property was verified only for a bounded model to date. While the consistency of many other previously published CRDTs had been shown immediately with their publication, the property for WOOT remained open for 14 years. We use a novel approach identifying a previously unknown sort-key based protocol that simulates the WOOT framework to show its consistency. We formalize the proof using the Isabelle/HOL proof assistant to machine-check its correctness.

MSC:

68M14 Distributed systems
68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)
68U15 Computing methodologies for text processing; mathematical typography
68V20 Formalization of mathematics in connection with theorem provers
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Archive of Formal Proofs. https://isa-afp.org. Accessed 11 Nov 2021
[2] Ahmed-Nacer, M., Ignat, C.-L., Oster, G., Roh, H.-G., Urso, P.: Evaluating CRDTs for real-time document editing. In: Proceedings of the 11th ACM Symposium on Document Engineering, pp. 103-112 (2011)
[3] Briot, L., Urso, P., Shapiro, M.: High responsiveness for group editing CRDTs. In: Proceedings of the 19th International Conference on Supporting Group Work, pp. 51-60. ACM, New York (2016)
[4] Brown, R., Cribbs, S., Meiklejohn, C., Elliott, S.: Riak DT map: A composable, convergent replicated dictionary. In: Proceedings of the First Workshop on Principles and Practice of Eventual Consistency. ACM, New York (2014)
[5] Dallaway, R.: WOOT Model for Scala and JavaScript via Scala.js. https://github.com/d6y/wootjs. Accessed 13 Nov 2021
[6] Ellis, C.A., Gibbs, S.J.: Concurrency control in groupware systems. In: Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data, vol. 18, pp. 399-407 (1989)
[7] Emanouilov, V.: Collaborative Rich Text Editor. https://github.com/kroky/woot. Accessed: 13 Nov 2021
[8] Gomes, V.B.F., Kleppmann, M., Mulligan, D.P., Beresford, A.R.: Verifying strong eventual consistency in distributed systems. Proceedings of the ACM on Programming Languages 1(OOPSLA) (2017). Article 109
[9] Kaplan, R.: A Real Time Collaboration Toy Project Based on WOOT. https://github.com/ryankaplan/woot-collaborative-editor. Accessed 13 Nov 2021
[10] Karayel, E., Gonzà lez, E.: Strong eventual consistency of the collaborative editing framework WOOT. Archive of Formal Proofs (2020). http://isa-afp.org/entries/WOOT_Strong_Eventual_Consistency.html Formal proof development
[11] Kleppmann, M., Gomes, V.B.F., Mulligan, D.P., Beresford, A.R.: Interleaving anomalies in collaborative text editors. In: Proceedings of the 6th Workshop on Principles and Practice of Consistency for Distributed Data. ACM, New York (2019). Article 6
[12] Kumawat, S.; Khunteta, A., A survey on operational transformation algorithms: challenges, issues and achievements, Int. J. Comput. Appl., 3, 12, 30-38 (2010)
[13] Lamport, L., Time, clocks, and the ordering of events in a distributed system, Commun. ACM, 21, 7, 558-565 (1978) · Zbl 0378.68027 · doi:10.1145/359545.359563
[14] Letia, M., Preguiça, N., Shapiro, M.: Consistency without concurrency control in large, dynamic systems. SIGOPS Oper. Syst. Rev. 44(2), 29-34 (2010)
[15] Li, D.; Li, R., An admissibility-based operational transformation framework for collaborative editing systems, Comput. Supp. Cooper. Work (CSCW), 19, 1, 1 (2010) · doi:10.1007/s10606-009-9103-1
[16] Marker, D.: Model Theory: An Introduction, edition1st edn. Graduate Texts in Mathematics, vol. 217. Springer (2002) · Zbl 1003.03034
[17] Nédelec, B., Molli, P., Mostefaoui, A., Desmontils, E.: LSEQ: an adaptive structure for sequences in distributed collaborative editing. In: Proceedings of the 2013 ACM Symposium on Document Engineering, pp. 37-46
[18] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283, 1st edn. Springer (2002) · Zbl 0994.68131
[19] Olson, T.: Real Time Group Editor without Operational Transformation. https://github.com/TGOlson/woot-haskell. Accessed 13 Nov 2021
[20] Oster, G., Urso, P., Molli, P., Imine, A.: Real time group editors without operational transformation. Technical Report RR-5580, INRIA (2005)
[21] Oster, G., Urso, P., Molli, P., Imine, A.: Data consistency for P2P collaborative editing. In: Conference on Computer Supported Cooperative Work (CSCW), pp. 259-268. ACM (2006a)
[22] Oster, G., Molli, P., Urso, P., Imine, A.: Tombstone transformation functions for ensuring consistency in collaborative editing systems. In: International Conference on Collaborative Computing: Networking, Applications and Worksharing (CollaborateCom) (2006b). IEEE
[23] Preguiça, N., Marques, J.M., Shapiro, M., Letia, M.: A commutative replicated data type for cooperative editing. In: 29th International Conference on Distributed Computing Systems, pp. 395-403 (2009). IEEE
[24] Raynal, M.: Distributed Algorithms for Message-Passing Systems. Springer (2013) · Zbl 1282.68004
[25] Roh, H-G; Jeon, M.; Kim, J-S; Lee, J., Replicated abstract data types: building blocks for collaborative applications, J. Parall. Distrib. Comput., 71, 3, 354-368 (2011) · Zbl 1219.68092 · doi:10.1016/j.jpdc.2010.12.006
[26] Sagher, Y., Counting the rationals, Am. Math. Mon., 96, 9, 823-823 (1989) · doi:10.1080/00029890.1989.11972288
[27] Shapiro, M., Preguiça, N., Baquero, C., Zawirski, M.: Conflict-free replicated data types. In: Stabilization. Safety, and Security of Distributed Systems, pp. 386-400. Springer (2011) · Zbl 1257.68039
[28] Sternagel, C., Thiemann, R.: Certification monads. Archive of Formal Proofs (2014). https://isa-afp.org/entries/Certification_Monads.html Formal proof development · Zbl 1416.68180
[29] Thiemann, R.: Generating linear orders for datatypes. Archive of Formal Proofs (2012). https://isa-afp.org/entries/Datatype_Order_Generator.html Formal proof development
[30] Weiss, S., Urso, P., Molli, P.: Wooki: a P2P wiki-based collaborative writing tool. In: Web Information Systems Engineering - WISE 2007, pp. 503-512. Springer
[31] Weiss, S., Urso, P., Molli, P.: Logoot: A scalable optimistic replication algorithm for collaborative editing on P2P networks. In: 29th IEEE International Conference on Distributed Computing Systems, pp. 404-412 (2009)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.