利用基准测试加速Echidna:Haskell性能优化实战

本文详细介绍了如何通过性能分析工具发现并修复Echidna智能合约模糊测试工具及其依赖hevm的内存泄漏问题,包含具体的Haskell性能分析方法和优化方案,使内存使用减少数GB。

利用基准测试加速Echidna

在我去年夏天担任Trail of Bits助理期间,我致力于优化Echidna(Trail of Bits用Haskell编写的开源智能合约模糊测试工具)的性能。通过广泛使用分析器和其他工具,我成功定位并调试了Echidna的一个依赖项hevm中的巨大空间泄漏。现在这个问题已经修复,Echidna和hevm在某些测试用例上预计比之前少使用几GB内存。

在这篇博客文章中,我将展示如何使用性能分析来识别hevm中的深层性能问题,以及我们如何修复它,从而提升Echidna的性能。

Echidna概述

假设我们正在跟踪一个固定供应池。用户可以在彼此之间转移代币或根据需要销毁代币。这个池的一个理想属性可能是供应量永远不会增长;它只保持不变或随着代币转移或销毁而减少。我们如何确保这个属性成立?我们可以尝试编写一些测试场景,或手动证明它……或者我们可以用Echidna对代码进行模糊测试!

Echidna的工作原理

Echidna接收智能合约和关于其行为的断言(这些断言应该始终为真),两者都用Solidity编写。然后,利用从合约本身提取的信息(如方法名称和常量),Echidna开始生成随机交易序列并在合约上重放它们。它从旧序列中不断生成更长和新的序列,例如通过在随机点拆分它们或更改方法调用中的参数。

我们如何知道这些随机序列的生成覆盖了足够的代码以最终找到错误?Echidna使用覆盖引导的模糊测试——也就是说,它跟踪智能合约中实际执行的代码量,并优先考虑覆盖更多代码的序列以创建新序列。一旦找到违反我们期望属性的交易序列,Echidna就会尝试缩小它以最小化。然后,Echidna将所有信息转储到文件中以供进一步检查。

性能分析概述

Glasgow Haskell编译器(GHC)提供了各种工具和标志,程序员可以用它们来理解不同粒度级别的性能。以下是两个:

  • 编译时启用分析:这会修改编译过程,添加一个分析系统,将成本分配给成本中心。成本是围绕表达式的注释,完全测量这些表达式的计算行为。通常,我们感兴趣的是顶级声明,基本上是从模块导出的函数和值。
  • 收集运行时统计信息:在分析的Haskell程序中添加+RTS -s会显示运行时统计信息。它比分析更粗略,只显示程序的聚合统计信息,例如堆中分配的总字节数或垃圾回收期间复制的字节数。启用分析后,还可以使用-hT选项,该选项按闭包类型分解堆使用情况。

这两个选项都可以生成人类和机器可读的输出以供进一步检查。例如,当我们用分析编译程序时,我们可以输出JSON,可以在像speedscope这样的火焰图查看器中显示。这使得浏览数据并缩放到相关时间片变得容易。对于运行时统计信息,我们可以使用eventlog2html来可视化堆配置文件。

查看下面的火焰图和其他类似图,我得出结论,至少从初步调查来看,Echidna在内存使用方面并不臃肿。事实上,随着时间的推移,各种变化直接针对性能。(实际上,2022年Trail of Bits的冬季实习生发现了其覆盖率的性能问题,随后得到了修复。)但是,注意到大的蓝色区域了吗?那是hevm,Echidna用它来评估候选序列。鉴于Echidna在模糊测试时间的大部分都花在这个任务上,hevm占用大量计算能力是合理的。那时我将注意力转向研究hevm的性能问题。

Echidna中函数和调用栈的时间使用

分析器有时可能误导

性能分析很有用,它帮助我找到了hevm中的一个错误,修复后提高了Echidna的性能(我们将在下一节中介绍),但你也应该知道它可能误导。

例如,在分析hevm时,我注意到一些不寻常的事情。各种与光学相关的操作符(getter和setter)主导了CPU时间和分配。这怎么可能?原因是光学库没有正确内联其某些操作符。因此,如果你在启用分析的情况下运行此代码,你会看到%操作符占用了绝大部分分配和时间,而不是实际进行计算增量函数。但在运行优化二进制文件时不会观察到这一点,因为GHC可能已经决定内联该操作符。我详细写下了这个问题,它帮助光学库开发者关闭了去年开的一个问题!这个小插曲让我意识到,今后我应该编译启用和不启用分析的程序,以确保分析忠实于实际使用。

在hevm中找到我的第一个巨大内存泄漏

考虑以下程序。它重复哈希一个数字,从0开始,并将哈希写入内存中的某个地方(直到地址m)。它这样做n次。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
contract A {
  mapping (uint256 => uint256) public map;
  function myFunction(uint256 n, uint256 m) public {
    uint256 h = 0;
    for (uint i = 0; i < n; i++) {
      uint256 x = h;
      h = uint256(keccak256(abi.encode(h)));
      map[x % m] = h;
    }
  }
}

当我们改变n和m的值时,我们期望程序做什么?如果我们保持m固定并继续增加n的值,直到m的内存块应该被完全填充。因此,我们预计不会使用更多内存。这如下图所示:

