Document Open Access Logo

Ensuring Convergence and Invariants Without Coordination

Authors Dina Borrego , Nuno Preguiça , Elisa Gonzalez Boix , Carla Ferreira

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.4.pdf
  • Filesize: 1.09 MB
  • 29 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computing methodologies → Distributed computing methodologies
  • Software and its engineering → Correctness
  • Theory of computation → Distributed algorithms
  • Computer systems organization → Availability
Keywords
  • distributed systems
  • conflict resolution
  • RDTs
  • invariant preservation

Metrics

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

Abstract

The CAP theorem demonstrates a trade-off between consistency and availability (and, by extension, latency) in systems where network partitions are unavoidable, such as in cloud computing and local-first software. While adopting weak consistency can preserve availability, it may result in inconsistencies that compromise application correctness. Replicated data types provide a principled, coordination-free approach to guarantee convergence but do not consider application invariants. Existing methods for maintaining invariants in replicated systems either rely on coordination - undermining the benefits of weak consistency - or suffer from limited applicability. This paper introduces the No-Op framework, a generic approach for enforcing consistency without coordination while guaranteeing both convergence and invariant preservation. The core idea of the No-Op approach is to resolve conflicts among concurrent operations by prioritising one operation over the other according to programmer-defined conflict resolution policies. This prioritisation transforms the less-preferred operation into a no-side-effect operation, ensuring conflict-free execution. We formalise the model underlying the No-Op framework and introduce a replication protocol built upon it, accompanied by a formal proof of correctness for both the framework and the protocol. Furthermore, we demonstrate the framework’s applicability by showcasing the design of widely used replicated data types and the preservation of a wide range of application invariants.

Cite As Get BibTex

Dina Borrego, Nuno Preguiça, Elisa Gonzalez Boix, and Carla Ferreira. Ensuring Convergence and Invariants Without Coordination. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.4

Author Details

Dina Borrego
  • NOVA School of Science and Technology, Caparica, Portugal
  • Vrije Universiteit Brussel, Belgium
Nuno Preguiça
  • NOVA School of Science and Technology, Caparica, Portugal
Elisa Gonzalez Boix
  • Vrije Universiteit Brussel, Belgium
Carla Ferreira
  • NOVA School of Science and Technology, Caparica, Portugal

Funding

This work is partially supported by PRT/BD/154519/2022 awarded by the EUTOPIA European University Alliance, UID/04516/NOVA LINCS with the financial support of FCT.IP and the European Commission through the TaRDIS project (agreement ID 101093006).

Acknowledgements

We would like to thank Kevin De Porre for the helpful discussions about VeriFx and the anonymous reviewers for their valuable feedback, which helped improve the paper.

Supplementary Materials

