摘要
本文提出了一个框架，用于统一和声明性地指定各种事务一致性模型。
作者：
- 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。
公理形式化定义
违反公理的示例
