Katara: Synthesizing CRDTs with Verified Lifting
summary
Katara automatically synthesizes verified CRDTs from sequential data-type implementations and a pairwise operation ordering policy, encoding correctness into SMT and using Metalift with Rosette + CVC5 to search and verify designs. It composes a library of joint semi-lattice primitives for merge and state, produces both state and operation code, reproduces classic CRDTs and novel representations, and uses bounded verification pruning to cut worst-case synthesis from about 2 hours down to ~20 minutes; the implementation is open source.
AI-written summary · about
chapters (10)
- 0:00Start
- 3:24CRDTs in Practice
- 6:26what's in a CRDT
- 6:57convergence by construction
- 9:03relaxing semantics
- 11:18verified lifting
- 12:31SMT verification: op-orders
- 13:13efficient runtime search
- 14:02synthesis results
- 15:08novel CRDT representations
related talks
36mConflict-Free Replicated Datatypes (CRDT)
40mPractical Demystification of CRDT
16mType-Checking CRDT Convergence
01h 30mImplementing, verifying and debugging distributed event-based systems
14mAutomatically Verifying Replication-aware Linearizability
29mComposing and decomposing op-based CRDTs with semidirect products
34mUsing CRDTs Beyond Text Editors
48mCRDTs: From sequential to concurrent executions