Cobra: Making Transactional Key-Value Stores Verifiably Serializable

1. The problem: can you trust a database you cannot see inside?

(from Abstract, §1, §2.1)

db = {"apples_in_stock": 5, "alice_balance": 100, "bob_balance": 20}

# one transaction
a = db["alice_balance"]          # read
b = db["bob_balance"]            # read
db["alice_balance"] = a - 10     # write
db["bob_balance"]   = b + 10     # write

Many modern cloud databases (the paper names Amazon DynamoDB and Aurora, Azure CosmosDB, CockroachDB, YugaByte DB and others) promise serializability. The paper calls it the "gold-standard" correctness property: lots of application code would be wrong if the database gave a weaker guarantee.

But these databases are black boxes. They are run by someone else, on someone else's machines. Bugs, misconfiguration, or operator mistakes inside them could break the promise, and real production systems have broken it. So the paper asks: can the customers check, from the outside only, that the database really kept its promise?

Cobra is the authors' answer. It records every request sent to the database and every answer that comes back (the history), and a separate verifier checks whether that history could have come from some one-at-a-time order. The paper says Cobra is the first system that combines (a) black-box checking, of (b) serializability, while (c) scaling to real-world online transactional processing workloads.

2. What "serializable" means, with a worked example

(from §2.2–§2.3)

Here is the hard part. From outside, you often do not know some of the arrows. The paper's own small example has three transactions on one key x:

T3 read the value 1, so T1 came before T3 (a solid, known arrow). T2 also wrote x. T2 cannot sit between T1 and T3, or T3 would have read 2. So either T2 came after T3, or T2 came before T1. Which one is true is unknown.

The paper calls this structure a polygraph: the arrows you know form the known graph, and each "one of these two" choice is a constraint. The history is serializable if and only if you can pick one option from every constraint so that the whole graph has no cycle. (This "if and only if" is proved in the extended version, Appendix B.)

3. Cobra's core idea: shrink the puzzle, then hand it to a solver

(from §1, §3, §3.1–§3.4, Figure 2)

The authors' starting intuition: although the problem is hard in general, modern solvers (programs that search for an assignment satisfying many logical conditions) often handle real-world cases well. Cobra uses one called MonoSAT, which is good at graph questions such as "is there a cycle?" On its own, though, MonoSAT is still too slow on the brute-force puzzle. So Cobra first shrinks the puzzle with three tricks that use patterns common in real programs:

Trick 1: combining writes (§3.1)

n = db["apples_in_stock"]       # read
db["apples_in_stock"] = n - 1   # write back

Cobra glues such writes into chains: ordered lists of writes to one key that must be consecutive. Then it only has to decide the order of whole chains, not of every single write. With two chains [W1, W2] and [W3, W4], only two orders remain: [W1, W2] before [W3, W4], or the reverse.

Trick 2: coalescing constraints (§3.2)

In most real workloads there are far more reads than writes. Many constraints end up asking the same underlying question, such as "did write W1 or write W2 happen first?" Cobra merges all those constraints into one bigger either/or choice between two groups of arrows, so the solver makes one decision instead of many.

Trick 3: pruning (§3.3)

If the known arrows already give a path from W2 to R3, then choosing "R3 before W2" would close a loop. That option is impossible, so Cobra settles the constraint without the solver and adds the other option to the known graph. To do this quickly, Cobra needs to know, for every pair of transactions, whether one can reach the other along known arrows. That computation can be done as repeated matrix multiplication, which is exactly what graphics cards (GPUs) are good at, so Cobra runs it on a GPU.

Step 4: solving (§3.4)

Whatever is left goes to MonoSAT, which searches for one choice per constraint that leaves no cycle. If it finds one, the history is accepted. If not (or if Cobra already found a cycle among the known arrows), the history is rejected, and Cobra outputs the problematic transactions as evidence (§5).

