{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:40:59Z","timestamp":1740109259433,"version":"3.37.3"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,1,4]],"date-time":"2022-01-04T00:00:00Z","timestamp":1641254400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,1,4]],"date-time":"2022-01-04T00:00:00Z","timestamp":1641254400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Distrib. Comput."],"published-print":{"date-parts":[[2022,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 Oster et al. (In: Conference on Computer Supported Cooperative Work (CSCW). ACM, New York, pp 259\u2013268, 2006a). 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.<\/jats:p>","DOI":"10.1007\/s00446-021-00414-6","type":"journal-article","created":{"date-parts":[[2022,1,4]],"date-time":"2022-01-04T00:03:16Z","timestamp":1641254596000},"page":"145-164","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Strong eventual consistency of the collaborative editing framework WOOT"],"prefix":"10.1007","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3290-5034","authenticated-orcid":false,"given":"Emin","family":"Karayel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9169-0769","authenticated-orcid":false,"given":"Edgar","family":"Gonz\u00e0lez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,1,4]]},"reference":[{"key":"414_CR1","unstructured":"Archive of Formal Proofs. https:\/\/isa-afp.org. Accessed 11 Nov 2021"},{"key":"414_CR2","doi-asserted-by":"crossref","unstructured":"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\u2013112 (2011)","DOI":"10.1145\/2034691.2034717"},{"key":"414_CR3","doi-asserted-by":"crossref","unstructured":"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\u201360. ACM, New York (2016)","DOI":"10.1145\/2957276.2957300"},{"key":"414_CR4","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/2596631.2596633"},{"key":"414_CR5","unstructured":"Dallaway, R.: WOOT Model for Scala and JavaScript via Scala.js. https:\/\/github.com\/d6y\/wootjs. Accessed 13 Nov 2021"},{"key":"414_CR6","doi-asserted-by":"crossref","unstructured":"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\u2013407 (1989)","DOI":"10.1145\/66926.66963"},{"key":"414_CR7","unstructured":"Emanouilov, V.: Collaborative Rich Text Editor. https:\/\/github.com\/kroky\/woot. Accessed: 13 Nov 2021"},{"key":"414_CR8","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/3133933"},{"key":"414_CR9","unstructured":"Kaplan, R.: A Real Time Collaboration Toy Project Based on WOOT. https:\/\/github.com\/ryankaplan\/woot-collaborative-editor. Accessed 13 Nov 2021"},{"key":"414_CR10","unstructured":"Karayel, E., Gonz\u00e0 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"},{"key":"414_CR11","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/3301419.3323972"},{"issue":"12","key":"414_CR12","first-page":"30","volume":"3","author":"S Kumawat","year":"2010","unstructured":"Kumawat, S., Khunteta, A.: A survey on operational transformation algorithms: challenges, issues and achievements. Int. J. Comput. Appl. 3(12), 30\u201338 (2010)","journal-title":"Int. J. Comput. Appl."},{"issue":"7","key":"414_CR13","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"414_CR14","doi-asserted-by":"crossref","unstructured":"Letia, M., Pregui\u00e7a, N., Shapiro, M.: Consistency without concurrency control in large, dynamic systems. SIGOPS Oper. Syst. Rev. 44(2), 29\u201334 (2010)","DOI":"10.1145\/1773912.1773921"},{"issue":"1","key":"414_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10606-009-9103-1","volume":"19","author":"D Li","year":"2010","unstructured":"Li, D., Li, R.: An admissibility-based operational transformation framework for collaborative editing systems. Comput. Supp. Cooper. Work (CSCW) 19(1), 1 (2010)","journal-title":"Comput. Supp. Cooper. Work (CSCW)"},{"key":"414_CR16","unstructured":"Marker, D.: Model Theory: An Introduction, edition1st edn. Graduate Texts in Mathematics, vol. 217. Springer (2002)"},{"key":"414_CR17","doi-asserted-by":"crossref","unstructured":"N\u00e9delec, 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\u201346","DOI":"10.1145\/2494266.2494278"},{"key":"414_CR18","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/3-540-45949-9"},{"key":"414_CR19","unstructured":"Olson, T.: Real Time Group Editor without Operational Transformation. https:\/\/github.com\/TGOlson\/woot-haskell. Accessed 13 Nov 2021"},{"key":"414_CR20","unstructured":"Oster, G., Urso, P., Molli, P., Imine, A.: Real time group editors without operational transformation. Technical Report RR-5580, INRIA (2005)"},{"key":"414_CR21","doi-asserted-by":"crossref","unstructured":"Oster, G., Urso, P., Molli, P., Imine, A.: Data consistency for P2P collaborative editing. In: Conference on Computer Supported Cooperative Work (CSCW), pp. 259\u2013268. ACM (2006a)","DOI":"10.1145\/1180875.1180916"},{"key":"414_CR22","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1109\/COLCOM.2006.361867"},{"key":"414_CR23","doi-asserted-by":"crossref","unstructured":"Pregui\u00e7a, 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\u2013403 (2009). IEEE","DOI":"10.1109\/ICDCS.2009.20"},{"key":"414_CR24","doi-asserted-by":"crossref","unstructured":"Raynal, M.: Distributed Algorithms for Message-Passing Systems. Springer (2013)","DOI":"10.1007\/978-3-642-38123-2"},{"issue":"3","key":"414_CR25","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1016\/j.jpdc.2010.12.006","volume":"71","author":"H-G Roh","year":"2011","unstructured":"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\u2013368 (2011)","journal-title":"J. Parall. Distrib. Comput."},{"issue":"9","key":"414_CR26","doi-asserted-by":"publisher","first-page":"823","DOI":"10.1080\/00029890.1989.11972288","volume":"96","author":"Y Sagher","year":"1989","unstructured":"Sagher, Y.: Counting the rationals. Am. Math. Mon. 96(9), 823\u2013823 (1989)","journal-title":"Am. Math. Mon."},{"key":"414_CR27","doi-asserted-by":"crossref","unstructured":"Shapiro, M., Pregui\u00e7a, N., Baquero, C., Zawirski, M.: Conflict-free replicated data types. In: Stabilization. Safety, and Security of Distributed Systems, pp. 386\u2013400. Springer (2011)","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"414_CR28","unstructured":"Sternagel, C., Thiemann, R.: Certification monads. Archive of Formal Proofs (2014). https:\/\/isa-afp.org\/entries\/Certification_Monads.html Formal proof development"},{"key":"414_CR29","unstructured":"Thiemann, R.: Generating linear orders for datatypes. Archive of Formal Proofs (2012). https:\/\/isa-afp.org\/entries\/Datatype_Order_Generator.html Formal proof development"},{"key":"414_CR30","doi-asserted-by":"crossref","unstructured":"Weiss, S., Urso, P., Molli, P.: Wooki: a P2P wiki-based collaborative writing tool. In: Web Information Systems Engineering \u2013 WISE 2007, pp. 503\u2013512. Springer","DOI":"10.1007\/978-3-540-76993-4_42"},{"key":"414_CR31","doi-asserted-by":"crossref","unstructured":"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\u2013412 (2009)","DOI":"10.1109\/ICDCS.2009.75"}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-021-00414-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00446-021-00414-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-021-00414-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,10]],"date-time":"2022-03-10T03:03:08Z","timestamp":1646881388000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00446-021-00414-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,4]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,4]]}},"alternative-id":["414"],"URL":"https:\/\/doi.org\/10.1007\/s00446-021-00414-6","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"type":"print","value":"0178-2770"},{"type":"electronic","value":"1432-0452"}],"subject":[],"published":{"date-parts":[[2022,1,4]]},"assertion":[{"value":"3 July 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 November 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 January 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of Interest"}}]}}