DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2025.4

Ensuring Convergence and Invariants Without Coordination

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

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{borrego_et_al:LIPIcs.ECOOP.2025.4,
  author =	{Borrego, Dina and Pregui\c{c}a, Nuno and Gonzalez Boix, Elisa and Ferreira, Carla},
  title =	{{Ensuring Convergence and Invariants Without Coordination}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{4:1--4:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.4},
  URN =		{urn:nbn:de:0030-drops-232978},
  doi =		{10.4230/LIPIcs.ECOOP.2025.4},
  annote =	{Keywords: distributed systems, conflict resolution, RDTs, invariant preservation}
}

Document

Artifact

DOI: 10.4230/DARTS.11.2.1

Ensuring Convergence and Invariants Without Coordination (Artifact)

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

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract

Our related paper introduces the No-Op framework, a generic approach for enforcing consistency without coordination while guaranteeing both convergence and invariant preservation. We implemented the core of the No-Op replication protocol in VeriFx [De Porre et al., 2023], a programming language for RDTs with automated proof capabilities. Alongside the algorithm implementation, we developed formal proofs to automatically verify the algorithm’s correctness properties when applied to specific data types or application implementations. This artifact bundles the implementation of the No-Op framework, various CRDTs [Marc Shapiro et al., 2011], and an eBay-like auction system akin to the RUBiS system [Emmanuel Cecchet et al., 2002] described in Section 5 of the paper. The artifact also provides a Dockerfile that can be used to reproduce the verification results (Section 4 of the paper).

Cite as

Dina Borrego, Nuno Preguiça, Elisa Gonzalez Boix, and Carla Ferreira. Ensuring Convergence and Invariants Without Coordination (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 1:1-1:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{borrego_et_al:DARTS.11.2.1,
  author =	{Borrego, Dina and Pregui\c{c}a, Nuno and Gonzalez Boix, Elisa and Ferreira, Carla},
  title =	{{Ensuring Convergence and Invariants Without Coordination (Artifact)}},
  pages =	{1:1--1:7},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Borrego, Dina and Pregui\c{c}a, Nuno and Gonzalez Boix, Elisa and Ferreira, Carla},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.1},
  URN =		{urn:nbn:de:0030-drops-233447},
  doi =		{10.4230/DARTS.11.2.1},
  annote =	{Keywords: distributed systems, conflict resolution, RDTs, invariant preservation}
}

Search Results

Documents authored by Borrego, Dina

Ensuring Convergence and Invariants Without Coordination

Abstract

Cite as

Ensuring Convergence and Invariants Without Coordination (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message