Search Results

Documents authored by Preguiça, Nuno

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}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2017.24
Non-Uniform Replication

Authors: Gonçalo Cabrita and Nuno Preguiça

Published in: LIPIcs, Volume 95, 21st International Conference on Principles of Distributed Systems (OPODIS 2017)

Abstract
Replication is a key technique in the design of efficient and reliable distributed systems. As information grows, it becomes difficult or even impossible to store all information at every replica. A common approach to deal with this problem is to rely on partial replication, where each replica maintains only a part of the total system information. As a consequence, a remote replica might need to be contacted for computing the reply to some given query, which leads to high latency costs particularly in geo-replicated settings. In this work, we introduce the concept of non- uniform replication, where each replica stores only part of the information, but where all replicas store enough information to answer every query. We apply this concept to eventual consistency and conflict-free replicated data types. We show that this model can address useful problems and present two data types that solve such problems. Our evaluation shows that non-uniform replication is more efficient than traditional replication, using less storage space and network bandwidth.
Cite as

Gonçalo Cabrita and Nuno Preguiça. Non-Uniform Replication. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{cabrita_et_al:LIPIcs.OPODIS.2017.24,
  author =	{Cabrita, Gon\c{c}alo and Pregui\c{c}a, Nuno},
  title =	{{Non-Uniform Replication}},
  booktitle =	{21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-061-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{95},
  editor =	{Aspnes, James and Bessani, Alysson and Felber, Pascal and Leit\~{a}o, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2017.24},
  URN =		{urn:nbn:de:0030-drops-86393},
  doi =		{10.4230/LIPIcs.OPODIS.2017.24},
  annote =	{Keywords: Non-uniform Replication, Partial Replication, Replicated Data Types, Eventual Consistency}
}
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