Katara: synthesizing CRDTs with verified lifting
Katara: synthesizing CRDTs with verified lifting
复制标题
Katara：通过验证提升来合成 CRDT
DOI：
10.1145/3563336
复制
发表时间：
2022
影响因子：
--
通讯作者：
Hellerstein, Joseph M.
中科院分区：
文献类型：
--
作者：
Laddad, Shadaj;Power, Conor;Milano, Mae;Cheung, Alvin;Hellerstein, Joseph M.
无冗余复制数据类型（CRDTs）是设计可伸缩、无协调的分布式系统的一个很有前途的工具。然而，构建正确的CRDT是困难的，即使是经验丰富的开发人员也面临挑战。因此，CRDT的开发在很大程度上仍然是学术界的领域，新的设计通常需要等待同行评审和手动证明正确性。在本文中，我们提出了卡塔拉，一个程序合成为基础的系统，需要顺序数据类型的实现，并自动合成验证CRDT设计。这个过程的关键是CRDT正确性的一个新的正式定义，它将引用顺序类型与解决非交换操作之间冲突的轻量级排序约束相结合。我们的过程遵循验证提升工作的传统，包括使用合成归纳不变量和手工制作的CRDT状态和运行时语法将正确性编码到SMT逻辑中。Katara能够自动合成各种场景的CRDT，从再现经典CRDT到基于现有文献中的规范合成新颖设计。至关重要的是，我们合成的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.
登录
查看更多内容
阿卡在行动
DOI：
--
发表时间：
2016
期刊：
影响因子：
--
作者：
Raymond Roestenburg;R. Bakker;R. B. Williams
通讯作者：
R. B. Williams
DOI：
10.1145/1294261.1294281
发表时间：
2007-10
期刊：
EAI Endorsed Trans. Scalable Inf. Syst.
影响因子：
--
作者：
Giuseppe DeCandia;D. Hastorun;M. Jampani;G. Kakulapati;A. Lakshman;A. Pilchin;S. Sivasubramanian
通讯作者：
Giuseppe DeCandia;D. Hastorun;M. Jampani;G. Kakulapati;A. Lakshman;A. Pilchin;S. Sivasubramanian
影响因子：
1.8
作者：
Kaki, Gowtham;Earanky, Kapil;Jagannathan, Suresh
通讯作者：
Jagannathan, Suresh
DOI：
10.1145/3183713.3196891
发表时间：
2018-01
期刊：
Proceedings of the 2018 International Conference on Management of Data
影响因子：
--
作者：
Maaz Bin Safeer Ahmad;Alvin Cheung
通讯作者：
Maaz Bin Safeer Ahmad;Alvin Cheung
可合并的复制数据类型
影响因子：
--
作者：
Kaki, Gowtham;Priya, Swarn;Sivaramakrishnan, KC;Jagannathan, Suresh
通讯作者：
Jagannathan, Suresh