Erlang maps深度测试

介绍

Erlang 在 17.0 版中引入了一个新的数据结构，即 map()。这种结构是从键（key）到值（value）的有限映射，具有扁平的内部表示：映射本质上是两个数组：一个排序的键数组和一个值数组。反过来，这种所谓的flatmap表示对于较小尺寸的map是有效的，但它们对于大尺寸的map表现不佳。

18.0 版将消除大尺寸map的问题。在 18.0 中，一旦map增长到足够大，map就会在内部切换为使用 HAMT（哈希数组映射树）。它是一种巧妙的数据结构，将哈希表的属性与（级别压缩的）trie 相结合，以提供快速查找和持久性。这与 Clojure、Scala 和 Haskell（无序容器）等数据结构语言使用的相同。它们是由现在已故的 Phil Bagwell 设计的，而 Erlang 变体依靠 Clojure 中 Rich Hickey 的工作。

然而，这种新结构需要测试。 Erlang 是一门以运行稳定性而不是执行速度而自豪的语言。因此，显然应该在 18.0 最终发布之前尝试广泛地测试 Erlang Maps。我决定通过为 Erlang 中的低级映射操作构建 Erlang QuickCheck 模型，然后针对当前的稳定版本以及 18.0-rc1 候选版本进行测试，看看我们能走多远。

这篇博文的目的是讲述有关当前 QuickCheck 模型的故事。模型中有多少行代码，以及通过生成测试开始测试所需的工作量有多少。它还作为如何在实际项目中使用 QuickCheck 的示例。它用于娱乐和教学——或者至少这是我的希望。

将有多个博客文章，因为将工作分成多个部分感觉是正确的。第一部分介绍如何生成数据和第一个简单的测试。后面的部分将讨论更复杂的模型，它使用状态机来驱动测试的生成。

QuickCheck primer

QuickCheck[1] 类似于模糊测试。模糊器用险恶的输入轰炸系统以破坏它——这样人们就可以利用错误——QC模型通过随机执行命令来检查系统的内部一致性。关键的区别在于，虽然 fuzzer 是黑盒的，并且通常对程序的内部工作有相对简单的理解，但 QC 测试是一个模型。它知道在给定情况下应该发生什么，并确保它是这样的。这使 QC 模型更加精确，因为它可以利用先验知识来指导接下来应该发生的事情。这种额外功能的代价是首先必须提出一个合适的模型。

在完整的模型检查中，首先要生成被测系统 (SUT) 的模型——一种简化的正式描述。然后，模型检查器通过系统地尝试每个可能的状态来详尽地验证模型相对于 SUT 的正确性。这种操作的复杂性在于某些模型表现出无限的命令序列。为了处理这些问题，可能有必要证明一个人有一个稳定的“循环”，以便在无限序列上打结，可以这么说。

QuickCheck[1] 作为概率模型检查器运行，因为我们不会详尽地检查模型。相反，我们从模型中得出随机事件轨迹并验证它们是否正确。用 John Hughes 的话来说，我们不写测试；我们生成它们。通过简单的配置，我们可以通过生成更多测试来调整我们对测试的信心。花更多的时间让我们更接近令人筋疲力尽的模型检查算法。我们还可以决定我们对模型的哪些区域感兴趣。我们可以权衡系统，将事件偏向某些我们知道在系统中更难纠正的区域。

任何测试系统都有一个无法进一步观察的规格限制。甚至像 Coq 这样的证明辅助系统也无法验证不属于规范的属性。我们只是希望有足够的测试在主题上形成一个保护性的网络：数学、程序或硬件，使得错误极不可能持续存在。我们希望保护网内的任何偏差都能在整个网络中引起反响，以便我们最终发现错误。简而言之，

Testing shows the presence, not the absence of bugs — Dijkstra, 1969

然而，事实证明 QuickCheck 在显示错误存在方面是有效的。 该方法倾向于在程序中发现非常细微的错误，这些错误后来被发现是恶意的而不是良性的。 这对于适度的额外编程工作。 虽然编写起来比单元测试慢，但一旦模型启动并运行，优势就会翻千倍。 能够在一夜之间运行几百万个测试，所有不同的测试通常会在代码库中发现问题。

