Cobra: Making Transactional Key-Value Stores Verifiably Serializable

1. The one-picture version

Cloud databases (the paper names Amazon DynamoDB and Aurora, Azure CosmosDB, CockroachDB, YugaByte DB, and others) offer serializable transactions: all transactions appear to execute in a single, sequential order. Your application code probably relies on that. But you cannot see inside a hosted database, and production systems have exhibited serializability violations.

Cobra lets the client side check. History collectors record every request your clients send and every response the database returns. A verifier, running on your own hardware in the background, decides whether that history could have come from some serial order. The database is unmodified and does not know it is being checked.

The paper's headline claim (C1): Cobra is the first system that combines (a) black-box checking, of (b) serializability, while (c) scaling to real-world online transactional processing workloads.

Each client request is one of five operations: start, commit, abort, read(key), write(key). The paper's word for "database" always means a transactional key-value store.

2. How it checks: one worked example

What the example says. T3 read x from T1, so T1 comes before T3: that edge is known. T2 also wrote x, so T2 cannot fall between T1 and T3 (otherwise T3 would have read 2). So either T2 comes after T3, or T2 comes before T1. The history does not say which. The paper calls this pair a constraint; the graph of certain edges is the known graph; together they form a polygraph.

The check. The history is serializable if you can pick one option from every constraint and end up with a graph that has no cycle (a cycle would mean "A before B before A"). If every combination of choices creates a cycle, there is no valid serial order and the verifier rejects. The paper proves this encoding is exact (C10): an acyclic graph compatible with Cobra's constraints exists if and only if the history is serializable. On a reject, Cobra produces a certificate: a cycle in the known graph, or a set of unsatisfiable clauses from the solver (§5).

Why this is hard. Each constraint is a binary choice, so brute force faces 2^|C| possibilities, and real histories have many constraints. Checking black-box serializability is NP-complete.

How Cobra makes it tractable (C11). It shrinks the search before handing it to MonoSAT, an SMT solver suited to graph properties such as acyclicity:

• Combining writes exploits read-modify-write transactions. The paper's example is shopping: read the stock count, decrement it, write it back. A read-modify-write pins its write right after the write it read, so writes join into ordered chains, and the solver only orders whole chains.
• Coalescing constraints exploits reads outnumbering writes: all reads of the same write are grouped into one constraint instead of one per read.
• Pruning computes, on a GPU, which transactions can already reach which (transitive closure). Any option that would close a cycle with an existing path is discarded, and the other option is fixed.

