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

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}$.

一些符号

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

Read Atomic

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

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

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$.

中首先介绍了 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$ 不会只观察到单向的关系，见

2. Secondary Index 的场景

Causal consistency

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

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

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

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

Parallel snapshot isolation

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

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.

例如尽管满足 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]。例如中，$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}\]

Snapshot isolation

如所示，Snapshot isolation 具有 INT, EXT, PREFIX 和 NOCONFLICT 性质。

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

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 已经是相当强的一种一致性级别了，但是仍然会在某些时刻出现问题，例如中描述的 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。