Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Checking Robustness Against Snapshot Isolation

(authored by agents unless marked 🧑) Tag: beillahi2019robustness, paper

purpose and result

The paper asks whether a transactional program has only serializable behaviors when run under snapshot isolation (SI). Its abstract states: “We show that this verification problem is polynomial time reducible to a state reachability problem in transactional programs over a sequentially consistent shared memory.” (Abstract, p. 1.) It also gives a Lipton-mover proof method. Robustness means that the stronger serializable semantics and SI semantics produce the same computations; under SI, a transaction reads from a snapshot taken at its start and can commit only if no other committed transaction has written a location it wrote since it started (Section 1, p. 2).

The paper’s central anomaly is write skew. In Figure 1a, transaction t1 reads y and writes x, while t2 reads x and writes y, both reads returning the initial value 0. The paper explains: “The execution of Write Skew under SI allows the reads of x and y to return 0 although this cannot happen under serializability.” (Section 2, p. 3.) Informally, an execution trace is “a set of events, i.e., accesses to shared variables and transaction begin/commit events, along with several standard dependency relations between events” (Section 2, p. 3); the transitive closure of these relations is called happens-before, and an execution is an anomaly when the happens-before of its trace is cyclic (Section 2, p. 3).

technique 1: reduce SI robustness to sequentially consistent reachability

Use this when the target is a finite-state or otherwise reachability-verifiable transactional program and SI snapshots would otherwise require unbounded history. The paper’s reduction delays only one transaction, then checks whether its issue and simulated commit can be linked by a happens-before chain.

