Shadaj Laddad and Conor Power and Mae Milano and Alvin Cheung and Joseph M. Hellerstein

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2023-2

January 11, 2023

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-2.pdf

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.

Advisors: Joseph M. Hellerstein and Alvin Cheung

---

BibTeX citation:

@mastersthesis{Laddad:EECS-2023-2,
    Author= {Laddad, Shadaj and Power, Conor and Milano, Mae and Cheung, Alvin and Hellerstein, Joseph M.},
    Title= {Katara: Synthesizing CRDTs with Verified Lifting},
    School= {EECS Department, University of California, Berkeley},
    Year= {2023},
    Month= {Jan},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-2.html},
    Number= {UCB/EECS-2023-2},
    Abstract= {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.},
}

EndNote citation:

%0 Thesis
%A Laddad, Shadaj 
%A Power, Conor 
%A Milano, Mae 
%A Cheung, Alvin 
%A Hellerstein, Joseph M. 
%T Katara: Synthesizing CRDTs with Verified Lifting
%I EECS Department, University of California, Berkeley
%D 2023
%8 January 11
%@ UCB/EECS-2023-2
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2023/EECS-2023-2.html
%F Laddad:EECS-2023-2