Detecting Incorrect Behavior of Cloud Databases as an Outsider

TL;DR

This paper introduces Cobra, a system that efficiently verifies serializability in cloud databases using hardware acceleration and SMT solvers, making the process practical on real-world workloads despite the NP-complete nature of the problem.

Contribution

Cobra is the first system to treat serializability verification as a systems problem, combining new encoding, hardware acceleration, and SMT solvers to handle larger problem sizes.

Findings

Cobra improves verification capacity by at least 10x over baselines.

Cobra imposes modest overhead on clients.

Effective handling of garbage collection in serializability verification.

Abstract

Cloud DBs offer strong properties, including serializability, sometimes called the gold standard database correctness property. But cloud DBs are complicated black boxes, running in a different administrative domain from their clients; thus, clients might like to know whether the DBs are meeting their contract. A core difficulty is that the underlying problem here, namely verifying serializability, is NP-complete. Nevertheless, we hypothesize that on real-world workloads, verifying serializability is tractable, and we treat the question as a systems problem, for the first time. We build Cobra, which tames the underlying search problem by blending a new encoding of the problem, hardware acceleration, and a careful choice of a suitable SMT solver. cobra also introduces a technique to address the challenge of garbage collection in this context. cobra improves over natural baselines by at least 10x in the problem size it can handle, while imposing modest overhead on clients.