Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels∗ Qiuhuan Xiong
Hengfeng Wei
Si Liu
Nanjing University [email protected]
Hunan University [email protected]
Texas A&M University [email protected]
Yuxing Chen
Jidong Ge
Renmin University of China [email protected]
Nanjing University [email protected] MixIso. We address these challenges by developing MixIso, a formal semantic framework for mixed isolation levels. It accommodates both traditional levels, such as SER and SI, and a range of emerging ones, including read atomicity (RA) [5], transactional causal consistency (CC) [2], prefix consistency (PC) [10], and parallel snapshot isolation (PSI) [28]. Underlying MixIso is a semantic characterization of mixed isolation levels based on per-transaction visibility: the effects of other transactions that a given transaction is allowed to observe in a database execution. The overall execution is then considered consistent if, for each transaction, the effects it observes conform to its assigned level. This per-transaction interpretation of visibility enables us to faithfully capture subtle semantic differences between isolation levels, while providing the flexibility to specify mixed isolation guarantees that reflect particular design choices or implementations. MixIso builds on the axiomatic framework in [12], which provides a declarative basis for specifying isolation levels while abstracting away implementation details. Yet, extending its axioms to mixed isolation settings is non-trivial. A key challenge lies in employing a shared global visibility relation across transactions running at different isolation levels while preserving isolation autonomy, i.e., a transaction’s isolation guarantee depends only on its own assigned level. Otherwise, a transaction with a stronger level could implicitly impose its visibility requirements on other transactions.
arXiv:2607.16696v1 [cs.DB] 18 Jul 2026
ABSTRACT Modern database systems widely support per-transaction isolation levels as a practical means of balancing consistency guarantees and performance. Yet, it remains largely unclear whether their concurrency control protocols correctly enforce the intended isolation guarantees under such mixed-isolation settings. In this paper, we address this semantic conformance question by developing MixIso, a formal semantic framework for mixed isolation levels. We demonstrate its applicability by establishing the semantic conformance of two concurrency control protocols, one combining two isolation levels and the other three.
1
INTRODUCTION
Strong database isolation guarantees, such as serializability (SER) [24], often come at the cost of increased concurrency control overheads. To mitigate this tension, production database systems, including Oracle, MySQL, PostgreSQL, CockroachDB, and TiDB, increasingly support assigning isolation levels on a per-transaction basis. This allows applications to execute certain transactions under weaker isolation levels like snapshot isolation (SI) [6], instead of enforcing SER system-wide, thereby achieving performance gains. However, this raises a natural question: when transactions execute under such mixed isolation settings, can the underlying concurrency control mechanisms correctly enforce the desired isolation guarantees? This question remains largely unanswered despite prior efforts [3, 17–19, 21, 22, 26, 32] on verifying isolation guarantees for concurrency control protocols, which focus on homogeneous isolation settings. The challenges are mainly twofold:
VIS
W(x, 1)
(1) The semantics of individual isolation guarantees and their variants are already subtle [15, 20]; mixing them introduces significantly greater semantic complexity. In fact, despite widespread support for per-transaction isolation, existing database documentation [11, 14, 23, 25, 27, 29, 31] typically leaves the semantics of mixing isolation levels underspecified or implementation-specific. (2) Answering this question demands a mathematically rigorous and systematic framework, ideally along with tool support, for formally verifying the semantic conformance of concurrency control protocols across a wide range of isolation level combinations.
T3 [RA]
T2 [SI]
T1 [PC] VIS
R(x, 1) W(y, 2)
VIS
R(x, init) R(y, 2) W(x, 3)
T4 [CC] VIS
R(x, 3) R(y, 2)
VIS
Figure 1: An illustration of isolation autonomy for 𝑇3 . For instance, as shown in Figure 1, transaction 𝑇4 , which is assigned CC, requires its visible set to be transitively closed: since 𝑇4 sees1 𝑇3 (by reading the value 3 of key 𝑥 written by 𝑇3 ) and 𝑇3 sees 𝑇2 , 𝑇4 must also see 𝑇2 , which indeed holds. Yet, 𝑇3 , which is assigned the weaker level RA and lies in the visible past of 𝑇4 , is not thereby required to satisfy transitive visibility. In particular, although 𝑇3 sees 𝑇2 and 𝑇2 sees 𝑇1 , 𝑇3 need not see 𝑇1 , which is allowed under RA.
∗ This work was accepted by and will be presented at 1st Symposium on Consistency 1“See” is indicated by the VIS relation between transactions; see Section 3.
Checking Principles (SCCP 2026). 1
Qiuhuan Xiong, Hengfeng Wei, Si Liu, Yuxing Chen, and Jidong Ge
In other words, the visibility requirements imposed on 𝑇4 by CC do not propagate to transactions assigned weaker isolation levels. We address this challenge by specifying, for each transaction, axioms over the set of transactions visible to it, based on its assigned isolation level.
Int(𝑇 ) ≡ ∀𝑟, 𝑥, 𝑣. (𝑟 = R(𝑥, 𝑣) ∧ po𝑥−1 (𝑟 ) ≠ ∅ ) =⇒ max (po𝑥−1 (𝑟 ) ) = _(𝑥, 𝑣). po
Ext(𝑇 ) ≡ ∀𝑥, 𝑣. 𝑇 ⊢ R(𝑥, 𝑣) =⇒ max (VIS −1 (𝑇 ) ∩ WriteTx𝑥 ) ⊢ W(𝑥, 𝑣). AR
Case Studies. Leveraging MixIso, we establish the semantic conformance of two concurrency control protocols: (i) the protocol used in Microsoft SQL Server and Oracle Berkeley DB [4, 16] combining SI and strict two-phase locking (S2PL); and (ii) a new protocol mixing three isolation levels (PC, SI, and SER). Our proofs follow prior construction-based approach [9, 30], and are currently carried out manually.
2
SO
VIS
VIS
VIS
AR
VIS
VIS
AR
VIS
TransVis(𝑇 ) ≡ ∀𝑇 ′ , 𝑆 ∈ T. 𝑇 ′ −−→ 𝑆 −−→ 𝑇 =⇒ 𝑇 ′ −−→ 𝑇 . Prefix(𝑇 ) ≡ ∀𝑇 ′ , 𝑆 ∈ T. 𝑇 ′ −−→ 𝑆 −−→ 𝑇 =⇒ 𝑇 ′ −−→ 𝑇 . NoConflict(𝑇 ) ≡ ∀𝑇 ′ ∈ T. 𝑇 ′ ⊲⊳ 𝑇 ∧ 𝑇 ′ −−→ 𝑇 =⇒ 𝑇 ′ −−→ 𝑇 . AR
VIS
TotalVis(𝑇 ) ≡ ∀𝑇 ′ ∈ T. 𝑇 ′ −−→ 𝑇 =⇒ 𝑇 ′ −−→ 𝑇 .
PRELIMINARIES
Figure 2: Consistency axioms for individual transactions.
Isolation Levels. Databases support a range of isolation levels to accommodate different trade-offs between consistency and performance. These include read atomicity (RA) [5], transactional causal consistency (CC) [2], prefix consistency (PC) [10], parallel snapshot isolation (PSI) [28], snapshot isolation (SI) [6], and serializability (SER) [24]. Appendix A illustrates these isolation levels with examples.
RA(𝑇 ) ≡ Int(𝑇 ) ∧ Ext(𝑇 ) ∧ Session(𝑇 ) CC(𝑇 ) ≡ RA(𝑇 ) ∧ TransVis(𝑇 ) PC(𝑇 ) ≡ RA(𝑇 ) ∧ Prefix(𝑇 ) PSI(𝑇 ) ≡ RA(𝑇 ) ∧ TransVis(𝑇 ) ∧ NoConflict(𝑇 )
Transactions. We consider a transactional key-value store (KVS) managing a set of keys K = {𝑥, 𝑦, 𝑧, . . . } with values from a set V. We denote by Op the set of read and write operations on keys: Op = {R𝜄 (𝑥, 𝑣), W𝜄 (𝑥, 𝑣) | 𝜄 ∈ OpId, 𝑥 ∈ K, 𝑣 ∈ V}, where OpId is the set of operation identifiers (omitted when unimportant). A transaction is a pair (O, po) where O ⊆ Op is a finite non-empty set of operations and po ⊆ O × O is a strict total order called the program order. For 𝑇 = (O, po) and 𝑜 ∈ O on key 𝑥, let po𝑥−1 (𝑜) ≜ {𝑜 ′ ∈ O | 𝑜 ′ =
SI(𝑇 ) ≡ RA(𝑇 ) ∧ Prefix(𝑇 ) ∧ NoConflict(𝑇 ) SER(𝑇 ) ≡ RA(𝑇 ) ∧ TotalVis(𝑇 )
Figure 3: Isolation levels for individual transactions.
T × T is an acyclic relation, and AR ⊆ T × T is a strict total order with VIS ⊆ AR. VIS We write 𝑇 ′ −−→ 𝑇 for (𝑇 ′,𝑇 ) ∈ VIS, and similarly for AR.
po
_(𝑥, _) ∧ 𝑜 ′ −−→ 𝑜 } be the set of operations on 𝑥 preceding 𝑜 in po. We write 𝑇 ⊢ W(𝑥, 𝑣) if 𝑇 writes 𝑣 to 𝑥, and 𝑇 ⊢ R(𝑥, 𝑣) if 𝑇 reads value 𝑣 from 𝑥. Let WriteTx𝑥 ≜ {𝑇 | 𝑇 ⊢ W(𝑥, _)}. Transactions 𝑇 and 𝑇 ′ write-write conflict, written 𝑇 ⊲⊳ 𝑇 ′ , if 𝑇 ,𝑇 ′ ∈ WriteTx𝑥 for some 𝑥.
VIS
VIS
VIS−1 (𝑇 ) ≜ {𝑆 | 𝑆 −−→ 𝑇 } is the visible set of 𝑇 . 𝑇 ′ −−→ 𝑇 abbreviAR
VIS
ates 𝑇 ′ −−→ 𝑇 ∧ ¬(𝑇 ′ −−→ 𝑇 ). Consistency Axioms. An isolation level ℓ for a transaction 𝑇 is specified as a set of axioms constraining its visible set VIS−1 (𝑇 ). The consistency axioms on 𝑇 are shown in Figure 2. A read 𝑟 = R(𝑘, _) of 𝑇 is external if po𝑥−1 (𝑟 ) = ∅ (𝑇 has not previously written to 𝑘), and internal otherwise. Int(𝑇 ) requires 𝑇 to read its own previous writes (internal consistency). Ext(𝑇 ) requires each external read observe the AR-maximal visible write to the same key. Session(𝑇 ) requires 𝑇 to observe all transactions that precede it in session order. TransVis(𝑇 ) makes visibility transitive: if 𝑇 observes 𝑆, it must also observe every transaction observed by 𝑆. Prefix(𝑇 ) forces the visible set of 𝑇 to be a prefix of AR. NoConflict(𝑇 ) forbids write-write conflicts between transactions concurrent with 𝑇 . TotalVis(𝑇 ) requires 𝑇 to observe all of its AR-predecessors.
Histories. Clients interact with the KVS by issuing transactions in sessions. A history records the client-visible outcomes of these interactions. Formally, a history is a triple H = (T , SO, level) where T is a set of transactions with disjoint operation sets, SO ⊆ T × T is the session order (a union of strict total orders, one per session), and level : T → L assigns an isolation level to each transaction. We consider L ≜ {RA, CC, PC, PSI, SI, SER}, ranged over by ℓ. We often write 𝑇 [ℓ] to denote a transaction 𝑇 with level(𝑇 ) = ℓ and call it an ℓ-transaction.
3
VIS
Session(𝑇 ) ≡ ∀𝑇 ′ ∈ T. 𝑇 ′ −−→ 𝑇 =⇒ 𝑇 ′ −−→ 𝑇 .
MIXISO: MIXING ISOLATION LEVELS
This section presents the MixIso semantic framework for mixed isolation levels. At a high level, it extends the (VIS, AR) axiomatic framework in [12] with per-transaction visibility.
Formalizing Mixed Isolation Levels. We now define consistency for abstract executions and histories. An abstract execution X = (T , SO, level, VIS, AR) is consistent if, for each transaction𝑇 ∈ T , all consistency axioms associated with its isolation level level(𝑇 ) hold on 𝑇 . Figure 3 presents the consistency axioms for each isolation level. A history H is then considered consistent if there exists a consistent abstract execution X = (H, VIS, AR).
Abstract Executions. An execution is modeled using two relations over transactions: visibility (VIS), which specifies whose effects are observed by each transaction, and arbitration (AR), which defines a global commit order. Formally, an abstract execution is X = (T , SO, level, VIS, AR), where (T , SO, level) is a history, VIS ⊆ 2
Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels
Table 1: Overview of the construction and verification steps for the two case studies. 𝑇 .sts and 𝑇 .cts denote the start and commit timestamps of transaction 𝑇 , respectively. Proof Step
SI–S2PL (Section 4.2)
PC–SI–SER (Appendix D)
Constructing AR Constructing VIS
Commit timestamp order: 𝑇 ′ .cts < 𝑇 .cts.
Commit timestamp order: 𝑇 ′ .cts < 𝑇 .cts. 𝑇 [ PC ] and 𝑇 [ SI ] read from snapshot 𝑇 .sts > 𝑇 ′ .cts; 𝑇 [ SER ] effectively reads from the latest 𝑇 ′ .cts < 𝑇 .cts due to conflict detection.
𝑇 [ SI ] reads from snapshot 𝑇 .sts > 𝑇 ′ .cts; 𝑇 [ SER ] reads from the latest 𝑇 ′ .cts < 𝑇 .cts.
Verifying weaker axioms Verifying axiom TotalVis
Int, Ext, Session, Prefix, NoConflict: NoConflict enforced by the first-committer-wins rule for SI. TotalVis via S2PL: SER holds exclusive locks until commit, ensuring visibility of all prior commits.
VIS
T1 [PC] W(x, 1)
T3 [PC]
T2 [SI] VIS
R(x, 1) W(y, 2)
VIS
R(x, init) R(y, 2) W(x, 3)
R(x, 3) R(y, 2)
VIS
Definition 3.1. A concurrency control protocol conforms to a set of mixed isolation guarantees if every history it produces is consistent with respect to them. In MixIso, VIS determines visibility on a per-transaction basis, whereas AR provides a shared total order over all transactions. Homogeneous isolation settings correspond to the special case where all transactions are assigned the same isolation level. Thus, MixIso generalizes the framework of [12] (see Appendix B). To validate MixIso, we also establish its equivalence to a recent formalization of mixed isolation levels [8] on their common isolation levels (i.e., RA, PC, SI, and SER); the proof is given in Appendix C. Example. Figures 1 and 4 show two abstract executions. Both VIS
share 𝑇1 [PC] −−→ 𝑇2 [SI] −−→ 𝑇4 [CC] and differ only in level(𝑇3 ). The execution in Figure 1 is consistent as all axioms required by each transaction’s isolation level are satisfied. In contrast, the execution in Figure 4 is inconsistent. 𝑇3 [PC] observes 𝑇2 (via R(𝑦, 2)) but not AR
VIS
4.2
VIS
CHECKING SEMANTIC CONFORMANCE
This section demonstrates how MixIso can be used to establish the semantic conformance of concurrency control protocols to their intended mixed isolation guarantees.
4.1
Case Study: The SI–S2PL Protocol
Algorithm 1 shows the pseudocode of the SI–S2PL protocol. Its key idea is to unify SI (optimistic, snapshot-based) and SER (pessimistic, lock-based) through a versioned store store : K → (T ⇀ V). Transactions of both levels buffer writes locally in 𝑇 .buffer (line 7), obtain commit timestamps (𝑇 .cts) from a shared clock (line 19), and install committed versions into the store at their commit timestamps (line 24). An SI transaction additionally records a start timestamp 𝑇 .sts that defines its snapshot (line 3). During execution, writes are buffered in 𝑇 .buffer (line 7). An SER transaction acquires slock (shared locks) on reads (line 14) and xlock (exclusive locks) on writes (line 6), whereas an SI transaction performs reads without locking and acquires xlock on its write set only during commit (line 18). All locks obey standard compatibility rules and are held until commit (S2PL). For reads, buffered values are returned whenever available (line 10). Otherwise, an SI transaction reads the latest version whose timestamp precedes 𝑇 .sts (line 12), while an SER transaction reads the latest version after acquiring the corresponding shared lock (lines 14–15). At commit, an SI transaction first acquires xlock on its write set (line 18). Both levels then obtain a fresh commit timestamp (line 19). An SI transaction then performs the first-committer-wins check [6] (line 21): if any concurrent transaction 𝑇 ′ whose commit
𝑇1 , which violates Prefix(𝑇3 ) as 𝑇1 −−→ 𝑇2 −−→ 𝑇3 implies 𝑇1 −−→ 𝑇3 .
4
VIS
❷ Verification. We show that the extracted relations satisfy the consistency axioms required by each transaction’s assigned isolation level. Typically, Int(𝑇 ) follows from local write buffering, while Session(𝑇 ), Prefix(𝑇 ), and TransVis(𝑇 ) reduce to reasoning over the construction of VIS. For instance, when VIS is derived from timestamps, these axioms follow from timestamp monotonicity and transitivity. More generally, any construction that derives VIS from a transitive order, e.g., logical clocks, establishes them directly. The main proof obligations are therefore Ext(𝑇 ), showing that each external read observes the AR-maximal visible write, and the level-specific axioms (e.g., NoConflict(𝑇 ) and TotalVis(𝑇 )), which are typically established using protocol-specific mechanisms for conflict detection and resolution. Table 1 outlines these steps for two case studies: the SI–S2PL protocol [4, 16], which mixes SI and SER and is used in Microsoft SQL Server and Oracle Berkeley DB, and a new protocol that combines PC, SI, and SER. In what follows, we focus on the former and defer the latter to Appendix D.
Figure 4: An inconsistent execution: Prefix(𝑇3 ) is violated.
VIS
AR
yielding ∀𝑇 ′ −−→𝑇 =⇒ 𝑇 ′ −−→𝑇 .
VIS from a strict partial order, (ii) from unique commit timestamps, and (iii) from the fact that visibility is bounded by commit order.
T4 [CC] VIS
Int, Ext, Session, Prefix, NoConflict: Prefix required by both PC and SI; NoConflict required only by SI. TotalVis via timestamp ordering: SER reads the latest value of every key,
Proof Approach
Our semantic conformance proof follows prior construction-based approaches [9, 30], which consists of two main steps. ❶ Construction. We extract the VIS and AR relations from the protocol specification, such as its pseudocode or operational semantics. Typically, AR is obtained from the commit order of transactions (e.g., commit timestamps), whereas VIS is derived by a case analysis on level(𝑇 ) to capture the visibility requirements of the corresponding isolation level. After constructing VIS and AR, one must first show that they form a valid abstract execution: (i) VIS is acyclic, (ii) AR is a strict total order, and (iii) VIS ⊆ AR. For example, (i) follows from deriving 3
Qiuhuan Xiong, Hengfeng Wei, Si Liu, Yuxing Chen, and Jidong Ge SO
Algorithm 1 The SI-S2PL protocol [4, 16]
– Session(𝑇 ): 𝑇 ′ −−→ 𝑇 implies that 𝑇 starts after 𝑇 ′ commits. By timestamp monotonicity, 𝑇 ′ .cts < 𝑇 .sts (if SI) or 𝑇 ′ .cts <
store : K → ( T ⇀ V) : versioned KV store, mapping each key to timestamped values 𝑇 .buffer : K ⇀ V: write buffer of transaction 𝑇 1: procedure Start(𝑇 ) 2: if level(𝑇 ) = SI then 3: 𝑇 .sts ← now() 4: procedure Write(𝑇 , 𝑘, 𝑣 ) 5: if level(𝑇 ) = SER then 6: 𝑇 .xlock (𝑘 ) 7: 𝑇 .buffer [𝑘 ] ← 𝑣
VIS
𝑇 .cts (if SER), so 𝑇 ′ −−→ 𝑇 . AR
VIS
– Prefix(𝑇 ) for 𝑇 [SI]: 𝑇 ′ −−→ 𝑆 −−→ 𝑇 implies 𝑇 ′ .cts < 𝑆.cts ⊲ no sts for SER transactions
VIS
and 𝑆.cts < 𝑇 .sts. Hence, 𝑇 ′ .cts < 𝑇 .sts and 𝑇 ′ −−→ 𝑇 . AR – NoConflict(𝑇 ) for 𝑇 [SI]: Let 𝑇 ′ ⊲⊳ 𝑇 with 𝑇 ′ −−→ 𝑇 . If 𝑇 .sts < 𝑇 ′ .cts, then 𝑇 ′ .cts ∈ (𝑇 .sts,𝑇 .cts) and the firstcommitter-wins check (line 21) forces 𝑇 to abort. Hence,
⊲ acquire an exclusive lock on 𝑘 ⊲ buffer 𝑣 and overwrite previous writes to 𝑘
VIS
𝑇 ′ .cts < 𝑇 .sts, yielding 𝑇 ′ −−→ 𝑇 .
8: procedure Read(𝑇 , 𝑘 ) 9: if 𝑘 ∈ dom (𝑇 .buffer ) then ⊲ internal read from my own write 10: return 𝑇 .buffer [𝑘 ] 11: if level(𝑇 ) = SI then ⊲ external read from snapshot 12: return value of store [𝑘 ] at latest timestamp < 𝑇 .sts 13: if level(𝑇 ) = SER then ⊲ external read from latest committed value 14: 𝑇 .slock (𝑘 ) ⊲ acquire a shared lock on 𝑘 15: return value of store [𝑘 ] at latest timestamp
• Verifying Axiom TotalVis(𝑇 ). For level(𝑇 ) = SER, the two AR
construction steps yield 𝑇 ′ −−→ 𝑇 ⇐⇒ 𝑇 ′ .cts < 𝑇 .cts and 𝑇 ′ .cts < VIS
𝑇 .cts ⇐⇒ 𝑇 ′ −−→ 𝑇 , respectively. Hence, VIS−1 (𝑇 ) = AR−1 (𝑇 ), satisfying TotalVis(𝑇 ).
16: procedure Commit(𝑇 ) 17: if level(𝑇 ) = SI then 18: 𝑇 .xlock (𝑘 ), ∀𝑘 ∈ dom (𝑇 .buffer ) ⊲ acquire exclusive locks 19: 𝑇 .cts ← now() ⊲ level(𝑇 ) ∈ { SI, SER } 20: if level(𝑇 ) = SI then ⊲ level(𝑇 ′ ) ∈ { SI, SER } ′ ′ 21: if ∃𝑇 ⊲⊳ 𝑇 . 𝑇 .cts ∈ (𝑇 .sts,𝑇 .cts) then 22: 𝑇 .unlocks ( ) 23: return aborted 24: store [𝑘 ] ← [𝑇 .cts ↦→ 𝑣 ] for all [𝑘 ↦→ 𝑣 ] ∈ 𝑇 .buffer ⊲ install writes 25: 𝑇 .unlocks ( ) ⊲ level(𝑇 ) ∈ { SI, SER } 26: return committed
The full proof is given in Appendix E.
5
FUTURE WORK
We have presented MixIso for reasoning about mixed isolation levels and demonstrated its applicability through two case studies. MixIso is designed as a general semantic framework. It can also be used to verify the semantic conformance of concurrency control protocols under homogeneous isolation settings. Our proofs currently rely on manual reasoning; automating the verification process is a natural next step. In addition, MixIso can support a variety of other applications. These include (i) black-box testing of mixed isolation guarantees [8] (e.g., by deriving a dependency-graph-based characterization in the style of [13] that is equivalent to MixIso), (ii) robustness checking [16] for safely allocating a wide range of different isolation levels across transaction workloads (e.g., by following the approach in [7]), and (iii) adaptive concurrency control [33] (e.g., by extending robustness checking to online settings).
timestamp lies in (𝑇 .sts,𝑇 .cts) wrote to a key in 𝑇 ’s write set, then 𝑇 aborts. An SER transaction skips this check, as conflicting writes are already prevented by exclusive locks. Finally, the buffered writes are installed into the store and all locks are released (lines 24–25). Theorem 4.1. Algorithm 1 conforms to the mixed isolation guarantees of SI and SER. Proof Sketch. We follow the proof steps shown in Table 1. AR
• Constructing AR. AR follows commit-timestamp order: 𝑇 ′ −−→ 𝑇 ⇐⇒ 𝑇 ′ .cts < 𝑇 .cts. Since commit timestamps are unique and strictly increasing, AR is a strict total order.
REFERENCES [1] A. Adya. 1999. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. Ph.D. Dissertation. Massachusetts Institute of Technology, USA. [2] Deepthi Devaki Akkoorath, Alejandro Z. Tomsic, Manuel Bravo, Zhongmiao Li, Tyler Crain, Annette Bieniusa, Nuno M. Preguiça, and Marc Shapiro. 2016. Cure: Strong Semantics Meets High Availability and Low Latency. In ICDCS 2016. IEEE Computer Society, 405–414. https://doi.org/10.1109/ICDCS.2016.98 [3] Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, and Lars Birkedal. 2025. Reasoning about Weak Isolation Levels in Separation Logic. Proc. ACM Program. Lang. 9, ICFP, Article 246 (Aug. 2025), 35 pages. https: //doi.org/10.1145/3747515 [4] Mohammad Alomari, Michael Cahill, Alan Fekete, and Uwe Röhm. 2008. Serializable Executions with Snapshot Isolation: Modifying Application Code or Mixing Isolation Levels?. In DASFAA 2008, Vol. 4947. 267–281. https: //doi.org/10.1007/978-3-540-78568-2_21 [5] Peter Bailis, Alan Fekete, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. 2016. Scalable Atomic Visibility with RAMP Transactions. ACM Trans. Database Syst. 41, 3 (July 2016), 15:1–15:45. https://doi.org/10.1145/2909870 [6] Hal Berenson, Phil Bernstein, Jim Gray, Jim Melton, Elizabeth O’Neil, and Patrick O’Neil. 1995. A critique of ANSI SQL isolation levels. SIGMOD Rec. 24, 2 (May 1995), 1–10. https://doi.org/10.1145/568271.223785 [7] Giovanni Bernardi and Alexey Gotsman. 2016. Robustness against Consistency Models with Atomic Visibility. In CONCUR 2016, Vol. 59. 7:1–7:15. https://doi. org/10.4230/LIPIcs.CONCUR.2016.7 [8] Ahmed Bouajjani, Constantin Enea, and Enrique Román-Calvo. 2025. On the Complexity of Checking Mixed Isolation Levels for SQL Transactions. In CAV 2025, Vol. 15934. 315–337. https://doi.org/10.1007/978-3-031-98685-7_15
• Constructing VIS. VIS is obtained by a case analysis on level(𝑇 ): VIS
𝑇 ′ −−→ 𝑇 ⇐⇒ (level(𝑇 ) = SI ∧ 𝑇 ′ .cts < 𝑇 .sts) ∨ (level(𝑇 ) = SER ∧ 𝑇 ′ .cts < 𝑇 .cts). For SI, VIS captures the snapshot at 𝑇 .sts (line 12). For SER, VIS includes all prior commits (line 15) using 𝑇 ′ .cts < 𝑇 .cts rather than 𝑇 ′ .cts < 𝑇 .sts so that every AR-predecessor of 𝑇 is visible. By construction, VIS is irreflexive and VIS ⊆ AR. • Verifying Weaker Axioms. – Int(𝑇 ) follows from the local write buffer (line 10). – Ext(𝑇 ): For 𝑇 [SI], the snapshot read (line 12) returns the version with the largest timestamp below 𝑇 .sts, i.e., maxAR (VIS−1 (𝑇 ) ∩ WriteTx𝑥 ). For 𝑇 [SER], 𝑇 acquires slock before reading the latest value (line 14) and holds it until commit. Hence, no transaction can install a later version of 𝑥 before 𝑇 commits, so the read returns the AR-maximal visible writer. 4
Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels
[9] Sebastian Burckhardt. 2014. Principles of Eventual Consistency. Foundations and Trends in Programming Languages 1, 1-2 (Oct. 2014), 1–150. https://doi.org/ 10.1561/2500000011 [10] Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich. 2015. Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. In ECOOP 2015, Vol. 37. 568–590. https://doi.org/10.4230/LIPIcs.ECOOP.2015.568 [11] Oracle Help Center. Accessed in December 2025. Data Concurrency and Consistency. https://docs.oracle.com/en/database/oracle/oracle-database/23/cncpt/ data-concurrency-and-consistency.html. [12] Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. 2015. A Framework for Transactional Consistency Models with Atomic Visibility. In CONCUR 2015, Vol. 42. 58–71. https://doi.org/10.4230/LIPIcs.CONCUR.2015.58 [13] Andrea Cerone and Alexey Gotsman. 2018. Analysing Snapshot Isolation. J. ACM 65, 2, Article 11 (Jan 2018), 41 pages. https://doi.org/10.1145/3152396 [14] CockroachDB. Accessed in December, 2025. CockroachDB Docs - SET TRANSACTION. https://www.cockroachlabs.com/docs/stable/set-transaction. [15] Natacha Crooks, Youer Pu, Lorenzo Alvisi, and Allen Clement. 2017. Seeing is Believing: A Client-Centric Specification of Database Isolation. In PODC’17. ACM, 73–82. https://doi.org/10.1145/3087801.3087802 [16] Alan Fekete. 2005. Allocating isolation levels to transactions. In PODS 2005. 206–215. https://doi.org/10.1145/1065167.1065193 [17] Shabnam Ghasemirad, Si Liu, Christoph Sprenger, Luca Multazzu, and David Basin. 2025. VerIso: Verifiable Isolation Guarantees for Database Transactions. Proc. VLDB Endow. 18, 5 (2025), 1362–1375. https://doi.org/10.14778/3718057. 3718065 [18] Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu, and David Basin. 2025. Pushing the Limit: Verified Performance-Optimal CausallyConsistent Database Transactions. In TACAS 2025. Springer-Verlag, Berlin, Heidelberg, 43–62. https://doi.org/10.1007/978-3-031-90660-2_3 [19] Si Liu. 2022. All in One: Design, Verification, and Implementation of SNOWoptimal Read Atomic Transactions. ACM Trans. Softw. Eng. Methodol. 31, 3, Article 43 (March 2022), 44 pages. https://doi.org/10.1145/3494517 [20] Si Liu, Luca Multazzu, Hengfeng Wei, and David A. Basin. 2024. NOC-NOC: Towards Performance-optimal Distributed Transactions. Proc. ACM Manag. Data 2, 1, Article 9 (March 2024), 25 pages. https://doi.org/10.1145/3639264 [21] Si Liu, Peter Csaba Ölveczky, Qi Wang, Indranil Gupta, and José Meseguer. 2019. Read atomic transactions with prevention of lost updates: ROLA and its formal analysis. Formal Aspects Comput. 31, 5 (2019), 503–540. https://doi.org/10.1007/ S00165-019-00489-W [22] Si Liu, Peter Csaba Ölveczky, Min Zhang, Qi Wang, and José Meseguer. 2019. Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude. In TACAS 2019 (LNCS), Vol. 11428. Springer, 40–57. https://doi.org/10. 1007/978-3-030-17465-1_3 [23] MySQL. Accessed in December, 2025. MySQL 8.4 Reference Manual - Transaction Isolation Levels. https://dev.mysql.com/doc/refman/8.4/en/innodb-transactionisolation-levels.html. [24] Christos H. Papadimitriou. 1979. The Serializability of Concurrent Database Updates. J. ACM 26, 4 (Oct. 1979), 631–653. https://doi.org/10.1145/322154.322158 [25] PostgreSQL. Accessed in December, 2025. PostgreSQL Documentation - Transaction Isolation. https://www.postgresql.org/docs/17/transaction-iso.html. [26] William Schultz and Murat Demirbas. 2025. Design and Modular Verification of Distributed Transactions in MongoDB. Proc. VLDB Endow. 18, 12 (Aug. 2025), 5045–5058. https://doi.org/10.14778/3750601.3750626 [27] SQL Server. Accessed in December, 2025. SET TRANSACTION ISOLATION LEVEL (Transact-SQL). https://learn.microsoft.com/en-us/sql/t-sql/statements/ set-transaction-isolation-level-transact-sql?view=sql-server-ver17. [28] Yair Sovran, Russell Power, Marcos K. Aguilera, and Jinyang Li. 2011. Transactional storage for geo-replicated systems. In SOSP ’11. 385–400. https: //doi.org/10.1145/2043556.2043592 [29] TiDB. Accessed in December, 2025. TiDB Transaction Isolation Levels. https: //docs.pingcap.com/tidb/stable/transaction-isolation-levels/. [30] Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner. 2020. Data Consistency in Transactional Storage Systems: A Centralised Semantics. In ECOOP 2020, Vol. 166. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 21:1–21:31. https://doi.org/10.4230/LIPIcs.ECOOP.2020.21 [31] YugabyteDB. Accessed in December, 2025. YugabyteDB Docs - Isolation Levels. https://docs.yugabyte.com/preview/explore/transactions/isolation-levels/. [32] Irene Zhang, Naveen Kr. Sharma, Adriana Szekeres, Arvind Krishnamurthy, and Dan R. K. Ports. 2018. Building Consistent Transactions with Inconsistent Replication. ACM Trans. Comput. Syst. 35, 4, Article 12 (Dec. 2018), 37 pages. https://doi.org/10.1145/3269981 [33] Qiyu Zhuang, Wei Lu, Shuang Liu, Yuxing Chen, Xinyue Shi, Zhanhao Zhao, Yipeng Sun, Anqun Pan, and Xiaoyong Du. 2025. TxnSails: Achieving Serializable Transaction Scheduling with Self-Adaptive Isolation Level Selection. In Proceedings of the VLDB Endowment (VLDB), Vol. 18. 4227–4240. https: //doi.org/10.14778/3749646.3749689
5
Qiuhuan Xiong, Hengfeng Wei, Si Liu, Yuxing Chen, and Jidong Ge
A
Proof. We only need to show that for any abstract execution X = (T , SO, level, VIS, AR), X ′ ≜ (T , SO, VIS, AR) |= NoConflict if and only if ∀𝑇 ∈ T . X |= NoConflict(𝑇 ) under the condition that level(𝑇 ) ∈ {PSI, SI, SER} for all 𝑇 ∈ T . Other consistency axioms correspond directly between mixed isolation levels and traditional isolation levels and thus the proof is omitted here. • The “ =⇒ ” direction. Suppose that X ′ |= NoConflict. Consider any transactions 𝑇 ,𝑇 ′ ∈ T such that 𝑇 ′ ⊲⊳ 𝑇 and
ISOLATION LEVELS
Read Atomicity (RA) [5] guarantees that if a transaction observes any update from another transaction, it must observe all updates from that transaction. In particular, it rules out fractured reads, e.g., Joey sees that Ross has added Rachel as a friend, but fails to observe Rachel’s addition of Ross, resulting in an inconsistent view of a bi-directional friendship. Transactional Causal Consistency (CC) [2] ensures that if a transaction 𝑇 ′ causally depends on another transaction 𝑇 (e.g., 𝑇 ′ reads a value written by 𝑇 ), then any transaction that observes 𝑇 ′ must also observe 𝑇 . For example, under CC, Ross observing the comment written by Rachel on Joey’s post without seeing the post itself is not allowed.
AR
NoConflict(𝑇 ) holds for 𝑇 . Now suppose that 𝑇 ′ −−→ 𝑇 . VIS We need to show that 𝑇 ′ −−→ 𝑇 holds. Suppose by contra-
diction that VIS
¬(𝑇 ′ −−→ 𝑇 ). ′ Since X |= NoConflict, we have
Prefix Consistency (PC) [10] strengthens CC by ensuring that concurrent transactions are not observed in different orders, which is illustrated by the long-fork anomaly:
VIS
Therefore, we have VIS
𝑇 −−→ 𝑇 ′ .
𝑇1 : W(𝑥, 1) 𝑇3 : R(𝑥, 1), R(𝑦, ⊥) 𝑇2 : W(𝑦, 2) 𝑇4 : R(𝑥, ⊥), R(𝑦, 2)
Since VIS ⊆ AR, we have AR
where 𝑇3 and 𝑇4 observe incompatible prefixes of the commit order. Equivalently, under PC, every transaction must observe a prefix of the global commit order.
𝑇 −−→ 𝑇 ′ . AR
This contradicts the assumption that 𝑇 ′ −−→ 𝑇 . Hence, VIS 𝑇 ′ −−→ 𝑇 holds, and thus X |= NoConflict(𝑇 ).
Parallel Snapshot Isolation (PSI) [28] also strengthens CC, but in a different way. In particular, PSI forbids lost updates, where concurrent transactions overwrite each other’s updates, e.g., when two transactions deposit money into the same bank account at the same time, but one deposit is lost because it is overwritten by the other. Unlike PC, PSI still allows long-fork anomalies.
• The “ ⇐= ” direction. Suppose that X |= NoConflict(𝑇 ) for all 𝑇 ∈ T with level(𝑇 ) ∈ {PSI, SI, SER}. Consider any transactions 𝑇 ,𝑇 ′ ∈ T such that 𝑇 ′ ⊲⊳ 𝑇 . We need to show that VIS VIS 𝑇 ′ −−→ 𝑇 ∨ 𝑇 −−→ 𝑇 ′ . Suppose by contradiction that
Snapshot Isolation (SI) [6] further enhances both PSI and PC by ruling out long forks and lost updates. In particular, in the earlier example, even if transactions 𝑇3 and 𝑇4 execute on different database replicas, they must observe a convergent snapshot of the database state. However, SI allows the write skew anomaly:
VIS
VIS
¬(𝑇 ′ −−→ 𝑇 ) ∧ ¬(𝑇 −−→ 𝑇 ′ ). Since ∀𝑇 ∈ T . X |= NoConflict(𝑇 ), we have that X |= NoConflict(𝑇 ) ∧ X |= NoConflict(𝑇 ′ ). AR
𝑇1 : R(a1, 10), R(a2, 10), W(a1, −15)
Suppose without loss of generality that 𝑇 ′ −−→ 𝑇 . Then, by X |= NoConflict(𝑇 ), we have
𝑇2 : R(a1, 10), R(a2, 10), W(a2, −15),
VIS
𝑇 ′ −−→ 𝑇 ,
where both transactions check whether the total balance of the two bank accounts exceeds $20 before withdrawing $15 from one of them. When executed concurrently, both checks succeed, resulting in a negative total balance.
VIS
VIS
which contradicts the assumption. Hence, 𝑇 ′ −−→ 𝑇 ∨𝑇 −−→ 𝑇 ′ holds, and thus X ′ |= NoConflict. □
Serializability (SER) [24] forbids all of the above anomalies. It requires every concurrent transaction execution to be equivalent to some serial order of those transactions.
B
VIS
𝑇 ′ −−→ 𝑇 ∨ 𝑇 −−→ 𝑇 ′ .
C
EQUIVALENCE BETWEEN MIXISO AND THE FRAMEWORK OF [8]
Recently, Bouajjani et al. [8] proposed an axiomatic semantics for mixed isolation levels. To validate our MixIso, we establish its equivalence to that semantics on their common isolation levels, namely RA, PC, SI, and SER.
GENERALIZING THE FRAMEWORK OF [12]
Homogeneous isolation settings correspond to the special case where all transactions are assigned the same isolation level. In this section, we prove that MixIso generalizes the framework of [12]. Tables 2 and 3 summarize the isolation levels and their corresponding consistency axioms defined in that framework.
Definition C.1 (Histories in [8]). A history h = (T , SO, level, WR) is a set T of transactions along with a strict partial session order SO ⊆ T ×T , an allocation function level : T → L, and a write-read relation WR : K → 2 T × T such that (∃! means “unique existence”):
Theorem B.1. For any history H = (T , SO, level) and traditional isolation level ℓ, (T , SO) |= ℓ iff H is consistent under mixed isolation level where ∀𝑇 ∈ T . level(𝑇 ) = ℓ.
WR(𝑥 )
• ∀𝑥 ∈ K, 𝑆 ∈ T . 𝑆 ⊢ R(𝑥, _) =⇒ ∃! 𝑇 ∈ T . 𝑇 −−−−−→ 𝑆. 6
Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels
Table 2: Consistency axioms that constrain an abstract execution X = (T , SO, VIS, AR).
∀𝑇 ∈ T . ∀𝑟, 𝑥, 𝑣. (𝑟 = R(𝑥, 𝑣) ∧ po𝑥−1 (𝑟 ) ≠ ∅) =⇒ max (po𝑥−1 (𝑟 )) = _(𝑥, 𝑣).
(Int)
po
−1
∀𝑇 ∈ T . ∀𝑥, 𝑣. 𝑇 ⊢ R(𝑥, 𝑣) =⇒ max (VIS (𝑇 ) ∩ WriteTx𝑥 ) ⊢ W(𝑥, 𝑣)
(Ext)
AR
SO ⊆ VIS ∀𝑇 ,𝑇 ′ ∈ T . 𝑇 ⊲⊳ 𝑇 ′
(Session) =⇒
VIS
VIS (𝑇 −−→ 𝑇 ′ ∨ 𝑇 ′ −−→ 𝑇 ) (NoConflict)
Table 3: Isolation levels defined by consistency axioms in Table 2. RA ≡ Int ∧ Ext ∧ Session
CC ≡ RA ∧ TransVis
PC ≡ RA ∧ Prefix
PSI ≡ RA ∧ TransVis ∧ NoConflict
SI ≡ RA ∧ Prefix ∧ NoConflict
SER ≡ RA ∧ TotalVis
VIS ; VIS ⊆ VIS (TransVis)
AR ; VIS ⊆ VIS (Prefix)
AR ⊆ VIS
(TotalVis)
A history h is called consistent if there exists a consistent abstract execution 𝜉 = (h, WR, CO) for h. The equivalence between our framework and that of Bouajjani et al. [8] is established as follows. Theorem C.5. Let h = (T , SO, level, WR) be a history in Bouajjani et al.’s framework and H = (T , SO, level) be the corresponding history in our framework. Then, h is consistent iff H is consistent. Proof of Theorem C.5. Suppose that ℎ = (T , SO, level, WR) is a history in Bouajjani et al.’s framework, and H = (T , SO, level) is the corresponding history in our framework. On the one hand, we show that if h is consistent, then H is consistent. Since h is consistent, by Definition C.4, there exists an abstract execution 𝜉 = (T , SO, level, WR, CO) such that for every transaction 𝑇 ∈ T , the consistency axioms corresponding to its isolation level level(𝑇 ) hold on 𝑇 . Now, we need to construct an abstract execution X = (H, VIS, AR) such that for every transaction 𝑇 ∈ T , the consistency axioms corresponding to its isolation level level(𝑇 ) in our framework hold on 𝑇 . To this end, we define AR = CO and VIS as in Figure 6. For X to be a valid abstract execution, we need to show that • AR is a strict total order. This holds since AR = CO, which is a strict total order by Definition C.2. • VIS ⊆ AR. We distinguish cases based on the isolation level of 𝑇 and its construction of VIS, and show that VIS ⊆ AR holds in each case. – Case level(𝑇 ) = RA. By the construction of VIS for level(𝑇 ) = RA in Figure 6, we need to show that
WR(𝑥 )
• ∀𝑥 ∈ K. ∀𝑇 , 𝑆 ∈ T . 𝑇 −−−−−→ 𝑆 =⇒ ∃𝑣 ∈ V. 𝑇 ≠ 𝑆 ∧ 𝑇 ⊢ W(𝑥, 𝑣) ∧ 𝑆 ⊢ W(𝑥, 𝑣). • (SO ∪ WR) is acyclic. For notational simplicity, Bouajjani et al.’s framework makes the following standard assumptions about histories. • OneWrite: Each transaction contains at most one write operation per key. • RYW: A read operation preceded by write operations on the same key returns the value written by the last preceding write to this key in the transaction. • InitTran: Each history contains a special transaction that writes initial value init to all keys. This transaction precedes all the other transactions in SO. Definition C.2 (Abstract Executions in [8]). An abstract execution 𝜉 = (T , SO, level, WR, CO) is a history h = (T , SO, level, WR) along with a strict total order CO ⊆ T × T called commit order such that (SO ∪ WR) ⊆ CO. Definition C.3 (Consistency Axioms for Individual Transactions in [8]). Let 𝜉 = (T , SO, level, WR, CO) be an abstract execution and 𝑇 ∈ T be a transaction. The consistency axioms for individual transactions are defined as in Figure 5.
(SO ∪ WR) ⊆ AR. This holds due to (SO ∪ WR) ⊆ CO (Definition C.2) and the fact that AR = CO. – Case level(𝑇 ) = PC. By the construction of VIS for level(𝑇 ) = PC in Figure 6, we need to show that
Read Atomic (ReadAtomic(𝑇 )), Prefix (Prefix(𝑇 )), and Serializability (Serializability(𝑇 )) axioms are defined using their homonymous axioms, and Snapshot Isolation (SnapshotIsolation(𝑇 )) is defined as a conjunction of Prefix(𝑇 ) and Conflict(𝑇 ). Note that the framework of Bouajjani et al. does not include the Causal(𝑇 ) axiom and, consequently, does not capture the CC or PSI isolation levels. Therefore, in the following equivalence theorem, we only consider the isolation levels in {RA, PC, SI, SER}. The notion of “consistent abstract executions” and “consistent histories” are defined in the same way as in our framework.
CO∗ ; (SO ∪ WR) ⊆ AR. This holds since (SO ∪ WR) ⊆ AR by Case level(𝑇 ) = RA and AR = CO is a strict total order. – Case level(𝑇 ) = SI. By the construction of VIS for level(𝑇 ) = SI in Figure 6, we need to show that CO
CO∗ ; (SO ∪ WR ∪ {(𝑇1,𝑇2 ) | 𝑇1 −−→ 𝑇2 ∧ 𝑇1 ⊲⊳ 𝑇2 }) ⊆ AR. This holds since (SO ∪ WR) ⊆ AR by Case level(𝑇 ) = RA and AR = CO is a strict total order. – Case level(𝑇 ) = SER. By the construction of VIS for level(𝑇 ) = SER in Figure 6, we need to show that
Definition C.4 (Consistent Histories in [8]). An abstract execution 𝜉 = (T , SO, level, WR, CO) is called consistent if for each transaction 𝑇 ∈ T , the consistency axioms corresponding to its isolation level level(𝑇 ) hold on 𝑇 .
CO ⊆ AR. 7
Qiuhuan Xiong, Hengfeng Wei, Si Liu, Yuxing Chen, and Jidong Ge
ReadAtomic(𝑇 ) ≡ ∀𝑥 ∈ K. ∀𝑇1,𝑇2 ∈ T . WR(𝑥 )
𝑇1 ≠ 𝑇2 ∧ 𝑇1 −−−−−→ 𝑇 ∧ 𝑇2 ∈ WriteTx𝑥 ∧ SO ∪ WR
CO
𝑇2 −−−−−−−→ 𝑇 =⇒ 𝑇2 −−→ 𝑇1 . Prefix(𝑇 ) ≡ ∀𝑥 ∈ K. ∀𝑇1,𝑇2 ∈ T . WR(𝑥 )
𝑇1 ≠ 𝑇2 ∧ 𝑇1 −−−−−→ 𝑇 ∧ 𝑇2 ∈ WriteTx𝑥 ∧ CO∗ ; (SO ∪ WR)
CO
𝑇2 −−−−−−−−−−−−−→ 𝑇 =⇒ 𝑇2 −−→ 𝑇1 . Conflict(𝑇 ) ≡ ∀𝑥 ∈ K. ∀𝑇1,𝑇2,𝑇3 ∈ T . WR(𝑥 )
𝑇1 ≠ 𝑇2 ∧ 𝑇1 −−−−−→ 𝑇 ∧ 𝑇2 ∈ WriteTx𝑥 ∧ CO∗
CO
CO
𝑇3 ⊲⊳ 𝑇 ∧ 𝑇2 −−−→ 𝑇3 −−→ 𝑇 =⇒ 𝑇2 −−→ 𝑇1 . SnapshotIsolation(𝑇 ) ≡ Prefix(𝑇 ) ∧ Conflict(𝑇 ). WR(𝑥 )
CO
CO
Serializability(𝑇 ) ≡ ∀𝑥 ∈ K. ∀𝑇1,𝑇2 ∈ T . 𝑇1 ≠ 𝑇2 ∧ 𝑇1 −−−−−→ 𝑇 ∧ 𝑇2 ∈ WriteTx𝑥 ∧ 𝑇2 −−→ 𝑇 =⇒ 𝑇2 −−→ 𝑇1 . Figure 5: Consistency axioms for individual transactions in the framework of Bouajjani et al. [8]. VIS
∀𝑆,𝑇 ∈ T . 𝑆 −−→ 𝑇 ⇐⇒ SO ∪ WR
(level(𝑇 ) = RA ∧ 𝑆 −−−−−−−→ 𝑇 ) ∨
(1)
CO∗ ; (SO ∪ WR)
(level(𝑇 ) = PC ∧ 𝑆 −−−−−−−−−−−−−→ 𝑇 ) ∨
(2) CO
−−→ 𝑇2 ∧ 𝑇1 ⊲⊳ 𝑇2 } ) (level(𝑇 ) = SI ∧ 𝑆 −−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−→ 𝑇 ) ∨ CO∗ ; (SO ∪ WR ∪ { (𝑇1 ,𝑇2 ) | 𝑇1
(3)
CO
(level(𝑇 ) = SER ∧ 𝑆 −−→ 𝑇 ).
(4)
Figure 6: Definition of VIS in terms of SO, WR, and CO in the framework of Bouajjani et al. [8]. This holds since AR = CO. • VIS is acyclic. This holds since VIS ⊆ AR and AR is acyclic.
𝑟 read the value written by that write operation, Since 𝑟 = R(𝑥, 𝑣), we have 𝑜 = R(𝑥, 𝑣) as well. Second, suppose there is no such a write operation, we show that both 𝑜 and 𝑟 must read from the same transaction. Suppose not, i.e., there ex-
In the following, we show that for every transaction 𝑇 ∈ T , the consistency axioms of our framework corresponding to its isolation level level(𝑇 ) hold on 𝑇 .
WR(𝑥 )
ists transactions 𝑇1 ≠ 𝑇2 such that 𝑇1 −−−−−→ 𝑇 WR(𝑥 )
• Case level(𝑇 ) = RA. Since 𝜉 is consistent, ReadAtomic(𝑇 ) holds. – Int(𝑇 ). Consider any internal read 𝑟 = R(𝑥, 𝑣) in 𝑇 for some 𝑥 and 𝑣. If 𝑟 does not exists, Int(𝑇 ) holds trivially. Otherwise, let 𝑜 ≜ maxpo (po𝑥−1 (𝑟 )) be the last operation on 𝑥 before 𝑟 in 𝑇 . We show that 𝑜 = _(𝑥, 𝑣), by distinguishing two cases depending on the type of 𝑜: ∗ 𝑜 is a write operation. By the RYW assumption about histories, 𝑟 reads the value written by 𝑜. Thus, 𝑜 = W(𝑥, 𝑣). ∗ 𝑜 is a read operation. By the choise of 𝑜, there is no write operation on 𝑥 between 𝑜 and 𝑟 in 𝑇 . We then distinguish two sub-cases depending on whether there is a write operation on 𝑥 in 𝑇 before 𝑜. First, suppose there is such a write operation, then by OneWrite and RYW, both 𝑜 and
and 𝑇2 −−−−−→ 𝑇 . By ReadAtomic(𝑇 ), we have CO
CO
𝑇1 −−→ 𝑇2 ∧ 𝑇2 −−→ 𝑇1 . Therefore, CO is cyclic, contradicting the fact that CO is a strict total order. Thus, there exists a unique transaction 𝑇 ′ such that both 𝑜 and 𝑟 read from𝑇 ′ . By OneWrite for 𝑇 ′ and 𝑟 = R(𝑥, 𝑣), we have 𝑜 = R(𝑥, 𝑣). – Ext(𝑇 ). Consider any external read 𝑟 = R(𝑥, 𝑣) in 𝑇 for some 𝑥 and 𝑣. If 𝑟 does not exists, Ext(𝑇 ) holds trivially. Otherwise, let 𝑇1 be the unique transaction such that WR(𝑥 )
𝑇1 ⊢ W(𝑥, 𝑣) ∧ 𝑇1 −−−−−→ 𝑇 . Hence, by the construction of VIS for level(𝑇 ) = RA, 𝑇1 ∈ (VIS−1 (𝑇 ) ∩ WriteTx𝑥 ). 8
Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels
• Case level(𝑇 ) = SER. Int(𝑇 ), Ext(𝑇 ), and Session(𝑇 ) hold by similar reasoning as in the case of level(𝑇 ) = RA. In the following, we show that TotalVis(𝑇 ) holds. Consider any 𝑇 ′ ∈ T such that
Consider any 𝑇2 ∈ T such that −1
𝑇1 ≠ 𝑇2 ∧ 𝑇2 ∈ (VIS (𝑇 ) ∩ WriteTx𝑥 ). That is,
AR
SO ∪ WR
𝑇 ′ −−→ 𝑇 .
𝑇1 ≠ 𝑇2 ∧ 𝑇2 ∈ WriteTx𝑥 ∧ 𝑇2 −−−−−−−→ 𝑇 .
By the construction of AR for level(𝑇 ) = SER,
By ReadAtomic(𝑇 ), we have
CO
CO
𝑇 ′ −−→ 𝑇 .
𝑇2 −−→ 𝑇1 .
By the construction of VIS for level(𝑇 ) = SER,
That is, AR
VIS
𝑇 ′ −−→ 𝑇 .
𝑇2 −−→ 𝑇1 . Therefore,
Therefore, TotalVis(𝑇 ) holds. On the other hand, we show that if H is consistent, then h is consistent. Since H is consistent, there exists an abstract execution X = (H, VIS, AR) such that for every transaction 𝑇 ∈ T , the consistency axioms corresponding to its isolation level level(𝑇 ) in our framework hold on𝑇 . By Definition C.4, we need to construct an abstract execution 𝜉 = (T , SO, level, WR, CO) such that for every transaction 𝑇 ∈ T , the consistency axioms corresponding to its isolation level level(𝑇 ) in Bouajjani et al.’s framework hold on 𝑇 . To this end, we define CO = AR, which is a strict total order. By Ext(𝑇 ), we define WR(𝑥) like:
−1
𝑇1 = max (VIS (𝑇 ) ∩ WriteTx𝑥 ). AR
Hence, Ext(𝑇 ) holds. SO
– Session(𝑇 ). Consider any 𝑇 ′ ∈ T such that 𝑇 ′ −−→ 𝑇 . By construction of VIS for level(𝑇 ) = RA, we have VIS
𝑇 ′ −−→ 𝑇 . • Case level(𝑇 ) = PC. Int(𝑇 ), Ext(𝑇 ), and Session(𝑇 ) hold by similar reasoning as in the case of level(𝑇 ) = RA. In the following, we show that Prefix(𝑇 ) holds. Consider any 𝑇1,𝑇2 ∈ T such that AR
WR(𝑥 )
VIS
𝑇 ′ −−−−−→ 𝑇 ⇐⇒ 𝑇 ′ = max (VIS−1 (𝑇 ) ∩ WriteTx𝑥 ). AR Ð and then WR = 𝑥 ∈K WR(𝑥). For 𝜉 to be a valid abstract execution, we need to show that
𝑇1 −−→ 𝑇2 −−→ 𝑇 . By the construction of VIS and AR for level(𝑇 ) = PC, CO∗ ; (SO ∪ WR)
CO
𝑇1 −−→ 𝑇2 −−−−−−−−−−−−−→ 𝑇 .
(SO ∪ WR) ⊆ CO.
That is, CO∗
CO
First, by the definition of WR(𝑥) above, we have
SO ∪ WR
∃𝑇3 ∈ T . 𝑇1 −−→ 𝑇2 −−−→ 𝑇3 −−−−−−−→ 𝑇 .
WR ⊆ VIS.
Since CO is transitive, we have CO
Since VIS ⊆ AR and CO = AR, we have
SO ∪ WR
𝑇1 −−→ 𝑇3 −−−−−−−→ 𝑇 .
WR ⊆ CO.
Hence, by the construction of VIS for level(𝑇 ) = PC,
Since is an abstract execution and all consistency levels we consider enforces SO(𝑇 ), we have
VIS
𝑇1 −−→ 𝑇 .
SO ⊆ AR = CO.
Therefore, Prefix(𝑇 ) holds. • Case level(𝑇 ) = SI. Int(𝑇 ), Ext(𝑇 ), Session(𝑇 ), and Prefix(𝑇 ) hold by similar reasoning as in the case of level(𝑇 ) = PC. In the following, we show that NoConflict(𝑇 ) holds. Consider any 𝑇 ′ ∈ T such that
Therefore, we have (SO ∪ WR) ⊆ CO. In the following, we show that for every transaction 𝑇 ∈ T , the consistency axioms of the framework of Bouajjani et al. corresponding to its isolation level level(𝑇 ) hold on 𝑇 . • Case level(𝑇 ) = RA. Since H is consistent, Int(𝑇 ), Ext(𝑇 ), and Session(𝑇 ) hold. We need to show that ReadAtomic(𝑇 ) holds. Consider any 𝑇1,𝑇2 ∈ T such that for some 𝑥,
AR
𝑇 ′ ⊲⊳ 𝑇 ∧ 𝑇 ′ −−→ 𝑇 . By the construction of AR for level(𝑇 ) = SI, CO
𝑇 ′ ⊲⊳ 𝑇 ∧ 𝑇 ′ −−→ 𝑇 .
WR(𝑥 )
SO ∪ WR
𝑇1 ≠ 𝑇2 ∧ 𝑇1 −−−−−→ 𝑇 ∧ 𝑇2 ∈ WriteTx𝑥 ∧ 𝑇2 −−−−−−−→ 𝑇 .
That is,
WR(𝑥 )
CO
By Ext(𝑇 ) and 𝑇1 −−−−−→ 𝑇 , we have
′ { (𝑇1 ,𝑇2 ) | 𝑇1 −−→ 𝑇2 ∧ 𝑇1 ⊲⊳ 𝑇2 }
𝑇 −−−−−−−−−−−−−−−−−−−−−−−−−→ 𝑇 .
𝑇1 = max (VIS−1 (𝑇 ) ∩ WriteTx𝑥 ).
By the construction of VIS for level(𝑇 ) = SI,
AR
SO ∪ WR
VIS
By Session(𝑇 ), Ext(𝑇 ), and 𝑇2 −−−−−−−→ 𝑇 , we have
𝑇 ′ −−→ 𝑇 .
VIS
Therefore, NoConflict(𝑇 ) holds.
𝑇2 −−→ 𝑇 . 9
Qiuhuan Xiong, Hengfeng Wei, Si Liu, Yuxing Chen, and Jidong Ge
Since 𝑇2 ∈ WriteTx𝑥 ,
Therefore, CO∗
−1
𝑇2 ∈ (VIS (𝑇 ) ∩ WriteTx𝑥 ). Thus,
VIS
Since 𝑇2 ∈ WriteTx𝑥 ,
AR
𝑇2 −−→ 𝑇1 .
𝑇2 ∈ (VIS−1 (𝑇 ) ∩ WriteTx𝑥 ).
Since CO = AR,
Therefore,
CO
AR
𝑇2 −−→ 𝑇1 .
𝑇2 −−→ 𝑇1 . Since CO = AR,
Thus, ReadAtomic(𝑇 ) holds. • Case level(𝑇 ) = PC. Since H is consistent, Int(𝑇 ), Ext(𝑇 ), Session(𝑇 ), and Prefix(𝑇 ) hold. We need to show that Prefix(𝑇 ) holds. Consider any 𝑇1,𝑇2 ∈ T such that for some 𝑥, CO∗
WR(𝑥 )
CO
𝑇2 −−→ 𝑇1 . Thus, Conflict(𝑇 ) holds. • Case level(𝑇 ) = SER. Since H is consistent, Int(𝑇 ), Ext(𝑇 ), Session(𝑇 ), and TotalVis(𝑇 ) hold. We need to show that Serializability(𝑇 ) holds. Consider any 𝑇1,𝑇2 ∈ T such that for some 𝑥,
SO ∪ WR
𝑇1 ≠ 𝑇2 ∧𝑇1 −−−−−→ 𝑇 ∧𝑇2 ∈ WriteTx𝑥 ∧∃𝑇3 . 𝑇2 −−−→ 𝑇3 −−−−−−−→ 𝑇 . WR(𝑥 )
By Ext(𝑇 ) and 𝑇1 −−−−−→ 𝑇 , we have
WR(𝑥 )
CO
𝑇1 ≠ 𝑇2 ∧ 𝑇1 −−−−−→ 𝑇 ∧ 𝑇2 ∈ WriteTx𝑥 ∧ 𝑇2 −−→ 𝑇 .
𝑇1 = max (VIS−1 (𝑇 ) ∩ WriteTx𝑥 ). AR
WR(𝑥 )
By Ext(𝑇 ) and 𝑇1 −−−−−→ 𝑇 , we have
SO ∪ WR
By Session(𝑇 ), Ext(𝑇 ), and 𝑇3 −−−−−−−→ 𝑇 ,
𝑇1 = max (VIS−1 (𝑇 ) ∩ WriteTx𝑥 ).
VIS
AR
𝑇3 −−→ 𝑇 .
CO
By TotalVis(𝑇 ), 𝑇2 −−→ 𝑇 , and CO = AR,
By Prefix(𝑇 ) and CO = AR, CO
VIS
𝑇2 −−−→ 𝑇3 −−→ 𝑇 =⇒ 𝑇2 −−→ 𝑇 .
VIS
VIS
VIS
𝑇2 −−→ 𝑇 .
𝑇2 −−→ 𝑇3 −−→ 𝑇 =⇒ 𝑇2 −−→ 𝑇 .
Since 𝑇2 ∈ WriteTx𝑥 ,
Therefore, CO∗
VIS
𝑇2 ∈ (VIS−1 (𝑇 ) ∩ WriteTx𝑥 ).
VIS
𝑇2 −−−→ 𝑇3 −−→ 𝑇 =⇒ 𝑇2 −−→ 𝑇 .
Therefore,
Since 𝑇2 ∈ WriteTx𝑥 ,
AR
𝑇2 −−→ 𝑇1 .
−1
𝑇2 ∈ (VIS (𝑇 ) ∩ WriteTx𝑥 ).
Since CO = AR,
Therefore,
CO
𝑇2 −−→ 𝑇1 .
AR
𝑇2 −−→ 𝑇1 .
Thus, Serializability(𝑇 ) holds.
Since CO = AR,
□
CO
𝑇2 −−→ 𝑇1 .
D
Thus, Prefix(𝑇 ) holds. • Case level(𝑇 ) = SI. Since H is consistent, Int(𝑇 ), Ext(𝑇 ), Session(𝑇 ), Prefix(𝑇 ), and NoConflict(𝑇 ) hold. We need to show that both Prefix(𝑇 ) and Conflict(𝑇 ) hold. Since SI(𝑇 ) ≡ PC(𝑇 )∧NoConflict(𝑇 ) and we have shown that Prefix(𝑇 ) holds if PC(𝑇 ) holds, it suffices to show that Conflict(𝑇 ) holds. Consider any 𝑇1,𝑇2,𝑇3 ∈ T such that for some 𝑥, CO∗
WR(𝑥 )
CO
𝑇1 ≠ 𝑇2 ∧𝑇1 −−−−−→ 𝑇 ∧𝑇2 ∈ WriteTx𝑥 ∧𝑇3 ⊲⊳ 𝑇 ∧𝑇2 −−−→ 𝑇3 −−→ 𝑇 . WR(𝑥 )
By Ext(𝑇 ) and 𝑇1 −−−−−→ 𝑇 , we have 𝑇1 = max (VIS−1 (𝑇 ) ∩ WriteTx𝑥 ). AR
CO
By NoConflict, 𝑇3 ⊲⊳ 𝑇 , 𝑇3 −−→ 𝑇 , and CO = AR, VIS
𝑇3 −−→ 𝑇 . By Prefix(𝑇 ) and CO = AR, CO
VIS
THE PC–SI–SER PROTOCOL
We propose a new concurrency control protocol called PC-SI-SER, which supports clients choosing among PC, SI, and SER isolation levels for each transaction. To the best of our knowledge, this is the first protocol that mixes three isolation levels spanning from the weakest (PC) to the strongest (SER) in a unified framework. Algorithm 2 presents its pseudocode, which adapts the well-known centralized SI protocol [1, 6] by extending its conflict-checking logic to distinguish among the three levels. All three levels follow the same basic flow: at begin, 𝑇 obtains a start timestamp𝑇 .sts (line 2:2); during execution, writes are buffered in 𝑇 .buffer (line 2:4), and reads return values from 𝑇 .buffer for keys already written by 𝑇 (line 2:7), or from the snapshot of store as of 𝑇 .sts for external reads (line 2:8); at commit, 𝑇 obtains a commit timestamp 𝑇 .cts and installs its writes (line 2:10). The levels differ only in conflict detection: PC performs no conflict checks; SI checks for write-write conflicts with concurrent transactions (𝑇 ′ .cts ∈ (𝑇 .sts,𝑇 .cts) and 𝑇 ′ ⊲⊳ 𝑇 ) and aborts if any are found (line 2:12); SER additionally checks for read-write conflicts (𝑇 ⊳𝑇 ′ ), aborting if a concurrent transaction has written to any key that 𝑇 read (line 2:14).
VIS
𝑇2 −−→ 𝑇3 −−→ 𝑇 =⇒ 𝑇2 −−→ 𝑇 . 10
Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels
Algorithm 2 The PC-SI-SER protocol
– Case I: level(𝑇 ) = PC. By definition of VIS for PC transactions,
store and 𝑇 .buffer as in Algorithm 1
VIS−1 (𝑇 ) = {𝑇 ′ ∈ T | 𝑇 ′ .cts < 𝑇 .sts}.
1: procedure Start(𝑇 ) 2: 𝑇 .sts ← now()
⊲ also for SER transactions
Since 𝑉 (𝑟 ) = VIS−1 (𝑇 ), by definition of 𝑆,
3: procedure Write(𝑇 , 𝑘, 𝑣) 4: 𝑇 .buffer [𝑘 ] ← 𝑣
𝑆 = max (𝑉 (𝑟 ) ∩ WriteTx𝑥 ). AR
That is, 𝑆 is the last transaction in 𝑉 (𝑟 ) that writes to 𝑥 according to AR. Therefore, 𝑆 ⊢ W(𝑥, 𝑣) holds. – Case II: level(𝑇 ) = SI. The proof is the same as that of Case I for PC transactions. – Case III: level(𝑇 ) = SER. By definition of VIS for SER transactions,
5: procedure Read(𝑇 , 𝑘) 6: if 𝑘 ∈ dom(𝑇 .buffer ) then 7: return 𝑇 .buffer [𝑘 ] 8: return value of store[𝑘 ] at latest timestamp < 𝑇 .sts 9: procedure Commit(𝑇 ) 10: 𝑇 .cts ← now() 11: if level(𝑇 ) = SI ∧ ∃𝑇 ′ . 𝑇 ′ .cts ∈ (𝑇 .sts,𝑇 .cts) ∧ 𝑇 ′ ⊲⊳ 𝑇 then 12: return aborted 13: if level(𝑇 ) = SER∧ ∃𝑇 ′ . 𝑇 ′ .cts ∈ (𝑇 .sts,𝑇 .cts) ∧ (𝑇 ⊲⊳ 𝑇 ′ ∨𝑇 ⊳𝑇 ′ ) 14: 15: 16:
VIS−1 (𝑇 ) = {𝑇 ′ ∈ T | 𝑇 ′ .cts < 𝑇 .cts}. In the following, we show that
then return aborted store[𝑘 ] ← [𝑇 .cts ↦→ 𝑣 ], ∀ [𝑘 ↦→ 𝑣 ] ∈ 𝑇 .buffer return committed
𝑉 (𝑟 ) ∩ WriteTx𝑥 = VIS−1 (𝑇 ) ∩ WriteTx𝑥 . On the one hand, since 𝑇 .sts < 𝑇 .cts, 𝑉 (𝑟 ) ⊆ VIS−1 (𝑇 ). Hence,
This graduated scheme captures the increasing strength from PC through SI to SER.
𝑉 (𝑟 ) ∩ WriteTx𝑥 ⊆ VIS−1 (𝑇 ) ∩ WriteTx𝑥 . On the other hand, suppose by contradiction that
Theorem D.1. Algorithm 2 conforms to the mixed isolation guarantees of PC, SI, and SER.
VIS−1 (𝑇 ) ∩ WriteTx𝑥 ⊈ 𝑉 (𝑟 ) ∩ WriteTx𝑥 . Then there exists a transaction 𝑇 ′ ∈ T such that
Proof. For any history H = (T , SO, level) produced by Algorithm 2, we define AR as follows:
𝑇 ′ ∈ WriteTx𝑥 ∧ 𝑇 ′ .cts ∈ (𝑇 .sts,𝑇 .cts). Since 𝑇 ⊢ R(𝑥, 𝑣), we have 𝑇 ⊳𝑇 ′ . By line 2:14, 𝑇 would abort, which is a contradiction. Therefore,
AR
∀𝑇 ′,𝑇 ∈ T . 𝑇 ′ −−→ 𝑇 ⇐⇒ 𝑇 ′ .cts < 𝑇 .cts. Clearly, AR is a strict total order. The visibility relation VIS is defined as
VIS−1 (𝑇 ) ∩ WriteTx𝑥 ⊆ 𝑉 (𝑟 ) ∩ WriteTx𝑥 . • Session(𝑇 ): Consider any transaction 𝑇 ′ ∈ T such that
VIS
∀𝑇 ′,𝑇 ∈ T . 𝑇 ′ −−→ 𝑇 ⇐⇒
SO
𝑇 ′ −−→ 𝑇 . By definition of SO, 𝑇 starts after 𝑇 ′ commits. – Case I: level(𝑇 ) = PC. Since 𝑇 starts after 𝑇 ′ commits and the wall time always increases, we have
(level(𝑇 ) = PC ∧ 𝑇 ′ .cts < 𝑇 .sts) ∨ (level(𝑇 ) = SI ∧ 𝑇 ′ .cts < 𝑇 .sts) ∨ (level(𝑇 ) = SER ∧ 𝑇 ′ .cts < 𝑇 .cts).
𝑇 ′ .cts < 𝑇 .sts.
It is easy to verify that VIS is irreflexive and VIS ⊆ AR. 2 In the
By definition of VIS for PC transactions,
following, we show that the corresponding abstract execution X = (H, VIS, AR) for H is consistent: Fix a transaction 𝑇 ∈ T . We show that the consistency axioms corresponding to level(𝑇 ) hold on 𝑇 . • Int(𝑇 ): If there is no internal read in 𝑇 , then Int(𝑇 ) holds vacuously. Otherwise, Int(𝑇 ) holds because 𝑇 buffers writes in its private buffer (line 2:4) and reads from buffer for internal reads (line 2:7). • Ext(𝑇 ): If there is no external read in 𝑇 , then Ext(𝑇 ) holds vacuously. Otherwise, consider any external read 𝑟 ≜ R(𝑥, 𝑣) in 𝑇 for some 𝑥 ∈ K and 𝑣 ∈ V. By line 2:8, 𝑣 is the value written to 𝑥 by the last transaction, according to AR, in
VIS
𝑇 ′ −−→ 𝑇 . – Case II: level(𝑇 ) = SI. The proof is the same as that of Case I for PC transactions. – Case III: level(𝑇 ) = SER. Since 𝑇 starts after 𝑇 ′ commits, 𝑇 commits after it starts, and the wall time always increases, we have 𝑇 ′ .cts < 𝑇 .cts. By definition of VIS for SER transactions, VIS
𝑇 ′ −−→ 𝑇 . • Prefix(𝑇 ): We need to show that for any transactions 𝑇 ′, 𝑆 ∈ T , the following holds:
𝑉 (𝑟 ) ≜ {𝑇 ′ ∈ T | 𝑇 ′ .cts < 𝑇 .sts}. Let 𝑆 ≜ maxAR (VIS−1 (𝑇 ) ∩WriteTx𝑥 ). We distinguish three cases depending on whether 𝑇 is at PC, SI, or SER level, and show that 𝑆 ⊢ W(𝑥, 𝑣).
AR
VIS
VIS
𝑇 ′ −−→ 𝑆 −−→ 𝑇 =⇒ 𝑇 ′ −−→ 𝑇 . AR
Since 𝑇 ′ −−→ 𝑆, by definition of AR, 𝑇 ′ .cts < 𝑆.cts.
2 The proof is similar to that in the proof of Theorem 4.1. We omit the details for brevity.
11
Qiuhuan Xiong, Hengfeng Wei, Si Liu, Yuxing Chen, and Jidong Ge
In the following, we consider three cases depending on whether 𝑇 is at PC, SI, or SER level. VIS – Case I: level(𝑇 ) = PC. Since 𝑆 −−→ 𝑇 , by definition of VIS for PC transactions,
E
PROOF OF THEOREM 4.1 (SI–S2PL)
Proof of Theorem 4.1. For any history H = (T , SO, level) produced by Algorithm 1, we define AR as follows: AR
∀𝑇 ′,𝑇 ∈ T . 𝑇 ′ −−→ 𝑇 ⇐⇒ 𝑇 ′ .cts < 𝑇 .cts.
𝑆.cts < 𝑇 .sts. Clearly, AR is a strict total order. The visibility relation VIS is defined as
Thus, 𝑇 ′ .cts < 𝑆.cts < 𝑇 .sts.
VIS
∀𝑇 ′,𝑇 ∈ T . 𝑇 ′ −−→ 𝑇 ⇐⇒
Therefore, by definition of VIS for PC transactions,
(level(𝑇 ) = SI ∧ 𝑇 ′ .cts < 𝑇 .sts) ∨
′ VIS
(level(𝑇 ) = SER ∧ 𝑇 ′ .cts < 𝑇 .cts).
𝑇 −−→ 𝑇 .
Note that we choose 𝑇 ′ .cts < 𝑇 .cts for SER transactions rather than 𝑇 ′ .cts < 𝑇 .sts (as for PC and SI transactions; see line 2:8) to ensure that SER transactions observe all its AR-predecessors, required by the TotalVis axiom. It is easy to verify that VIS is irreflexive and VIS ⊆ AR:
– Case II: level(𝑇 ) = SI. The proof is the same as that of Case I for PC transactions. VIS – Case III: level(𝑇 ) = SER. Since 𝑆 −−→ 𝑇 , by definition of VIS for SER transactions, 𝑆.cts < 𝑇 .cts.
• VIS is irreflexive: For any transaction 𝑇 ∈ T , by definition Thus,
VIS
of VIS, 𝑇 −−→ 𝑇 implies either ′
𝑇 .cts < 𝑆.cts < 𝑇 .cts.
level(𝑇 ) = SI ∧ 𝑇 .cts < 𝑇 .sts,
Therefore, by definition of VIS for SER transactions,
or
VIS
𝑇 ′ −−→ 𝑇 .
level(𝑇 ) = SER ∧ 𝑇 .cts < 𝑇 .cts, which is impossible in both cases. • VIS ⊆ AR: Consider any transactions 𝑇 ′,𝑇 ∈ T such that
• NoConflict(𝑇 ): Note that in this case, level(𝑇 ) = SI or level(𝑇 ) = SER. Consider a transaction 𝑇 ′ ≠ 𝑇 such that
VIS
AR
𝑇 ′ −−→ 𝑇 . By definition of VIS, we have either
𝑇 ⊲⊳ 𝑇 ′ . Suppose that 𝑇 ′ −−→ 𝑇 . By definition of AR, 𝑇 ′ .cts < 𝑇 .cts.
level(𝑇 ) = SI ∧ 𝑇 ′ .cts < 𝑇 .sts,
In the following, we consider two cases depending on
or
VIS whether 𝑇 is at SI or SER level, and show that 𝑇 ′ −−→ 𝑇 .
level(𝑇 ) = SER ∧ 𝑇 ′ .cts < 𝑇 .cts.
– Case I: level(𝑇 ) = SI. If 𝑇 .sts < 𝑇 ′ .cts, then we have
In both cases, we have (due to 𝑇 .sts < 𝑇 .cts)
𝑇 ′ .cts ∈ (𝑇 .sts,𝑇 .cts) ∧ 𝑇 ′ ⊲⊳ 𝑇 .
𝑇 ′ .cts < 𝑇 .cts.
By line 2:12, 𝑇 should be aborted. Therefore,
Therefore, by definition of AR,
𝑇 ′ .cts < 𝑇 .sts.
AR
𝑇 ′ −−→ 𝑇 .
By definition of VIS for SI transactions,
In the following, we show that the corresponding abstract execution X = (H, VIS, AR) for H is consistent: Fix a transaction 𝑇 ∈ T . We show that the consistency axioms corresponding to level(𝑇 ) hold on 𝑇 .
VIS
𝑇 ′ −−→ 𝑇 . – Case II: level(𝑇 ) = SER. By definition of VIS for SER transactions,
• Int(𝑇 ): If there is no internal read in 𝑇 , then Int(𝑇 ) holds vacuously. Otherwise, Int(𝑇 ) holds because 𝑇 , whether at SI or SER level, buffers writes in its private buffer (line 1:7) and reads from buffer for internal reads (line 1:10). • Ext(𝑇 ): If there is no external read in 𝑇 , then Ext(𝑇 ) holds vacuously. Otherwise, consider any external read 𝑟 ≜ R(𝑥, 𝑣) in 𝑇 for some 𝑥 ∈ K and 𝑣 ∈ V. Let 𝑆 ≜ maxAR (VIS−1 (𝑇 ) ∩ WriteTx𝑥 ). We distinguish two cases depending on whether 𝑇 is at SI or SER level, and show that 𝑆 ⊢ W(𝑥, 𝑣). – Case I: level(𝑇 ) = SI. By definition of VIS for SI transactions,
VIS
𝑇 ′ −−→ 𝑇 . • TotalVis: Note that in this case, level(𝑇 ) = SER. Consider a transaction 𝑇 ′ ∈ T such that AR
𝑇 ′ −−→ 𝑇 . By definition of AR, 𝑇 ′ .cts < 𝑇 .cts. By definition of VIS for SER transactions, VIS
𝑇 ′ −−→ 𝑇 .
VIS−1 (𝑇 ) = {𝑇 ′ ∈ T | 𝑇 ′ .cts < 𝑇 .sts}.
□ 12
Semantic Conformance of Concurrency Control Protocols under Mixed Isolation Levels
• Prefix(𝑇 ): We need to show that for any transactions 𝑇 ′, 𝑆 ∈ T , the following holds:
By line 1:12, 𝑣 is the value written to 𝑥 by the last transaction, according to AR, in 𝑉 (𝑟 ) ≜ {𝑇 ′ ∈ T | 𝑇 ′ .cts < 𝑇 .sts},
AR
VIS
AR
Since 𝑉 (𝑟 ) = VIS (𝑇 ), by definition of 𝑆,
Since 𝑇 ′ −−→ 𝑆, by definition of AR,
𝑆 = max (𝑉 (𝑟 ) ∩ WriteTx𝑥 ).
𝑇 ′ .cts < 𝑆.cts.
AR
That is, 𝑆 is the last transaction in 𝑉 (𝑟 ) that writes to 𝑥 according to AR. Therefore, 𝑆 ⊢ W(𝑥, 𝑣) holds. – Case II: level(𝑇 ) = SER. By definition of VIS for SER transactions,
In the following, we consider two cases depending on whether 𝑇 is at SI or SER level. VIS – Case I: level(𝑇 ) = SI. Since 𝑆 −−→ 𝑇 , by definition of VIS for SI transactions,
VIS−1 (𝑇 ) = {𝑇 ′ ∈ T | 𝑇 ′ .cts < 𝑇 .cts}.
𝑆.cts < 𝑇 .sts.
By line 1:15, 𝑣 is the value written to 𝑥 by the last transaction, according to AR, in ′
VIS
𝑇 ′ −−→ 𝑆 −−→ 𝑇 =⇒ 𝑇 ′ −−→ 𝑇 .
−1
Thus, 𝑇 ′ .cts < 𝑆.cts < 𝑇 .sts.
′
𝑉 (𝑟 ) ≜ {𝑇 ∈ T | 𝑇 .cts < 𝑟 .now()},
Therefore, by definition of VIS for SI transactions,
where 𝑟 .now() is the time when 𝑟 is performed (line 1:15). In the following, we show that
VIS
𝑇 ′ −−→ 𝑇 . VIS
𝑉 (𝑟 ) ∩ WriteTx𝑥 = VIS−1 (𝑇 ) ∩ WriteTx𝑥 .
– Case II: level(𝑇 ) = SER. Since 𝑆 −−→ 𝑇 , by definition of VIS for SER transactions,
On the one hand, since 𝑟 .now() < 𝑇 .cts,
𝑆.cts < 𝑇 .cts.
𝑉 (𝑟 ) ⊆ VIS−1 (𝑇 ). Thus,
Hence,
𝑇 ′ .cts < 𝑆.cts < 𝑇 .cts.
𝑉 (𝑟 ) ∩ WriteTx𝑥 ⊆ VIS−1 (𝑇 ) ∩ WriteTx𝑥 .
Therefore, by definition of VIS for SER transactions,
On the other hand, suppose by contradiction that
VIS
𝑇 ′ −−→ 𝑇 .
VIS−1 (𝑇 ) ∩ WriteTx𝑥 ⊈ 𝑉 (𝑟 ) ∩ WriteTx𝑥 .
• NoConflict(𝑇 ): Consider a transaction 𝑇 ′ ≠ 𝑇 such that
Then there exists a transaction 𝑇 ′ ∈ T such that
AR
𝑇 ⊲⊳ 𝑇 ′ . Suppose that 𝑇 ′ −−→ 𝑇 . By definition of AR,
𝑇 ′ ∈ WriteTx𝑥 ∧ 𝑇 ′ .cts ∈ (𝑟 .now(),𝑇 .cts).
𝑇 ′ .cts < 𝑇 .cts.
By line 1:14, 𝑇 acquires a shared lock on 𝑥 before 𝑟 .now(). By line 1:18 for SI transactions or line 1:6 for SER transactions, 𝑇 ′ acquires an exclusive lock on 𝑥. Furthermore, both 𝑇 and 𝑇 ′ hold these locks until they commits (line 1:25), particularly after they are assigned commit timestamps (line 1:19). Since shared and exclusive locks on the same key are incompatible, it cannot be that 𝑇 ′ .cts ∈ (𝑟 .now(),𝑇 .cts). Therefore,
In the following, we consider two cases depending on VIS
whether 𝑇 is at SI or SER level, and show that 𝑇 ′ −−→ 𝑇 . – Case I: level(𝑇 ) = SI. If 𝑇 .sts < 𝑇 ′ .cts, then we have 𝑇 ′ .cts ∈ (𝑇 .sts,𝑇 .cts) ∧ 𝑇 ′ ⊲⊳ 𝑇 . By line 1:21, 𝑇 should be aborted. Therefore, 𝑇 ′ .cts < 𝑇 .sts.
VIS−1 (𝑇 ) ∩ WriteTx𝑥 ⊆ 𝑉 (𝑟 ) ∩ WriteTx𝑥 .
By definition of VIS for SI transactions,
• Session(𝑇 ): Consider any transaction 𝑇 ′ ∈ T such that
VIS
𝑇 ′ −−→ 𝑇 .
SO 𝑇 ′ −−→ 𝑇 . By definition of SO, 𝑇 starts after 𝑇 ′ commits.
– Case II: level(𝑇 ) = SER. By definition of VIS for SER transactions,
– Case I: level(𝑇 ) = SI. Since 𝑇 starts after 𝑇 ′ commits and the wall time always increases, we have
VIS
𝑇 ′ −−→ 𝑇 .
𝑇 ′ .cts < 𝑇 .sts.
• TotalVis(𝑇 ): Note that in this case, level(𝑇 ) = SER. Consider a transaction 𝑇 ′ ∈ T such that
By definition of VIS for SI transactions, VIS
𝑇 ′ −−→ 𝑇 .
AR
𝑇 ′ −−→ 𝑇 .
– Case II: level(𝑇 ) = SER. Since 𝑇 starts after 𝑇 ′ commits, 𝑇 commits after it starts, and the wall time always increases, we have
By definition of AR, 𝑇 ′ .cts < 𝑇 .cts.
𝑇 ′ .cts < 𝑇 .cts.
By definition of VIS for SER transactions, VIS
By definition of VIS for SER transactions,
𝑇 ′ −−→ 𝑇 .
VIS
𝑇 ′ −−→ 𝑇 .
□ 13
Qiuhuan Xiong, Hengfeng Wei, Si Liu, Yuxing Chen, and Jidong Ge
(2) 𝑇 ′ begins after 𝑡. 𝑇 ′ receives a start timestamp 𝑠 ′ with 𝑠 ′ > 𝑡 and performs its first read of 𝑘. Since 𝑇 ’s write has not yet been installed, 𝑇 ′ reads the old version (value 𝑣 0 ). (3) 𝑇 acquires xlock(𝑘) in Commit. 𝑇 continues its commit procedure, acquiring an exclusive lock on 𝑘 and installing the new value 𝑣𝑡 into store with its commit time 𝑡. (4) 𝑇 ′ reads 𝑘 again. 𝑇 ′ now reads the current version of 𝑘 and sees 𝑣𝑡 . Thus, 𝑇 ′ has read two different values (𝑣 0 and 𝑣𝑡 ) for the same key in the same transaction, violating the repeatable read guarantee.
Example E.1. We show that if the procedure Commit(𝑇 ) was not executed atomically and line 1:19 was moved before line 1:17, then Non-RepeatableRead anomaly may arise. Consider the scenario where two transactions 𝑇 and 𝑇 ′ with level(𝑇 ) = level(𝑇 ′ ) = SI operate on the same key 𝑘 with initial value 𝑣 0 ; 𝑇 is a writer while 𝑇 ′ is a reader. (1) 𝑇 executes Commit. Because the commit procedure assigns 𝑇 .cts before acquiring locks (in the modified algorithm), 𝑇 immediately sets its commit timestamp to 𝑡. The write to 𝑘 has not been installed into store yet.
14