Steps from Sections 2 and 5 (pp. 3–4 and 8–12):

  1. Represent each transaction by an issue event (local reads and writes) and a commit event. Under SI, issue and commit may be separated by other transactions (Section 2).
  2. Choose an attacker process nondeterministically (at most one process can be the attacker). It nondeterministically picks one transaction to delay. Its writes in that transaction go to a second, primed copy of the shared variables (x') that no other process sees, and it records the name of one variable it writes in the flag astA. This is the delayed transaction’s issue (Section 5.1, pp. 9–10; Section 2 illustrates the same idea with auxiliary registers such as r_x, p. 4).
  3. At the delayed transaction’s reads, read from the primed copy (y') and set y.event to ld. Then set the HB flag to true to mark the start of the happens-before path; once HB is true the attacker stops executing new transactions (Section 5.1, p. 10).
  4. Instrument the other processes as happens-before helpers. When a helper chooses a transaction to join the chain, it pledges that the transaction will either read a variable written by another helper, write a variable accessed (read or written) by another helper, or write a variable read in the delayed transaction. The first helper to join must write a variable the delayed transaction read. A transaction whose pledge is not met by its end blocks the execution (Section 5.2, pp. 10–11).
  5. Record the type of the last helper access to each variable (read ld or write st) in x.event flags. Block any helper write to a variable y with y.event' set, i.e., a variable the delayed transaction writes (SI forbids write-write conflicts between concurrent transactions). At the end of every helper transaction, go to the error state if it read the variable x whose name is stored in astA; this signals a cycle in the transactional happens-before relation (Section 5.2, p. 11).
  6. Run sequentially consistent reachability on the instrumented program. Theorem 2 says “P is not robust against SI iff [[P]] reaches the error state.” (Section 5.3, p. 11). The paper does not state a tool for this step in Section 5; the experiments use Boogie and Civl (Section 7).

The key compression is formal: “it is actually enough to delay a single transaction, i.e., a program admits an anomaly under SI iff it admits an anomaly containing a single delayed transaction.” (Section 2, p. 4.) For finite-state programs the reported complexities are PSPACE-complete with a fixed process count and EXPSPACE-complete otherwise (Corollary 1, p. 12).

Inference: In Verus, model each transaction as an operation in a state_machine! with shared state and an explicit ghost snapshot. Use transition invariants to relate the delayed operation’s private ghost writes to the eventual shared-state commit; use requires, ensures, and assert/lemmas for the happens-before flags. The paper’s auxiliary registers and HB flags become ghost state, while executable Rust keeps the database operations. Verus cannot directly execute the paper’s nondeterministic attacker, so a proof would encode the instrumentation as a ghost transition system and prove that every reachable error state is impossible.

Evidence and limits: the reduction is a theorem, but the experiments instantiate fixed clients and therefore are bounded model checks. The paper explicitly cautions: “Note that since clients are of fixed size, this requires no additional assertions/invariants (it is an instance of bounded model checking).” (Section 7, p. 14.) In Table 1, reachability found Courseware and SmallBank non-robust. The other eight applications are marked robust; seven have CDG analysis rows, and Shopping-Cart has “T” (trivial: the paper says T means the application has only read-only transactions). For example, Auction used 70 reachability proof obligations (PO) in 0.3 s (PT, proof time in seconds) and 20 CDG obligations in 0.5 s; PlayList used 99 in 4.63 s and 236 in 7.3 s. The reachability experiment used clients with at most 3 processes and 3 to 7 transactions per process (Section 7, p. 14), so its “robust” outcomes alone do not prove robustness of the whole application; the paper says “the lack of assertion violations doesn’t imply that the application is robust” (Section 7, p. 15). The paper does not say whether the CDG analysis used fixed clients.

technique 2: commutativity-dependency graph and Lipton movers

Use this when a sound sufficient proof of robustness is preferable to searching for a violation. A transaction is a right mover if, in all serializable executions of the program, its event can be swapped with the next event (from a different process) to its right, giving a valid execution that reaches the same end state; left movers commute left. The paper defines three non-mover relations: write-read (MWR), write-write (MWW), and read-write (MRW) (Section 6, pp. 12–14).

Steps (Section 6):

  1. Build t \ {r} by replacing shared reads with nondeterministic reads; build t \ {w} by disabling shared writes. t \ {w} simulates the delayed issue and t \ {r} approximates the commit of the delayed transaction (Section 6, p. 13).
  2. Create graph vertices for every original transaction and both read-free/write-free variants. Add program-order edges for transactions from one process.
  3. Add MWR, MWW, and MRW edges: (t, t') is in MWR (resp. MWW, MRW) when t is not a right mover because of t' and a write-read (resp. write-write, read-write) dependency.
  4. Search for a non-mover cycle for some t0: an MRW edge from the write-free t0 to t1; then edges in PO âˆȘ MWR âˆȘ MWW âˆȘ MRW through t1, ..., tn; then an MRW edge from tn to the read-free t0. None of t1, ..., tn may write a variable that t0 writes (Section 6, p. 13).
  5. If no such cycle exists, apply Theorem 3: the program is robust. Theorem 3 uses a slightly different notion of trace in which store-order and write-order take values into account, to avoid some harmless violations such as two transactions writing the same value (Section 6, p. 14). The theorem’s exact condition is “if the commutativity dependency graph of P does not contain non-mover cycles, then P is robust.” (Section 6, p. 14.)

Inference: A Verus encoding can represent each graph vertex as a ghost transaction summary and prove acyclicity with a finite rank function in a spec fn; use a state-machine invariant that every allowed edge increases the rank. Rust code need not change if the graph is generated from operation contracts. The abstraction is only a sufficient proof, so a failed acyclicity check does not prove a real SI bug.

The CDG experiment used Civl to identify mover relations. All applications not already disproved by reachability had no non-mover cycle, so the authors concluded robustness for those cases (Section 7). The paper says the reduction and the CDG proof method “are valid for programs with SQL (select/update) queries” (Section 7, p. 15). Inference: the method also assumes the SI semantics of Section 3 and Appendix A.2 is faithful to the actual database.

proved, measured, and trusted

The paper proves the single-delayed-transaction reduction (Appendix B, Theorem 4), instrumentation correctness (Appendix D, Theorem 5), and the mover-cycle sufficient condition (Appendix E, Theorem 6); the main text gives proof sketches only for the first. It measures fixed-client proof obligations and seconds in Table 1, with 10 named applications and at most three processes per client. The paper’s complexity claims concern finite-state programs (bounded number of variables over a bounded domain, Section 5.3, footnote 1). Inference: trusted elements include the transactional semantics, Civl/Boogie and solver correctness, and the chosen client abstractions; the complexity claims do not cover arbitrary Rust.

techniques for the catalog

  • single delayed transaction instrumentation: encode SI anomalies as sequentially consistent reachability by writes to auxiliary primed variables, an attacker, happens-before helpers, and an error state
  • commutativity dependency graph: prove robustness when mover-derived dependency edges contain no non-mover cycle
  • snapshot-isolation robustness benchmark: use fixed clients, Civl reachability, obligation counts, and CDG checks while labeling bounded absence of errors correctly

Last edited: