优化高性能计算工具

模型检查

如今，许多计算机系统都通过样本测试来检查其“正确性”：测试工程师编写场景并运行测试系统。捕获系统的实际输出，并与预期输出进行比较，如果匹配，则测试通过。

但对于像卫星、火箭、铁路信号、机载飞行控制器和防洪堤坝这样高度关键（且复杂）的系统来说，这远远不够。它们通常不引人注目，但对日常生活有着巨大的影响，尤其是在它们开始出现故障时。想象一下，太空火箭从天而降，或者火车因系统中的小错误而相撞。没有人希望这样；失败的代价太高，无论是在生命还是金钱方面。许多专注于质量保证、安全、可靠性、稳定性和可执行性（performability）的工程师付出了全部努力来防止这种情况发生，但这并非易事。他们如此彻底分析的系统通常是高度多线程或事件驱动的，由于它们可能响应的方式数量巨大，因此彻底测试其正确性非常困难。

为了测试给定系统的所有可能响应，科学界在过去几十年中一直在研究模型检查。

模型检查工具会探索所有场景，并验证在每个实例中响应是否符合预期。这些技术已成功应用于验证 NASA 的火星探测器、Lucent Technologies 的 PathStar 电话交换机以及荷兰三角洲工程（Delta Works）防洪堤坝的防风暴潮控制系统。到目前为止，一切顺利。但过去，模型检查技术要求工程师创建并验证系统的模型，而最终需要正确运行的是系统本身。因此，在过去十年中，NASA 的人们开始在系统层面应用模型检查技术。

考虑到这一点，一个由我、我的前任和我们的主管 Theo Ruys 组成的团队在特温特大学开发了 MoonWalker 模型检查器。MoonWalker 通过检查 CIL 字节码指令并探索所有可能的线程交错来验证多线程 .NET 程序。它也是迄今为止唯一公开可用的 .NET 模型检查器，它采用了一组高效的算法，并且在性能方面与最先进的工具相当。您可以在《Mono 的软件模型检查》（Software Model Checking for Mono）一书中阅读所有相关内容，该书包含模型检查的介绍性章节和对现有算法的深入解释。

算法

高效的模型检查在于采用最佳算法，否则您很容易达到计算机处理能力的极限。我们见过许多案例研究，其中模型检查器完全消耗了拥有数十 GB 内存和数十个处理核心的集群。这是模型检查界普遍存在的问题，它促使我们和世界各地的同事们热切地开发更好的算法。

因此，我们最近花了几个月时间为 MoonWalker 开发了三种新算法；理论上它们看起来好得多，但我们想看看它们在实践中是否真的能加速 MoonWalker。自然，我们需要尽可能高效地实现它们，以最大限度地发挥它们的潜力，但这对于像模型检查器这样复杂的工具来说并不容易，它是由一些最先进的算法构建的。因此，我们大量使用了分析器来了解瓶颈并积极优化算法。

先测量，后优化

在开发 MoonWalker 时，我们阅读了一些关于模型检查中哈希处理的有趣论文，并回忆起我们的经验，即在平均验证过程中，哈希函数会被调用数十亿次。这是一个设计更快的哈希函数的绝佳机会！基于循环多项式和 Knuth 哈希，具有恒定的时间复杂度，这将比传统算法的线性时间复杂度快得多。于是，随着兴奋感的增长，这个新算法在纸上被开发出来，并命名为增量哈希。当我们证明了它背后的理论是健全的后，我们便充满热情地将其实现到 MoonWalker 中。

首次验证运行的结果并非如我们所料。我们使用了小的 .NET 模型，并简单地使用 cygwin time 命令来测量执行时间。没有出现任何下降，起初我们认为这是由于模型过于简单。我们构建了一些更复杂的模型并重新运行了验证——执行时间也没有下降。这令人费解且沮丧，因为理论上，我们的增量哈希应该快得多。

我们开始怀疑 .NET 虚拟机是否能够优化旧算法，使其效率与新算法一样高。于是，我们通过添加一些无法优化的循环来“撑爆”旧的哈希算法，但这也没有让我们减少执行时间。

完全困惑之下，我们开始搜索答案，特别是试图了解编译器和 CPU 如何优化指令代码。我们甚至使用 Visual Studio 内置的调试器，一步一步地检查了优化的 CIL 字节码。

灵光一闪，我们意识到我们应该测量在旧哈希函数和增量哈希函数中花费的累计时间，并寻找绝对差异。

我们立即开始搜索 .NET 分析器，并找到了几个。我们最终选择了 ANTS Profiler，因为它以一种可以快速概览并易于理解的方式显示分析结果。在详细模式下使用分析器，我们发现花费在旧哈希函数上的绝对时间远高于增量哈希函数。事实上，是多倍。所以最大的问题是：

为什么这个差异没有反映在总运行时间中？

在详细模式下，ANTS 可以显示一部分源代码，并指示每行花费的时间。我们以这种极其精细的方式分析了旧哈希函数和增量哈希函数……但仍然无法解释为什么没有差异！

这时，我们想起了旧的优化智慧——我们几年前在一篇关于“优化 Java 代码”的老文章中读到的东西。

我们应该只优化瓶颈，而瓶颈由它们在总执行时间中所占的相对比例来衡量。

快速查看表格后发现，旧的哈希算法的相对比例接近零，因此插入一个更好的哈希算法对总执行时间没有影响。我们还意识到，绝对时间差虽然仍然很大，但以毫秒为单位。所以，我们花费了所有时间和精力进行的优化，是 MoonWalker 一个不需要优化的部分。

幸运的是，我们的增量哈希的优点不必仅限于一个巧妙的理论结果。我们对 NASA 开发的另一个模型检查器——SPIN 模型检查器——进行了分析，并观察到它们的哈希处理是一个瓶颈。我们将增量算法在那里实现，并立即看到了性能高达两倍的提升，具体取决于模型。我们的算法和广泛的实验结果也已在 SPIN'08（一个知名的模型检查会议）上发表。

此外，在分析和测量 MoonWalker 中哈希处理效果的同时，我们确实发现其垃圾收集器算法（不要与虚拟机中的垃圾收集器混淆）的占比要大得多——平均为 55%。我们将其视为一个绝佳的优化机会，并开发了一个新算法来降低这个占比。