保持m固定并增加n应该最终填满m。

令人惊讶的是,这不是我观察到的。hevm使用的内存随着n和m的函数线性增长。所以,出于某种原因,hevm继续分配内存,即使它应该重用它们。事实上,这个程序使用了如此多的内存,以至于可能使用数百GB的RAM。我在这里写了这个问题。

显示分配快速增长图

我认为如果这个内存问题影响hevm,它肯定也会影响Echidna。

不要只测量一次,测量N次!

性能分析为你提供单次运行的时间和空间数据,但这不足以理解程序运行更长时间时会发生什么。例如,如果你在数组长度小于20时分析Python的insertionSort函数,你可能会得出结论它比quickSort快,但渐近地我们知道情况并非如此。

同样,我对不同的以太坊程序“昂贵”(从hevm的角度来看)有一些直觉,但直到我测量了在EVM上运行的智能合约的性能,我才确定。以下是智能合约可以做什么以及它们如何与EVM交互的简要概述。

EVM由一个栈、内存和存储组成。栈限制为1024项。内存和存储都初始化为0,并由无符号256位整数索引。

内存是瞬态的,其生命周期限于交易的范围,而存储跨交易持久化。

合约可以在内存或存储中分配内存。虽然写入存储(持久区块链数据)在gas方面比内存(每交易的瞬态内存)昂贵得多,但当我们运行本地节点时,我们不应期望两种存储类型之间存在任何性能差异。

我编写了八个简单的智能合约,这些合约会压力测试这些各种组件。它们之间的基本共同点是它们都用一个数字(n)参数化,并且预计相对于该数字具有线性运行时。任何非线性运行时变化因此将指示异常值。这些是合约及其作用:

  • simple_loop: 循环和添加数字
  • primes: 质数的计算和存储
  • hashes: 重复哈希
  • hashmem: 重复哈希和存储
  • balanceTransfer: 重复转移1 wei到地址
  • funcCall: 重复函数调用
  • contractCreation: 重复合约创建
  • contractCreationMem: 重复合约创建和内存

你可以在此文件中找到它们的完整源代码。

我分析了这些合约,以收集它们在广泛n值范围内的性能信息。我按2的幂增加n,以便效果在早期更明显。这是我看到的:

我立即注意到hashes和hashmem测试用例肯定有问题。如果合约的运行时随着n的增加线性增加,hashes和hashmem线不会与其他线交叉。我们如何尝试证明这一点?既然我们知道每个点应该大致翻倍(忽略常数项),我们可以简单地绘制从一个点到下一个点的运行时比率,并画一条线指示我们期望什么。

宾果。hashes和hashmem明显偏离基线。然后我将精力转向分析这些特定示例,并查看它们依赖的任何代码。经过额外的分析,似乎重复拼接和重新拼接不可变字节数组(以模拟合约中写入的工作方式)导致字节数组相关的内存类型大小爆炸。本质上,hevm没有正确丢弃旧版本的内存。

ST来救援!

修复在概念上很简单,幸运的是,我的经理Artur Cygan几个月前已经提出了。首先,我们改变了hevm处理EVM计算中状态的方式:

1
2
- type EVM a = State VM a
+ type EVM s a = StateT (VM s) (ST s) a

然后,我们遍历了hevm处理EVM内存的所有地方,并实现了一个可以原地修改的可变向量(!)这是如何工作的?在Haskell中,操作状态概念的计算封装在State monad中,但不能保证程序执行期间只有一个内存副本。使用ST monad代替允许我们确保计算使用的内部状态对程序的其余部分不可访问。这样,hevm可以在仍然将程序视为纯函数的同时,破坏性地更新状态。

这是PR后的图表样子。最后一个测试用例的减速现在大约为3而不是5.5,并且就实际运行时而言,线性性更加明显。很好!

尾声:具体还是符号?

在我助理项目的最后几周,我运行了更详细的带有来源信息的分析。现在我们真正获得了x射线视觉,精确地看到内存分配在程序中的位置:

显示哪些数据构造函数使用最多内存的详细堆配置文件

所有生成的Prop术语是怎么回事?hevm支持符号执行,允许各种形式的静态分析。然而,Echidna只使用完全具体的执行。因此,我们从不接触hevm生成的约束。这留给未来的工作,希望将导致一个解决方案,其中hevm可以支持更优化的仅具体模式,而不损害其符号方面。

最后思考

在像Echidna这样的软件项目中,其有效性与其执行模糊测试的速度成正比,我们总是在寻找方法使其更快,而不使代码不必要地复杂。在像Haskell这样的环境中进行性能工程揭示了一些有趣的问题,并且肯定需要一个人准备好深入并推理编译过程和语言语义的行为。这是一门与计算机科学本身一样古老的艺术。

我们应该忘记小的效率,大约97%的时间:过早优化是万恶之源。然而,我们不应该放弃那关键3%的机会。 — Donald Knuth

如果你喜欢这篇文章,请分享: Twitter LinkedIn GitHub Mastodon Hacker News

comments powered by Disqus
使用 Hugo 构建
主题 StackJimmy 设计