Modular Verification of State-Based CRDTs in Separation Logic


Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal: Modular Verification of State-Based CRDTs in Separation Logic. In ECOOP 2023, July 2023. https://doi.org/10.4230/LIPICS.ECOOP.2023.22
Conference Paper
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.

The bibtex source for this publication:
@inproceedings{DBLP:conf/ecoop/NietoDGTB23,
 author = {Abel Nieto and
  Arnaud Daby{-}Seesaram and
  L{\'{e}}on Gondelman and
  Amin Timany and
  Lars Birkedal},
 editor = {Karim Ali
  and Guido Salvaneschi},
 title = {Modular Verification of State-Based CRDTs in Separation Logic},
 booktitle    = {37th European Conference on Object-Oriented Programming, {ECOOP} 2023,
  July 17-21, 2023, Seattle, Washington, United States},
 series = {LIPIcs},
 volume = {263},
 pages = {22:1--22:27},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 year = {2023},
 url = {https://doi.org/10.4230/LIPIcs.ECOOP.2023.22},
 doi = {10.4230/LIPICS.ECOOP.2023.22},
 timestamp = {Tue, 11 Jul 2023 17:14:10 +0200},
 biburl = {https://dblp.org/rec/conf/ecoop/NietoDGTB23.bib},
 bibsource = {dblp computer science bibliography, https://dblp.org}
}