The authors prove that this shrunken puzzle is still faithful: an acyclic graph compatible with Cobra's constraints exists if and only if the history is serializable (§3; proof in Appendix B of the extended version).

4. Checking forever: rounds, epochs, and fence transactions

(from §1, §4)

A real database runs all day, so the history never stops growing. Cobra checks it in rounds, each round handling a new piece of history. The catch: in a serializable database, a transaction today could legally read a value written long ago, so the verifier cannot simply forget old transactions; doing so could hide a cycle.

Cobra's fix: every client periodically (for example, every 20 transactions) runs a tiny fence transaction that reads and writes a special key named "EPOCH". Fences divide history into epochs, and they let the verifier prove that sufficiently old transactions are always "before" all future ones. The verifier tracks the frontier (the latest writes that future transactions could still read) and marks older transactions as superseded. Even a superseded transaction is deleted only if it cannot be part of a cycle that future transactions might complete. This garbage collection keeps each round's problem small.

5. What the authors showed

(from §1, §5, §6, Figures 6, 9, 10, 12, 13)

Catching real bugs (Figure 6)

The authors downloaded histories from public bug reports of three real databases, each known to contain a serializability violation, and fed them to Cobra. It found all five.

Speed compared with other checkers (Figure 5, Figure 9)

The paper's Figure 5 plots verification time (seconds, 0–14, lower is better) against number of transactions (0–10k) for Cobra and four baseline checkers on one benchmark. Cobra's line is lowest, and time grows faster than linearly as the history grows. The exact plotted values are not reproduced here; see the published PDF.

For strict serializability (a stricter version where the order must also respect real clock time), on 2,000 transactions with a clock drift threshold of 100 ms, Cobra beat the baselines by 45× and 107× in verification time.

Keeping up over time (Figure 10)

Running round after round, the best verification capacity was 2.3k txn/sec for one test workload (BlindW-RM, at 5k transactions per round) and 1.2k txn/sec for an eBay-like auction workload (C-RUBiS, at 2.5k per round). The paper's headline 2k txn/sec corresponds to 170M per day. For comparison the paper cites Apple Pay at 33M txn/day and Visa at 150M txn/day, while noting that a "transaction" there means something slightly different, so the comparison is inexact. The verifier only needs to match the database's average load, not its peak, because it works in the background and can catch up.

Cost to the people using the database (Figures 12, 13)

• RocksDB: 90th-percentile latency (waiting time) rose 2×, with a 50% throughput penalty, which the authors attribute to recording history on the same disk the database uses.
• PostgreSQL: minor overhead.
• Google Datastore: a throughput penalty, reflecting the service's limit on operations per second plus the extra operations from fence transactions.
• Network: the extra traffic was 2.17%–7.28% across the four workloads measured.

def construct_encoding(history):                                  # 1
    g, readfrom, wwpairs = create_known_graph(history)            # 2
    con = gen_constraints(g, readfrom, wwpairs)                   # 3
    con, g = prune(con, g)       # §3.3, executed one or more times  # 4
    return con, g                                                 # 5
                                                                  # 6
def create_known_graph(history):                                  # 7
    g = Graph()                  # the known graph                # 8
    wwpairs = {}     # {(key, tx): tx}  consecutive writes        # 9
    readfrom = {}    # {(key, tx): set of tx}  maps a write to its readers  # 10
    for tx in history:                                            # 11
        g.nodes.add(tx)                                           # 12
        for rop in tx.reads:                                      # 13
            g.edges.add((rop.read_from_tx, tx))   # read-dependencies  # 14
            readfrom.setdefault((rop.key, rop.read_from_tx), set()).add(tx)  # 15
                                                                  # 16
        # detect RMW (read-modify-write) transactions             # 17
        for key in tx.keys_both_read_and_written():               # 18
            rop = tx.read_of(key)                                 # 19
            if wwpairs.get((key, rop.read_from_tx)) is not None:  # 20
                reject()   # multiple consecutive writes, not serializable  # 21
            wwpairs[(key, rop.read_from_tx)] = tx                 # 22
                                                                  # 23
    add_session_order_edges(g)   # §4.2                           # 24
    return g, readfrom, wwpairs                                   # 25
                                                                  # 26
