在 TLA+ 中扩展 MVCC 以实现可串行化 (2024)

# 扩展MVCC以实现可串行化：基于TLA+的方法 来源：https://surfingcomplexity.blog/2024/11/03/extending-mvcc-to-be-serializable-in-tla/ 在[上一篇博客](https://surfingcomplexity.blog/2024/10/31/multi-version-concurrency-control-in-tla/)中，我们看到基于多版本并发控制（MVCC）的事务隔离策略并未实现[可串行化](https://jepsen.io/consistency/models/serializable)隔离级别，而是实现了一种称为[快照隔离](https://jepsen.io/consistency/models/snapshot-isolation)的更弱的隔离级别。本文将讨论如何基于 Michael Cahill、Uwe Röhm 和 Alan Fekete 发表的研究成果，对该MVCC模型进行扩展以实现可串行化。 我编写的模型可在 https://github.com/lorin/snapshot-isolation-tla 仓库的 SSI 模块中找到（[源码](https://github.com/lorin/snapshot-isolation-tla/blob/main/SSI.tla)、[PDF](https://github.com/lorin/snapshot-isolation-tla/blob/main/SSI.pdf)）。 ## 关于符号约定的快速说明 本文中，我用 r[x,1] 表示读取 x 的值为1，即事务读取对象 x 并返回值为1。如上一篇所述，可以将读取想象为以下SQL语句： ```sql SELECT v FROM obj WHERE k='x'; ``` 类似地，我用 w[y,2] 表示写入 y←2，即事务将对象 y 的值设为2。可将其想象为： ```sql UPDATE obj SET v=2 WHERE k='y'; ``` 最后，我们假设存在一个初始事务 T0，它将所有对象的值设为0，并在任何其他事务开始之前提交。  ## 背景 ### SQL隔离级别与现象 [ANSI/ISO SQL标准](http://web.cecs.pdx.edu/~len/sql1999.pdf)定义了四种事务隔离级别：读未提交、读已提交、可重复读和可串行化。标准根据这些级别所预防的"现象"来定义它们。例如，"脏读"现象是指一个事务读取了另一个尚未提交的并发事务所做的写入。这些现象很危险，因为它们可能会违反软件开发人员对数据库行为的假设，从而导致软件行为不正确。 ### 标准的问题与新隔离级别 Berenson 等人指出标准的表述存在歧义，在两种可能的解释中，一种是不正确的（允许无效的执行历史），另一种则过于严格（禁止了有效的执行历史）。过于严格的解释隐含地假设并发控制将使用锁来实现，这排除了基于替代方案（特别是多版本并发控制）的有效实现。他们还提出了一种新的隔离级别：快照隔离。 ### 形式化现象与反依赖 Adya 在其博士论文中引入了一种新的形式化方法来推理事务隔离。该形式化基于事务之间直接依赖关系的图。 Adya 引入的一种依赖类型称为**反依赖**，它对于区分快照隔离和可串行化至关重要。 两个并发事务之间的反依赖是指一个事务读取了某个对象，而另一个事务将该对象写成了不同的值，例如：  T1 对 T2 存在反依赖：T1 必须在串行化顺序中先于 T2：  在依赖图中，反依赖用 **rw** 标记，因为执行读取的事务必须排在执行写入的事务之前，如上所示。 Adya 证明，对于支持快照隔离的实现来说，要产生非可串行化的执行历史，依赖图中必须存在一个包含反依赖的环。 ### 快照隔离中的非可串行化执行历史 在《让快照隔离可串行化》论文中，Fekete 等人进一步缩小了快照隔离导致非可串行化执行历史的条件，证明了以下定理： > 定理2.1：假设 H 是在快照隔离下产生的多版本历史，并且不是可串行化的。那么在串行化图 DSG(H) 中至少存在一个环，并且我们声称在每个环中，存在三个连续的事务 Ti.1、Ti.2、Ti.3（Ti.1 和 Ti.3 可能是同一个事务），使得 Ti.1 和 Ti.2 是并发的，存在边 Ti.1 → Ti.2；Ti.2 和 Ti.3 也是并发的，存在边 Ti.2 → Ti.3。 他们还指出： > 由引理2.3，这两个并发边都必须是反依赖：Ti.1 → Ti.2 和 Ti.2 → Ti.3。 这意味着，在非可串行化的快照隔离历史中，必须始终出现以下两种模式之一：  ### 修改MVCC以避免非可串行化历史 Cahill 等人提出了一种对MVCC的修改，可以动态识别可能导致非可串行化历史的潜在有问题的交易，并将其中止。通过中止这些交易，所得算法保证了可串行化。 正如 Fekete 等人所证明的，在快照隔离下，只有当存在一个同时具有入站和出站反依赖边的事务（称为**枢轴事务**）时，才可能形成环。  他们的方法是识别并中止枢轴事务：如果一个活动事务同时包含出站和入站反依赖，则该事务被中止。注意这是一个保守算法：它中止的一些事务可能本身仍然会产生可串行化的执行历史。但它确实保证了可串行化。 他们对MVCC的修改涉及一些额外的簿记： 1. 每个事务执行的读取操作 2. 哪些事务有出站反依赖 3. 哪些事务有入站反依赖 跟踪读取是必要的，因为反依赖总是涉及一个读取（出站依赖边）和一个写入（入站依赖边）。 ## 为可串行化扩展我们的MVCC TLA+模型 ### 添加变量 我创建了一个名为 *SSI* 的新模块，代表"可串行化快照隔离"。我扩展了MVCC模型，添加了三个变量来实现Cahill等人算法所需的额外簿记。MVCC已经跟踪了每个事务写入的对象，但现在我们还需要跟踪读取。 - *rds* – 哪些事务读取了哪些对象 - *outc* – 具有出站反依赖的事务集合 - *inc* – 具有入站反依赖的事务集合  ### 行为变化：新的中止机会 以下是MVCC中 *Next* 动作与SSI中等价动作的对比。  在我们原始的MVCC实现中，读取和提交总是成功的。现在，尝试读取或尝试提交也可能导致中止，因此我们需要添加一个动作，我将其命名为 *AbortRdS*。 提交现在也可能失败，因此我们不再使用单步的 *Commit* 动作，而是使用一个 *BeginCommit* 动作，该动作将通过 *EndCommit* 成功完成，或通过 *AbortCommit* 动作失败中止。写入也可能因引入枢轴事务而中止。 ### 用模型检查器查找中止行为 以下是我如何使用TLC模型检查器生成新中止行为的见证： ### 中止读取 为了让模型检查器生成一个中止读取的跟踪，我在 MCSSI.tla 文件中定义了以下不变量：  然后在 MCSSI.cfg 文件中将其指定为模型检查器要检查的不变量： ``` INVARIANT NeverAbortsRead ``` 由于中止读取确实可能发生，模型检查器返回了一个错误，并给出了以下错误跟踪：  生成的跟踪如下所示，红色箭头表示反依赖。  ### 中止提交 类似地，我们可以通过指定以下不变量来让模型检查器识别提交失败的情景：  检查器找到了以下违反该不变量的例子：  当 T2 正在提交过程中时，T1 执行了一次读取，这使 T2 变成了枢轴事务，导致 T2 中止。  ### 使用精化映射检查可串行化 就像之前对MVCC所做的那样，我们可以定义从SSI规范到可串行化规范的精化映射。你可以在 SSIRefinement 模块中找到它（[源码](https://github.com/lorin/snapshot-isolation-tla/blob/main/SSIRefinement.tla)、[PDF](https://github.com/lorin/snapshot-isolation-tla/blob/main/SSIRefinement.pdf)）。它与 MVCCRefinement 模块（[源码](https://github.com/lorin/snapshot-isolation-tla/blob/main/MVCCRefinement.tla)、[PDF](https://github.com/lorin/snapshot-isolation-tla/blob/main/MVCCRefinement.pdf)）几乎相同，只是做了些微小的调整来处理新的中止场景。 主要区别在于，现在精化映射应该确实成立，因为SSI保证了可串行化！当我针对精化映射运行模型检查器时，未能找到反例，这让我对模型有了一定的信心。当然，这并不能*证明*我的实现是正确的，但对于学习练习来说已经足够。 ## 尾声：扩展TLA+规范 可串行化快照隔离提供了一个很好的例子，说明何时可以扩展现有规范，而不是从头开始创建新规范。 即便如此，扩展现有规范仍然需要不少工作。我怀疑采用复制-粘贴-修改的方法会更省力。不过，我发现在学习如何通过扩展来修改规范的过程中，这是一次有用的练习。