在软件开发中，测试是确保软件质量的关键环节。测试工程师通过编写测试用例并运行测试系统来验证实际输出是否符合预期。如果实际输出与预期相符，则测试通过。然而，对于像卫星、火箭、铁路信号、飞行控制器和防洪屏障这样至关重要且复杂的系统，仅仅通过测试是远远不够的。这些系统虽然不常被注意到，但它们对日常生活的影响巨大，一旦开始出现故障，后果不堪设想。想象一下，如果因为系统中的小错误导致火箭从天而降，或者火车因为系统的小错误而相撞，那将是多么可怕的事情。没有人愿意看到这样的失败，因为它们在生命和金钱上的代价都太高了。
为了确保这些关键系统的安全和可靠性，许多专门从事质量保证、安全性、可靠性、可靠性和性能的工程师们付出了巨大的努力，但这不是一项容易的任务。他们分析的系统通常是高度多线程或事件驱动的，由于它们可以响应的方式众多，因此很难进行全面的测试以确保正确性。
为了测试给定系统的所有可能响应，科学界在过去几十年里一直在研究模型检查。模型检查工具探索所有场景并验证响应是否满足预期。这些技术已经成功应用于验证NASA的火星探测器、朗讯科技的PathStar电话交换机和荷兰三角洲工程的风暴潮屏障控制系统。到目前为止，情况还不错。但是，过去的模型检查技术要求工程师创建并验证系统的模型，而最终需要正确运行的是系统本身。因此，在过去的十年里，来自NASA的人们开始在系统级别应用模型检查技术。
基于这个想法，和前任以及导师Theo Ruys组成了一个团队，在特温特大学开发了MoonWalker模型检查器。MoonWalker通过检查CIL字节码指令并探索线程的所有可能的交错来验证多线程.NET程序。它也是迄今为止唯一公开可用的.NET模型检查器，采用了一组高效的算法，在性能上与其他最先进的工具相当。可以在《Mono的软件模型检查》中了解到所有这些，它包含了模型检查的入门章节和现有算法的深入解释。
图1。使用MoonWalker的概念性概述。用户将.NET程序集及其内部指定的断言加载到MoonWalker模型检查器中，该检查器探索程序集的状态空间。如果没有发现断言违规，则输出OK。否则，生成一条导致断言违规的CIL指令跟踪。
算法：高效的模型检查就是采用最好的算法，否则很容易就会达到计算机处理能力的极限。已经看到许多案例研究，模型检查器完全消耗了数十GB内存和数十个处理核心的集群。这是模型检查社区普遍存在的问题，它促使和世界各地的同事急切地开发更好的算法。
因此，最近花了几个月的时间为MoonWalker开发了三种新算法；从理论上看，它们看起来好多了，但想看看它们是否真的能在实践中加速MoonWalker。自然地，需要尽可能高效地实现它们，以最大限度地利用它们，但这在一个像模型检查器这样复杂的工具中并不容易做到，它构建了一些最先进的算法。因此，大量使用了分析器来理解瓶颈并积极优化算法。
首先测量，然后优化：在开发MoonWalker时，读了一些关于模型检查中哈希的有趣论文，并回忆起经验，哈希函数在平均验证过程中被调用高达数十亿次。这里有一个机会来设计一个更快的哈希函数！基于循环多项式和具有恒定时间复杂度的Knuth哈希，这将比传统算法的线性时间复杂度快得多。因此，带着越来越兴奋的心情，这个新算法在纸上被设计出来，并被称为增量哈希。当证明了它背后的理论是正确的，热情地在MoonWalker中实现了它。
第一次验证运行的结果并不是预期的。使用了小型.NET模型，并简单地使用了cygwin时间命令来测量执行时间。没有减少，最初认为这是因为模型的简单性。制作了一些更复杂的模型并重新运行了验证——执行时间也没有减少。这令人困惑和失望，因为在理论上，增量哈希应该快得多。
图2。左边是用C#编写的一个简单的数据竞争。MoonWalker模型检查器（在左边的命令提示符中）成功地检测到了数据竞争。
开始怀疑.NET虚拟机是否能够将旧算法优化到与新算法一样高效。因此，旧的哈希算法被放大，增加了一些不可优化的循环，但这也没有导致执行时间的减少。
完全困惑，开始在谷歌上寻找答案，具体来说，是试图理解编译器和CPU如何优化指令代码。甚至使用Visual Studio内置的调试器逐步检查优化的CIL字节码。
突然，意识到应该测量在旧哈希函数和增量哈希函数中花费的累积时间，并寻找绝对差异。
立即开始在谷歌上搜索.NET分析器，并找到了几个。最终选择了ANTS分析器，因为它以一种快速理解的方式显示分析结果。使用详细模式的分析器，发现在旧哈希函数中花费的绝对时间比增量哈希函数高得多。事实上，是多次。所以大问题是：为什么这个差异没有反映在总运行时间上？
当处于详细模式时，ANTS可以显示一段源代码，并指示在每一行上花费的时间量。以这种难以置信的细粒度方式分析了旧的哈希函数和增量哈希函数……但仍然无法解释为什么没有差异！
然后，旧的优化智慧浮现在脑海中——在几年前的一篇旧的“优化Java代码”文章中读到的东西：应该只优化瓶颈，这是通过它们在总执行时间中的相对份额来测量的。快速查看表格显示，旧的哈希算法的相对份额接近零，所以插入一个更好的哈希算法不会对总执行时间产生影响。还意识到，尽管绝对时间差异仍然很大，但它是以毫秒为单位的。所以花费了所有的时间和精力去优化一个不需要优化的MoonWalker部分。
幸运的是，增量哈希的优点并不局限于一个漂亮的理论结果。对NASA开发的另一个模型检查器——SPIN模型检查器进行了分析，并观察到它们的哈希是一个瓶颈。在那里实现了增量算法，并立即看到了高达两倍的性能提升，这取决于模型。算法和广泛的实验结果最近也在SPIN'08（一个著名的模型检查会议）上发表。
同时，在分析和测量MoonWalker中哈希的影响时，确实发现它的垃圾收集器算法（不要与虚拟机中的垃圾收集器混淆）的份额要大得多——平均55%。认为这是一个巨大的优化机会，并制定了一个新的算法来减少这个份额。
图3。来自MoonWalker的分析数据。如图所示，大部分时间都花在了MarkAndSweepGC.Run()方法上。
测量、解释和优化：有很多机会可以优化模型检查器。但重要的是要优化那些重要的东西：在执行过程中占据最大相对份额的算法。发明了一个在纸上效果很好的算法，但在MoonWalker中并没有区别，过早地进行了优化。
除了测量瓶颈之外，解释结果同样重要——当最初使用ANTS分析器时，看了绝对时间，而应该看百分比。在这里正确使用分析器是很重要的！真正需要学习的教训是：首先测量，仔细解释，明智地优化。