Document Open Access Logo

Ensuring Convergence and Invariants Without Coordination (Artifact)

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

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.11.2.1.pdf
  • Filesize: 0.68 MB
  • 7 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

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 Get BibTex

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) https://doi.org/10.4230/DARTS.11.2.1

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 Afonso Vilalonga for his help in testing the artifact.

Artifact

  MD5 Sum: 9b1d59df8ae8bdad45e0f83868d4674f (Get MD5 Sum)

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2025 Call for Artifacts and the ACM Artifact Review and Badging Policy.

Related Article

References

  1. 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.
  2. 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.
  3. 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
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