\[ \def\T{\mathcal{T}} \def\P{\mathcal{P}} \]
摘要
数据库客户程序鲁棒性问题是数据库一致性领域的一个分支，是验证客户程序在弱一致性模型下的执行结果是否一定会满足某个强隔离级别（一般是 SER）。
本文梳理了数据库客户程序鲁棒性问题领域的现有工作成果并形成综述。本文还整理了 Vandevoort、Gotsman 和 Enea 等人在鲁棒性问题上的贡献。
现有工作综述
主要学者：
- [Fekete TODS'05] 研究了 SI 下的鲁棒性
- Gotsman, Bernardi, Cerone 等人在 2016-2017 研究了 Atomic Visibility 和 SI/PSI 下的鲁棒性
- Beillahi, Bouajjani, Enea 等人在 2019-2021 研究了弱隔离级别之间的鲁棒性，并开源了首个原型工具 Boogie
- Vandevoort，Ketsman 等人在 2021-2023 研究了 RC 下的鲁棒性，扩展了事务模板、谓词读等功能
| 运行环境 | PC | SI | SER |
|---|---|---|---|
| RU | [Ketsman PODS'20] 充要条件 | ||
| RC（优先1） | [Ketsman PODS'20] 充要条件 [Vandevoort VLDB'21] 事务模板的充要条件，有实验数据，未开源 |
||
| RA（优先2） | |||
| CC（优先2） | [Bouajjani ESOP'21] 充要条件，转化为 CC 对 SER 鲁棒性 | [Bouajjani ESOP'21] 充要条件，\(CC \to PC \land PC \to SI\) | [Bernardi CONCUR'16] 充分条件 [Beillahi CONCUR'19] CC、CM、CCv 下充要条件 |
| PC（不常用） | / | [Bouajjani ESOP'21] 充要条件，依赖程序搜索 | [Bernardi CONCUR'16] 充分条件 |
| PSI（优先3） | / | [Cerone PODC'16] 充分条件（纯数学，无算法） | [Bernardi CONCUR'16] 充分条件 |
| SI（优先1） | / | / | [Fekete TODS'05] 充分条件（太长没看，可以不看） [Cerone PODC'16 & JACM'18] 充要条件（纯数学，无算法） [Bouajjani CAV'19] [Bernardi CONCUR'16] 充分条件 |
问题：
- 静态的充要条件，或者做一个更好、更精确的充分？
- 事务模板。
- 遍历用 SMC。
- 能不能做个原型工具？
Gotsman 等人在 Robustness 上的贡献
- CONCUR'16-Robustness against Consistency Models with Atomic Visibility
- 给出 CC、PC、PSI、SI 下静态鲁棒性的充分条件
- PODC'16-Analysing Snapshot Isolation & JACM'18-Analysing Snapshot Isolation（更长）
- 用集合不等式定义 SI，似乎是基于 Kleene Algebra with Tests [Kozen CSL'96]
- 对 SI 下的事务斩断进行静态分析
- 给出鲁棒性 SI \(\to\) SER 和 PSI \(\to\) SI 的充要条件，但过于简略且未给出算法
- 整篇文章完全基于数学分析，没有原型工具和实验
- CONCUR'17-Algebraic Laws for Weak Consistency
- 揭示了抽象执行和依赖图两种形式化模型的内在联系
Beillahi 等人在 Robustness 上的贡献
- CONCUR'19-Robustness Against Transactional Causal Consistency
- 给出 CC、CCv、CM（CC 的几个变体） 下鲁棒性的充分条件
- CAV'19-Checking Robustness Against Snapshot Isolation
- ESOP'21-Checking Robustness Between Weak Transactional Consistency Models
- 验证了 CC-PC-SI-SER 四种隔离级别间的鲁棒性（除了 PC-SER）
- 将这些问题归结为可序列化下的状态可达性问题，在多项式时间内解决
- 目前唯一一个开源的工具：Boogie
Vandevoort 等人在 Robustness against RC 上的贡献
- PODS'20-Deciding Robustness for Lower SQL Isolation Levels
- 理论细节最完善，是后续工作的基础；
- 提出了判定事务集合 \(\T\) 在无隔离级别、RU、RC 下鲁棒性的充要条件
- VLDB'21-Robustness Against Read Committed for Transaction Templates
- 提出了判定事务集合 \(\T\) 和事务模板 \(\P\) 在 RC 下鲁棒性的充要条件和多项式时间算法
- 给出了 SmallBank 和 TPC-Ckv 的鲁棒子集
- 有实验数据，未开源
- PODS'22-Robustness Against Read Committed-A Free Transactional Lunch
- 引入干涉图（interference graph）用于解释 VLDB'21 提出的算法，但并未给出证明
- 无实验数据
- ICDT'22-Robustness Against Read Committed for Transaction Templates with Functional Constraints
- 对事务模板扩展了功能约束（functional constraints），看不懂
- 纯数学分析，无原型工具和实验
- EDBT'23-Detecting Robustness against MVRC for Transaction Programs with Predicate Reads
- 扩展了具有控制结构（循环和条件）以及插入、删除和谓词读取的事务程序
- 有新算法和实验，未开源
- SIGMOD'23-When is it safe to run a transactional workload under Read Committed
- 对以上所有文章的综述
