SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Thu 8 Dec 2022 11:00 - 11:30 at Lecture Theatre 2 - Synthesis I Chair(s): Hakjoo Oh

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.

Thu 8 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
Synthesis IOOPSLA at Lecture Theatre 2
Chair(s): Hakjoo Oh Korea University
10:30
30m
Research paper
Complexity-guided container replacement synthesisDistinguished Paper
OOPSLA
Chengpeng Wang Hong Kong University of Science and Technology, Peisen Yao Hong Kong University of Science and Technology, Wensheng Tang Hong Kong University of Science and Technology, Qingkai Shi Ant Group, Charles Zhang Hong Kong University of Science and Technology
DOI
11:00
30m
Talk
Katara: Synthesizing CRDTs with Verified Lifting
OOPSLA
Shadaj Laddad University of California at Berkeley, Conor Power University of California at Berkeley, Mae Milano University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein University of California at Berkeley
DOI
11:30
30m
Talk
Specification-Guided Component-Based Synthesis from Effectful Libraries
OOPSLA
Ashish Mishra Purdue University, Suresh Jagannathan Purdue University
DOI