一句话：在分离逻辑中提出模块化框架，用可靠因果广播库简化 op-based CRDT 实现的安全性质验证，并在 Coq 中机器化验证 12 个实例。
基于操作的无冲突复制数据类型（op-based CRDT）要求所有操作可交换以使副本状态最终收敛，且操作必须按因果序在副本间传播。本文提出一个用分离逻辑验证 CRDT 实现安全性质的框架，由两个库组成：一个实现可靠因果广播（RCB）协议，使副本能按因果序交换消息；另一个 OpLib 库基于 RCB 简化 op-based CRDT 的构造与正确性证明。借助 OpLib，客户端可将新 CRDT 实现为纯函数式数据结构，无需处理网络操作、并发控制与可变状态，也无需重复实现因果广播。作者用该框架实现了文献中 12 个 CRDT 实例，包括多个版本的复制寄存器与复制集合、product 与 map 两个 CRDT 组合子及其 map 组合子的两个用例。所有证明在 Aneris 分布式分离逻辑中进行并在 Coq 中形式化。该工作是首个同时满足模块化、且面向可执行实现（而非高层协议）的 op-based CRDT 验证技术。
Operation-based Conflict-free Replicated Data Types (op-based CRDTs) are a family of distributed data structures where all operations are designed to commute, so that replica states eventually converge. Additionally, op-based CRDTs require that operations be propagated between replicas in causal order. This paper presents a framework for verifying safety properties of CRDT implementations using separation logic. The framework consists of two libraries. One implements a Reliable Causal Broadcast (RCB) protocol so that replicas can exchange messages in causal order. A second “OpLib” library then uses RCB to simplify the creation and correctness proofs of op-based CRDTs. OpLib allows clients to implement new CRDTs as purely-functional data structures, without having to reason about network operations, concurrency control and mutable state, and without having to each time re-implement causal broadcast. Using OpLib, we have implemented 12 example CRDTs from the literature, including multiple versions of replicated registers and sets, two CRDT combinators for products and maps, and two example use cases of the map combinator. Our proofs are conducted in the Aneris distributed separation logic and are formalized in Coq. Our technique is the first work on verification of op-based CRDTs that satisfies both of the following properties: it is modular and targets executable implementations , as opposed to high-level protocols.
@article{paperbot1414,
title = {Modular verification of op-based CRDTs in separation logic},
author = {Abel Nieto and Léon Gondelman and Alban Reynaud and Amin Timany and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563351}
}