pith. sign in

arxiv: 2605.31569 · v2 · pith:7SE6QQUGnew · submitted 2026-05-29 · 💻 cs.DC · cs.DB· cs.LO· cs.PL

A Datalog Framework for Conflict-Free Replicated Data Types

Elena Yanakieva , Annette Bieniusa , Stefania Dumbrava This is my paper

Pith reviewed 2026-06-28 20:48 UTC · model grok-4.3

classification 💻 cs.DC cs.DBcs.LOcs.PL
keywords CRDTDatalogreplicated data typesconflict-freeproperty-based testingdistributed systemsconcurrencylogic programs
0
0 comments X

The pith

Datalog programs over operation contexts model CRDT semantics to support automated analysis and testing of concurrent behavior.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a framework that expresses the semantics of conflict-free replicated data types as Datalog logic programs. These programs operate on operation contexts to make concurrent interactions explicit and compositional. A sympathetic reader would care because this turns CRDT design into executable specifications that can be checked automatically rather than through ad-hoc reasoning. The authors apply the framework to a collaborative graph editing case study and test correctness and scalability as the number of operations and replicas grows.

Core claim

The central claim is that CRDT semantics can be specified declaratively in Datalog as executable logic programs over operation contexts. This modeling makes concurrency explicit and compositional, enabling automated analysis such as property-based testing to compare implementations against the specifications.

What carries the argument

Datalog programs over operation contexts, which capture CRDT semantics by defining rules on how operations interact in concurrent settings.

If this is right

  • CRDT compositions can be analyzed systematically without manual intervention.
  • Implementations can be tested for correctness using property-based methods derived from the specs.
  • The framework supports validation and scalability checks on applications with growing numbers of operations and replicas.
  • Developers can prototype CRDT-based applications in a declarative and compositional way.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same declarative approach could apply to other forms of replicated state beyond CRDTs.
  • Early semantic mismatches in distributed collaborative tools might be caught before code is written.
  • The framework opens a path to generating test suites directly from high-level CRDT descriptions.

Load-bearing premise

Expressing CRDT semantics as Datalog programs over operation contexts will accurately capture intended concurrent behaviors.

What would settle it

A CRDT implementation whose observed behavior under concurrent updates differs from predictions of the corresponding Datalog program.

Figures

Figures reproduced from arXiv: 2605.31569 by Annette Bieniusa, Elena Yanakieva, Stefania Dumbrava.

