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.

翻译：分布式应用越来越多地支持对共享数据的本地优先协作，允许多个用户在没有全局协调的情况下同时执行更新。这种协作需要精心设计以捕获并发交互的预期语义。我们引入了一个声明式框架，用于在Datalog中指定和推理无冲突复制数据类型（CRDTs）及基于CRDT的应用的语义。该框架将CRDT语义建模为操作上下文上的可执行逻辑程序，使并发性明确且可组合，从而适合自动分析。作为一项应用，我们使用基于属性的测试来比较不同实现。据我们所知，这是首个系统性地利用Datalog作为原型设计和分析复杂CRDT及其组合的工作。我们通过一个协作图数据编辑案例研究评估了我们的方法，并报告了在验证正确性以及随操作和副本数量增加的可扩展性方面的实验结果。