论文笔记：[CONCUR'15] A Framework for Transactional Consistency Models with Atomic Visibility

在数据库领域，Transaction是一个非常重要的抽象，其关键在于保证并发请求的正确性。由于Serialisability级别的一致性所需要付出的代价较高，所以通常会使用弱一些的一致性级别来换取性能提升。特别的，在一些特殊场景下，使用弱一致性并不会带来错误。遗憾的是，ANSI SQL对于一致性级别的分类还不够细致，特别的，对于一些常见的弱一致性实现没有形式化规范。这导致人们很难确认特定供应商提供的弱一致性实现在某个特定场景下是否真的不会引入错误。[2]

近年来，不断有一些使用形式化方法分析Transaction一致性的论文，如[3][4]，以及本文希望介绍的[1]。形式化的表述有助于推理和验证，但是仍需要非形式化的解释以进行直观解释，本文将介绍[1]所做的形式化工作，并解释其直觉含义。

基本模型

[1]使用Abstract Executions模型分析Transactional一致性。

假设数据库就是一堆slots，每个slot能存放一个整数，对于数据库的操作有读和写2种操作：

\[\mathrm{Op} = \{ \mathrm{read}(x,n), \mathrm{write}(x,n) \mid x \in \mathrm{Obj}, n \in \mathbb{Z} \}\]

如果给每个操作编上唯一标识，则我们可以得到一些 history event

\[\begin{align} \mathrm{WEvent}_x &= \{ (\tau, \mathrm{write}(x,n)) \mid \tau \in \mathrm{EventId}, n \in \mathbb{Z} \} \\ \mathrm{REvent}_x &= \{ (\tau, \mathrm{read}(x,n)) \mid \tau \in \mathrm{EventId}, n \in \mathbb{Z} \} \\ \mathrm{HEvent}_x &= \mathrm{WEvent}_x \cup \mathrm{REvent}_x \end{align}\]

进一步的，我们可以定义Transaction：

A transaction $T, S, \ldots$ is a pair $(E, \mathrm{po})$, where $E \subseteq \mathrm{HEvent}$ is a finite, non-empty set of events with distinct identifiers, and the program order $\mathrm{po}$ is a total order over $E$. A history $\mathcal{H}$ is a (finite or infinite) set of transactions with disjoint sets of event identifiers.

All transactions in a history are assumed to be committed: to simplify presentation, our specifications do not constrain values read inside aborted or ongoing transactions.

简单的来说，Transaction就是一组具有全序关系的history events（还有一些为了严谨性的额外条件，但是对于直觉理解没什么意义）。history由已提交的一些Transactions组成。

更进一步的，我们可以定义abstract execution：

We call a relation prefix-finite, if every element has finitely many predecessors in the transitive closure of the relation.

An abstract execution is a triple $\mathcal{A} = (\mathcal{H}, \mathrm{VIS}, \mathrm{AR})$ where:

1. visibility: $\mathrm{VIS} \subseteq \mathcal{H} \times \mathcal{H}$ is a prefix-finite, acyclic relation; and

2. arbitration: $\mathrm{AR} \subseteq \mathcal{H} \times \mathcal{H}$ is a prefix-finite, total order such that $\mathrm{AR} \supseteq \mathrm{VIS}$.

abstract execution的直观含义就不太明显了，只能认为是带有两种序关系的history。然而这里并没有定义$\mathrm{VIS}$和$\mathrm{AR}$的具体含义，只是大概解释了一下它们的直观含义：

1. $T \stackrel{\mathrm{VIS}}{\longrightarrow} S$大体上可以认为$S$发现了$T$，一般来说是$S$读到了$T$产生的内容。

2. $T \stackrel{\mathrm{AR}}{\longrightarrow} S$大体上可以认为是$S$写入的内容（部分或全部）覆盖了$T$写入的内容。尽管论文中是这么解释的，但是我认为理解成这样更通顺一些，即$S$“实际上”在$T$之后发生。我认为这么理解更合适的原因是因为在论文Figure 3(a)中有$T_1 \stackrel{\mathrm{AR}}{\longrightarrow} T_3$（这个关系源自于$\mathrm{AR}$是传递自反的），但是$T_3$根本没有进行写操作，这个用原论文中的说法根本没法理解。

3. $\mathrm{AR} \supseteq \mathrm{VIS}$意味着$( (T \stackrel{\mathrm{VIS}}{\longrightarrow} S) \Rightarrow (T \stackrel{\mathrm{AR}}{\longrightarrow} S)) \land ( (T \stackrel{\mathrm{AR}}{\longrightarrow} S) \nRightarrow (T \stackrel{\mathrm{VIS}}{\longrightarrow} S))$，也就是说我可以在不知道你的情况下就把你写入的东西给覆盖了，或者理解成尽管我“实际上”在你之前发生，但是你不知道我在你之前发生。或者可以认为$\mathrm{VIS}$相当于是在$\mathrm{AR}$中去掉了一些元素。

实际上$\mathrm{VIS}$和$\mathrm{AR}$是由consistency model的约束决定的，因此在这里才没有一个精确的定义。本文所使用的方法就是从通过对$\mathrm{VIS}$和$\mathrm{AR}$增加约束，将某些违反直觉的情况从abstract executions中排除。所增加的约束被定义为某种（好的）性质，通过组合这些性质进一步定义出一致性模型。

总之abstract execution $\mathcal{A}$就是带有$\mathrm{VIS}$和$\mathrm{AR}$两种序关系的event history $\mathcal{H}$。其中$\mathrm{AR}$就是comitted transaction“实际上”串行化后“生效”的顺序，$\mathrm{VIS}$是从用户（客户端）的视角能够发现transaction之间的逻辑因果关系。

关于abstract execution模型的概念在论文中写的不是很详细，如果对这部分内容感兴趣，建议阅读[5]。但是需要注意的是[5]中具体描述的abstract execution模型和这里的场景不一样，是建立在operation上的，而[1]的abstract execution是建立在transaction上的。

一致性模型和性质总结

论文中提到的一致性模型见figure 1。

其中并没有提到ANSI SQL中常见的几个一致性级别：

1. Read Uncommitted

2. Read Committed

3. Repeatable Read（这里取[7]中的定义，和ANSI SQL中的定义有微妙的区别，详见P9 Remark 8上面一点。这么取是因为[6]的P15:11最上面特别提了一下。）

特别的，其中Repeatable Read和Read Atomic比较类似，容易引起一些混淆，但是两者并不是相同的一致性级别，见[6]的RAMP figure 1（注意是TODS 2016，不是SIGMOD 2014的同名文献）。

一些符号

论文中为了叙述方便，还定义了一些符号。

$R^{-1}(u)$

For a relation $R \subseteq A \times A$ and an element $u \in A$, we let $R^{−1}(u) = \{ v \mid (v, u) \in R \}$.

直觉上$R^{-1}$就是$R$的反序，但是需要注意的是$R$有可能是一个偏序关系。

例如上面提到的Transaction内部的program order $\mathrm{po}$的反序$\mathrm{po}^{-1}$。

$\max_\mathrm{R}(A)$和$\min_\mathrm{R}(A)$

For a total order $\mathrm{R}$ and a set $A$, we let $\max_\mathrm{R}(A)$ be the element $u \in A$ such that $\forall v \in A. \ v = u \lor (v, u) \in R$; if $A = \emptyset$, then $\max_\mathrm{R}(A)$ is undefined. In the following, the use of $\max_\mathrm{R}(A)$ in an expression implicitly assumes that it is defined.

直觉上，$\max_\mathrm{R}(A)$（$\min_\mathrm{R}(A)$）表示了非空集合$A$在序关系$\mathrm{R}$上的最后（早）一个元素。

例如figure 3(e)中的$\max_{\mathrm{po}}(T_1)$就是$\mathrm{write}(\text{acct1}, -40)$。

$T \vdash \mathrm{Write} \ x : n$和$T \vdash \mathrm{Read} \ x : n$

defining certain attributes of a transaction $T = (E, \mathrm{po})$. We let $T \vdash \mathrm{Write} \ x : n$ if $T$ writes to $x$ and the last value written is $n: \max_\mathrm{po}(E \cap \mathrm{WEvent}_x) = (\_, write(x, n))$.

直觉上$T \vdash \mathrm{Write} \ x : n$（$T \vdash \mathrm{Read} \ x : n$）表示在Transaction $T$内部的Event，按照program order，最后（早）一个对$x$的写入（读取）为$n$。

例如figure 3(e)中$T_1 \vdash \mathrm{Write} \ \text{acct1} : -40$。

Read Atomic

首先我们先学习一下论文中提到的几个基本性质以及一些较弱的隔离性级别。论文中介绍的最弱的隔离性级别是Read Atomic（RA），但是从RAMP figure 1可以看出，这一隔离性级别仍然高于ANSI SQL中定义的几种较弱的隔离性级别，并且RA和RR是略有区别的两种不同的隔离级别。比较RA和RU/RC/RR以及[1]中定义的各种性质之间的关系，涉及到如何形式化的表述RU/RC/RR，以及这些定义和各种性质之间的关系，限于篇幅不在本文进行解释，有兴趣的话可以在[6]的3.3中找到相关内容。

非形式化的，RA不允许出现 fractured reads [6]：

Definition 3.1 (Fractured Reads). A transaction $T_j$ exhibits the fractured reads phenomenon if transaction $T_i$ writes versions $x_a$ and $y_b$ (in any order, where $x$ and $y$ may or may not be distinct items), $T_j$ reads version $x_a$ and version $y_c$, and $c < b$.

[1]中首先介绍了2个基本性质：internal consistency axiom（INT）和 external consistency axiom（EXT）。

\[\forall(E, \mathrm{po}) \in \mathcal{H} . \forall e \in E . \forall x, n .\left(e=(\_, \operatorname{read}(x, n)) \land\left(\mathrm{po}^{-1}(e) \cap \mathrm{HEvent}_{x} \neq \emptyset\right)\right) \\ \implies \max_{\mathrm{po}}\left(\mathrm{po}^{-1}(e) \cap \mathrm{HEvent}_{x}\right)=(\_,\_(x, n)) \tag{INT}\]

直觉上，INT性质保证了，在一个Transaction内，如果读$x$读到了$n$，那么在同一个Transaction内如有上一个对$x$的操作，则一定是$\operatorname{read}(x, n)$或$\operatorname{write}(x, n)$，因此被称为 internal consistency axiom。

特别的，INT性质保证了一旦读到了一个值，那么之后无论读多少次，只要中间没有插入写操作，这个值都不会发生变化，即排除了 unrepeatable reads 的可能。

\[\forall T \in \mathcal{H} . \forall x, n . T \vdash \mathrm{Read} \ x : n \implies \\ \left(\left(\mathrm{VIS}^{-1}(T) \cap\{S \mid S \vdash \mathrm{Write} \ x :\_ \}=\emptyset \land n=0\right) \lor \\ \max_{\mathrm{AR}}\left(\mathrm{VIS}^{-1}(T) \cap\{S \mid S \vdash \mathrm{Write} \ x :\_ \}\right) \vdash \mathrm{Write} \ x : n\right) \tag{EXT}\]

直觉上，EXT性质保证了，在$T_1$中第一个读到$x = n$的操作，是因为在$\mathrm{VIS}$序中$T_1$的上一个Transaction中如存在$T_0$，则$T_0$中最后一次对$x$的写操作写入了$n$；否则$n = 0$（读到初始值）。这里由于$\mathrm{VIS}$是偏序关系，可能不止一个$T_0$这样的Transaction，此时取他们之间在$\mathrm{AR}$序中的最后一个。EXT性质保证了第一次读到$x$的值是因为“之前”的某个其他的Transaction写入的，因此被称为 external consistency axiom。

特别的，EXT性质保证了不会出现 dirty reads，因为没有commit（不管是abort还是on-going的）的Transaction不会出现在abstract execution中（这里不太严谨，因为没有INT性质的话不会保证中间不能读到任意奇怪的结果）。因此这一性质已经超出了Read Committed的要求（这里是我自己不太严谨的结论，不严谨的地方在于没有约定关于 dirty writes 的性质）。

此外，EXT性质保证了 atomic visibility：either all or none of its writes can be visible to another transaction。这也是为什么这个隔离性级别叫做Atomic Read的原因，它保证了不会出现fractured reads，因此可以用于一些需要完整性验证的场合，例如：

1. $T_1$写入了Alic和Bob之间双向成为了朋友关系，那么之后的$T_1$不会只观察到单向的关系，见Figure 3(b)

2. Secondary Index的场景

Causal consistency

尽管Read Atomic已经是一个比较强的一致性级别了，它能够保证一个Transaction中写入的内容总是一起被其他Transaction看到（不会只看到其中的一部分，fractured reads），但是不能保证这些写入在什么情况下被观察到。这意味着两种情况：

1. 在“真实时间”上过了足够久还没有被发现，极端情况下我们可以实现一个trivial数据库所有的写入其实都不生效，关于这方面的扩展讨论见[8]

2. 有可能违背因果（Causal）关系，例如Figure 3(a)中$T_3$已经读到了$T_2$写入的$\operatorname{write}(y,\text{comment})$，因此也应该能读到$T_2$读到的$\operatorname{read}(x,\text{post})$

Causal consistency要求不能违背因果关系，在当前的模型中，$\mathrm{VIS}$实际上捕获了因果关系，因此只需$\mathrm{VIS}$具有传递性即可保证因果一致性，即Figure 1中的TRANSVIS性质。

Parallel snapshot isolation

在[4]中论述过，Causal consistency是能够达到100% High Availability的最高一致性级别，这意味着不需要Replica之间进行任何通信，也可以实现Causal consistency，由此可能带来 lost update[2]的问题：

P4 (Lost Update): The lost update anomaly occurs when transaction $T_1$ reads a data item and then $T_2$ updates the data item (possibly based on a previous read), then $T_1$ (based on its earlier read value) updates the data item and commits.

例如Figure 3(c)尽管满足causual consistency，但是$T_1$的$\operatorname{write}(\text{acct}, 50)$就被冲掉了。为此，我们引入NOCONFLICT性质来约束这种情况：

\[\forall T, S \in \mathcal{H} .\left(T \neq S \land T \vdash\text{Write} \ x :\_ \land S \vdash\text{Write} \ x :\_\right) \\ \implies (T \stackrel{\mathrm{VIS}}{\longrightarrow} S \vee S \stackrel{\mathrm{VIS}}{\longrightarrow} T) \tag{NOCONFLICT}\]

直觉上，如果$T$和$S$都对同一个对象执行了写操作，那么这两个Transaction不能是Concurrent的，即其中一个必须知道另一个在它之前committed，这样就不会出现一个写入将另一个写入冲掉了的情况了。

Prefix consistency

TRANSVIS保证了一个具有因果关系的链条中的每个节点都可以观察到在它之前的所有因果关系，但是如果从一开始就出现了两组相互之间没有因果关系的链条，就会出现一些奇怪的现象，这些现象的根本原因在于写入没有在有界的时间内对其他Transaction可见[unbounded-staleness]。例如Figure 3(d)中，$T_1$和$T_2$分别写入了$x$和$y$，$T_3$看到了对$x$的写入但是没看到对$y$的写入，$T_4$看到了对$y$的写入但是没看到对$x$的写入。我们可以通过加强TRANSVIS来禁止这种情况出现，PREFIX：

If $T$ observes $S$, then it also observes all $\mathrm{AR}$-predecessors of $S$.

这里observes就是$\mathrm{VIS}$，由于$\mathrm{AR}$具有传递性，因此PREFIX性质蕴含TRANSVIS性质。形式化一点：

\[\mathrm{AR}; \mathrm{VIS} \subseteq \mathrm{VIS} \tag{PREFIX}\]

这意味着$T$能看到的Transactions，在其“实际提交”之前的所有Transactions以及他们之间的“实际提交”关系都是可见的。

Snapshot isolation

如[figure-1]所示，Snapshot isolation具有INT, EXT, PREFIX和NOCONFLICT性质。

Snapshot Isolation和Repeatable Read略有区别[6]（[2]的Remark 9也对两者进行了比较，但是不如[6]的模型细致）：

1. Definition 3.16 (Snapshot Isolation). A system provides Snapshot Isolation if it prevents phenomena G0, G1a, G1b, G1c, PMP, OTV, and Lost Updates.

2. Definition 3.20 (Repeatable Read). A system provides Repeatable Read isolation if it prevents phenomena G0, G1a, G1b, G1c, and Write Skew for nonpredicate reads and writes.

Serialisability

尽管Snapshot Isolation已经是相当强的一种一致性级别了，但是仍然会在某些时刻出现问题，例如Figure 3(e)中描述的 write skew 问题。$T_1$和$T_2$都检查了两个账户的余额之和大于100，并且分别从两个账户中取出了100。由于$T_1$和$T_2$是并发执行的，因此在检查时刻都能通过；由于$T_1$和$T_2$分别对不同的账户进行操作，因此也不会违背NOCONFLICT性质。但是最终，$T_1$和$T_2$都执行的结果将会使得最开始的检查限制被绕过，两个账户的总额变成负数。

对于这一点，我们可以使用性质TOTALVIS进行限制，即令VIS具有全序。考虑到$\mathrm{AR} \supseteq \mathrm{VIS}$，我们有$\mathrm{AR} = \mathrm{VIS}$，也就是Serialisability。

附录

总结

这篇论文对于建模和理解比较强的一致性有很大的帮助，但是缺点是模型不够细致以至于有些一致性级别表示不了或者区分不出来，有些anomaly的情况也没有列出来，但是对于大多数常见情况足够了。

后面省略了一些refinement正确性，和其他模型等价性相关的内容，对于工程师来说意义不大。

题外话

如[4]中的HAT Figure 2所示，其中左半部分主要是和multi-key之间协调相关的一致性级别，右半部分主要是single-key multi-replica之间协调相关的一致性级别，但是两者之间又有交叉。这篇论文主要论述的是Transaction的一致性模型，关于replication的一致性模型见[9]。

References

• [1] Cerone, A., Bernardi, G., & Gotsman, A. (2015). A Framework for Transactional Consistency Models with Atomic Visibility. 26th International Conference on Concurrency Theory, {CONCUR} 2015, Madrid, Spain, September 1.4, 2015, 42(Concur), 58–71. https://doi.org/10.4230/LIPIcs.CONCUR.2015.58

• [2] BERENSON H, BERNSTEIN P, GRAY J, et al. A critique of ANSI SQL isolation levels[J]. ACM SIGMOD Record, 1995, 24(2): 1–10.

• [3] ADYA A. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions[J]. 1999: 198.

• [4] Bailis, P., Davidson, A., Fekete, A., Ghodsi, A., Hellerstein, J. M., & Stoica, I. (2013). Highly Available Transactions: Virtues and Limitations. Proceedings of the VLDB Endowment, 7(3), 181–192. https://doi.org/10.14778/2732232.2732237

• [5] BURCKHARDT S. Principles of Eventual Consistency[J]. Foundations and Trends® in Programming Languages, Hanover, MA, USA: Now Publishers Inc., 2014, 1(1–2): 1–150.

• [6] Bailis, P., Fekete, A., Ghodsi, A., Hellerstein, J. M., & Stoica, I. (2016). Scalable Atomic Visibility with RAMP Transactions. ACM Trans. Database Syst., 41(3), 15:1—​15:45. https://doi.org/10.1145/2909870

• [7] ADYA A, LISKOV B, O’NEIL P. Generalized isolation level definitions[C]//Proceedings of 16th International Conference on Data Engineering (Cat. No.00CB37073). IEEE Comput. Soc, 2002(March): 67–78.

• [8] BAILIS P, VENKATARAMAN S, FRANKLIN M J, et al. Quantifying eventual consistency with PBS[J]. The VLDB Journal, 2014, 23(2): 279–302.

• [9] VIOTTI P, VUKOLIĆ M. Consistency in Non-Transactional Distributed Storage Systems[J]. ACM Computing Surveys, 2016, 49(1): 1–34.