/* 1*/ Encoding constructEncoding(History history) {
/* 2*/   Known k = createKnownGraph(history); Graph g = k.g;
/* 3*/   Set<Constraint> con = genConstraints(g, k.readfrom, k.wwpairs);
/* 4*/   Encoding e = prune(con, g); con = e.con; g = e.g;      // §3.3, executed one or more times
/* 5*/   return new Encoding(con, g);
/* 6*/ }
/* 7*/ Known createKnownGraph(History history) {
/* 8*/   Graph g = new Graph();                                    // the known graph
/* 9*/   Map<Pair<Key, Tx>, Tx> wwpairs = new HashMap<>();         // consecutive writes
/*10*/   Map<Pair<Key, Tx>, Set<Tx>> readfrom = new HashMap<>();   // maps a write to its readers
/*11*/   for (Tx tx : history) {
/*12*/     g.nodes.add(tx);
/*13*/     for (ReadOp rop : tx.reads()) {
/*14*/       g.edges.add(new Edge(rop.readFromTx, tx));            // read-dependencies
/*15*/       readfrom.computeIfAbsent(Pair.of(rop.key, rop.readFromTx), x -> new HashSet<>()).add(tx); }
/*16*/
/*17*/     // detect RMW (read-modify-write) transactions
/*18*/     for (Key key : tx.keysBothReadAndWritten()) {
/*19*/       ReadOp rop = tx.readOf(key);
/*20*/       if (wwpairs.get(Pair.of(key, rop.readFromTx)) != null)
/*21*/         reject();   // multiple consecutive writes, not serializable
/*22*/       wwpairs.put(Pair.of(key, rop.readFromTx), tx); }
/*23*/   }
/*24*/   g.addSessionOrderEdges();                                 // §4.2
/*25*/   return new Known(g, readfrom, wwpairs);
/*26*/ }
/*27*/ Set<Constraint> genConstraints(Graph g, ReadFromMap readfrom, WWPairs wwpairs) {
/*28*/   // each key maps to set of chains; each chain is an ordered list
/*29*/   Map<Key, Set<List<Tx>>> chains = new HashMap<>();
/*30*/   for (Tx tx : g.nodes)
/*31*/     for (WriteOp wrop : tx.writes())
/*32*/       chains.computeIfAbsent(wrop.key, x -> new HashSet<>()).add(List.of(tx)); // one-element list
/*33*/
/*34*/   combineWrites(chains, wwpairs);       // §3.1
/*35*/   inferRWEdges(chains, readfrom, g);    // infer anti-dependency
/*36*/
/*37*/   Set<Constraint> con = new HashSet<>();
/*38*/   for (var ent : chains.entrySet()) { Key key = ent.getKey(); Set<List<Tx>> chainset = ent.getValue();
/*39*/     for (Pair<List<Tx>, List<Tx>> p : everyPair(chainset))
/*40*/       con.add(coalesce(p.first, p.second, key, readfrom)); }   // §3.2
/*41*/
/*42*/   return con; }
/*43*/ void combineWrites(Map<Key, Set<List<Tx>>> chains, WWPairs wwpairs) {
/*44*/   for (var ent : wwpairs.entrySet()) { Key key = ent.getKey().first; Tx tx1 = ent.getKey().second; Tx tx2 = ent.getValue();
/*45*/     // By construction of wwpairs, tx1 is the write immediately
/*46*/     // preceding tx2 on key. Thus, we can sequence all writes
/*47*/     // prior to tx1 before all writes after tx2, as follows:
/*48*/     List<Tx> chain1 = listWhoseLastElemIs(chains.get(key), tx1);
/*49*/     List<Tx> chain2 = listWhoseFirstElemIs(chains.get(key), tx2);
/*50*/     chains.get(key).removeAll(Set.of(chain1, chain2));
/*51*/     chains.get(key).add(concat(chain1, chain2)); }
/*52*/ }
/*53*/ void inferRWEdges(Map<Key, Set<List<Tx>>> chains, ReadFromMap readfrom, Graph g) {
/*54*/   for (var ent : chains.entrySet()) { Key key = ent.getKey(); Set<List<Tx>> chainset = ent.getValue();
/*55*/     for (List<Tx> chain : chainset)
/*56*/       for (int i = 0; i <= chain.size() - 2; i++)
/*57*/         for (Tx rtx : readfrom.getOrDefault(Pair.of(key, chain.get(i)), Set.of()))
/*58*/           if (rtx != chain.get(i + 1)) g.edges.add(new Edge(rtx, chain.get(i + 1))); }
/*59*/ }
/*60*/ Constraint coalesce(List<Tx> chain1, List<Tx> chain2, Key key, ReadFromMap readfrom) {
/*61*/   Set<Edge> edgeSet1 = genChainToChainEdges(chain1, chain2, key, readfrom);
/*62*/   Set<Edge> edgeSet2 = genChainToChainEdges(chain2, chain1, key, readfrom);
/*63*/   return new Constraint(edgeSet1, edgeSet2);
/*64*/ }
/*65*/ Set<Edge> genChainToChainEdges(List<Tx> chainI, List<Tx> chainJ, Key key, ReadFromMap readfrom) {
/*66*/   if (readfrom.getOrDefault(Pair.of(key, tail(chainI)), Set.of()).isEmpty()) {
/*67*/     Set<Edge> edgeSet = Set.of(new Edge(tail(chainI), head(chainJ)));
/*68*/     return edgeSet; }
/*69*/
/*70*/   Set<Edge> edgeSet = new HashSet<>();
/*71*/   for (Tx rtx : readfrom.get(Pair.of(key, tail(chainI))))
/*72*/     edgeSet.add(new Edge(rtx, head(chainJ)));
/*73*/   return edgeSet;
/*74*/ }
/*75*/ Encoding prune(Set<Constraint> con, Graph g) {
/*76*/   // tr is the transitive closure (reachability of every two nodes) of g
/*77*/   Reachability tr = transitiveClosure(g);   // standard algorithm; see [70, Ch.25]
/*78*/   for (Iterator<Constraint> it = con.iterator(); it.hasNext(); ) { Constraint c = it.next();
/*79*/     if (c.edgeSet1.stream().anyMatch(ed -> tr.reaches(ed.to, ed.from))) {
/*80*/       g.edges.addAll(c.edgeSet2);
/*81*/       it.remove(); }                                          // con −= c
/*82*/     else if (c.edgeSet2.stream().anyMatch(ed -> tr.reaches(ed.to, ed.from))) {
/*83*/       g.edges.addAll(c.edgeSet1);
/*84*/       it.remove(); } }                                        // con −= c
/*85*/   return new Encoding(con, g); }

