Modulo: Finding Convergence Failure Bugs in Distributed Systems with Divergence...
summary
Modulo is a model-based tester that uses Divergence Resync Models to focus state exploration on interleavings of divergence and resync, generating schedules from an AEM and executing them via CEM wrappers. It runs as ~8k LOC, reuses AEMs across systems, and injects timed crashes, writes, restarts and log-check resyncs. Applied to ZooKeeper, MongoDB and Redis it finds 11 CFBs (6 new) and demonstrates AEM/CEM separation that keeps the explored state space small.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:29Background: Various Services Rely on Replicated Distributed Storage Systems
- 3:49Replicas Become Converged via Replication
- 4:01Clients Read Consistent Data
- 4:31Replication Does Not Occur and Replicas Remain Diverged
- 4:53Problem 2: Software Bugs in Resync Mechanisms May Cause Convergence Failures
- 7:19Key Idea 2: Separating Abstraction from Concrete Execution (Divergence Resync Model)
- 10:03Modulo Architecture: Checking if Converge Fails after Each Schedule Execution
- 11:20Abstract Execution Model: Predefined Write Sequence is Generated
- 16:30Implementation
- 18:15Conclusion
related talks
15mTesting Consensus Implementations using Communication Closure
41mProgramming Distributed Systems
22mCompositional Programming and Testing of Dynamic Distributed Systems
22mTowards Modelling and Verification of Coupler Behaviour in Climate Models
16mA Search-Based and Fault-Tolerant Approach to Concurrent Model Synchronisation
22mMonarch: A Fuzzing Framework for Distributed File Systems
19mCAFault: Enhance Fault Injection Technique in Practical Distributed Systems via...
57mChaos Engineering Primer