References

  1. Daniel Abadi. Consistency tradeoffs in modern distributed database system design: CAP is only part of the story. Computer, 45(2):37-42, February 2012. URL: https://doi.org/10.1109/MC.2012.33.
  2. Mustaque Ahamad, Gil Neiger, James E. Burns, Prince Kohli, and Phillip W. Hutto. Causal memory: Definitions, implementation, and programming. Distrib. Comput., 9(1):37-49, March 1995. URL: https://doi.org/10.1007/BF01784241.
  3. Peter Alvaro, Neil Conway, Joseph M. Hellerstein, and David Maier. Blazes: Coordination analysis and placement for distributed programs. ACM Trans. Database Syst., 42(4), October 2017. URL: https://doi.org/10.1145/3110214.
  4. 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.
  5. Jason Baker, Chris Bond, James C. Corbett, J. J. Furman, Andrey Khorlin, James Larson, Jean-Michel Leon, Yawei Li, Alexander Lloyd, and Vadim Yushprakh. Megastore: Providing scalable, highly available storage for interactive services. In Proceedings of the Fifth Biennial Conference on Innovative Data Systems Research, CIDR 2011, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings, pages 223-234. www.cidrdb.org, 2011. URL: http://cidrdb.org/cidr2011/Papers/CIDR11_Paper32.pdf.
  6. 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. URL: https://doi.org/10.14778/3297753.3297760.
  7. Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, Nuno Preguiça, Mahsa Najafzadeh, and Marc Shapiro. Putting consistency back into eventual consistency. In Proceedings of the Tenth European Conference on Computer Systems, EuroSys '15, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2741948.2741972.
  8. Valter Balegas, Diogo Serra, Sérgio Duarte, Carla Ferreira, Marc Shapiro, Rodrigo Rodrigues, and Nuno M. Preguiça. Extending eventually consistent cloud databases for enforcing numeric invariants. In 34th IEEE Symposium on Reliable Distributed Systems, SRDS 2015, Montreal, QC, Canada, September 28 - October 1, 2015, pages 31-36. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/SRDS.2015.32.
  9. 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.
  10. Hal Berenson, Philip A. Bernstein, Jim Gray, Jim Melton, Elizabeth J. O'Neil, and Patrick E. O'Neil. A critique of ANSI SQL isolation levels. In Michael J. Carey and Donovan A. Schneider, editors, Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data, San Jose, California, USA, May 22-25, 1995, pages 1-10. ACM Press, 1995. URL: https://doi.org/10.1145/223784.223785.
  11. Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987. Google Scholar
  12. Dina Borrego, Nuno Preguiça, Elisa Gonzalez Boix, and Carla Ferreira. Ensuring convergence and invariants without coordination (appendix), 2025. URL: https://soft.vub.ac.be/Publications/2025/vub-tr-soft-25-02.pdf.
  13. Sebastian Burckhardt, Manuel Fähndrich, Daan Leijen, and Benjamin P. Wood. Cloud types for eventual consistency. In James Noble, editor, ECOOP 2012 - Object-Oriented Programming - 26th European Conference, Beijing, China, June 11-16, 2012. Proceedings, volume 7313 of Lecture Notes in Computer Science, pages 283-307. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31057-7_14.
  14. Emmanuel Cecchet, Julie Marguerite, and Willy Zwaenepoel. Performance and scalability of EJB applications. In Mamdouh Ibrahim and Satoshi Matsuoka, editors, Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, Seattle, Washington, USA, November 4-8, 2002, pages 246-261. ACM, 2002. URL: https://doi.org/10.1145/582419.582443.
  15. Brian F. Cooper, Raghu Ramakrishnan, Utkarsh Srivastava, Adam Silberstein, Philip Bohannon, Hans-Arno Jacobsen, Nick Puz, Daniel Weaver, and Ramana Yerneni. PNUTS: Yahoo!’s hosted data serving platform. Proc. VLDB Endow., 1(2):1277-1288, August 2008. URL: https://doi.org/10.14778/1454159.1454167.
  16. James C. Corbett, Jeffrey Dean, Michael Epstein, Andrew Fikes, Christopher Frost, J. J. Furman, Sanjay Ghemawat, Andrey Gubarev, Christopher Heiser, Peter Hochschild, Wilson Hsieh, Sebastian Kanthak, Eugene Kogan, Hongyi Li, Alexander Lloyd, Sergey Melnik, David Mwaura, David Nagle, Sean Quinlan, Rajesh Rao, Lindsay Rolig, Yasushi Saito, Michal Szymaniak, Christopher Taylor, Ruth Wang, and Dale Woodford. Spanner: Google’s globally distributed database. ACM Trans. Comput. Syst., 31(3), August 2013. URL: https://doi.org/10.1145/2491245.
  17. Kevin De Porre, Carla Ferreira, and Elisa Gonzalez Boix. VeriFx: Correct Replicated Data Types for the Masses. In Karim Ali and Guido Salvaneschi, editors, 37th European Conference on Object-Oriented Programming (ECOOP 2023), volume 263 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:45, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2023.9.
  18. 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), October 2021. URL: https://doi.org/10.1145/3485484.
  19. Giuseppe DeCandia, Deniz Hastorun, Madan Jampani, Gunavardhan Kakulapati, Avinash Lakshman, Alex Pilchin, Swaminathan Sivasubramanian, Peter Vosshall, and Werner Vogels. Dynamo: Amazon’s highly available key-value store. In Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, SOSP '07, pages 205-220, New York, NY, USA, 2007. Association for Computing Machinery. URL: https://doi.org/10.1145/1294261.1294281.
  20. Hector Garcia-Molina and Kenneth Salem. Sagas. SIGMOD Rec., 16(3):249-259, December 1987. URL: https://doi.org/10.1145/38714.38742.
  21. Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. 'Cause I'm strong enough: Reasoning about consistency choices in distributed systems. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pages 371-384, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2837614.2837625.
  22. Julian Haas, Ragnar Mogk, Elena Yanakieva, Annette Bieniusa, and Mira Mezini. Lore: A programming model for verifiably safe local-first software. ACM Trans. Program. Lang. Syst., 46(1), January 2024. URL: https://doi.org/10.1145/3633769.
  23. Maurice P. Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, July 1990. URL: https://doi.org/10.1145/78969.78972.
  24. 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.
  25. Gowtham Kaki, Kapil Earanky, KC Sivaramakrishnan, and Suresh Jagannathan. Safe replication through bounded concurrency verification. Proc. ACM Program. Lang., 2(OOPSLA), October 2018. URL: https://doi.org/10.1145/3276534.
  26. 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.
  27. Martin Kleppmann, Adam Wiggins, Peter van Hardenberg, and Mark McGranaghan. Local-first software: you own your data, in spite of the cloud. In Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2019, pages 154-178, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3359591.3359737.
  28. Avinash Lakshman and Prashant Malik. Cassandra: A decentralized structured storage system. SIGOPS Oper. Syst. Rev., 44(2):35-40, April 2010. URL: https://doi.org/10.1145/1773912.1773922.
  29. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, July 1978. URL: https://doi.org/10.1145/359545.359563.
  30. Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno M. Preguiça, and Rodrigo Rodrigues. Making geo-replicated systems fast as possible, consistent when necessary. In Chandu Thekkath and Amin Vahdat, editors, 10th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2012, Hollywood, CA, USA, October 8-10, 2012, pages 265-278. USENIX Association, 2012. URL: https://www.usenix.org/conference/osdi12/technical-sessions/presentation/li.
  31. Cheng Li, Nuno M. Preguiça, and Rodrigo Rodrigues. Fine-grained consistency for geo-replicated systems. In Haryadi S. Gunawi and Benjamin C. Reed, editors, Proceedings of the 2018 USENIX Annual Technical Conference, USENIX ATC 2018, Boston, MA, USA, July 11-13, 2018, pages 359-372. USENIX Association, 2018. URL: https://www.usenix.org/conference/atc18/presentation/li-cheng.
  32. 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.
  33. Jed Liu, Tom Magrino, Owen Arden, Michael D. George, and Andrew C. Myers. Warranties for faster strong consistency. In Ratul Mahajan and Ion Stoica, editors, Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2014, Seattle, WA, USA, April 2-4, 2014, pages 503-517. USENIX Association, 2014. URL: https://www.usenix.org/conference/nsdi14/technical-sessions/presentation/liu_jed.
  34. Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. Don't settle for eventual: Scalable causal consistency for wide-area storage with cops. In Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles, SOSP '11, pages 401-416, New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/2043556.2043593.
  35. Pedro Lopes, João Sousa, Valter Balegas, Carla Ferreira, Sérgio Duarte, Annette Bieniusa, Rodrigo Rodrigues, and Nuno M. Preguiça. Antidote SQL: relaxed when possible, strict when necessary, 2019. URL: https://arxiv.org/abs/1902.03576.
  36. Patrick E. O'Neil. The escrow transactional method. ACM Trans. Database Syst., 11(4):405-430, December 1986. URL: https://doi.org/10.1145/7239.7265.
  37. Nuno M. Preguiça. Conflict-free replicated data types: An overview. CoRR, abs/1806.10254, 2018. URL: https://arxiv.org/abs/1806.10254.
  38. Nuno M. Preguiça, José Legatheaux Martins, Miguel Cunha, and Henrique João L. Domingos. Reservations for conflict avoidance in a mobile database system. In Daniel P. Siewiorek, Mary Baker, and Robert T. Morris, editors, Proceedings of the First International Conference on Mobile Systems, Applications, and Services, MobiSys 2003, San Francisco, CA, USA, May 5-8, 2003, pages 43-56. USENIX, 2003. URL: https://doi.org/10.1145/1066116.1189038.
  39. Marc Shapiro, Nuno M. Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In Xavier Défago, Franck Petit, and Vincent Villain, editors, Stabilization, Safety, and Security of Distributed Systems - 13th International Symposium, SSS 2011, Grenoble, France, October 10-12, 2011. Proceedings, volume 6976 of Lecture Notes in Computer Science, pages 386-400. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24550-3_29.
  40. Marc Shapiro, Nuno M. Preguiça, Carlos Baquero, and Marek Zawirski. A comprehensive study of convergent and commutative replicated data types. Technical report, INRIA, 2011. Google Scholar
  41. Liuba Shrira, Hong Tian, and Douglas B. Terry. Exo-leasing: Escrow synchronization for mobile clients of commodity storage servers. In Valérie Issarny and Richard E. Schantz, editors, Middleware 2008, ACM/IFIP/USENIX 9th International Middleware Conference, Leuven, Belgium, December 1-5, 2008, Proceedings, volume 5346 of Lecture Notes in Computer Science, pages 42-61. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-89856-6_3.
  42. KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan. Declarative programming over eventually consistent data stores. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '15, pages 413-424, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2737924.2737981.
  43. Yair Sovran, Russell Power, Marcos K. Aguilera, and Jinyang Li. Transactional storage for geo-replicated systems. In Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles, SOSP '11, pages 385-400, New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/2043556.2043592.
  44. D. B. Terry, M. M. Theimer, Karin Petersen, A. J. Demers, M. J. Spreitzer, and C. H. Hauser. Managing update conflicts in bayou, a weakly connected replicated storage system. SIGOPS Oper. Syst. Rev., 29(5):172-182, December 1995. URL: https://doi.org/10.1145/224057.224070.
  45. Werner Vogels. Eventually consistent. Commun. ACM, 52(1):40-44, January 2009. URL: https://doi.org/10.1145/1435417.1435432.
  46. Michael Whittaker and Joseph M. Hellerstein. Interactive checks for coordination avoidance. Proc. VLDB Endow., 12(1):14-27, September 2018. URL: https://doi.org/10.14778/3275536.3275538.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact