Analysing Snapshot Isolation
This paper (PODC'2016) presents a clean and declarative treatment of Snapshot Isolation (SI) using dependency graphs. It builds on the foundation laid by prior work, including the SSI paper we reviewed recently, which had already identified that SI permits cycles with two adjacent anti-dependency (RW) edges, the so-called inConflict and outConflict edges. While the SSI work focused on algorithmic results and implementation, this paper focuses more on the theory (this is PODC after all) of defining a declarative dependency-graph-based model for SI. It strips away implementation details such as commit timestamps and lock management, and provides a purely symbolic framework. It also proves a soundness result (Theorem 10), and leverages the model for two practical static analyses: transaction chopping and robustness under isolation-level weakening.
Soundness result and dependency graph model
Building on foundational work by Adya, this model represents executions as graphs whose nodes are transactions and whose edges capture observable transactional dependencies in terms of 3 edge types: write-read (WR), write-write (WW), and the anti-dependency capturing read-write (RW) edges. The SI, Serializability (SER), and Parallel SI (PSI) isolation levels are then defined in terms of the structural properties in these graphs, specifically by the presence or absence of certain cycles. This abstraction supports symbolic reasoning about anomalies like write skew or long fork manifest as specific, checkable subgraphs. Informally, a WR edge from T to S means that S reads T’s write to some object x; a WW edge means that S overwrites T’s write; and a RW edge indicates that S overwrites the value of x read by T, introducing an anti-dependency.
Definition 4 and Figure 1 provide an elegant axiomatization of abstract executions. The visibility relation (VIS) must always be a subset of the commit order (CO), and in the case of Serializability, the two are equal. In my mind, this captures the key conceptual divide between SER and SI: Serializability enforces a total order over committed transactions, wheras SI permits partial orders.
Figure 2 illustrates the anomalies that differentiate SER, SI, and PSI. Figure 2(d) captures the classic write skew anomaly, which SI allows but SER prohibits. This scenario arises when two transactions read disjoint keys and then write disjoint values based on those reads, each unaware of the other's effects. SI permits this since it allows partial visibility so long as snapshots are consistent. On the other hand, the long fork anomaly shown in Figure 2(c) is prohibited by SI but allowed by PSI, which weakens the snapshot guarantees further.
Applications of the model
The second half of the paper shows applications of the model for static analyses. The first application is transaction chopping, where large transactions are split into smaller subtransactions to improve performance. The challenge here is to ensure that the interleaving of chopped pieces does not introduce new behaviors/anomalies that the original monolithic transaction would have prevented. This is captured through spliceability: whether an execution of chopped transactions can be "stitched back" into an execution that would have been legal under SI for the unchopped program. Spliceability is formulated through a chopping graph, which augments standard dependencies with session-local ordering among chopped subtransactions. A cycle in the chopping graph DCG(G) is considered critical if (1) it does not contain two occurrences of the same vertex, (2) it includes a sequence of three edges where a conflict edge is followed by a session (predecessor) edge and then another conflict edge, and (3) any two RW (anti-dependency) edges in the cycle are not adjacent. Such critical cycles represent dependency patterns that cannot be reconciled with the atomicity guarantees expected by the original transaction, and thus cannot be realized under SI. Figures 4, 5 and 6 illustrate how small structural differences in the chop can lead to either results that are sound (Figure 6) or unsound (Figure 5 creates a critical cycle). Compared to serializability, SI's more relaxed visibility rules allow for a wider range of safe chops, but care must still be taken to avoid dependency structures that violate snapshot consistency.
The second application of the dependency graph model is in analyzing robustness across isolation levels. The central question is whether a program behaves identically under SI and a weaker or stronger model. An interesting case here is the relation between SI and Parallel SI (PSI). We covered PSI in our earlier review of Walter (SOSP 2011). PSI weakens SI by discarding the prefix requirement on snapshots: it ensures only that visibility is transitive, not that it forms a prefix of the commit order. Thus, PSI admits behaviors that SI prohibits. Theorem 22 formalizes one such divergence. It shows that if a cycle in the dependency graph contains at least two RW edges and no two of them are adjacent, then this cycle is allowed under PSI but not under SI. This captures the long fork anomaly, in which concurrent writers are seen inconsistently by different readers (each reader forming a different branch of the history).
To illustrate the long fork, consider a cycle where T1 and T2 are concurrent writers, and two readers, T3 and T4, observe them inconsistently.
- T1 --WR--> T3
- T2 --WR--> T4
- T3 --RW--> T2
- T4 --RW--> T1
In this scenario, T3 sees T1's write but not T2's, and T4 sees T2's write but not T1's. Both readers construct transitive but incompatible snapshots that fork the timeline. SI prohibits this because it cannot construct prefix-closed snapshots that explain both T3 and T4's observations. But since PSI lacks the prefix constraint, it allows this behavior, while still disallowing anomalies like lost update (through its NOCONFLICT axiom).
Robustness from SI to PSI therefore requires ruling out that specific structural pattern: cycles with multiple RW edges where none are adjacent. If such a cycle appears in the dependency graph, PSI will admit the behavior, while SI will not, and robustness would fail.
Discussion
This does invite comparison to the Seeing is Believing (SiB) paper (PODC'17), one of my favorite papers, and its state-centric formulation of isolation guarantees. In SiB, executions are modeled as sequences of global states and snapshots. Transactions observe one of these states and transition the system to a new one. Isolation models are defined in terms of whether there exists a sequence of global states consistent with the observations and effects of each transaction.
While structurally different, the two models are not in conflict. It appears feasible to translate between the dependency graph and state-centric views. The SI model used in this PODC2016 paper already adopts a declarative, axiomatic approach centered on visibility and commit order that is already close to SiB.
For static program analysis, the dependency graph model seems to offer advantages. By abstracting away from global states, it allows symbolic reasoning directly over transactional dependencies. This makes it well-suited to analyses like transaction chopping and robustness checking, which rely on detecting structural patterns such as cycles with certain edge configurations. While the SiB model is semantically expressive and well-suited to observational reasoning, it may be less conducive to structural checks like cycle-freedom or anti-dependency adjacency.
Comments