Figure 1
Figure 1. Figure 1: Dangling edge scenario. executes rmvN(m). To avoid an invalid graph state, a conflict-resolution strategy is re￾quired to preserve the invariant. One possible outcome is to remove m and discard the edge; another is to discard the removal of m. No resolution is universally correct: the appropriate behavior depends on the intended application semantics. Developers must therefore specify how conflicting opera… view at source ↗
Figure 2
Figure 2. Figure 2: Example operation context for an add-wins set and its Datalog encoding. [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Workflow for deriving and validating CRDT compositions. From application re [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Layered transformation for update-wins Map [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Layered transformation for isolate-delete graph. [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Transformation rules for detach-delete graph. [PITH_FULL_IMAGE:figures/full_fig_p012_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Scalability of SLS and ICS for isolate-delete (ID) and detach-delete (DD). [PITH_FULL_IMAGE:figures/full_fig_p014_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Single vs. incremental SLS and ICS for isolate-delete (ID) and detach-delete (DD). [PITH_FULL_IMAGE:figures/full_fig_p016_8.png] view at source ↗
read the original abstract

Distributed applications increasingly support local-first collaboration over shared data, allowing multiple users to perform updates concurrently without global coordination. Such collaboration requires careful design to capture the intended semantics of the concurrent interactions. We introduce a declarative framework for specifying and reasoning about the semantics of conflict-free replicated data types (CRDTs) and CRDT-based applications in Datalog. The framework models CRDT semantics as executable logic programs over operation contexts, making concurrency explicit and compositional, and thus amenable to automated analysis. As one application, we use property-based testing to compare implementations. To the best of our knowledge, this is the first work to systematically use Datalog as a foundation for prototyping and analyzing complex CRDTs and their compositions. We evaluate our methodology using a collaborative graph data editing case study and report experimentation results assessing correctness validation and scalability with an increasing number of operations and replicas.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces a declarative Datalog framework for specifying CRDT semantics as executable logic programs over operation contexts. This makes concurrency explicit and compositional, enabling automated analysis and property-based testing of CRDT implementations and compositions. The approach is evaluated via a collaborative graph-editing case study that assesses correctness validation and scalability with increasing operations and replicas.

Significance. If the Datalog encoding is shown to faithfully preserve CRDT convergence, commutativity, and causality properties, the framework could offer a practical declarative layer for prototyping and verifying complex CRDT-based applications, which is a novel contribution given the absence of prior systematic Datalog use for this purpose. The explicit handling of operation contexts and support for property-based testing are potential strengths for local-first collaboration tools.

major comments (2)
  1. [§4] §4 (Evaluation, correctness validation subsection): The reported correctness validation results for the graph-editing case study compare implementations via property-based testing but provide no explicit argument, bisimulation, or exhaustive enumeration establishing that the Datalog programs are equivalent to standard CRDT merge semantics (e.g., no check against mathematical definitions of convergence under arbitrary interleavings or commutativity).
  2. [§3] §3 (Datalog Framework): The modeling of CRDT operations as logic programs over contexts is presented as capturing intended concurrent behavior, yet the manuscript supplies no derivation or invariant showing preservation of key CRDT axioms such as idempotence and associativity of the merge operation when encoded in Datalog.
minor comments (2)
  1. [Abstract and §4] The abstract and evaluation description mention scalability experiments but do not specify the exact metrics (e.g., runtime vs. number of replicas) or the Datalog engine used, which would aid reproducibility.
  2. [§3] Notation for operation contexts and Datalog predicates could be clarified with a small running example early in §3 to make the encoding more accessible.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. The comments highlight opportunities to strengthen the formal links between our Datalog encodings and standard CRDT properties. We address each point below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [§3] §3 (Datalog Framework): The modeling of CRDT operations as logic programs over contexts is presented as capturing intended concurrent behavior, yet the manuscript supplies no derivation or invariant showing preservation of key CRDT axioms such as idempotence and associativity of the merge operation when encoded in Datalog.

    Authors: We agree that an explicit invariant would make the preservation clearer. The encodings are constructed by directly translating the standard CRDT merge definitions into Datalog rules that operate over explicit operation contexts; because Datalog evaluation is monotonic and the merge is expressed via set-union over contexts, the algebraic properties follow from the underlying CRDT definitions. In the revised version we will add a short derivation subsection in §3 that shows idempotence and associativity are preserved by construction, using the fact that repeated application of the same rule set yields the same minimal model. revision: yes

  2. Referee: [§4] §4 (Evaluation, correctness validation subsection): The reported correctness validation results for the graph-editing case study compare implementations via property-based testing but provide no explicit argument, bisimulation, or exhaustive enumeration establishing that the Datalog programs are equivalent to standard CRDT merge semantics (e.g., no check against mathematical definitions of convergence under arbitrary interleavings or commutativity).

    Authors: The property-based testing in the case study empirically checks that the Datalog model produces the same outcomes as reference CRDT implementations under random interleavings. We acknowledge that this is not a formal equivalence proof. In revision we will augment the correctness-validation subsection with a high-level argument that maps the standard CRDT convergence proof (based on commutativity and idempotence of the merge) onto the Datalog rules via the context encoding; we will also note that exhaustive enumeration is infeasible for the graph case study but that the testing regime covers the relevant interleavings. A full bisimulation is left for future work. revision: partial

Circularity Check

0 steps flagged

No circularity: independent declarative modeling framework

full rationale

The paper presents a new Datalog encoding of CRDT semantics over operation contexts as an executable modeling layer for analysis and testing. No equations, fitted parameters, or predictions are defined; the central claim is the introduction of this framework itself rather than a derivation that reduces to prior results by construction. No self-citations are invoked as load-bearing uniqueness theorems or ansatzes, and the graph-editing case study is an application of the framework rather than a self-referential validation. The derivation chain is self-contained as a modeling contribution without reduction to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review yields no explicit free parameters, axioms, or invented entities; the Datalog framework itself is the core new modeling construct but is not broken down into sub-components here.

pith-pipeline@v0.9.1-grok · 5686 in / 1086 out tokens · 22063 ms · 2026-06-28T20:48:20.733244+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

14 extracted references · 13 canonical work pages

  1. [1]

    doi: 10.1007/978-3-642-24206-9\

    work page doi:10.1007/978-3-642-24206-9

  2. [2]

    Sebastian Burckhardt

    doi: 10.1145/3721473.3722141. Sebastian Burckhardt. Principles of eventual consistency.Found. Trends Program. Lang., 1(1-2): 1–150,

    work page doi:10.1145/3721473.3722141

  3. [3]

    Principles of eventual consistency

    doi: 10.1561/2500000011. Koen Claessen and John Hughes. Quickcheck: a lightweight tool for random testing of Haskell programs. InICFP, pages 268–279. ACM,

    work page doi:10.1561/2500000011

  4. [4]

    QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs,

    doi: 10.1145/351240.351266. Seth Gilbert and Nancy Lynch. Brewer’s conjecture and the feasibility of consistent, avail- able, partition-tolerant web services.SIGACT News, 33(2):51–59,

    work page doi:10.1145/351240.351266

  5. [5]

    doi: 10.1145/564585. 564601. Herbert Jordan, Bernhard Scholz, and Pavle Subotic. Souffl´ e: On synthesis of program analyzers. InCA V (2), LNCS, pages 422–430. Springer,

    work page doi:10.1145/564585

  6. [6]

    doi: 10.1007/978-3-319-41540-6\

    work page doi:10.1007/978-3-319-41540-6

  7. [7]

    Automerge.https://github.com/automerge/(visited: 2026-01),

    Martin Kleppmann. Automerge.https://github.com/automerge/(visited: 2026-01),

    2026

  8. [8]

    Lindsey Kuper and Ryan R

    doi: 10.4230/DARTS.9.2.26. Lindsey Kuper and Ryan R. Newton. LVars: lattice-based data structures for deterministic parallelism. InFHPC@ICFP, pages 71–84. ACM,

    work page doi:10.4230/darts.9.2.26

  9. [9]

    Shadaj Laddad, Conor Power, Mae Milano, Alvin Cheung, Natacha Crooks, and Joseph M

    doi: 10.1145/2502323.2502326. Shadaj Laddad, Conor Power, Mae Milano, Alvin Cheung, Natacha Crooks, and Joseph M. Hellerstein. Keep CALM and CRDT on.PVLDB, 16(4):856–863,

    work page doi:10.1145/2502323.2502326

  10. [10]

    doi: 10.14778/3574245. 3574268. Christopher Meiklejohn and Peter Van Roy. Lasp: a language for distributed, coordination-free programming. InPPDP, pages 184–195. ACM,

    work page doi:10.14778/3574245

  11. [11]

    Petru Nicolaescu, Kevin Jahns, Michael Derntl, and Ralf Klamma

    doi: 10.1145/2790449.2790525. Petru Nicolaescu, Kevin Jahns, Michael Derntl, and Ralf Klamma. Yjs: A framework for near real-time P2P shared editing on arbitrary data types. InICWE, LNCS, pages 675–678. Springer,

    work page doi:10.1145/2790449.2790525

  12. [12]

    doi: 10.1007/978-3-319-19890-3\

    work page doi:10.1007/978-3-319-19890-3

  13. [13]

    doi: 10.1007/978-3-642-24550-3\

    work page doi:10.1007/978-3-642-24550-3

  14. [14]

    18Cambridge Author Appendix A Evaluation details This section reports additional details of the experimental evaluation summarized in Sec- tion

    doi: 10.1145/ 3519939.3523735. 18Cambridge Author Appendix A Evaluation details This section reports additional details of the experimental evaluation summarized in Sec- tion

    work page arXiv