Document Open Access Logo

VeriFx: Correct Replicated Data Types for the Masses

Authors Kevin De Porre , Carla Ferreira , Elisa Gonzalez Boix

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.9.pdf
  • Filesize: 1.62 MB
  • 45 pages

Document Identifiers

Author Details

Kevin De Porre
  • Vrije Universiteit Brussel, Belgium
Carla Ferreira
  • NOVA School of Science and Technology, Caparica, Portugal
Elisa Gonzalez Boix
  • Vrije Universiteit Brussel, Belgium

Funding

  • De Porre, Kevin: Funded by the Research Foundation - Flanders. Project number 1S98519N.
  • Ferreira, Carla: Partly funded by EU Horizon Europe under Grant Agreement no. 101093006 (TaRDIS), and FCT-Portugal under grants UIDB/04516/2020 and PTDC/CCI-INF/32081/2017.

Acknowledgements

The authors would like to thank Nuno Preguiça, Carlos Baquero, and Imine Abdessamad for their early feedback on this work.

Cite AsGet BibTex

Kevin De Porre, Carla Ferreira, and Elisa Gonzalez Boix. VeriFx: Correct Replicated Data Types for the Masses. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 9:1-9:45, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.9

Abstract

Distributed systems adopt weak consistency to ensure high availability and low latency, but state convergence is hard to guarantee due to conflicts. Experts carefully design replicated data types (RDTs) that resemble sequential data types and embed conflict resolution mechanisms that ensure convergence. Designing RDTs is challenging as their correctness depends on subtleties such as the ordering of concurrent operations. Currently, researchers manually verify RDTs, either by paper proofs or using proof assistants. Unfortunately, paper proofs are subject to reasoning flaws and mechanized proofs verify a formalization instead of a real-world implementation. Furthermore, writing mechanized proofs is reserved for verification experts and is extremely time-consuming. To simplify the design, implementation, and verification of RDTs, we propose VeriFx, a specialized programming language for RDTs with automated proof capabilities. VeriFx lets programmers implement RDTs atop functional collections and express correctness properties that are verified automatically. Verified RDTs can be transpiled to mainstream languages (currently Scala and JavaScript). VeriFx provides libraries for implementing and verifying Conflict-free Replicated Data Types (CRDTs) and Operational Transformation (OT) functions. These libraries implement the general execution model of those approaches and define their correctness properties. We use the libraries to implement and verify an extensive portfolio of 51 CRDTs, 16 of which are used in industrial databases, and reproduce a study on the correctness of OT functions.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Domain specific languages
  • Computing methodologies → Distributed programming languages
  • Theory of computation → Distributed algorithms