def gen_constraints(g, readfrom, wwpairs):                        # 27
    # each key maps to set of chains; each chain is an ordered list  # 28
    chains = {}      # {key: list of chains}                      # 29
    for tx in g.nodes:                                            # 30
        for wrop in tx.writes:                                    # 31
            chains.setdefault(wrop.key, []).append([tx])  # one-element list  # 32
                                                                  # 33
    combine_writes(chains, wwpairs)        # §3.1                 # 34
    infer_rw_edges(chains, readfrom, g)    # infer anti-dependency  # 35
                                                                  # 36
    con = []                                                      # 37
    for key, chainset in chains.items():                          # 38
        for chain_i, chain_j in all_pairs(chainset):              # 39
            con.append(coalesce(chain_i, chain_j, key, readfrom))  # §3.2  # 40
                                                                  # 41
    return con                                                    # 42
def combine_writes(chains, wwpairs):                              # 43
    for (key, tx1), tx2 in wwpairs.items():                       # 44
        # By construction of wwpairs, tx1 is the write immediately  # 45
        # preceding tx2 on key. Thus, we can sequence all writes  # 46
        # prior to tx1 before all writes after tx2, as follows:   # 47
        chain1 = next(c for c in chains[key] if c[-1] == tx1)     # 48
        chain2 = next(c for c in chains[key] if c[0] == tx2)      # 49
        chains[key].remove(chain1); chains[key].remove(chain2)    # 50
        chains[key].append(chain1 + chain2)                       # 51
                                                                  # 52
def infer_rw_edges(chains, readfrom, g):                          # 53
    for key, chainset in chains.items():                          # 54
        for chain in chainset:                                    # 55
            for i in range(len(chain) - 1):   # i in [0, len(chain)-2]  # 56
                for rtx in readfrom.get((key, chain[i]), set()):  # 57
                    if rtx != chain[i + 1]: g.edges.add((rtx, chain[i + 1]))  # 58
                                                                  # 59
def coalesce(chain1, chain2, key, readfrom):                      # 60
    edge_set1 = gen_chain_to_chain_edges(chain1, chain2, key, readfrom)  # 61
    edge_set2 = gen_chain_to_chain_edges(chain2, chain1, key, readfrom)  # 62
    return (edge_set1, edge_set2)                                 # 63
                                                                  # 64
def gen_chain_to_chain_edges(chain_i, chain_j, key, readfrom):    # 65
    if not readfrom.get((key, chain_i[-1])):     # tail has no readers  # 66
        edge_set = {(chain_i[-1], chain_j[0])}   # tail -> head   # 67
        return edge_set                                           # 68
                                                                  # 69
    edge_set = set()                                              # 70
    for rtx in readfrom[(key, chain_i[-1])]:                      # 71
        edge_set.add((rtx, chain_j[0]))                           # 72
    return edge_set                                               # 73
                                                                  # 74
def prune(con, g):                                                # 75
    # tr is the transitive closure (reachability of every two nodes) of g  # 76
    tr = transitive_closure(g)   # standard algorithm; see [70, Ch.25]  # 77
    for c in list(con):          # c = (edge_set1, edge_set2)     # 78
        if any(tr.reaches(tx_j, tx_i) for (tx_i, tx_j) in c[0]):  # 79
            g.edges |= c[1]                                       # 80
            con.remove(c)                                         # 81
        elif any(tr.reaches(tx_j, tx_i) for (tx_i, tx_j) in c[1]):  # 82
            g.edges |= c[0]                                       # 83
            con.remove(c)                                         # 84
    return con, g                                                 # 85