Model Checking Distributed Software Systems
summary
An implementation-level model checker called Must embeds a small message-passing DSL in Rust and exhaustively explores nonisomorphic execution graphs with partial order reduction, guaranteeing completeness and visiting each graph exactly once with only polynomial memory overhead. Applied to replicated-log implementations it handles the K! interleavings of concurrent writes and preserves the K−1 fault tolerance claim, letting developers swap a Rust trait network for testing via conditional compilation. Scaling and team integration remain hard in real deployments.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 3:53MUST project at AWS
- 7:30Distributed log protocols
- 13:17MUST modeling language
- 17:53Academic to product
- 21:25Research lessons
- 24:15Q&A
related talks
15mTowards Verifying Crash Consistency
27mLet's Bring System Dynamics Back to CS!
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
01h 08mFireside chat
25mContinuous compliance with Rust in automotive software
30mTrustworthy Runtime Verification via Bisimulation
25mResponsive Parallelism with Synchronization