Erlang QuickCheck 是 QuickCheck 理念的一个实现。 它定义了一种用于编写模型的领域特定语言。 然后它包含了针对真实世界代码运行这些模型的工具。

策略

必须做的第一件事是想出一个测试map的策略。我们立即将低级映射从与编译器有关的事物中分离出来。映射语法是特定于编译器的。但在测试符号之前，我们应该测试“map”模块是否正确。如果没有在较低水平上建立信心，测试一个没有什么意义。

其次，测试用例应该是无状态的还是有状态的。在无状态测试用例中，快速检查模型没有状态，因此在调用map之间没有知识（也就是说，它更接近于 fuzzer）。对于纯函数，这通常是一种足够的测试方法，但真正的程序很少是完全纯粹的。我们想利用关于“什么”和“什么时候”的知识：我们想知道map内任何时间点的内容，以便我们决定要做什么。例如，我们想检查我们是否可以删除map中的现有元素。为此，我们必须知道map中有哪些元素——即状态。同样要检查map中不存在的元素是否被删除，我们必须知道map中没有哪些元素——同样是状态。

此外，我们需要查看两种类型的数据生成：

一，我们需要生成随机的map key和map value，我们可以用来操作map。我们还需要能够快速生成随机map。也就是说，我们需要生成可以推送到我们在“map”模块中调用的函数的具体数据。第二，我们需要从“map”模块生成随机命令。这使我们能够避免命令总是相同的静态测试。我们将在每个测试中运行数十个（有时是数百个）命令，随机决定要做什么，以确保“映射”调用的任何组合都是稳定的。在 Erlang QuickCheck 中，我们有“eqc_statem”系统，它将测试编码为状态机。反过来允许有状态的命令生成。 对于状态机模型，我们可以利用同构。受某些约束的 K/V 对列表在任何时候都与映射同构。使用“maps”模块中的函数更改map对列表有相应的操作。这导致模型应该使用map的列表表示，然后验证map是否以正确的方式操作。这是 QuickCheck 建模的一个常见技巧：模型具有高级数据结构的简单表示。因此我们可以使用简单且未优化的模型来确保复杂且优化的结构是正确的。

注意：有人可能认为有必要让模型快速执行。这种情况很少发生，如果有的话。模型应该专注于清晰度和可读性。阅读高级数据表示比阅读简单表示要困难得多。此外，模型如何缩小对于生成最少的反例很重要。通常，这意味着您需要一个效率较低的模型，但这种牺牲会产生最小化的反例。

为了检查地图，我们使用了两个模型。一个是对映射的简单同构属性的简单无状态测试。另一种是使用上述 list({K, V}) 表示的更高级的有状态测试。通过将模型一分为二，我们可以先剔除简单的属性。如果简单的无状态模型失败，通常更容易找到罪魁祸首。此外，一旦简单模型通过，它提供了一些可以替代更高级模型的信心。它可能不会以某些方式失败。

生成map数据

首先，我们需要解决如何生成map内容。 如果我们要针对map触发随机命令，我们需要能够为map生成参数。 假设我们要生成一个 maps:put/3 命令。 它被称为 maps:put(Key, Value, Map)，因此我们需要能够生成随机键、随机值以及随机映射。

我们定义映射键和值将使用相同的生成器：

%% Keys and values are map terms
map_key() -> map_term().
map_value() -> map_term().

然后我们可以在 map_term() 函数中定义真正的map生成器：

map_term() ->
    ?SIZED(Sz, map_term(Sz)).

我们在 QuickCheck 中使用标准技巧。 ?SIZED 宏允许我们通过将生成的内容放入显式变量 Sz 中来获取当前大小。 大小通常在运行中从 0 左右开始，然后在随机测试过程中增加到 40 左右。 通过访问大小，我们可以控制如何生成给定大小的map项：

