Certified Mergeable Replicated Data Types
summary
A certified MRDT library implemented in F provides machine-checked specifications and proofs that three-way merge implementations preserve intents like add-wins, fixes a broken OR-set by using unique IDs, and gives the first certified replicated queue with constant-time push/pop queue and linear-time merge. Proofs use an event-based spec and a simulation relation; verified, efficient OR-set variants and balanced-tree sets exist, code extracts to OCaml and runs on Irmin, and the design yields composition by construction*.
AI-written summary · about
chapters (14)
- 0:00Collaborative Apps
- 0:35Network Partitions
- 1:07Distributed Version Control Systems
- 1:56Mergeable Replicated Data Types
- 3:56Observed-Removed Set
- 6:06Concretising Intent
- 8:16Fixing OR-Set
- 9:51Specifying OR-Set
- 11:30Simulation Relation
- 12:29Verification effort
- 13:14Composing RDTs is HARD!
- 14:12Composing IRC-style chat
- 14:47Generic Map MRDT
- 15:35Summary
related talks
14mAutomatically Verifying Replication-aware Linearizability
39mEventually Consistent Data Structures
36mConflict-Free Replicated Datatypes (CRDT)
29mAbout Combining Functional Reactive Programming and Replicated Data Types
40mPractical Demystification of CRDT
48mCRDTs: From sequential to concurrent executions
22mKatara: Synthesizing CRDTs with Verified Lifting
01h 13mCRDTs: The hard parts