混合隔离级别综述

$$ \newcommand{\rel}[1]{\xrightarrow{#1}} \newcommand{\WR}{\textsf{WR}} \newcommand{\WW}{\textsf{WW}} \newcommand{\RW}{\textsf{RW}} \newcommand{\RC}{\textbf{\textup{RC}}} \newcommand{\RA}{\textbf{\textup{RA}}} \newcommand{\CC}{\textbf{\textup{CC}}} \newcommand{\PC}{\textbf{\textup{PC}}} \newcommand{\PSI}{\textbf{\textup{PSI}}} \newcommand{\SI}{\textbf{\textup{SI}}} \newcommand{\StwoPL}{\textbf{\textup{S2PL}}} \newcommand{\SSI}{\textbf{\textup{SSI}}} \newcommand{\SER}{\textbf{\textup{SER}}} \newcommand{\SERm}{\textbf{$\textup{SER}^{-}$}} $$

摘要

[Fekete PODS'05]

DB2，SQL Server 和 ASE 使用了 S2PL 算法
Oracle 和 PostgreSQL 使用了 SI 算法
Oracle 使用 SI 算法来实现 SERIALIZABLE，但允许显式使用锁
预告 Yukon release of SQL Server 支持 S2PL+SI 算法
S2PL+SI 下的静态鲁棒性充分条件：如果所有的 pivot 事务都使用了 S2PL，则整个程序鲁棒；
我们对 SI-SER 的定义与 Fekete 相同，但我们给出的充分条件比 Fekete 更精确。

[Fekete DASFAA'08]

明确指出 SQL Server 2005 支持 S2PL+SI
实验：SI、S2PL、pivot-S2PL 下的 throughput 对比

[Gotsman CONCUR'16]

提出了弱隔离级别和 SER 混合的语义；
给出该混合隔离级别下的静态鲁棒性。

[Enea CAV'25]

给出了混合隔离级别（RC、RA、PC、SI、SER）的形式语义规约，在 SI-SER 上保持了与 Fekete 一致，该形式语义与我们的贡献几乎相同；
使用 PostgreSQL 在 RC-SI-SER 下产生的历史完成实验

[Vandervoort VLDB'25]

基于调度定义了 RC-SI-SSI 混合；
使用读提升（Read Promotion）实现鲁棒；
不适用于分布式系统。

本文关于鲁棒性判定有两个贡献：

定理 33 用于判定 SI-SER 下鲁棒性的充分条件，这是目前为止最精确（最接近充要条件）的 SI-SER 鲁棒性判定条件；
定理 36 是首个用于判定 {RA, CC, PC, PSI, SI, SER} 任意混合的鲁棒性的充分条件。

此前混合隔离级别下的鲁棒性工作有：

[Fekete 2005] 最早提出了一个判定 S2PL-SI 鲁棒性的充分条件：所有 pivot 都为 S2PL，则程序执行可靠。
[Gotsman 2016] 提出了一个判定 wm-SER 鲁棒性的方案，其中 wm 为 SI，PC，PSI，CC，且 Gotsman 的 mixing 规约比我们的更弱。
[Vandervoort TODS'25] 提出了 RC-SI-SSI 下的鲁棒性，但不支持分布式系统。
Enea 做了多个隔离级别的语义规约和历史验证，没有鲁棒性相关工作。
Enea 的鲁棒性做的是 trace 而不是 history。
$\ge 3$ 个隔离级别。
并不局限于 RDBMS，distributed-kv 存在，因此 CC、PC 等有存在的意义。

我们的定理 33 比 Feteke 方法能判定更多的程序为鲁棒，即“更接近充要条件”。后两份工作和我们的不具备比较意义。

TODO：干净的系统做实验。

目前只有 [Vandervoort VLDB'25] 有关于 Robust Allocation 的直接结论，其他文章只给出了判定定理。

各种分布式一致性在分布式系统下实现方式

CausalDeliv：副本 r 传播消息时应包括所有 r 可见的更新；
MonTS：仲裁序 AR 应按照提交时间单调分配
TotalDeliv：副本 r 的事务 T 传播消息 m 到 r' 时，r' 应该接收到 T 的 AR 前序的所有更新
ConflictCheck：事务 T 提交

混合隔离级别在分布式系统下的实现方式

主节点（即 god CPU）：掌握全部的 AR 和 VIS 信息，根据提交序确定 AR（MonTS）

副本节点：存储一份副本，每个线程仅在一个副本执行，副本间通过主节点通信

Int & Ext：副本间可以按照任意规则通信（也可以不通信）
CausalDeliv(T)：副本 r 上的事务 T 开始前，向主节点请求开始，主节点检查副本 r 的是否满足 TransVis 公理，若满足则允许开始（换言之，若不满足，则等待同步至满足再开始或 abort）
TotalDeliv(T)：副本 r 上的事务 T 开始前，向主节点请求开始，主节点检查副本 r 的是否满足 Prefix 公理，若满足则允许开始（换言之，若不满足，则等待同步至满足再开始或 abort）
ConflictCheck(T)：副本 r 上的事务 T 提交前向主节点请求提交，主节点检查 NoCoflict(T) 公理，若满足则允许提交（换言之，若存在并发 ww 冲突则拒绝提交）
TotalVis(T)：开始前请求检查 Prefix(T) 公理，提交前请求检查并发 ww 冲突和并发 wr 冲突，若检测到这些并发冲突则 abort，否则 commit。

隔离级别	应该满足的操作语义
CC, PSI	CausalDeliv(T)
PC, SI, SER	TotalDeliv(T)
PSI, SI, SER	ConflictCheck(T)
SER	TotalVis(T)

\begin{definition}
	\label{def:axiom-on-txn}
	For each abstract excution $\A$ and each transaction $T = (O, \po) \in \A.\T$, we define axioms on $T$:
	\begin{align*}
		\Int(T) \equiv            & \forall r \in O. \forall x. (r = (\_, \R(x, v)) \land (\po^{-1}(r) \cap \Op_x \neq \emptyset))                                           \\
		                          & \implies \max{_{\po}}(\po^{-1}(r) \cap \Op_x) = (\_, \_(x,v))                                                                            \\
		\Ext(T) \equiv            & \forall x, v. T \vdash \R(x, v) \implies (\VIS^{-1}(T) \cap \WriteTx_{x} = \emptyset \land v = \init)                                    \\
		                          & \lor \max{_{\AR}}(\VIS^{-1}(T) \cap \WriteTx_{x}) \vdash \W(x, v)                                                                        \\
		\TransVis(T) \equiv       & \forall T_1, T_2 \in \A.\T. T_1 \rel{\VIS} T_2 \land T_2 \rel{\VIS} T \implies T_1 \rel{\VIS} T                                          \\
		\Prefixaxiom(T) \equiv    & \forall T_1, T_2 \in \A.\T. T_1 \rel{\AR} T_2 \land T_2 \rel{\VIS} T \implies T_1 \rel{\VIS} T                                           \\
		\NoConflict(T) \equiv     & \forall T' \conflict T. (T' \rel{\AR} T \implies T' \rel{\VIS} T)                                                                        \\
		\TotalVis(T) \equiv       & \forall T' \in \A.\T. (T' \rel{\AR} T \implies T' \rel{\VIS} T)                                                                          \\
	\end{align*}
\end{definition}

请根据以上描述，修改 Executor 类，模拟分布式数据库执行不同隔离级别的事务。