一句话：提出 Katara，从顺序数据类型实现自动合成并验证 CRDT 设计，降低正确构造 CRDT 的门槛。
CRDT 能支持可扩展、无协调的分布式系统，但正确构造 CRDT 十分困难，通常依赖人工证明。本文提出 Katara：输入顺序数据类型实现，自动合成经过验证的 CRDT 设计。其核心是一种新的 CRDT 正确性定义，将参考顺序类型与轻量级排序约束结合，以解决非交换操作间的冲突；并将正确性编码为 SMT 逻辑，借助合成的归纳不变式以及手工设计的 CRDT 状态与运行时语法，沿用 verified lifting 路线。评估显示，Katara 能为多种场景自动合成 CRDT，既复现经典设计，也能依据已有文献规范合成新设计，且合成结果完全自动验证，从而把新 CRDT 的开发从繁琐的人工正确性证明简化为轻量级规范。
Conflict-free replicated data types (CRDTs) are a promising tool for designing scalable, coordination-free distributed systems. However, constructing correct CRDTs is difficult, posing a challenge for even seasoned developers. As a result, CRDT development is still largely the domain of academics, with new designs often awaiting peer review and a manual proof of correctness. In this paper, we present Katara, a program synthesis-based system that takes sequential data type implementations and automatically synthesizes verified CRDT designs from them. Key to this process is a new formal definition of CRDT correctness that combines a reference sequential type with a lightweight ordering constraint that resolves conflicts between non-commutative operations. Our process follows the tradition of work in verified lifting, including an encoding of correctness into SMT logic using synthesized inductive invariants and hand-crafted grammars for the CRDT state and runtime. Katara is able to automatically synthesize CRDTs for a wide variety of scenarios, from reproducing classic CRDTs to synthesizing novel designs based on specifications in existing literature. Crucially, our synthesized CRDTs are fully, automatically verified, eliminating entire classes of common errors and reducing the process of producing a new CRDT from a painstaking paper proof of correctness to a lightweight specification.
@article{paperbot1469,
title = {Katara: synthesizing CRDTs with verified lifting},
author = {Shadaj Laddad and Conor Power and Mae Milano and Alvin Cheung and Joseph M. Hellerstein},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563336}
}