Elle：黑盒数据库的事务一致性检查器

Elle 是一个用于黑盒数据库的事务一致性检查器。纯粹基于客户对交易的观察，并给定对数据类型和操作的一些最小约束，它可以告诉您该观察是否表现出各种交易异常。就像聪明的律师一样，Elle 会在故事中寻找不可能按该顺序发生的一系列事件，并使用该推论来证明故事不能自洽。概述：Elle 适用于多种数据类型，并且仅对事务结构设置了最小的、实用的约束。高效：Elle 在历史长度上是 ~线性的，并且 ~constant，而不是指数，关于并发性。有效：Elle 在我们检查过的每个数据库中都发现了意外异常，从内部一致性违规到反依赖循环、脏读、更新丢失到实时违规。声音：Elle 可以从 Adya、Liskov 和 O'Neil 的广义隔离级别定义中找到所有（非谓词）异常。 Elucidative：Elle 可以指出见证一致性违规的最小交易集；其结论易于理解和验证。该存储库包含 Elleconsistency 检查器的 Clojure 实现及其随附的测试套件，您可以使用它来检查自己的历史记录。我们的论文深入了解了 Elle 背后的目标和直觉，并对其稳健性证明进行了粗略的形式化。一个远未完成的正式证明草图是用 Isabelle/HOL 证明语言编写的。

如果您想使用 Elle 检查数据库，请参阅 https://jepsen.io； Elle 是内置的。如果你想在不使用 Jepsen 的情况下使用 Elle 检查你自己的历史记录，你可以将 Elle 作为依赖添加到任何 JVM 项目，并直接调用它的检查器函数。如果您使用的是非 JVM 语言，则可以将历史记录写入文件或流，并调用一个小型包装程序来生成输出。 Elle 仍在积极开发中，我们对其推理规则还不是 100% 有信心。 Jepsen 建议手动检查报告的异常以确保它们有效。如果您愿意做出贡献，我们特别欢迎您在形式证明和严格定义一致性模型方面提供帮助。想象一个数据库，其中每个对象（由 :x 或 :y 之类的键标识）都是一个数字列表。事务由读取 [:r :x [1 2 3]] 组成，它返回给定列表的当前值，并写入 [:append :y 4]，将一个数字附加到列表的末尾。我们构建了三个事务的历史记录，每个事务都已知已提交（:type :ok）。第一个事务将 1 附加到 :x 并观察到 ​​:y = [1]。第二个附加 2 到 :x 和 1 到 :y。第三个观察 x，并将其值视为 [1 2]。 => ( def h [{ :type :ok, :value [[ :append :x 1] [ :r :y [ 1]]]} { :type :ok, :value [[ :append :x 2] [ :append :y 1]]} { :type :ok, :value [[ :r :x [ 1 2]]]}])h 现在，我们要求 Elle 检查这个历史记录，期望它是可序列化的，并拥有它将异常转储到名为 out/ 的目录。 => ( pprint ( a/check { :consistency-models [ :serializable], :directory "out "} h)){ :valid? false, :anomaly-types ( :G1c), :anomalies { :G1c [{ :cycle [{ :type :ok, :value [[ :append :x 2] [ :append :y 1]]} { :type :好的, :value [[ :append :x 1] [ :r :y [ 1]]]} { :type :ok, :value [[ :append :x 2] [ :append :y 1]]}], :steps ({ :type :wr, :key :y, :value 1, :a-mop-index 1, :b-mop-index 1} { :type :ww, :key :x, :value 1, : value' 2, :a-mop-index 0, :b-mop-index 0}), :type :G1c}]}, :not #{ :read-committed}, :also-not #{ :consistent-view :cursor-stability :forward-consistent-view :monotonic-atomic-view :monotonic-snapshot-read :monotonic-view :repeatable-read :serializable :snapshot-isolation :strict-serializable :update-serializable}}

这里Elle可以根据T1和T2各自的读写情况推断出T1和T2之间的读写关系。 T2 和 T1 之间的写-写关系是可推断的，因为 T3 观察到 x = [1,2]，这限制了可能的追加顺序。这是一个 G1c 异常：循环信息流。 :cycle 字段显示该循环中的操作，而 :steps 显示循环中每对操作之间的依赖关系。基于这个异常，Elle 得出的结论是这个历史不是 read-committed ---这是 Elle 可以证明被违反的最弱的级别。此外，此历史记录还违反了几个更强的隔离级别，例如一致视图和更新可序列化。 $ cat out/G1c.txtG1c #0Let: T1 = {:type :ok, :value [[:append :x 2] [:append :y 1]]} T2 = {:type :ok, :value [[: append :x 1] [:r :y [1]]]}然后： - T1 < T2，因为 T2 观察到 T1 将 1 附加到键 :y。 - 但是，T2 < T1，因为 T1 在 T2 将 1 附加到 :x 之后附加了 2：矛盾！除了为每个单独的循环绘制一个图形之外，Elle 还为依赖图的每个强连接组件生成一个图。这有助于处理异常行为的范围，而周期显示尽可能小的交易集。这是一个来自更复杂历史的图，涉及实时边缘、写-写、写-读和读-写依赖关系： 作为用户，您进入 Elle 的主要入口点将是 elle.list-append/check 和 elle.rw-register/查看。两个命名空间也有用于生成事务序列的代码，您可以将这些代码应用于您的数据库；参见，例如，elle.list-append/gen。 Elle 有各种各样的异常和一致性模型；参见 elle.consistency-model 的定义。并非每个异常都可以检测到，但我们的目标是完整性。 Elle 期望其观察到的历史与 Jepsen 的格式相同。一个观察到的历史应该是一个按实时顺序排列的操作列表，其中每个操作都是一个如下形式的映射：

