1 Search Results for "Gondelman, Léon"

Document
DOI: 10.4230/LIPIcs.ECOOP.2023.22
Modular Verification of State-Based CRDTs in Separation Logic

Authors: Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Conflict-free Replicated Datatypes (CRDTs) are a class of distributed data structures that are highly-available and weakly consistent. The CRDT taxonomy is further divided into two subclasses: state-based and operation-based (op-based). Recent prior work showed how to use separation logic to verify convergence and functional correctness of op-based CRDTs while (a) verifying implementations (as opposed to high-level protocols), (b) giving high level specifications that abstract from low-level implementation details, and (c) providing specifications that are modular (i.e. allow client code to use the CRDT like an abstract data type). We extend this separation logic approach to verification of CRDTs to handle state-based CRDTs, while respecting the desiderata (a)-(c). The key idea is to track the state of a CRDT as a function of the set of operations that produced that state. Using the observation that state-based CRDTs are automatically causally-consistent, we obtain CRDT specifications that are agnostic to whether a CRDT is state- or op-based. When taken together with prior work, our technique thus provides a unified approach to specification and verification of op- and state-based CRDTs. We have tested our approach by verifying StateLib, a library for building state-based CRDTs. Using StateLib, we have further verified convergence and functional correctness of multiple example CRDTs from the literature. Our proofs are written in the Aneris distributed separation logic and are mechanized in Coq.
Cite as

Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal. Modular Verification of State-Based CRDTs in Separation Logic. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 22:1-22:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{nieto_et_al:LIPIcs.ECOOP.2023.22,
  author =	{Nieto, Abel and Daby-Seesaram, Arnaud and Gondelman, L\'{e}on and Timany, Amin and Birkedal, Lars},
  title =	{{Modular Verification of State-Based CRDTs in Separation Logic}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{22:1--22:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.22},
  URN =		{urn:nbn:de:0030-drops-182154},
  doi =		{10.4230/LIPIcs.ECOOP.2023.22},
  annote =	{Keywords: separation logic, distributed systems, CRDT, replicated data type, formal verification}
}
  • Refine by Author
  • 1 Birkedal, Lars
  • 1 Daby-Seesaram, Arnaud
  • 1 Gondelman, Léon
  • 1 Nieto, Abel
  • 1 Timany, Amin

  • Refine by Classification
  • 1 Theory of computation → Distributed algorithms
  • 1 Theory of computation → Program verification
  • 1 Theory of computation → Separation logic

  • Refine by Keyword
  • 1 CRDT
  • 1 distributed systems
  • 1 formal verification
  • 1 replicated data type
  • 1 separation logic

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2023

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact