Cobra - Making Transactional Key-Value Stores Verifiably Serializable

Explore a conference talk that delves into Cobra, a groundbreaking system designed to verify serializability in transactional key-value stores. Learn how this innovative approach combines black-box checking and scalability for real-world online transactional processing workloads. Discover the technical challenges faced in addressing the computationally expensive search problem and the novel techniques employed, including a new encoding of the validity condition, hardware acceleration for input pruning, and a transaction segmentation mechanism. Gain insights into Cobra's performance improvements, its ability to handle high transaction volumes, and its support for continuous verification. Understand the importance of serializability in cloud databases and how Cobra provides clients with assurance about database correctness in cloud environments.

Intro
Serializability is a correctness contract
The underlying problem is...
Cobra: verifying serializability of black-box databases
Starting point: brute-force search on a polygraph
Outline
Checking serializability may be tractable in practice
Cobra aims at real-world workloads
How to reduce constraints in a polygraph?
Combining writes exploits a common pattern
Combining writes: exploit common patterns
Cobra exploits characteristics of the problem
Pruning via graph paths (reachability)
Cobra verifies in rounds to support growing histories
Experimental evaluation
Experiment setup
Cobra can handle 10x larger workloads
Decomposition of Cobra's verification runtime
Recap
Related work
Summary