Cobra: Making transactional key-value stores verifiably serializable

Cheng Tan, Changgeng Zhao, Shuai Mu, Michael Walfish

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Today's cloud databases offer strong properties, including serializability, sometimes called the gold standard database correctness property. But cloud databases are complicated black boxes, running in a different administrative domain from their clients. Thus, clients might like to know whether the databases are meeting their contract. To that end, we introduce cobra; cobra applies to transactional key-value stores. It is the first system that combines (a) black-box checking, of (b) serializability, while (c) scaling to real-world online transactional processing workloads. The core technical challenge is that the underlying search problem is computationally expensive. Cobra tames that problem by starting with a suitable SMT solver. Cobra then introduces several new techniques, including a new encoding of the validity condition; hardware acceleration to prune inputs to the solver; and a transaction segmentation mechanism that enables scaling and garbage collection. Cobra imposes modest overhead on clients, improves over baselines by 10× in verification cost, and (unlike the baselines) supports continuous verification. Our artifact can handle 2000 transactions/sec, equivalent to 170M/day.

Original languageEnglish (US)
Title of host publicationProceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020
PublisherUSENIX Association
Pages63-80
Number of pages18
ISBN (Electronic)9781939133199
StatePublished - 2020
Event14th USENIX Symposium on Operating Systems Design and Implementation,OSDI 2020 - Virtual, Online
Duration: Nov 4 2020Nov 6 2020

Publication series

NameProceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020

Conference

Conference14th USENIX Symposium on Operating Systems Design and Implementation,OSDI 2020
CityVirtual, Online
Period11/4/2011/6/20

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Hardware and Architecture
  • Information Systems

Fingerprint Dive into the research topics of 'Cobra: Making transactional key-value stores verifiably serializable'. Together they form a unique fingerprint.

Cite this