map_term(0) ->
    frequency([
       {100, oneof([int(), largeint(), atom(), binary(),
                    bitstring(), bool(), char(), evil_real()])},
       {10, oneof([function0(int()), function2(int())])},
       {10, eqc_gen:largebinary()}
    ]);
map_term(K) ->
    frequency([
        {40,
          map_term(0)},
        {1,
          ?LAZY(list(map_term(K div 8)))},
        {1,
          ?LAZY(?LET(L, list(map_term(K div 8)),
                     list_to_tuple(L)))},
        {1,
          ?LAZY(eqc_gen:map(map_term(K div 8),
                            map_term(K div 8)))}
    ]).

这里有两种情况。 生成大小为 0 的map将始终创建一个标量值。 它将加重它的一代。 120 次中有 100 次将生成整数、原子、二进制文件、布尔值等。 120 次中有 10 次将生成一个包含 0 或 2 个参数的函数（它们是纯的、确定的并返回整数）。 120 个中有 10 个会生成一个大的二进制文件（65 字节到 64 KB 之间）。 现实是邪恶的：

evil_real() ->
   frequency([
     {20, real()},
     {1, return(0.0)},
     {1, return(0.0/-1)}]).

如果有人想知道为什么这些很有趣，请考虑 erlang:phash2(0.0) 与 erlang:phash2(0.0/-1)…[2]。

如果生成大小为 K 的映射项，则 43 次中的 40 次会生成一个标量。 但有时会生成映射项列表、元组或映射项映射。 递归调用将大小除以很多，以确保下一代更小，并且我们最终会达到标量。 ?LAZY 参数避免生成递归复合变体，除非频率/1 组合器最终选择该分支。 如果我们不使用 ?LAZY，那么我们每次都会生成所有的树，然后在树中挑选。 有了这个，我们只在树中生成一个“路径”，这要快得多。 Haskell 程序员免费获得此功能，但在严格的语言中，需要明确说明何时需要延迟运行。

现在，我们可以查看生成键/值对列表：

gen_map() ->
  ?SIZED(Sz, resize(Sz * 15,
     list({resize(Sz, map_key()), resize(Sz, map_value())}))).

map_list() ->
gen_map().

map_map() ->
?LET(ML, map_list(), maps:from_list(ML)).

gen_map() 使用 ?SIZED 宏来获取当前的生成大小。 然后我们将列表生成器调整为 15 倍，但对键和值保持正常。 这使我们可以默认生成非常大的列表，而无需进行更多调整。

Erlang 18.0 内部具有 HAMT 结构，其切换到 HAMT 的内部断点目前是 32 个元素。 因此，我们需要确保在该范围内很好地生成列表，以测试 HAMT 结构的行为是否符合预期。 此外，如果我们发现错误，拥有 400 个元素的列表也不是问题。 QuickCheck 通过查找可以从列表中删除的元素来缩小列表。 因此，我们很可能会找到一个小得多的列表作为反例。

使用 gen_map()，我们可以直接生成适合map的列表。 我们可以通过调用 map_list() 生成map，然后使用 maps:from_list/1 的输出来构建包含内容的map。

无状态测试

map支持函数 f = maps:from_list/1 和 g = maps:to_list/1。 这两个函数在 map(A,B) 的域 M 和 list({A, B})[3] 的域 L 之间形成了结构同构。 我们可以利用这一点，因为如果 m 是 M 中的任何映射，则 f(g(m)) = m。 如果 l 在 L 中，则 g(f(l)) = l。 这建立了与数学范畴相同意义上的同构。

我们可以在两个 QuickCheck 属性中实现这些规则。 fg 变体如下：

prop_list_iso_fg() ->
    ?FORALL(M, maps_eqc:map_map(),
        begin
            List = maps:to_list(M),
            M2 = maps:from_list(List),
            equals(M, M2)
        end).

它本质上是上述要求的实现。 运行 gf 路径的对应项涉及更多：

prop_list_iso_gf() ->
    ?FORALL(L, maps_eqc:map_list(),
      begin
        LD = dedup(L),
        M = maps:from_list(L),
        LD2 = maps:to_list(M),
        equals(lists:sort(LD), lists:sort(LD2))
      end).

