A Deep Specification for Dropbox
summary
A formal QuickCheck-style specification is implemented as a state machine and run against real Dropbox clients in VMs using Clojure test.check, with operations read/write plus a special stabilize operation and conjectured up/down server messages to model non-determinism. The harness generates randomized sequences with sleeps and shrinking, finds timing-dependent surprises (including a reproducible data-loss case and unexpected file resurrection), and validates that specification-based random testing can expose real synchronizer bugs.
AI-written summary · about
chapters (13)
- 0:00Start
- 2:34A Specification
- 6:50Deep specifications
- 12:39Expressive type systems
- 15:20Key ideas
- 19:12QuickCheck
- 21:34Goals
- 22:56Test Setup
- 25:40Basic Specification
- 33:38Approach
- 34:39Final specification
- 37:09Using the specification for testing
- 38:39Modeling the operations
related talks
40mThe Mysteries of Dropbox
47mTesting the Hard Stuff and Staying Sane
32mGenerative Testing: Properties, State and Beyond
27mBreak It Yourself
43mspec loves data structures
25mPowerful Testing with test.check
36mTesting Stateful and Concurrent Systems Using test.check
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)