Papers with Friends: Katara - Synthesizing CRDTs with Verified Lifting
At Fission, we really like reading papers, and, sometimes, implementing them (check out https://lu.ma/reactor!). Though we already run the ongoing, monthly distributed systems reading group, we end up running into papers that just need to be read and discussed "in the now," which may involve other topics like programming languages, cryptography, networking, or a concoction of many subjects. This is that kind of series.
For this rendition, we'll be reading and talking about the paper Katara: Synthesizing CRDTs with Verified Lifting by Laddad, et. al, which was accepted to OOPSLA 2022. We'll also have authors Shadaj Laddad & Mae Milano introduce it and participate in the discussion!
The abstract is as follows:
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.
You can also find an open source implementation of the work on Github.
Update: Video and chat log from the session are now available: https://talk.fission.codes/t/papers-with-friends-katara-synthesizing-crdts-with-verified-lifting/3493/2.