Cobra: Making Transactional Key-Value Stores Verifiably Serializable

1. How this version is arranged

2. The decision problem (from Abstract, §1, §2.1–§2.2)

Setting. Cobra checks a transactional key-value store (the paper calls this "the database") that claims to provide serializability: all transactions appear to execute in a single, sequential order. The database is an untrusted black box, typically a cloud service. Clients talk to it through a client library; one or more history collectors record every request and every (possibly wrong) response; a verifier reads the collected history and outputs accept or reject. Clients, collectors, and verifier share one trust domain; the database is outside it (Figure 1). The verifier is off the critical path but must keep up with the database's average load, not its peak.

Each client request is one of five operations: start, commit, abort (on transactions), and read and write (on keys). Clients issue operations through sessions; within a session, transactions do not overlap, because requests block. A client may therefore be multithreaded but not event-driven.

Formal framework. The paper works in Adya's framework. Two assumptions make reads attributable: each write creates a unique version for its key, and each transaction reads and writes a given key at most once. So every read can be associated with the transaction whose write it observed. Cobra's client library discharges the uniqueness assumption by embedding a unique id in each write and stripping it on read (§5).

A history is a set of operations. In Adya's formalism it also carries a version order: for each key, a total order on committed versions. The version order lives inside the database and is not externally visible; Cobra's history, collected outside the database, does not contain it.

A history induces read-dependencies: T_i → T_j when T_j reads the value T_i wrote. Adding a version order induces two more kinds: write-dependency (T_i writes a key and T_j overwrites it) and anti-dependency (T_i reads a value that T_j overwrites). The serialization graph of a history and a version order has all committed transactions as vertices and all three kinds of dependency as edges. Aborted and ongoing transactions are excluded.

The core fact and the core problem. A history H is serializable iff there exists a version order such that the serialization graph arising from H and that version order is acyclic. So the problem is: find such a version order and acyclic graph, or show none exists. If the database revealed its version order, this would be a single acyclicity test. Without it, one must in effect quantify over all version orders.

Strict variant. A history is strictly serializable if, in addition, the total order respects real time: if T_i commits before T_j starts, T_i precedes T_j. The paper treats both variants but weights the non-strict one, because it is the harder computational problem: real-time edges shrink the space of candidate schedules. The strict case can degenerate into the non-strict one under heavy concurrency or clock drift (§3.5).

Complexity. Checking black-box serializability is NP-complete. Biswas and Enea (BE) lowered it 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¹⁴)), and BE has no mechanism for a continuous, ever-growing history.

What Cobra claims. Cobra is the first system that combines (a) black-box checking, of (b) serializability, while (c) scaling to real-world online transactional processing workloads. Its bet is that SAT/SMT heuristics make the intractable general problem tractable on real workloads, given a good encoding and preprocessing.

3. Brute force: polygraphs (from §2.3)

A polygraph P = (V, E, C) is a directed graph (V, E), the known graph, together with a set C of constraints (bipaths): pairs of edges, not necessarily in E, of the form ⟨(v, u), (u, w)⟩ with (w, v) ∈ E, read as "either u happened after v, or else u happened before w". The polygraph associated with a history is:

• V: all committed transactions;
• E = {(T_i, T_j) | T_j reads from T_i}, written T_i →_wr(x) T_j;
• C = {⟨(T_j, T_k), (T_k, T_i)⟩ | T_i →_wr(x) T_j ∧ T_k writes x ∧ T_k ≠ T_i ∧ T_k ≠ T_j}.

So every other writer of x must land either after the reader or before the writer it read from.

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

The brute-force check is therefore: build the polygraph, search for an acyclic compatible graph. That is |C| binary choices (2^|C| possibilities), and |C| is large: it is ∑_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.

4. Cobra's encoding (from §3, §3.1–§3.3, Figures 2–3)

Within a round, the verifier's pipeline is: history collectors → create the known graph → combining writes → coalescing constraints → pruning constraints → MonoSAT → accept or reject. Garbage collection carries the graph g from round i−1 into round i (Figure 2; §7 of this version covers rounds).

Generalized constraints. Cobra replaces edge-pair constraints with pairs of sets of edges. Meeting ⟨A, B⟩ means including all of A and none of B, or vice versa. Formally, (V′, E′) is compatible with known graph G = (V, E) and generalized constraints C if V = V′, E ⊆ E′, and