{ :type 之一:invoke, ok, :info, :fail :process 单个执行线程的逻辑标识符:value 事务;结构和语义各不相同}每个进程应该交替执行 :invoke 和 :ok/ :info/ :failoperations。 :ok 表示明确提交的操作。 :failed 表示它肯定没有发生——例如它被中止，从未提交到数据库等。 :info 表示不确定状态；交易可能发生也可能没有发生。在 :info 之后，一个进程可能不会执行另一个操作；调用在历史的其余部分保持开放。 elle.core：Elle 推理系统的核心。计算事务图并找到它们的循环。包括每个流程和实时订单的通用图表。 elle.rw-register：写/读寄存器。推理规则较弱，但基本适用于所有系统。对象是寄存器；写入盲目替换值。 elle.list-append：Elle 最强大的推理规则。对象是列表，写入将唯一元素附加到这些列表中。下图显示了 Elle 在一致性模型之间的关系：a -> b 表示如果 a 成立，那么 b 也成立。该结构的来源可以在 elle.consistency-model 中找到。此图显示了 Elle 异常之间的关系。箭头 a -> bimplies 如果我们在历史中观察到异常 a，那么 b 也存在于历史中。

Elle 可以从 Adya、Liskov 和 O'Neil 的广义隔离级别定义中检查每个非谓词异常。其中包括： 特定检查器可使用其他异常（例如垃圾读取、脏更新、不一致的版本顺序）。并非所有这些都已完全实现——有关详细信息，请参阅论文。不一致的版本顺序：推理规则建议对单个密钥进行循环更新。垃圾读取：读取观察到的状态不可能是任何写入的产物。此外，Elle 可以根据进程（例如会话）或实时顺序推断事务依赖关系，使其能够区分严格的可串行化和可串行化。对于列表，Elle 可以基于单次读取推断出键的 Adya 版本顺序的完整前缀。对于寄存器，Elle 可以根据初始状态、writes-follow-reads、进程和实时顺序推断版本顺序。当 Elle 声称可观察历史中的异常时，它具体意味着在与该观察历史兼容的任何抽象的 Adya 风格的历史中，要么存在相应的异常，要么发生了更糟的事情——例如中止的阅读。这是测试真实世界数据库的自然结果；如果数据库以正确的方式存在，它可能会表现出实际上没有发生的异常，或者掩盖了确实发生的异常。我们通过能够区分许多类别的读取并对许多异常进行采样来限制这个问题的影响——希望最终我们能幸运地看到异常的“真实情况”。

Elle 不完整：它可能无法识别被测系统中存在的异常。这是两个因素的结果：Elle 检查从真实数据库中观察到的历史记录，其中交易结果可能未被观察到，并且时间信息可能不像人们希望的那样精确。可串行化检查是 NP 完全的； Elle 有意将其推断限制为可在线性（或对数线性）时间内解决的推断。在实践中，我们认为 Elle 是“足够完整”的。不确定性通常仅限于未观察到的交易，或历史末尾的一小部分交易。这些图显示了 Elle 的性能与 Knossos 线性化检查器的对比，验证了不同长度 (l) 和并发 (c) 的历史记录，这些历史记录是从模拟的可序列化快照隔离的内存数据库中记录的。越低越好。一般来说，Elle 在几秒钟到几分钟内检查现实世界的历史，而不是几秒钟到几千年。在 Knossos 通常仅限于每个历史记录数百次操作的情况下，Elle 可以轻松处理数十万次操作。 Knossos 运行时随着并发呈指数变化； Elle 是有效的常量。随着并发性的增加，运行时会略有下降，因为更多的事务会因冲突而中止。 Knossos 也是温和的超线性历史长度； Elle实际上是线性的。

我还没有真正优化 Elle ---我相信它可以随着时间的推移变得更快。有一些地方（特别是在注册测试期间从事务图中推断版本顺序）可能会很痛苦；我会边走边打磨粗糙的边缘。 Elle 的版权为 2019--2020 Jepsen, LLC 和 Peter Alvaro。 Elle 库在 Eclipse 公共许可证 2.0 版下可用，或者，您可以选择 GPL-2.0 和类路径例外。 Elle 的灵感来自与 Asha Karim 的对话，Kit Patella (@mkcp) 编写了 Elle 检查器的第一个原型。