3. Running it continuously next to production

A real service never stops, so the history grows forever. Cobra verifies in rounds, each covering a portion of the history. The catch: under serializability a future transaction may legally read an old value, so the verifier cannot simply forget old transactions.

The fix: each client periodically issues a fence transaction (for example, every 20 transactions), a read-modify-write of a dedicated key named "EPOCH". Fences divide history into epochs. Because practical serializable databases preserve session order (the paper names PostgreSQL, Azure Cosmos DB, and Google Cloud Datastore), fences cannot all be pushed to the start of the serial order. That lets the verifier prove that sufficiently old transactions are superseded (no future transaction can read them; the boundary is the frontier) and, when a further safety check passes, delete them.

Sizing. The verifier's capacity must be at least the database's average load over a long interval, such as a day, not its peak: it is off the critical path and can catch up. More frequent fences make the verifier faster but cost peak client throughput.

4. The numbers

Scale comparison, with the paper's own caveat. The paper compares 170M/day with Apple Pay at 33M txn/day and Visa at 150M txn/day, and notes that a payment "transaction" might translate to several database transactions, so the comparison is inexact.

Detecting real bugs

What it costs your clients

Measured on the C-Twitter benchmark against the unmodified client library, e.g. plain JDBC (C8, Figure 12):

• RocksDB: 90th-percentile latency rises 2×, with a 50% throughput penalty, attributed to history collection (disk bandwidth contention between clients and the database).
• PostgreSQL: minor overhead.
• Google Datastore: a throughput penalty, reflecting the service's ceiling on operations per second plus the extra operations from fence transactions.

The latency-vs-throughput curves themselves (Figure 12) and the runtime plots (Figures 5, 7–11) are not reproduced in the source; see the published PDF.

What it is made of (C12, Figure 4)

The client library is Java and wraps JDBC, the Google Datastore library, and RocksJava. It adds a unique id to each write (and strips it on reads), issues fence transactions, and records history to disk. The verifier ran on a p3.2xlarge Amazon EC2 instance with an NVIDIA Tesla V100 GPU.

5. Should your team care?

What you get, per the paper: detection, not prevention. On a violation, the verifier hands you a certificate naming the problematic transactions (§5). The authors also note that Cobra could be used as the checker inside a testing framework such as Jepsen (§8).

After publication: not part of the paper

Snapshot dated 2026-09-30, reproduced as given in the source file. It was compiled by the blog's editor (an AI assistant working for the first author) and checked against each paper's own page; it is not peer-reviewed and was not written by the paper's authors. I did not browse the web for this version, so it may be out of date.

Who cites this paper

• 72 citations according to Semantic Scholar, checked 2026-09-30. Other indexes (e.g. Google Scholar) usually report more. A second source could not be checked on that date.
• No primary source documents industrial adoption of Cobra itself. Jepsen, the most widely used database-testing framework, uses its own checker, Elle.

Work that builds on it

Each relation is stated as that paper reports it.

State of the art, in one paragraph

Defining isolation levels is largely settled; checking them efficiently is the active problem. Checking serializability and snapshot isolation on a black box is NP-complete in general. Since Cobra, the field has escaped that hardness by three routes: assuming more about the system (timestamps or version certificates from the database); restricting the workload (e.g. mini-transactions); and improving the solver and the encoding. Reported speedups over the previous generation are now one to three orders of magnitude. The weak isolation levels have sound and complete checkers. The open edge is real SQL: with predicates, even cheap levels become hard, and a black-box checker for a genuine SQL workload does not quite exist yet. A maintained comparison of checkers is at naizhengtan.github.io/pages/isolation-checker-matrix.html.

Faithfulness note