Keywords
  • distributed systems
  • eventual consistency
  • replicated data types
  • verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Deepthi Devaki Akkoorath and Annette Bieniusa. Antidote: The highly-available geo-replicated database with strongest guarantees. Technical report, Technical Report. Tech. U. Kaiserslautern., 2016. Google Scholar
  2. Paulo Sérgio Almeida, Ali Shoker, and Carlos Baquero. Efficient state-based CRDTs by delta-mutation. In Ahmed Bouajjani and Hugues Fauconnier, editors, Int. Conference on Networked Systems, pages 62-76, Agadir, Morocco, 2015. Springer-Verslag. Google Scholar
  3. AntidoteDB. Implementation of a Disable-Wins Flag CRDT in AntidoteDB. https://github.com/AntidoteDB/antidote/blob/master/apps/antidote_crdt/src/antidote_crdt_flag_dw.erl. Accessed: 2022-07-19.
  4. AntidoteDB. Implementation of an Enable-Wins Flag CRDT in AntidoteDB. https://github.com/AntidoteDB/antidote/blob/master/apps/antidote_crdt/src/antidote_crdt_flag_ew.erl. Accessed: 2022-07-19.
  5. Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, and Marek Zawirski. Specification and complexity of collaborative text editing. In Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, PODC '16, pages 259-268, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2933057.2933090.
  6. Peter Bailis, Alan Fekete, Michael J. Franklin, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. Coordination avoidance in database systems. Proc. VLDB Endow., 8(3):185-196, November 2014. URL: https://doi.org/10.14778/2735508.2735509.
  7. Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, and Nuno Preguiça. IPA: Invariant-preserving applications for weakly consistent replicated databases. Proc. VLDB Endow., 12(4):404-418, December 2018. Google Scholar
  8. Carlos Baquero, Paulo Sérgio Almeida, and Ali Shoker. Pure operation-based replicated data types. CoRR, abs/1710.04469, 2017. URL: https://arxiv.org/abs/1710.04469.
  9. Carlos Baquero, Omer Katz, Brian Cannard, and Georges Younes. JGraphT: a Java library of graph theory data structures and algorithms. https://github.com/CBaquero/delta-enabled-crdts. Accessed: 22-11-2022.
  10. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Methods for Components and Objects, pages 364-387, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  11. Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean, editors, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pages 49-69, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  12. Basho Technologies. Riak KV. https://riak.com/products/riak-kv/index.html. Accessed: 22-11-2022.
  13. Jim Bauwens and Elisa Gonzalez Boix. Nested pure operation-based CRDTs. In To Appear in 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, WA, LIPIcs, 2023. Google Scholar
  14. Annette Bieniusa, Marek Zawirski, Nuno M. Preguiça, Marc Shapiro, Carlos Baquero, Valter Balegas, and Sérgio Duarte. An optimized conflict-free replicated set. CoRR, abs/1210.3368, 2012. URL: https://arxiv.org/abs/1210.3368.
  15. Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, and Tjark Weber. Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, pages 183-198, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  16. Sascha Böhme and Tjark Weber. Fast LCF-style proof reconstruction for Z3. In International Conference on Interactive Theorem Proving, pages 179-194. Springer, 2010. Google Scholar
  17. Eric Brewer. CAP twelve years later: How the "rules" have changed. Computer, 45:23-29, February 2012. Google Scholar
  18. Eric A. Brewer. Towards robust distributed systems (abstract). In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Distributed Computing, PODC '00, page 7, New York, NY, USA, 2000. ACM. URL: https://doi.org/10.1145/343477.343502.
  19. Sebastian Burckhardt, Manuel Fähndrich, Daan Leijen, and Benjamin P. Wood. Cloud types for eventual consistency. In 26th European Conference on Object-Oriented Programming, ECOOP'12, pages 283-307, Berlin, Heidelberg, 2012. Springer-Verlag. Google Scholar
  20. Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. Replicated data types: Specification, verification, optimality. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 271-284, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2535838.2535848.
  21. Cristiano Calcagno, Dino Distefano, Jeremy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter O'Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. Moving fast with software verification. In Klaus Havelund, Gerard Holzmann, and Rajeev Joshi, editors, NASA Formal Methods, pages 3-11, Cham, 2015. Springer International Publishing. Google Scholar
  22. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  23. Leonardo de Moura and Nikolaj Bjørner. Generalized, efficient array decision procedures. In 2009 Formal Methods in Computer-Aided Design, pages 45-52, 2009. URL: https://doi.org/10.1109/FMCAD.2009.5351142.
  24. Kevin De Porre, Carla Ferreira, Nuno Preguiça, and Elisa Gonzalez Boix. ECROs: Building Global Scale Systems from Sequential Code. Proc. ACM Program. Lang., 5(OOPSLA), November 2021. Google Scholar
  25. C. A. Ellis and S. J. Gibbs. Concurrency control in groupware systems. In Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data, SIGMOD '89, pages 399-407, New York, NY, USA, 1989. ACM. URL: https://doi.org/10.1145/67544.66963.
  26. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems, pages 125-128, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  27. Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. Verifying strong eventual consistency in distributed systems. Proc. ACM Program. Lang., 1(OOPSLA), October 2017. URL: https://doi.org/10.1145/3133933.
  28. Google. Protocol buffers. https://developers.google.com/protocol-buffers. Accessed: 10-10-2022.
  29. Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. 'cause i'm strong enough: Reasoning about consistency choices in distributed systems. SIGPLAN Not., 51(1):371-384, January 2016. URL: https://doi.org/10.1145/2914770.2837625.
  30. Pat Helland. Immutability changes everything: We need it, we can afford it, and the time is now. Queue, 13(9):101-125, November 2015. URL: https://doi.org/10.1145/2857274.2884038.
  31. Farzin Houshmand and Mohsen Lesani. Hamsaz: Replication coordination analysis and synthesis. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290387.
  32. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst., 23(3):396-450, May 2001. URL: https://doi.org/10.1145/503502.503505.
  33. Abdessamad Imine. Exchange of mails regarding OT, and unpublished register and stack designs. personal communication. Google Scholar
  34. Abdessamad Imine, Pascal Molli, Gérald Oster, and Michaël Rusinowitch. Proving correctness of transformation functions in real-time groupware. In Proceedings of the Eighth Conference on European Conference on Computer Supported Cooperative Work, ECSCW'03, pages 277-293, USA, 2003. Kluwer Academic Publishers. Google Scholar
  35. The SMT-LIB Initiative. SMT-LIB Version 3.0 - Preliminary Proposal. http://smtlib.cs.uiowa.edu/version3.shtml. Accessed: 23-11-2022.
  36. Radha Jagadeesan and James Riely. Eventual consistency for CRDTs. In Amal Ahmed, editor, Programming Languages and Systems, pages 968-995, Cham, 2018. Springer International Publishing. Google Scholar
  37. Gowtham Kaki and Suresh Jagannathan. A relational framework for higher-order shape analysis. SIGPLAN Not., 49(9):311-324, August 2014. URL: https://doi.org/10.1145/2692915.2628159.
  38. Gowtham Kaki, Swarn Priya, KC Sivaramakrishnan, and Suresh Jagannathan. Mergeable replicated data types. Proc. ACM Program. Lang., 3(OOPSLA), October 2019. URL: https://doi.org/10.1145/3360580.
  39. Martin Kleppmann. A critique of the CAP theorem. CoRR, abs/1509.05393, 2015. URL: https://arxiv.org/abs/1509.05393.
  40. Martin Kleppmann. Assessing the understandability of a distributed algorithm by tweeting buggy pseudocode. Technical Report UCAM-CL-TR-969, University of Cambridge, Computer Laboratory, May 2022. URL: https://doi.org/10.48456/tr-969.
  41. Martin Kleppmann and Alastair R Beresford. A conflict-free replicated JSON datatype. IEEE Trans. on Parallel and Distributed Systems, 28(10):2733-2746, 2017. Google Scholar
  42. Shadaj Laddad, Conor Power, Mae Milano, Alvin Cheung, and Joseph M. Hellerstein. Katara: Synthesizing CRDTs with verified lifting. Proc. ACM Program. Lang., 6(OOPSLA2), October 2022. URL: https://doi.org/10.1145/3563336.
  43. Leslie Lamport. Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM, 21(7):558-565, 1978. Google Scholar
  44. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 348-370, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  45. K. Rustan M. Leino and Michał Moskal. Usable auto-active verification. In Usable Verification Workshop, 2010. Google Scholar
  46. Cheng Li, João Leitão, Allen Clement, Nuno Preguiça, Rodrigo Rodrigues, and Viktor Vafeiadis. Automating the choice of consistency levels in replicated systems. In Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference, USENIX ATC'14, pages 281-292, Berkeley, CA, USA, 2014. USENIX Association. Google Scholar
  47. Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguiça, and Rodrigo Rodrigues. Making geo-replicated systems fast as possible, consistent when necessary. In Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation, OSDI’12, pages 265-278, USA, 2012. USENIX Association. Google Scholar
  48. Cheng Li, Nuno Preguiça, and Rodrigo Rodrigues. Fine-grained consistency for geo-replicated systems. In 2018 USENIX Annual Technical Conference (USENIX ATC 18), pages 359-372, Boston, MA, 2018. USENIX Association. Google Scholar
  49. Du Li and Rui Li. Preserving operation effects relation in group editors. In Proceedings of the 2004 ACM Conference on Computer Supported Cooperative Work, CSCW '04, pages 457-466, New York, NY, USA, 2004. ACM. URL: https://doi.org/10.1145/1031607.1031683.
  50. Xiao Li, Farzin Houshmand, and Mohsen Lesani. Hampa: Solver-aided recency-aware replication. In Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I, pages 324-349, Berlin, Heidelberg, 2020. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-53288-8_16.
  51. Hongjin Liang and Xinyu Feng. Abstraction for conflict-free replicated data types. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 636-650, New York, NY, USA, 2021. ACM. URL: https://doi.org/10.1145/3453483.3454067.
  52. Lightbend, Inc. Akka. https://akka.io/. Accessed: 22-11-2022.
  53. Lightbend Inc. Serialization. https://doc.akka.io/docs/akka/current/serialization.html. Accessed: 10-10-2022.
  54. Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, and Niki Vazou. Verifying replicated data types with typeclass refinements in liquid Haskell. Proc. ACM Program. Lang., 4(OOPSLA), November 2020. URL: https://doi.org/10.1145/3428284.
  55. Mae Milano and Andrew C. Myers. MixT: A language for mixing consistency in geodistributed transactions. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pages 226-241, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3192366.3192375.
  56. Kartik Nagar and Suresh Jagannathan. Automated parameterized verification of CRDTs. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification, pages 459-477, Cham, 2019. Springer International Publishing. Google Scholar
  57. Sreeja S. Nair, Gustavo Petri, and Marc Shapiro. Proving the safety of highly-available distributed objects. In Programming Languages and Systems: 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, pages 544-571, Berlin, Heidelberg, 2020. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-44914-8_20.
  58. Mahsa Najafzadeh, Alexey Gotsman, Hongseok Yang, Carla Ferreira, and Marc Shapiro. The CISE tool: proving weakly-consistent applications correct. In Peter Alvaro and Alysson Bessani, editors, Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, PaPoC@EuroSys 2016, London, United Kingdom, April 18, 2016, pages 2:1-2:3. ACM, 2016. URL: https://doi.org/10.1145/2911151.2911160.
  59. Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, and Lars Birkedal. Modular verification of op-based CRDTs in separation logic. Proc. ACM Program. Lang., 6(OOPSLA2), October 2022. URL: https://doi.org/10.1145/3563351.
  60. Peter W. O'Hearn. Continuous reasoning: Scaling the impact of formal methods. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 13-25, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3209108.3209109.
  61. OpenJDK. jmh - OpenJDK. https://openjdk.java.net/projects/code-tools/jmh/. Accessed: 13-05-2020.
  62. Gérald Oster, Pascal Molli, Pascal Urso, and Abdessamad Imine. Tombstone transformation functions for ensuring consistency in collaborative editing systems. In 2006 International Conference on Collaborative Computing: Networking, Applications and Worksharing, pages 1-10, 2006. URL: https://doi.org/10.1109/COLCOM.2006.361867.
  63. Aurel Randolph, Hanifa Boucheneb, Abdessamad Imine, and Alejandro Quintero. On synthesizing a consistent operational transformation approach. IEEE Transactions on Computers, 64(4):1074-1089, 2015. URL: https://doi.org/10.1109/TC.2014.2308203.
  64. Matthias Ressel, Doris Nitsche-Ruhland, and Rul Gunzenhäuser. An integrating, transformation-oriented approach to concurrency control and undo in group editors. In Proceedings of the 1996 ACM Conference on Computer Supported Cooperative Work, CSCW '96, pages 288-297, New York, NY, USA, 1996. ACM. URL: https://doi.org/10.1145/240080.240305.
  65. Scalameta. Scalameta: Library to read, analyze, transform and generate Scala programs. https://scalameta.org/. Accessed: 24-11-2022.
  66. Marc Shapiro. Replicated Data Types. In Ling Liu and M. Tamer Özsu, editors, Encyclopedia Of Database Systems, volume Replicated Data Types, pages 1-5. Springer-Verlag, July 2017. URL: https://doi.org/10.1007/978-1-4899-7993-3_80813-1.
  67. Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. A comprehensive study of convergent and commutative replicated data types. Research Report RR-7506, INRIA - Centre Paris-Rocquencourt, January 2011. Google Scholar
  68. Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In Xavier Défago, Franck Petit, and Vincent Villain, editors, 13th Int. Symp. on Stabilization, Safety, and Security of Distributed Systems, SSS'11, pages 386-400, Grenoble, France, 2011. Springer-Verslag. Google Scholar
  69. Maher Suleiman, Michèle Cart, and Jean Ferrié. Serialization of concurrent operations in a distributed collaborative environment. In Proceedings of the International ACM SIGGROUP Conference on Supporting Group Work: The Integration Challenge, GROUP '97, pages 435-445, New York, NY, USA, 1997. ACM. URL: https://doi.org/10.1145/266838.267369.
  70. Maher Suleiman, Michèle Cart, and Jean Ferrié. Concurrent operations in a distributed and mobile collaborative environment. In Proceedings of the Fourteenth International Conference on Data Engineering, ICDE '98, pages 36-45, USA, 1998. IEEE Computer Society. Google Scholar
  71. Chengzheng Sun and Clarence Ellis. Operational Transformation in Real-time Group Editors: Issues, Algorithms, and Achievements. In Proc. of the 1998 ACM Conference on Computer Supported Cooperative Work, CSCW '98, pages 59-68, 1998. Google Scholar
  72. Chengzheng Sun, Xiaohua Jia, Yanchun Zhang, Yun Yang, and David Chen. Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems. ACM Trans. Comput.-Hum. Interact., 5(1):63-108, March 1998. URL: https://doi.org/10.1145/274444.274447.
  73. The Apache Software Foundation. Cassandra: Open source NoSQL database. https://cassandra.apache.org/_/index.html. Accessed: 24-11-2022.
  74. The SMT-LIB Initiative. SMT-LIB. https://smtlib.cs.uiowa.edu. Accessed: 24-11-2022.
  75. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, pages 269-282, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2628136.2628161.
  76. Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. Refinement reflection: Complete verification with SMT. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158141.
  77. Chao Wang, Constantin Enea, Suha Orhun Mutluergil, and Gustavo Petri. Replication-aware linearizability. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pages 980-993, New York, NY, USA, 2019. ACM. URL: https://doi.org/10.1145/3314221.3314617.
  78. Michael J. Whittaker and Joseph M. Hellerstein. Interactive checks for coordination avoidance. Proc. VLDB Endow., 12(1):14-27, 2018. URL: https://doi.org/10.14778/3275536.3275538.
  79. Peter Zeller, Annette Bieniusa, and Arnd Poetzsch-Heffter. Formal specification and verification of CRDTs. In Erika Ábrahám and Catuscia Palamidessi, editors, Formal Techniques for Distributed Objects, Components, and Systems, pages 33-48, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. Google Scholar
  80. Peter Zeller, Annette Bieniusa, and Arnd Poetzsch-Heffter. Combining state- and event-based semantics to verify highly available programs. In Farhad Arbab and Sung-Shik Jongmans, editors, Formal Aspects of Component Software, pages 213-232, Cham, 2020. Springer International Publishing. Google Scholar
  81. Xin Zhao and Philipp Haller. Observable atomic consistency for CvRDTs. In Proceedings of the 8th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control, pages 23-32, 2018. Google Scholar
  82. Xin Zhao and Philipp Haller. Replicated data types that unify eventual consistency and observable atomic consistency. Journal of Logical and Algebraic Methods in Programming, 114:100561, 2020. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact