Completed
Pruning via graph paths (reachability)
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Cobra - Making Transactional Key-Value Stores Verifiably Serializable
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Serializability is a correctness contract
- 3 The underlying problem is...
- 4 Cobra: verifying serializability of black-box databases
- 5 Starting point: brute-force search on a polygraph
- 6 Outline
- 7 Checking serializability may be tractable in practice
- 8 Cobra aims at real-world workloads
- 9 How to reduce constraints in a polygraph?
- 10 Combining writes exploits a common pattern
- 11 Combining writes: exploit common patterns
- 12 Cobra exploits characteristics of the problem
- 13 Pruning via graph paths (reachability)
- 14 Cobra verifies in rounds to support growing histories
- 15 Experimental evaluation
- 16 Experiment setup
- 17 Cobra can handle 10x larger workloads
- 18 Decomposition of Cobra's verification runtime
- 19 Recap
- 20 Related work
- 21 Summary