Implementing, verifying and debugging distributed event-based systems
summary
Argues that sequential data types can be lifted to replicated, mostly coordination-free objects by attaching concurrency invariants and feeding them to a static analyzer; prototype toolchain includes a Scala-like DSL called VeryFix, a verifier that emits SMT for Orana, and a transpiler that produces deployable RDTs — the group auto-verifies about 50 CRDT variants. Builds out‑of‑place debuggers for clusters and IoT (M5 stick + WebAssembly VM), validates debugging UI with a 22‑participant study, and reports hybrid lock insertion when static analysis finds unavoidable conflicts.
AI-written summary · about
chapters (15)
- 0:00Workshop introduction
- 1:08Keynote introduction
- 2:14From master thesis to distributed event systems
- 11:03Handling failures in AmbientTalk
- 13:51Replicated data types and CRDTs
- 23:07Reflection on AmbientTalk's evolution
- 25:35Designing general-purpose RDTs
- 37:25Validating CRDTs with static analysis
- 47:40Introducing VeryFix for RDTs
- 53:44Limitations of automated verification
- 56:55Need for tool support in distributed programming
- 1:04:30Debugging big data applications
- 1:13:26Debugging IoT systems with out-of-place debugging
- 1:18:21Challenges and future directions
- 1:20:30Q&A on constraints and failures
related talks
41mTowards language support for distributed systems
15mECROs: Building Global Scale Systems from Sequential Code
41mProgramming Distributed Systems
28mNew insights into distributed and concurrent programming
36mConflict-Free Replicated Datatypes (CRDT)
38mThe Verification of a Distributed System
29mAbout Combining Functional Reactive Programming and Replicated Data Types
28mReasoning about Distributed Reconfigurable Systems