CRDT Emulation, Simulation, and Representation Independence
summary
Formalizes CRDT emulation as weak simulation between transition systems and gives constructive translations both ways, focusing on the op-based→state-based case where the state is represented as state as sets of messages and merges are interpreted by partitioning concurrent messages. Proof forces frequent broadcasts to ensure matching deliveries, yields a trace equivalence that preserves safety properties, and proves a co-termination result for an imperative client language; equivalence is sensitive to network semantics and the translation as given is correct but not optimized for performance.
AI-written summary · about
chapters (12)
- 0:00CRDT introduction
- 1:05CRDT background and flavors
- 4:17Op-based vs state-based equivalence
- 7:28Simulation proof for translations
- 9:12Op-based to state-based translation
- 13:55Simulation proof steps
- 17:51Observational equivalence conclusion
- 19:15Q&A
- 20:17Negative results and simulations
- 21:04Arbitrary merging soundness
- 21:45Use cases and performance
- 22:48Adjunctions between translations
related talks
36mConflict-Free Replicated Datatypes (CRDT)
48mCRDTs: From sequential to concurrent executions
15mModular Verification of Op-Based CRDTs in Separation Logic
29mComposing and decomposing op-based CRDTs with semidirect products
15mComposing and Decomposing Op-Based CRDTs with Semidirect Products
41mTowards language support for distributed systems
29mAbout Combining Functional Reactive Programming and Replicated Data Types
40mPractical Demystification of CRDT