\[ \def\AR{\mathsf{\textcolor{brown}{AR}}} \def\VIS{\mathsf{\textcolor{orange}{VIS}}} \]
摘要
现代分布式系统通常依赖于数据库，这些数据库通过仅提供关于分布式事务处理一致性的弱保证来实现可扩展性。与此类数据库交互的程序的语义取决于其一致性模型，该模型定义了这些保证。不幸的是，一致性模型通常是非正式的或使用不同的形式主义，通常与数据库内部相关。为了解决这个问题，我们提出了一个框架，用于统一和声明性地指定各种事务一致性模型。
我们的规范以弱内存模型的形式给出，使用事件和关系结构。这些规范特别简洁，因为它们利用了许多一致性模型保证的原子可见性属性：事务的所有更新或所有更新都对另一个事务可见。这允许规范从事务内部的单个事件中抽象出来。我们通过指定几个现有的一致性模型来说明我们框架的使用。为了验证我们的规范，我们证明它们等同于替代操作规范，这些规范是更接近实际实现的算法。我们的工作为开发弱一致性大规模数据库中出现的新形式并发的元理论提供了严格的基础。
作者：
- Andrea Cerone, IMDEA Software Institute
- Giovanni Bernardi, IMDEA Software Institute
- Alexey Gotsman, IMDEA Software Institute
隔离级别的公理定义
事务中有两种偏序，仲裁序 AR 和可见序 VIS，且 \(\VIS \subseteq \AR\)。
其中：
- Int 是内部一致性公理，对于事务内先写后读，要求所写即所读；
- Ext 是外部一致性公理，对于事务内不写即读，要求读到的是最后一个外部写；
- Int 和 Ext 共同避免不完整的读 Fractured reads，保证了原子读 RA；
- TransVis 是可见性传递公理，要求事务间的可见性关系 VIS 是传递性的，避免了因果违规 Causality violation，保证了 CC；
- NoConflict 公理要求不会对同一个变量并发写入，避免了丢失更新 Lost update，保证了 PSI；
- Prefix 公理要求，如果 T 能观察到 S，则 T 也能观察到 S 的所有 AR-前缀，该公理避免了 Long fork；
- NoConflict 和 Prefix 共同保证了 SI；
- TotalVis 公理要求 VIS 是一个全序，保证了 SER。
公理形式化定义
违反公理的示例
Gotsman 在 Database Isolation Levels Part 1 (SPTDC; Alexey Gotsman)_哔哩哔哩_bilibili 中用下图描述所有的隔离级别。
