$$ \newcommand{\rel}[1]{\xrightarrow{#1}} \newcommand{\WR}{\textsf{WR}} \newcommand{\wr}{\textsf{wr}} \newcommand{\read}{\textsf{read}} \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）实现鲁棒；
- 不适用于分布式系统。
Related Work
本文关于鲁棒性判定有两个贡献：
- 定理 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) |
请根据以上描述，修改 Executor 类，模拟分布式数据库执行不同隔离级别的事务。
[OOPLSA'19] 对 history 的定义为：
其中包含了 $\wr$ 关系，即对于每个读操作 $r = \read(x,v)$，都明确了一个事务 $t \vdash W(x,v)$。因此在任意隔离级别（包括 RC）中，对于任意 $r$ 可以找到唯一的 $t$。既然已经明确了 $\wr$ 关系，那么引入 unique value 只是为了方便描述和实验实现。
但是，在 (VIS, AR) 框架中：
- 对于 $\RA$ 及以上的隔离级别，通过 Ext 公理和 AR 全序保证能 $t$ 唯一；
- 对于不满足 Ext 的隔离级别（例如 RC），如果不引入 unique value 假设，则无法保证 $t$ 唯一。例如，$\alpha = R(x,1)$，另有 $t_1 \vdash W(x,1), t_3 \vdash W(x,1)$，无法判定 $t_1, t_3$ 哪一个应该作为 $\wr^{-1}(r)$。如果贸然引入谓词如 $\forall t. t \vdash W(x,v)$ 或 $\exists t. t \vdash W(x,v)$ 都会导致定义的公理与 [OOPLSA'19] 中的不等价。
结论：在不引入 unique value 假设和 $\wr$ 关系的情况下，(VIS, AR) 框架内无法给出与 [OOPLSA'19] 中等价的 RC 公理定义。
在上述 OOPLSA'19 定义 (a) 中，我们要根据 $t_1 \rel{\WR_x} \alpha$ 和 $t_2 \rel{\WR} \beta$ 来枚举 $t_1, t_2$，这个枚举过程本身就依赖了 unique 假设。
操作语义和实现方式
SI-SER 的分布式实现方式
DC'21-Multi-shot distributed transaction commit.pdf
PSI 实现方式
SOSP'11-Transactional storage for geo-replicated systems.pdf
