Composing and decomposing op-based CRDTs with semidirect products
summary
Presents a concrete construction that composes two op-based CRDTs into one using an explicit semidirect product action that transforms noncommuting ops (proofs show correctness under causality), with worked examples: an add+multiply numeric register using distributivity-like transformations, decomposition of existing add/remove sets into components, and a causal-plus-for-each set for formatting ranges. Implements the idea in a TypeScript library collabs, ships demos (end-to-end encrypted rich text via matrix.org and a collaborative shapes demo) and reports the approach as practical and functional.
AI-written summary · about
chapters (12)
- 0:00CRDTs and shared state
- 3:50CRDT challenges
- 4:53Semi-direct products for CRDTs
- 6:56Conflict resolution in CRDTs
- 10:27Semi-direct product workflow
- 11:30Example: Number CRDT
- 14:37New CRDT results
- 17:00Unique set and causal plus
- 20:30Collabs library
- 21:31Demos: Rich text and PowerPoint
- 23:15Recap and future
- 23:59Q&A
related talks
15mComposing and Decomposing Op-Based CRDTs with Semidirect Products
15mModular Verification of Op-Based CRDTs in Separation Logic
48mCRDTs: From sequential to concurrent executions
34mUsing CRDTs Beyond Text Editors
36mConflict-Free Replicated Datatypes (CRDT)
24mCRDT Emulation, Simulation, and Representation Independence
22mKatara: Synthesizing CRDTs with Verified Lifting
29mAbout Combining Functional Reactive Programming and Replicated Data Types