该变体必须从列表中删除重复键，以使 L 域以明确定义的方式与 M 同构。 并且必须对结果进行排序，以确保列表具有规范的表示。 Maps 可以以任何顺序返回 K/V 对。

在使用 18.0 之前，我们在当前稳定版本 17.4.1 上运行测试用例。 对这些中的每一个运行 100 次测试结果都很好：

4> eqc:quickcheck(maps_iso_eqc:prop_list_iso_fg()).
....................................................................................................
OK, passed 100 tests
true
5> eqc:quickcheck(maps_iso_eqc:prop_list_iso_gf()).
....................................................................................................
OK, passed 100 tests
true

Binary变体

map可以通过函数 term_to_binary/2 和 binary_to_term/1 进行转换。 这些函数用于序列化数据，是 Erlang 的核心。 分发协议使用这些的变体。 许多需要传输erlang项目的地方都受益于紧凑、压缩的二进制表示。 同样，它是一个同构，因为我们可以从一个映射来回转换。 如果有足够的耐心，我们还可以构建一个二进制文件，将其解码为一个映射项。 但通常这被忽略了，因为从头开始构建二进制文件并不容易。

term_to_binary/2 函数接受一个选项列表，我们可以在测试中对其进行编码：

opts() ->
  ?LET({Compressed, MinorVersion},
    {oneof([[], [compressed], [{compressed, choose(0,9)}]]),
     oneof([[], [{minor_version, choose(0,1)}]])},
       Compressed ++ MinorVersion).

然后我们可以使用 opts() 生成器来生成真正的测试用例：

prop_binary_iso_fg() ->
    ?FORALL([Opts, M],
      [opts(), maps_eqc:map_map()],
         begin
           Binary = term_to_binary(M, Opts),
           M2 = binary_to_term(Binary),
           equals(M, M2)
         end).

它的工作原理与 list_fg 的情况完全相同：在二进制表示之间来回翻转并验证是否相等。 我们在 Erlang 17.4.1（稳定版）上运行了 100 个测试用例：

13> eqc:quickcheck(maps_iso_eqc:prop_binary_iso_fg()).
....Failed! After 5 tests.
#{-3878269413 => hill,
  -1 => stone,
  #Fun<eqc_gen.133.121384563> => sand,
  <<3:2>> => 0.0} /= 
#{-1 => stone,
  -3878269413 => hill,
  #Fun<eqc_gen.133.121384563> => sand,
  <<3:2>> => 0.0}
Shrinking xxxx.x.xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx................................xxxxxxxxxxxxxxxxxxxxxxxxxxxx(x10)xxxxxxx(x1).x(35 times)

#{-1 => flower,2147483647 => flower} /=
#{2147483647 => flower,-1 => flower}
false

啊哈！ 5次测试失败，看起来很可疑！ map的内部顺序突然颠倒了。 这违反了关于内部flatmap表示的假设。 事实上，Wolfram Alpha 报告说——除了是素数——2147483647 也是 2³¹-1。 当我报告它时，它引起了一些警钟[4]，并且一个更新的稳定版本的 Erlang 将有一个修复（OTP-12623 在当前的维护分支上，如果运气好的话，它将在 17.5 中）。

更进一步深入

稍后的文章将介绍用于检查map模块的状态机“maps_eqc”模型。 它验证“map”模块的每个命令并报告更多统计信息。 目前的工作正在进行中，我们正在使用这些模型从 Erlang 18.0 中清除错误，并获得信心，我们不会在新的 HAMT 实现中引入明显的错误。 在这里，我们还修复了我们发现的现有错误[5]。 该模型已经在候选版本 18.0-rc1 中证明了它的价值，并发现了错误。 但随着 OTP 团队在候选版本之上的最新补丁，这些模型不再引发错误。

如果您对完整模型感兴趣，它是在 Apache 2.0 许可下开源的（在撰写本文时，提交 ID 为 5a9523f98635。预计模型会随着时间而改变）：