Mixed & Verified Consistency with Propel and ConOpY
summary
ConOpY is an object-oriented language that annotates replicated objects and methods with consistency levels and enforces them in the type system so programs mix strong and weak consistency safely, preventing data-flow violations across atomic transactions. Propel is a Scala-embedded verification DSL that types CRDT implementations and automatically proves commutativity, associativity and idempotence; it verifies common state-based CRDTs, compares against four state-of-the-art tools (sometimes beating timeouts), detects a known LWW op-based bug, and runs as a browser prototype.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:04Research goals
- 2:07Propel verification tool
- 4:13CRDT commutativity
- 5:57Demo: CRDT correctness
- 6:18Mixed consistency
- 7:42Mix consistency in applications
- 9:31Replicated objects
- 10:14Summary
- 10:36Q&A
- 10:57Industry readiness
- 12:02Dependencies
- 13:04TypeScript plans
- 14:08Consensus implementation
- 15:34Programming models
- 16:37Closing
related talks
16mType-Checking CRDT Convergence
15mRethinking Safe Consistency in Distributed Object-Oriented Programming
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
41mProgramming Distributed Systems
15mMuch ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D
01h 30mImplementing, verifying and debugging distributed event-based systems
41mTowards language support for distributed systems
22mLayers of Confluence for Actors