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中规范与推理无冲突复制数据类型（CRDT）及基于CRDT的应用程序的语义。该框架将CRDT语义建模为操作上下文上的可执行逻辑程序，使并发性显式化且可组合，从而适用于自动化分析。作为一项应用，我们使用基于属性的测试来比较不同实现。据我们所知，这是首个系统性地利用Datalog作为原型设计与分析复杂CRDT及其组合的基础工作。我们通过一个协作图数据编辑案例研究来评估该方法，并报告了在验证正确性以及随着操作数和副本数增加时扩展性方面的实验结果。