Cobra: Making Transactional Key-Value Stores Verifiably Serializable

1. The problem, as a search problem

What is being checked. A cloud database runs transactions: groups of reads and writes on keys. It promises serializability: there exists one total order of the committed transactions such that running them one at a time in that order produces exactly the results the clients saw (§2.2). The strict variant additionally requires that order to agree with real time. The paper's question: can the clients check that promise while treating the database as a black box, seeing only the requests they sent and the responses they got back (§1)?

Why it is a search. If the database told you, for each key, the order in which its versions were written (Adya's version order), you would build the dependency graph and test it for a cycle. But the version order lives inside the database and is not exposed. So you must ask whether any version order yields an acyclic dependency graph (§2.2). Checking black-box serializability has long been known to be NP-complete (§1).

Why existing exact methods do not scale. Biswas and Enea (BE) lowered the complexity to polynomial time under natural restrictions that hold here, but the number of clients appears in the exponent (e.g., 14 clients means O(n^14)), and BE has no mechanism for a continuous, ever-growing history (§1).

The paper's bet. SAT and SMT solvers routinely "solve" problems whose general form is intractable, so it ought to be possible to verify serializability in many real-world cases (§1). Cobra starts from an SMT solver suited to graph properties (MonoSAT) and adds domain-specific techniques that shrink the search before the solver sees it.

Headline claim. Cobra is the first system that combines (a) black-box checking, of (b) serializability, while (c) scaling to real-world online transactional processing workloads (Abstract, §1, §7).

2. Who checks whom: the setup

• Database: untrusted; its results can be arbitrary. Each client request is one of five operations: start, commit, abort (on transactions), read and write (on keys).
• History collectors: sit between clients and database and record requests and (possibly wrong) responses. The union of their fragments is the history.
• Verifier: pulls fragments and checks serializability in rounds. Each round is a witness search whose input is the previous round's output plus new fragments. It needs the full history of requests and responses. Cobra assumes neither verifier nor collectors crash.
• Clients use sessions; within a session transactions do not overlap (requests block). So a client can be multithreaded but not event-driven.
• Clients, collectors and verifier are in one trust domain, e.g. an enterprise's application servers using a cloud database, or an online game whose user data is in a cloud database. Collectors can be middleboxes at the enterprise edge, or run in an untrusted cloud inside a TEE such as Intel SGX.

Performance requirement. Verifier capacity (transactions/sec) must be at least the database's average offered load over a long interval such as a day, not its peak: being off the critical path, it can catch up.

3. Brute force: the polygraph

The figure in §1 above is a polygraph, the data structure the brute-force approach is built on. Formally, a polygraph P = (V, E, C) is a directed graph (V, E), the known graph, together with a set C of bipaths: pairs of edges ⟨(v, u), (u, w)⟩ with (w, v) ∈ E. Read it as "either u happened after v, or else u happened before w". For a history:

• V = all committed transactions (aborted and ongoing ones are excluded).
• E = {(Ti, Tj) | Tj reads from Ti}, written Ti →wr(x) Tj. These are visible because every written value is unique (Cobra's client library enforces this by embedding a unique id in each write, §2.2, §5).
• C = {⟨(Tj, Tk), (Tk, Ti)⟩ | Ti →wr(x) Tj, Tk writes x, Tk ≠ Ti, Tk ≠ Tj}: every other writer of x goes after the read or before the write.

A graph (V′, E′) is compatible with (V, E, C) if V = V′, E ⊆ E′, and for every ⟨e1, e2⟩ ∈ C exactly one of e1, e2 is in E′. A fact proved in Appendix B of the extended version: there is an acyclic graph compatible with the polygraph of history H iff there is an acyclic serialization graph of H, i.e. iff H is serializable.

Why brute force fails. The search has |C| binary choices, so 2^|C| possibilities, and |C| itself is large: ∑_k∈K r_k · (w_k − 1), where K is the set of keys and r_k, w_k are the numbers of reads and writes of key k. A sum of quadratic terms.

4. Cobra's pipeline

Cobra keeps the brute-force skeleton (known graph + binary constraints + acyclicity) but changes the constraint format. A constraint is now a pair of sets of edges ⟨A, B⟩: meeting it means including all of A and none of B, or vice versa. A graph (V′, E′) is compatible with known graph G = (V, E) and generalized constraints C if V = V′, E ⊆ E′, and for all ⟨A, B⟩ ∈ C: (A ⊆ E′ ∧ B ∩ E′ = ∅) ∨ (A ∩ E′ = ∅ ∧ B ⊆ E′).

Validity (C10). The authors prove (Appendix B of the extended version) that there exists an acyclic graph compatible with the constraints Cobra constructs on a history if and only if the history is serializable. So the shrinking loses nothing.

The three refinements, each motivated by a common workload pattern: combining writes (read-modify-write transactions, §3.1), coalescing constraints (reads outnumber writes, §3.2), and pruning with all-pairs reachability computed on a GPU (§3.3). Then MonoSAT solves what remains (§3.4).

5. Technique 1: combining writes

The pattern. A read-modify-write (RMW) transaction reads a key and then writes it: e.g. read stock count, decrement, write back. If T reads key k from T′ and then writes k, then T's write must come immediately after T′'s write in k's version order. Two RMWs cannot both claim to be the immediate successor of the same write; if they do, Cobra rejects on the spot (Figure 3 lines 20–21: "multiple consecutive writes, not serializable").

Chains. A chain is a sequence of transactions whose writes to a key are consecutive. Cobra starts with every write as a one-element chain (line 32), then for each RMW t and the transaction t′ holding the prior write, concatenates t′'s chain with t's chain (lines 22, 44–51). The uncertainty is now only about the order of chains, not individual writes: in the figure, [W1, W2] → [W3, W4] or [W3, W4] → [W1, W2]. The basic polygraph still considers W3 immediately before W1; Cobra recognizes that as impossible.

Inferred anti-dependencies. If a non-RMW transaction t reads from u, and v is u's successor in the chain, then t must precede v; otherwise t would sit downstream of v and should have read v's value (or later). Cobra adds t → v directly as a known edge (InferRWEdges, line 53). In the brute-force encoding the analogous edges appear as the first component of a constraint; here they are certain.

Constraints between chains. For each pair of chains on a key, Cobra builds one constraint ⟨ES1, ES2⟩. ES1 = edges from the readers of chain_i's tail to chain_j's head (lines 71–72); if the tail has no readers, ES1 is the single edge chain_i.tail → chain_j.head (line 67). ES2 is the same in the other direction (line 62). Pointing from the readers of the tail, rather than from the tail itself, is enough because each reader already has a known edge from the tail.

6. Technique 2: coalescing constraints

Many real-world workloads have far more reads than writes. All three constraints above ask the same question: did W1 or W2 happen first? So Cobra groups all reads of the same write into one constraint. The full version would be ⟨A′, B′⟩ with A′ = {(W1, W2), (R3, W2), (R4, W2)} and B′ = {(W2, W1), (R5, W1)}. Cobra drops (W1, W2) because the known edge (W1, R3) plus (R3, W2) already implies W1 → R3 → W2; likewise it drops (W2, W1) because of the known edge (W2, R5). Result: ⟨A, B⟩ = ⟨{(R3, W2), (R4, W2)}, {(R5, W1)}⟩.

In Figure 3 this is Coalesce (line 60): for every pair of chains on a key, one constraint, regardless of how many readers each chain's tail has.

7. Technique 3: pruning on the GPU

The logic is almost trivial (the paper's word): compute which transaction can reach which in the known graph; then for each constraint ⟨ES1, ES2⟩, if some edge (tx_i, tx_j) in ES1 points backwards along an existing path (tx_j ⇝ tx_i), ES1 is impossible, so add all of ES2 to the known graph and drop the constraint; symmetrically for ES2 (lines 78–84). The interesting part is the design decision to compute reachability on parallel hardware, which works because the computation is iterated Boolean matrix multiplication.

Pruning can run more than once: adding forced edges creates new paths, which may resolve further constraints. The implementation iterates until nothing more is pruned or a configurable maximum number of iterations is reached (to bound the verifier's work). The authors note that a better implementation would stop when the cost of one more iteration exceeds the solver time it saves (§5).

GPU details (§5)

• Algorithm: repeated squaring of the Boolean adjacency matrix while the matrix keeps changing, up to log |V| matrix multiplications. log |V| is the worst case (two nodes connected by a (≥ |V|/2 + 1)-step path); the authors report this does not arise much in their experiments.
• Platform: cuBLAS (dense) and cuSPARSE (sparse) matrix multiplication routines.
• Triangular trick: test the graph for acyclicity, index vertices by a topological sort, which makes the matrix triangular, then call a specialized triangular matrix multiplication routine.
• Sparse to dense switch: start with sparse multiplication; move to dense when density exceeds a threshold, namely "5% of the matrix elements are non-zero", the empirical cross-over point the authors observed.

import numpy as np

def transitive_closure(A):              # A: |V| x |V| 0/1 adjacency matrix
    R = (A + np.eye(len(A), dtype=A.dtype)) > 0
    while True:
        R2 = (R.astype(np.int32) @ R.astype(np.int32)) > 0   # Boolean matmul
        if (R2 == R).all():
            return R                    # R[i, j]: j is reachable from i
        R = R2

8. Solving with MonoSAT

What remains: find an acyclic graph that contains the known graph and satisfies every remaining constraint. Cobra's encoding:

• One Boolean variable E(i,j) per vertex pair: True means the searched-for graph has edge (i, j).
• Every known edge: its variable is set True.
• Every constraint ⟨A, B⟩: ((∀e_a ∈ A, e_a) ∧ (∀e_b ∈ B, ¬e_b)) ∨ ((∀e_a ∈ A, ¬e_a) ∧ (∀e_b ∈ B, e_b)).
• Acyclicity of the graph formed by the True variables: enforced by a primitive the solver provides.

Why not plain SAT. Encoding graph acyclicity as SAT formulas is expensive (a claim by Janota et al., which the authors also observed, §6.1). MonoSAT is an SMT solver that includes SAT modulo monotonic theories and efficiently encodes and checks graph properties such as acyclicity.

Why not drop the solver. In the limit, Cobra could re-implement the solver. The authors' framing of the division of labor: Cobra's preprocessing exploits structure specific to verifying serializability, while the solver exploits residual structure common to many graph problems, and brings many prior optimizations with it.

9. Worked example, end to end added for you

Six transactions on one key x, plus one session-order fact. The example is mine; every step follows Figure 3's line numbers.

1. CreateKnownGraph (lines 7–25). Read-dependency edges: (T1,T2), (T3,T4), (T2,T5), (T1,T6). readfrom: ⟨x,T1⟩ → {T2, T6}, ⟨x,T3⟩ → {T4}, ⟨x,T2⟩ → {T5}. T2 is an RMW reading from T1, so wwpairs[⟨x,T1⟩] = T2 (line 22); no other RMW claims T1, so no reject. Session order adds (T3, T5) (line 24).
2. Initial chains (lines 29–32). chains[x] = {[T1], [T2], [T3]}.
3. CombineWrites (lines 43–51). wwpairs says T2 immediately follows T1: chains[x] = {[T1, T2], [T3]}.
4. InferRWEdges (lines 53–58). In chain [T1, T2], readers of T1 are {T2, T6}; T2 is the successor itself, so only (T6, T2) is added: T6 read 1, so it must precede the write of 2.
5. Coalesce (lines 38–40, 60–73). One pair of chains. ES1 = GenChainToChainEdges([T3], [T1,T2]): readers of tail T3 are {T4}, so ES1 = {(T4, T1)}. ES2 = GenChainToChainEdges([T1,T2], [T3]): readers of tail T2 are {T5}, so ES2 = {(T5, T3)}.
6. Prune (lines 75–85). Is there a path T1 ⇝ T4 (would make ES1 cyclic)? No. Is there a path T3 ⇝ T5 (would make ES2 cyclic)? Yes, the session edge. So ES2 is impossible: add ES1's edge (T4, T1) to the known graph and drop the constraint.
7. Solve. No constraints remain; MonoSAT only has to confirm the known graph is acyclic. It is: one valid serial order is T3, T4, T1, T6, T2, T5. Accept.

Size of the search, compared. Counting the basic polygraph's constraints directly from the definition in §2.3: read-dependency T1→T2 has 1 other writer (T3), and T1→T6, T3→T4, T2→T5 have 2 each, so |C| = 7 and the brute-force space is 2^7 = 128 (derived). After combining and coalescing there is 1 constraint (2 possibilities, derived: 2^1), and after pruning there are 0. (The paper's general expression ∑ r_k(w_k − 1) gives 4 × 2 = 8 here; it counts one more because the definition of C excludes T_k = T_j when the reader T2 also writes x.)

10. Figure 3 in Python

Translation of the paper's pseudocode. Cobra's actual implementation is in Java and CUDA/C++ (Figure 4). Line-for-line with the original; the original line number is the trailing comment. Helpers the pseudocode also leaves abstract (Graph, Reject, add_session_order_edges, transitive_closure, tr.reaches, a transaction's read/write accessors) are assumed. Python mechanics only: reject becomes raise Reject; sets of lists become lists of lists (lists are unhashable); line 78 iterates over a copy because the loop removes from con.

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 = defaultdict(set)     # {(key, tx): {tx}} write -> 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[(rop.key, rop.read_from_tx)].add(tx)         # 15
                                                                  # 16
        # detect RMW (read-modify-write) transactions                # 17
        for key in tx.keys_read & tx.keys_written:                # 18
            rop = tx.read_op(key)                                 # 19
            if wwpairs.get((key, rop.read_from_tx)) is not None:  # 20
                raise 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 = defaultdict(list)      # {key: [chain, ...]}               # 29
    for tx in g.nodes:                                            # 30
        for wrop in tx.writes:                                    # 31
            chains[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 itertools.combinations(chainset, 2):  # 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] is tx1)     # 48
        chain2 = next(c for c in chains[key] if c[0] is 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(0, len(chain) - 1):  # i in [0, len-2]    # 56
                for rtx in readfrom[(key, chain[i])]:             # 57
                    if rtx is not 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[(key, chain_i[-1])]:       # tail has no readers  # 66
        edge_set = {(chain_i[-1], chain_j[0])}                    # 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 (edge_set1, edge_set2) in list(con):                      # 78
        if any(tr.reaches(tx_j, tx_i) for (tx_i, tx_j) in edge_set1):    # 79
            g.edges |= edge_set2                                  # 80
            con.remove((edge_set1, edge_set2))                    # 81
        elif any(tr.reaches(tx_j, tx_i) for (tx_i, tx_j) in edge_set2):  # 82
            g.edges |= edge_set1                                  # 83
            con.remove((edge_set1, edge_set2))                    # 84
    return con, g                                                 # 85

After construct_encoding, Cobra feeds the known graph g and constraints con to the solver (§3.4), which searches for a graph that includes g's edges, meets every constraint, and is acyclic.

11. Strict serializability and clock drift

For the strict variant, Cobra adds real-order edges (capturing the order of transactions that do not overlap in real time) to the known graph, then runs the same algorithm. Timestamps come from the database if it exposes them (e.g. Google Spanner) or from Cobra's collectors. Instead of comparing all pairs (quadratic), Cobra borrows a prior algorithm that materializes the time-precedence partial order in O(n + z) time, where n is the number of transactions and z is the minimum number of real-order edges needed.

Clock drift. Collector clocks may disagree, so Cobra assumes they differ by less than a clock drift threshold (100 ms by default) and adds the threshold to every commit timestamp. Two transactions then get a real-order edge only if one's original commit is earlier than the other's start by at least the threshold; everything within a threshold window counts as concurrent. If clocks actually differ by more than the threshold, Cobra may falsely reject a serializable history.

Why the paper weights the non-strict variant: it is the harder computational problem (real-time edges shrink the search), some databases claim only the non-strict variant or do not specify, and the strict case degenerates toward the non-strict one under heavy concurrency or clock drift, where the techniques of §3.1–§3.3 are needed again.

12. Verifying forever: rounds, fences, garbage collection

Cobra verifies in rounds, for two reasons: new history keeps arriving, and there is a limit to the problem size one solve can handle. Each round reuses the graph g from the previous round (Figure 3, line 5) and adds new nodes and edges. The problem is keeping g bounded: which transactions can be deleted safely?

Why deletion is dangerous (§4.1)

Epochs and fence transactions (§4.2)

• Clients periodically issue a fence transaction: a transaction that reads and writes the single key "EPOCH" (for example, every 20 transactions). Because fences are RMWs on one key, the verifier can chain them (§3.1) and number them: that number is the fence's epoch. Epochs are not rounds; a round includes multiple epochs.
• Why the database cannot just push all fences to the front of its serial order: Cobra relies on preserved session order, a property of practical serializable databases (e.g. PostgreSQL, Azure Cosmos DB, Google Cloud Datastore). For databases without it, clients enforce it, e.g. each transaction in a session does an RMW on a per-session key. The verifier adds session-order edges to the known graph (Figure 3, line 24), so fences are interleaved with the workload.
• A normal transaction between fences with epochs i and j (j ≥ i + 1) in its session gets epoch j − 1. epoch_agree is the largest epoch number seen or surpassed by every session.

Guarantee. For any transaction Ti with epoch ≤ (epoch_agree − 2) and any transaction Tj, including future ones, with epoch ≥ epoch_agree, the known graph contains a path Ti ⇝ Tj. Proof sketch from the paper: Ti ⇝ (the next fence in Ti's session, epoch ≤ epoch_agree − 1) ⇝ (the fence with epoch epoch_agree) ⇝ Tj via session order.

Garbage collection (§4.3)

Cobra deletes a transaction T only if (i) T is superseded: no future transaction can precede T or directly succeed T in the known graph; and (ii) T is not on any potential cycle through constraint edges whose resolution future transactions could affect.

• Frontier: among transactions with epoch ≤ (epoch_agree − 2), those holding the most recent write to each key; the earliest transactions a future transaction could still read.
• Superseded: T is not in the frontier, T has epoch ≤ (epoch_agree − 2), and every T′ with a path to T also has epoch ≤ (epoch_agree − 2). (The last condition is not implied by the second: the Guarantee does not cover epochs that differ by one.)
• Superseded is not disposable. The paper's example: old transactions T1 = W1(d) W1(a), T2 = W2(d) W2(a), T3 = R3(a) W3(b) (superseded), T4 = W4(b) W4(c), T5 = R5(b) W5(c), T6 = W6(b); future T7 = R7(d), T8 = R8(c). T8 reading c from T5 resolves a key-b constraint to T4 → T3; T7 reading d resolves a key-a constraint to T3 → T1; together they form the cycle T1 ⇝ T4 → T3 → T1. Deleting T3 would hide it. Future transactions can resolve constraints among old ones.
• Procedure. Clone g into g′, add both edge sets of every constraint to g′, and delete a superseded T only if it lies on no cycle in g′, or only on cycles made entirely of superseded transactions. Appendix C of the extended version argues this meets (i) and (ii).

13. Implementation

• The client library wraps JDBC, the Google Datastore library, and RocksJava. It enforces unique written values (adds a unique id to writes, strips it from reads), issues fence transactions, and implements history collection by writing operations to disk before sending them to the database. The authors note a better implementation would put collection in a proxy.
• Pruning iteration and GPU acceleration: see section 7.
• On a violation, the verifier outputs a certificate: a cycle in the known graph, or a set of unsatisfiable clauses from MonoSAT.

14. Evaluation

Three questions: the verifier's costs and limits versus baselines; its sustainable round-to-round capacity; and its overhead on clients, storage and network.

Setup

• Benchmarks. TPC-C (one warehouse, 10 districts, 30k customers; new order 45%, payment 43%, order status 4%, delivery 4%, stock level 4%). C-Twitter (1000 users; Zipfian follow/unfollow, α = 100). C-RUBiS (eBay-like bidding; 20k users, 200k items). BlindW (10k keys; read-only and write-only transactions of eight operations each; variants RM = 90% read-only, RW = even split, WM = 90% write-only). Blind writes are the fundamental source of uncertainty in constraints.
• Databases. Google Cloud Datastore (over the wide-area Internet), RocksDB (same process as clients), PostgreSQL (local 1 Gbps network; Cobra translates SQL to key-value operations). One client starts one session.
• Verifier hardware. Amazon EC2 p3.2xlarge: NVIDIA Tesla V100 GPU, 8-core CPU, 64GB memory.
• Baselines. nonSAT (Biswas and Enea's Rust implementation); MiniSAT-BE (BE's SAT encoding on MiniSAT); MonoSAT-polygraph (the §2.3 polygraph fed directly to MonoSAT, i.e. Cobra without its techniques); Z3-arith (linear-arithmetic encoding: each node gets an integer index, O(|V|^2) constraints, Z3 default configuration). All use session-order edges. For TPC-C only, a special-case baseline matches Cobra, because TPC-C has only RMW transactions and the whole history coalesces into one chain.

One-shot verification (§6.1)

C2, C3: what "10×" measures. Cobra's core (single-round) verification improves on baselines by 10× in the problem size it can handle for a given time budget, i.e. in verification cost. This is not a throughput figure. Example: Cobra finishes checking 10k transactions in 14 seconds, whereas baselines can handle only 1k or less in the same time budget (§1, §6.4).

C5: real bugs. Cobra detects all five serializability violations collected from real systems' bug reports, in reasonable time:

From Figure 6. * The bug report contains only a small fragment of the history. #Txns is the size of the violation history; Time is Cobra's runtime to detect it.

C6: strict serializability under clock drift. Eight clients run BlindW-RW on 1k keys for one second at 2k transaction/sec, issuing 20 transactions every 10ms; 2,000 transactions in total; clock drift threshold up to 100 ms. Cobra outperforms the baselines (MonoSAT-polygraph and Z3-arith) by 45× and 107× in verification time.

Scaling (§6.2)

Verification capacity for a workload = max over round size #tx_r of (#tx_r / t_r), where t_r is the average time for one round. Setup: RocksDB, 24 concurrent clients, a fence every 20 transactions, a 100k-transaction history generated ahead of time.

C7. Best capacity is 2.3k txn/sec for BlindW-RM (at #tx_r = 5k) and 1.2k txn/sec for C-RUBiS (at #tx_r = 2.5k). C-Twitter and TPC-C are similar (not depicted). Too-small rounds leave too little to garbage-collect, so work from prior rounds is re-analyzed; too-large rounds hit the superlinear growth of verification time.

Out of memory. On BlindW-RW and BlindW-WM, history eventually exceeds GPU memory: blind writes cannot benefit from combining writes, so many constraints remain, transactions stay involved in uncertain constraints, and they cannot be collected.

Fence frequency trade-off. More frequent fences give smaller epochs, earlier garbage collection, smaller and easier per-round problems (fences add ordering), so higher verifier throughput; but they cost peak client throughput. If client load is constant, choose the frequency where verifier throughput equals client offered load.

Online overheads (§6.3)

Baseline: the legacy system (unmodified database library, no history recording). Up to 256 clients to saturate each database.

C8 (C-Twitter).

• 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.

C9: network and storage per 1k transactions (Figure 13). Overhead comes from fence transactions and the metadata (transaction ids and write ids) added by the client library. Network overhead is 2.17%–7.28% of traffic across the four workloads.

Summary (§6.4)

C4. Sustainable verification throughput of 2k txn/sec on the workloads tested ("2000 transactions/sec, equivalent to 170M/day"). The requirement is to match the database's average load (§2.1). For comparison the paper cites Apple Pay at 33M txn/day and Visa at 150M txn/day, noting that a payment "transaction" may be several database transactions, so the comparison is inexact.

15. Related work and discussion

• Black box + serializability. Biswas and Enea (compared in §6); Sinha et al. (SMT search over interleavings of a concurrent program); Gretchen (an experimental checker of non-strict serializability on Cobra-style histories, constraint encoding solved with fzn-gecode).
• Elle (part of Jepsen) has found many isolation bugs. In one mode it checks Adya serializability but needs workloads that reveal the version order (e.g. list appends), which is not black box in the paper's sense. In its other mode it works on arbitrary key-value observations with heuristics that are useful but not comprehensive, e.g. a cycle through anti-dependencies among concurrent transactions is not detected.
• Consistency checking (linearizability, sequential consistency, eventual consistency) is an analogous search for a total order; prior cloud-storage checkers rely on extra ordering information such as synchronized clocks, client-to-client communication, or a sequencing gateway. Cobra neither modifies the database nor depends on external synchronization; its epochs are for scaling, not core to verification.
• Execution integrity (BFT, TEEs, Verena, Orochi, AVM, Ripley, cryptographic systems): TEEs ensure the right code runs, not that the code is right; end-to-end systems are not black box. Obladi pays 1-2 orders of magnitude overhead in throughput and latency.
• Testing (Jepsen and others): complementary; Cobra uses several Jepsen traces in Figure 6.

Who would use it (§8). The §2.1 scenarios, or as the checker in a testing framework such as Jepsen, injecting faults into OS, storage or network without instrumenting the database. The verifier must match the database only in long-term average transactions/sec; it does different work per transaction (the database handles geo-replication, concurrency control, durability and more; the verifier is a single machine and purely algorithmic). Given a certificate, a user could supply a candidate serialization order to enable roll back and replay.

Future work named by the authors. Fault tolerance for verifier and collectors (even partial histories give meaningful results: a cycle in a partial history is a violation of the full history); other isolation levels; native range queries and operators like sum and join; more aggressive garbage collection, e.g. letting the verifier query the database to resolve constraints; and whether real-world workloads ever trigger the exponential worst case. Their intuition: low contention per key yields few constraints, and high contention with enough reads imposes more ordering.

After publication: not part of the paper

Snapshot dated 2026-09-30, 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 when compiling this version, so it is reproduced as given and 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

Black-box checking of transactional isolation became an active line of work after 2020. The entries below cite Cobra and build on it directly: they reuse its techniques, extend it, or use it as the baseline. 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

Ledger items included

• Claims: all of C1–C12. C1 (§1 of this version), C2 and C3 (section 14, with the explicit note that 10× is verification cost / problem size for a time budget, not throughput), C4 (section 14 summary), C5 (Figure 6 table), C6, C7, C8, C9 (section 14), C10 (sections 3–4), C11 (sections 4–8, 12), C12 (section 13 table).
• Limitations: all of L1–L8, in the Limitations box.

Ledger items omitted

• None. Parts of Part D outside the ledger were shortened rather than dropped: related work (§7) is condensed to one list; benchmark and machine details for the client side (§6 setup: client and PostgreSQL machine specs) are omitted as not needed to understand the algorithm; the reference list and acknowledgments are omitted (the links to the published paper and extended version carry them). Plots in Figures 5 and 7–12 are described without data because their values are not in the source.

Additions (mine, not the authors')

• Bridges: version order as a latent variable (section 1); hypothesis-space framing of 2^|C| (section 3); SMT-as-SAT-plus-theory explanation of MonoSAT (section 8); the remark that the pruning hot loop is a matmul (section 7).
• Glossary of database terms (section 1), rephrasing §2.1–§2.2 definitions.
• Worked example (section 9): a six-transaction history I constructed, traced through Figure 3, with derived counts 2^7 = 128 and 2^1 = 2, and a note on why the paper's ∑ r_k(w_k − 1) gives 8 rather than 7 there.
• Translated code: Figure 3 in Python, line-aligned (section 10); a NumPy transitive-closure sketch that is explicitly not Cobra's code (section 7).
• Redrawn diagrams from Part D descriptions: polygraph example, Figure 1, Figure 2, combining-writes, coalescing, pruning, and unsafe-deletion figures. In the combining-writes figure, the specific chain-to-chain edges (T2, T3) and (T4, T1) are derived by me from Figure 3.
• New diagrams: the two-option orientation panel (section 1), the Boolean-matrix-squaring grids (section 7), the worked-example graph (section 9), and the fence/epoch schematic with its epoch_agree = 5 illustration (section 12).
• Questions for the reader: the variant of the worked example with an extra session edge (section 9) and the "hardest workload" question (section 14).
• The table and contents layout, and section ordering (search problem first) chosen for this reader.