一句话：为事务模板引入函数约束以提升建模能力，并刻画其对 Read Committed 鲁棒性判定的不可判定性与可处理片段。
该文研究事务工作负载在 Multiversion Read Committed（RC）隔离级别下执行时是否仍能保证可串行化，即工作负载对 RC 的鲁棒性。已有工作针对事务模板这一程序模型给出了可处理的鲁棒性判定过程，其关键洞见是更精确地建模事务程序能够识别出更大的鲁棒工作负载集合。本文通过为事务模板引入函数约束（可用于刻画外键等数据依赖）来增强其建模能力，并证明引入函数约束能够识别出原本无法被判定为鲁棒的更多工作负载。作者进一步表明，鲁棒性问题在最一般形式下是不可判定的，但通过对函数约束施加多种限制，可以得到可判定乃至可处理的片段，从而能够在现实场景中建模并测试对 RC 的鲁棒性。
The popular isolation level Multiversion Read Committed (RC) trades some of the strong guarantees of serializability for increased transaction throughput. Sometimes, transaction workloads can be safely executed under RC obtaining serializability at the lower cost of RC. Such workloads are said to be robust against RC. Previous work has yielded a tractable procedure for deciding robustness against RC for workloads generated by transaction programs modeled as transaction templates. An important insight of that work is that, by more accurately modeling transaction programs, we are able to recognize larger sets of workloads as robust. In this work, we increase the modeling power of transaction templates by extending them with functional constraints, which are useful for capturing data dependencies like foreign keys. We show that the incorporation of functional constraints can identify more workloads as robust that otherwise would not be. Even though we establish that the robustness problem becomes undecidable in its most general form, we show that various restrictions on functional constraints lead to decidable and even tractable fragments that can be used to model and test for robustness against RC for realistic scenarios.
@article{paperbot2155,
title = {Robustness against Read Committed for Transaction Templates with Functional Constraints},
author = {Brecht Vandevoort and Bas Ketsman and Christoph Koch and Frank Neven},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:39)2023}
}