The validity theorem for Cobra's encoding (Appendix B of the extended version): there exists an acyclic graph compatible with the constraints Cobra constructs on a history if and only if the history is serializable. The source file I compiled from does not contain the proof, so I cannot tell you its structure.

4.1 Combining writes (from §3.1)

Cobra exploits the RMW pattern (e.g., read an item's stock count, decrement, write back). If T_t is an RMW on key k that read from T_t′, then T_t′'s write must immediately precede T_t's write in the version order of k. Cobra therefore groups writes into chains: sequences of transactions whose writes to a key are consecutive. Every write starts as a one-element chain (Figure 3, line 32); for each RMW, the chain ending with the prior write and the chain starting with the RMW are concatenated (lines 22 and 44–51). Ordering uncertainty now exists only between chains, not between individual writes. If two RMWs read from the same write, there would be two consecutive writes after one write, which is rejected immediately (lines 20–21).

A non-RMW transaction t that reads from u needs an anti-dependency edge to u's successor v in u's chain; otherwise t could be placed after v, which would mean t read from v or later. InferRWEdges adds these t → v edges (line 53). In the brute-force polygraph, analogous edges appear as the first component of a constraint.

Constraints are then generated only between pairs of chains on the same key. For chains chain_i, chain_j: ES1 is the set of edges from the readers of chain_i.tail to chain_j.head (lines 71–72), or the single edge chain_i.tail → chain_j.head if that tail has no readers (line 67); ES2 is the same in the other direction; the constraint is ⟨ES1, ES2⟩ (line 63).

4.2 Coalescing constraints (from §3.2)

Real workloads usually have far more reads than writes. Cobra merges all constraints that hinge on the same question, "which write came first?". The paper's example: on one key, writes W1 and W2; reads R3 and R4 read from W1; R5 reads from W2. The basic polygraph has three constraints, all deciding W1 vs. W2. They can be represented as ⟨A′, B′⟩ with A′ = {(W1, W2), (R3, W2), (R4, W2)} and B′ = {(W2, W1), (R5, W1)}. The edge (W1, W2) is redundant, because the known edge (W1, R3) together with (R3, W2) already implies W1 → R3 → W2; likewise (W2, W1) via known edge (W2, R5). Cobra's single constraint is ⟨{(R3, W2), (R4, W2)}, {(R5, W1)}⟩. In Figure 3 this is exactly what GenChainToChainEdges produces when a chain tail has readers.

4.3 Pruning constraints (from §3.3)

Compute the transitive closure of the known graph. For a constraint ⟨ES1, ES2⟩, if some edge (t_i, t_j) in ES1 has t_j ⇝ t_i already, choosing ES1 closes a cycle, so ES2 must hold: add ES2 to the known graph and drop the constraint (lines 78–84). Symmetrically for ES2. The paper's example: constraint ⟨(R3, W2), (W2, W1)⟩ with known path W2 ⇝ R3 (R3 reads from W2); the first choice is impossible, so the second is added. Pruning can be repeated, since added edges create new paths (§5). The logic is, in the authors' words, "almost trivial"; the point is that reachability is iterated Boolean matrix multiplication and so can run on GPUs.

4.4 Worked example: Figure 3 on the combining-writes scenario

4.5 Figure 3, translated to Python

Translation of the paper's pseudocode. Cobra's actual implementation is in Java and CUDA/C++ (Figure 4). Each line carries the original line number as a trailing comment (# Ln), followed by the original comment where there was one.

def construct_encoding(history):                                # L1
    g, readfrom, wwpairs = create_known_graph(history)           # L2
    con = gen_constraints(g, readfrom, wwpairs)                  # L3
    con, g = prune(con, g)                                       # L4: §3.3, executed one or more times
    return con, g                                                # L5
                                                                 # L6
def create_known_graph(history):                                 # L7
    g = Graph()                                                  # L8: the known graph
    wwpairs = {}                                                 # L9: {(key, tx): tx}, consecutive writes
    readfrom = defaultdict(set)                                  # L10: {(key, tx): set of tx}, maps a write to its readers
    for tx in history:                                           # L11
        g.nodes.add(tx)                                          # L12
        for rop in tx.read_ops:                                  # L13
            g.edges.add((rop.read_from_tx, tx))                  # L14: read-dependencies
            readfrom[(rop.key, rop.read_from_tx)].add(tx)        # L15
                                                                 # L16
        # detect RMW (read-modify-write) transactions            # L17
        for key in tx.read_keys & tx.write_keys:                 # L18: keys both read and written by tx
            rop = tx.read_op(key)                                # L19: the operation in tx that reads key
            if wwpairs.get((key, rop.read_from_tx)) is not None: # L20
                reject()                                         # L21: multiple consecutive writes, not serializable
            wwpairs[(key, rop.read_from_tx)] = tx                # L22
                                                                 # L23
    add_session_order_edges(g)                                   # L24: §4.2
    return g, readfrom, wwpairs                                  # L25
                                                                 # L26
def gen_constraints(g, readfrom, wwpairs):                       # L27
    # each key maps to set of chains; each chain is an ordered list   # L28
    chains = defaultdict(list)                                   # L29: {key: [chain, ...]}
    for tx in g.nodes:                                           # L30
        for wrop in tx.write_ops:                                # L31
            chains[wrop.key].append([tx])                        # L32: one-element list
                                                                 # L33
    combine_writes(chains, wwpairs)                              # L34: §3.1
    infer_rw_edges(chains, readfrom, g)                          # L35: infer anti-dependency
                                                                 # L36
    con = []                                                     # L37
    for key, chainset in chains.items():                         # L38
        for chain_i, chain_j in combinations(chainset, 2):       # L39: every pair of chains
            con.append(coalesce(chain_i, chain_j, key, readfrom))  # L40: §3.2
                                                                 # L41
    return con                                                   # L42
def combine_writes(chains, wwpairs):                             # L43
    for (key, tx1), tx2 in wwpairs.items():                      # L44
        # By construction of wwpairs, tx1 is the write immediately    # L45
        # preceding tx2 on key. Thus, we can sequence all writes      # L46
        # prior to tx1 before all writes after tx2, as follows:       # L47
        chain1 = next(c for c in chains[key] if c[-1] == tx1)    # L48: list whose last elem is tx1
        chain2 = next(c for c in chains[key] if c[0] == tx2)     # L49: list whose first elem is tx2
        chains[key].remove(chain1); chains[key].remove(chain2)   # L50
        chains[key].append(chain1 + chain2)                      # L51: concat
                                                                 # L52
def infer_rw_edges(chains, readfrom, g):                         # L53
    for key, chainset in chains.items():                         # L54
        for chain in chainset:                                   # L55
            for i in range(0, len(chain) - 1):                   # L56: i in [0, length(chain) - 2]
                for rtx in readfrom[(key, chain[i])]:            # L57
                    if rtx != chain[i + 1]: g.edges.add((rtx, chain[i + 1]))  # L58
                                                                 # L59
def coalesce(chain1, chain2, key, readfrom):                     # L60
    edge_set1 = gen_chain_to_chain_edges(chain1, chain2, key, readfrom)  # L61
    edge_set2 = gen_chain_to_chain_edges(chain2, chain1, key, readfrom)  # L62
    return (edge_set1, edge_set2)                                # L63
                                                                 # L64
def gen_chain_to_chain_edges(chain_i, chain_j, key, readfrom):   # L65
    if not readfrom[(key, chain_i[-1])]:                         # L66: tail has no readers
        edge_set = {(chain_i[-1], chain_j[0])}                   # L67: tail -> head
        return edge_set                                          # L68
                                                                 # L69
    edge_set = set()                                             # L70
    for rtx in readfrom[(key, chain_i[-1])]:                     # L71
        edge_set.add((rtx, chain_j[0]))                          # L72
    return edge_set                                              # L73
                                                                 # L74
def prune(con, g):                                               # L75
    # tr is the transitive closure (reachability of every two nodes) of g   # L76
    tr = transitive_closure(g)                                   # L77: standard algorithm; see [70, Ch.25]
    for edge_set1, edge_set2 in con:                             # L78
        if any(tr.reaches(tx_j, tx_i) for (tx_i, tx_j) in edge_set1):    # L79
            g.edges |= edge_set2                                 # L80
            con.remove((edge_set1, edge_set2))                   # L81
        elif any(tr.reaches(tx_j, tx_i) for (tx_i, tx_j) in edge_set2):  # L82
            g.edges |= edge_set1                                 # L83
            con.remove((edge_set1, edge_set2))                   # L84
    return con, g                                                # L85

5. Solving with MonoSAT (from §3.4)

Traditional solvers do poorly here because encoding graph acyclicity as SAT formulas is expensive (a claim of Janota et al. that the authors also observed, §6.1). Cobra uses MonoSAT, an SMT solver for SAT modulo monotonic theories, which efficiently encodes and checks graph properties such as acyclicity.

The encoding: a Boolean variable E(i,j) per vertex pair, true iff the searched-for compatible graph has edge (i, j). Known edges are asserted true. Each constraint ⟨A, B⟩ becomes

and acyclicity of the graph of true E(i,j) is enforced by a primitive the solver provides.

Division of labor. Why not push domain knowledge further and replace MonoSAT? The authors' answer: MonoSAT carries many prior optimizations; Cobra's preprocessing exploits structure specific to serializability, while the solver exploits residual structure common to many graph problems.

On a violation, the verifier emits a certificate: either a cycle in the known graph (found by Cobra's own algorithms) or a set of unsatisfiable clauses produced by MonoSAT (§5).

6. Strict serializability (from §3.5)

To check strict serializability, the verifier adds real-order edges (order of non-overlapping transactions in real time) to the known graph and runs the same algorithm. Timestamps come from the database if it exposes them (e.g., Google Spanner) or from Cobra's collectors. Instead of the quadratic all-pairs comparison, Cobra uses a prior algorithm that materializes the time-precedence partial order in O(n + z), where n is the number of transactions and z is the minimum number of real-order edges needed.

Clock drift among collectors makes timestamps unsafe. Cobra assumes collector clocks differ by less than a clock drift threshold (100 ms by default) and adds the threshold to every commit timestamp. Two transactions get a real-order edge only if one's original commit timestamp precedes the other's start by at least the threshold, so all transactions within one threshold are concurrent. Inside such a window the verifier faces the full non-strict difficulty, which is why §3.1–§3.3 matter even for the strict variant. If the drift assumption is violated, Cobra may falsely reject a serializable history.

7. Rounds, epochs, and garbage collection (from §4)

Cobra verifies in rounds, both because history keeps arriving and because there is a maximum problem size the verifier can handle. Round 1 builds the graph from scratch; each later round reuses the previous round's g (Figure 3, line 5) and adds new nodes and edges. The question is which transactions can be safely deleted so the input stays bounded. The full specification and correctness proof are in Appendix C of the extended version, not in this source.

7.1 Why deletion is unsafe in general (§4.1)

Serializability does not respect real time, so a future transaction may read a value that, in real time, was overwritten long ago. Example: T1 = W1(x); T2 = R2(x) W2(x) (reads x from T1); T3 = W3(y). Later T4 = R4(x) R4(y) reads x from T1 and y from T3. T2 is logically after T4, giving the cycle T4 → T2 ⇝ T3 → T4. If T2 had been deleted, no cycle would be visible. This needs no malice: a geo-replicated database can serve a stale version from a local replica.

7.2 Epochs and fence transactions (§4.2)

Clients periodically issue fence transactions (e.g., every 20 transactions): each reads and writes a dedicated key named "EPOCH". To stop the database from placing all fences at the start of a notional serial schedule, Cobra relies on preserved session order: the serialization order must obey execution order within each session. Many production databases provide this (PostgreSQL, Azure Cosmos DB, Google Cloud Datastore are named); otherwise clients must build it, e.g., by having every transaction in a session do an RMW on a per-session key. The verifier adds session-order edges to the known graph (line 24), using per-session order observed by the collectors.

Because fences are RMWs on one key, they form a single chain; a fence's position in it is its epoch number. 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. Epochs are distinct from rounds: a round spans multiple epochs.

Guarantee. For any T_i with epoch ≤ epoch_agree − 2, and any T_j (including future ones) with epoch ≥ epoch_agree, the known graph contains a path T_i ⇝ T_j.

The paper's argument: let F_ea be the fence with epoch epoch_agree; session-order edges give F_ea ⇝ T_j. Let F_ea−Δ be the next fence after T_i in T_i's session; then T_i ⇝ F_ea−Δ, and its epoch is ≤ epoch_agree − 1, so F_ea−Δ ⇝ F_ea along the fence chain.

7.3 Garbage collection (§4.3)

Cobra is conservative. T can be deleted if (i) T is superseded: no future transaction can precede T or directly succeed it in the known graph; and (ii) T is not on any potential cycle that uses constraint edges whose resolution future transactions could affect.

Frontier and superseded. The frontier is the set of transactions holding the most recent writes to keys among transactions with epoch ≤ epoch_agree − 2: the earliest transactions a future transaction may still read. T is superseded if (1) T is not in the frontier, (2) T's epoch ≤ epoch_agree − 2, and (3) every T′ with a path to T has epoch ≤ epoch_agree − 2. Condition (2) does not subsume (3), because the Guarantee does not apply to epochs that differ by one. Intuition: a future transaction reading from a superseded T would have to be ordered before some frontier transaction, which by the Guarantee closes a cycle back to it.

Superseded does not imply disposable. The paper's counterexample has T1 = W1(d) W1(a), T2 = W2(d) W2(a), T3 = R3(a) W3(b), T4 = W4(b) W4(c), T5 = R5(b) W5(c), T6 = W6(b), all with epoch ≤ epoch_agree − 2, and future T7 = R7(d), T8 = R8(c). T3 is superseded. T8 forces W4(c) before W5(c), which resolves the key-b constraint ⟨(T5, T4), (T4, T3)⟩ to T4 → T3; T7 similarly resolves the key-a constraint to T3 → T1; so T1 ⇝ T4 → T3 → T1 is a cycle, invisible if T3 were deleted. Future transactions can resolve constraints among old transactions.

Procedure. Clone the known graph into g′; add both edge sets of every constraint to g′; delete each superseded T that is on no cycle in g′, or only on cycles made entirely of superseded transactions. The authors argue in Appendix C that this meets (i) and (ii).

8. Implementation (from §5, Figure 4)

The client library wraps JDBC, the Google Datastore library, and RocksJava. It adds unique ids to writes and strips them on reads, issues fence transactions, and also performs history collection (writing operations to disk before sending them); the authors note a proxy would be a better place for collection.

Pruning is iterated within a round until nothing more is pruned or a configurable iteration cap is reached; the authors suggest a better stopping rule would compare the marginal pruning cost against the solver time it saves.

Transitive closure uses the standard algorithm: repeated squaring of the Boolean adjacency matrix while it keeps changing, up to log |V| multiplications (the worst case needs a path of ≥ |V|/2 + 1 steps, which the authors say did not arise much in their experiments). It runs on cuBLAS (dense) and cuSPARSE (sparse). Optimizations: after testing the graph for acyclicity, vertices are indexed by a topological sort so the matrix is triangular and a specialized triangular multiplication applies; sparse multiplication is used until density exceeds 5% non-zero elements (the empirically observed cross-over), then dense.

9. Evaluation: every number and what it measures (from §6)

Benchmarks. TPC-C (one warehouse, 10 districts, 30k customers; five transaction types: new order 45%, payment 43%, order status 4%, delivery 4%, stock level 4%). C-Twitter (1000 users, Zipfian follow/unfollow with α = 100). C-RUBiS (bidding; 20k users and 200k items). BlindW (10k keys, read-only and write-only transactions of eight operations each), in three variants: BlindW-RM (90% read-only), BlindW-RW (even split), BlindW-WM (90% write-only). Blind writes are "the fundamental source of uncertainty in constraints".

Databases and hardware. 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). Verifier: a p3.2xlarge Amazon EC2 instance with an NVIDIA Tesla V100 GPU, 8-core CPU, 64GB memory.

9.1 One-shot verification (§6.1)

The verifier gets one history and decides; the database is RocksDB (PostgreSQL and Datastore give similar results). Baselines:

• nonSAT: Biswas and Enea's algorithm, their Rust implementation.
• MiniSAT-BE: BE's own SAT baseline, encoding into SAT for MiniSAT.
• MonoSAT-polygraph: the §2.3 polygraph fed directly to MonoSAT, without Cobra's techniques ("Cobra, subtracted").
• Z3-arith: a linear-arithmetic encoding (a distinct integer per node, inequalities from read-from and writes, O(|V|²) constraints) solved by Z3 in default configuration; all four built-in linear integer arithmetic tactics gave similar results.

For TPC-C specifically, an alternative baseline (iteratively add inferred dependencies for RMWs, topologically sort, check) matches Cobra's performance, because TPC-C has only RMW transactions and the whole history coalesces into one correctly ordered chain. All baselines and Cobra use session-order edges.

• Single-round verification cost (C2, C3). Cobra's core verification improves on baselines by 10× in the problem size it can handle for a given time budget, that is, in verification cost (this is not a throughput figure). Concretely, Cobra finishes checking 10k transactions in 14 seconds, whereas baselines handle only 1k or less in the same time budget. §6.4 phrases the summary as "at least 10× on baselines in verification cost (Figure 5)".
• Figure 5 (BlindW-RW, 24 clients): verification time in seconds (axis 0–14, lower is better) against number of transactions (0–10k), for MiniSAT-BE, nonSAT, Z3-arith, MonoSAT-polygraph, and Cobra. Caption: Cobra's running time is shorter than the baselines'; the same holds on other benchmarks; verification runtime grows superlinearly. Text: on all benchmarks, Cobra beats MonoSAT-polygraph and Z3-arith, which beat MiniSAT-BE and nonSAT. Plotted values are not in the source; see the published PDF.
• Real violations (C5, Figure 6). Cobra detects all five serializability violations collected from real systems' bug reports:

  Violation	Database	#Txns	Time
  G2-anomaly	YugaByteDB 1.3.1.0	37.2k	66.3s
  Disappearing writes	YugaByteDB 1.1.10.0	2.8k	5.0s
  G2-anomaly	CockroachDB-beta 20160829	446	1.0s
  Read uncommitted	CockroachDB 2.1	20*	1.0s
  Read skew	FaunaDB 2.5.4	8.2k	11.4s

  #Txns is the size of the violating history; Time is Cobra's detection runtime. * The bug report contains only a small fragment of the history.
• Figure 7 (runtime decomposition on 10k-transaction workloads, stacked bars of constructing / pruning / solving in seconds for all six benchmarks). Caption: pruning dominates for read-mostly workloads; solving dominates for workloads with many writes. Text: TPC-C has no constraints, so no pruning; with many blind writes, solving grows because fewer constraints are eliminated. Plotted values not in the source.
• Figure 8 (differential analysis, log scale, 10-minute timeout): Cobra, Cobra without pruning, Cobra without pruning and coalescing (i.e., MonoSAT plus write combining), and MonoSAT, on TPC-C, C-Twitter, BlindW-RW. Caption: on TPC-C, combining writes alone solves all constraints; on C-Twitter each component contributes meaningfully; on BlindW-RW pruning is essential. Plotted values not in the source.
• Strict serializability under clock drift (C6, Figure 9). Workload: 2,000 transactions of BlindW-RW, eight clients on 1k keys for one second at 2k transaction/sec, 20 transactions every 10ms, clock drift threshold up to 100 ms. Cobra outperforms the baselines (MonoSAT-polygraph, Z3-arith) by 45× and 107× in verification time. The plot (verification time vs. drift threshold 0–100 ms) is not reproduced in the source.

9.2 Scaling (§6.2)

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

• C7, Figure 10. Best verification 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). Plot axes: verification throughput (txn/sec) vs. transactions per round (1k–10k); values not in the source. Too-small rounds waste work re-analyzing transactions not yet collectable; too-large rounds hit superlinear solve time.
• Memory limit. BlindW-RW and BlindW-WM run out of memory: history eventually exceeds GPU memory because blind writes leave many constraints open, so transactions cannot be garbage collected.
• Figure 11 (BlindW-RM, round size fixed at 5k, x-axis: transactions between fences per client, 10–60; client throughput normalized to the fence-free workload; fences have 1–2 operations vs. 8 for normal transactions). More frequent fences raise verifier throughput (smaller epochs, earlier collection, extra ordering) but cost peak client throughput. Values not in the source.

9.3 Online overheads (§6.3)

• C8, Figure 12 (C-Twitter, up to 256 clients, baseline is the unmodified library with no history recording). RocksDB: 90th-percentile latency increases by 2× with a 50% throughput penalty, attributed to history collection (disk bandwidth contention between clients and the DB). PostgreSQL: minor overhead. Google Datastore: a throughput penalty reflecting the service's ceiling on operations per second plus the extra operations from fence transactions. Plot values not in the source.
• C9, Figure 13 (per 1k transactions; network overhead comes from fence transactions and the metadata the client library adds). Network overhead is 2.17%–7.28% of traffic.

  workload	network traffic	network percentage	history size
  BWrite-RW	227.4 KB	7.28%	245.5 KB
  C-Twitter	292.9 KB	4.46%	200.7 KB
  C-RUBiS	107.5 KB	4.53%	148.9 KB
  TPC-C	78.2 KB	2.17%	1380.8 KB

9.4 Sustained throughput (Abstract, §1, §6.4)

C4. Cobra achieves a sustainable verification throughput of 2k txn/sec on the workloads tested; the abstract states "2000 transactions/sec, equivalent to 170M/day". 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. The relevant requirement is matching the database's average load, not its peak (§2.1).

10. Positioning against prior checkers (from §1, §7)

Three earlier works address black-box checking of serializability: Biswas and Enea (polynomial under restrictions, clients in the exponent, no continuous-history mechanism); Sinha et al. (SMT search over interleavings of a concurrent program); and Gretchen (an experimental checker for non-strict serializability of a Cobra-style history, constraints solved with fzn-gecode, similar to the MiniSAT-BE baseline).

Elle (part of Jepsen) has two modes. One verifies Adya's serializability but requires a workload that makes the version order manifest (e.g., writes as list appends), which the authors say does not meet their notion of black box. The other works on arbitrary key-value observations, Cobra's setup, using heuristics that are useful but not comprehensive; for example, a cycle of concurrent transactions through anti-dependencies is not detected by Elle's current heuristics.

Other neighbors are distinguished by what they assume: consistency checkers for cloud storage use extra ordering information (synchronized clocks, client-to-client communication, sequencing gateways); Concerto and execution-integrity systems modify the storage layer or the stack; application-anomaly detectors use SAT/SMT on graph problems but treat storage as trusted. The authors leave open whether non-graph definitions of isolation (anomaly-exclusion, client-centric) would yield a more intuitive or more easily implemented encoding.

11. What you'd need to rebuild this (built only from §3–§5)

12. Open problems the paper names (from §7, §8)

• Whether real-world workloads ever trigger the exponential worst case, or only contrived instances like those in the NP reduction do. The authors expect real workloads not to, with the intuition that low contention gives few constraints, and high contention with enough reads gives many dependencies and hence more ordering.
• Fault tolerance of verifier and collectors (state machine replication, or protocol extensions). They note a cycle found in a partial history is also a violation in the full history, and suggest inferring what missing transactions would have to be for serializability.
• Other isolation levels beyond serializability and strict serializability.
• Native range queries and high-level operators (sum, join), which would require reasoning about keys that are not returned.
• More aggressive garbage collection, e.g., letting the verifier query the database to resolve some constraints.
• Whether other definitions of isolation yield a better encoding (§7).

15. Faithfulness note

Ledger items included: all claims C1–C12 (C1 in §2; C2, C3, C5, C6 in §9.1; C7 in §9.2; C8, C9 in §9.3; C4 in §9.4; C10 in §4; C11 across §4–§7; C12 in §8) and all limitations L1–L8 (§13).

Ledger items omitted: none. Part D material condensed or left out because it is out of scope for a build-on reading by a PL researcher: most of the related-work survey in §7 (consistency checking, cloud-storage checkers, execution integrity, TEEs/BFT, cryptographic systems, application-anomaly detectors are only summarized in one paragraph); client machine hardware details in §6; the fence-frequency tuning discussion in §6.2 is shortened; the "Who would use Cobra?" and applicability discussion in §8 (Jepsen as host, recovery via certificates, verifier vs. database work per transaction) is omitted; the reference list is not reproduced.

Additions (all mine, all marked in green asides):

• Reading guide (§1) and the contents list.
• Bridges: database vocabulary in PL terms (§2); the correspondence between Adya's dependencies and memory-model relations rf/co/fr/po (§2); the solver view of the polygraph (§3); pruning as up-front theory propagation (§4.3); a note on what "monotonic" means for acyclicity (§5); g′ as an over-approximation (§7.3); Boolean-semiring transitive closure and what cuBLAS/cuSPARSE are (§8).
• Worked example: a step-by-step trace of Figure 3 on the paper's §3.1 combining-writes scenario (§4.4).
• Translated code: Figure 3 rendered line-for-line in Python with original line numbers (§4.5), plus a note on representation choices and why it is not runnable as-is.
• Redrawn diagrams: the §2.3 example polygraph and Figure 2's pipeline, both redrawn from the source's content descriptions. No plotted data drawn for Figures 5, 7–12.
• The rebuild checklist (§11), assembled from §3–§5, with a list of what the source does not contain.
• Four questions for the reader (§12).
• Places where I state that the source cannot answer: proof contents (Appendices B, C), MonoSAT internals and configuration, GPU-less performance, default pruning iteration cap.

No derived numbers are used. Every number above appears in the source's Part C or Part D.