algorithm - 程序员如何确保编译器创建正确的代码？

Question

在 SO 上阅读这个引人入胜的（也是投票率最高的问题），为什么处理排序数组比处理未排序数组更快？让我想知道编译器代码的正确性。

例如，答案指出：

Intel Compiler 11 做了一些神奇的事情。它交换了两个循环......

编译器程序员如何知道何时可以交换循环？

而且，一般来说，他们是否使用数学证明来证明结论？

编译器程序员如何知道他们的编译器会生成正确的代码？他们如何检验他们的结论？他们是否必须编写一个运行编译器的测试套件，并检查生成的代码是否正确？

Answer 1

编译器程序员如何知道何时可以交换循环？

编译器对代码运行一系列检查以确定交换循环是否安全。例如，如果代码没有完全内联，它可能无法交换循环。如果代码修改了 volatile 变量，它不会交换循环。如果代码存储在先前循环迭代中计算的值，编译器将不会交换循环。如果他们可以确定它是安全的，因为这些条件都没有被触发，编译器可以交换循环。

而且，一般来说，他们是否使用数学证明来证明结论？

不，他们只是制定优化和一组保守的测试来确保优化是安全的。随着时间的推移，他们开发了更多优化和更复杂的算法，以检测优化何时安全，即使在不太明显的情况下也是如此。

编译器程序员如何知道他们的编译器会生成正确的代码？

他们尽其所能。偶尔他们会犯错误。人们提交错误报告，然后他们修复它。

他们如何检验他们的结论？他们是否必须编写一个运行编译器的测试套件，并检查生成的代码是否正确？

他们绝对确实使用测试套件。当在 GCC 中检测到错误时，会专门将测试添加到测试套件中，以确保错误已修复且不会重新引入。

Answer 2

编译器程序员如何知道何时可以交换循环？

当修改不会根据语言标准改变程序的行为时，当更改不违背标准本身时。

例如，C 和 C++ 标准在一些地方说函数参数和子表达式的求值顺序是未指定的。这使编译器可以自由地生成代码，以它认为合适的任何顺序评估它们。如果您的程序依赖于特定的顺序，则它不符合标准，您无权责怪编译器“破坏”它。

编译器可能并且经常使用代码分析、逻辑和数学以及所有这些定理来优化代码。

在实践中，测试表明编译器是否做了正确的工作。

Answer 3

编译是一个复杂的过程。该程序被构造为一个图，编译器会根据开发人员提出的规则尽力“优化”这个图。

但是，不能保证生成的代码接近“最佳”。已经对所谓的“超级优化器”进行了研究，它们试图使用自动证明引擎生成真正优化的代码......即他们可以回答诸如“有没有办法编译这个算法使得它花费少于 X循环”。Denali就是我读过的这样一位超级优化者。对于某些架构，该技术比其他架构更容易。不利的一面是，这些超级优化器可能需要数小时甚至数天来编译一个简单的例程，这对大多数人来说是不可接受的。

Answer 4

任何用自己的语言编写的编译器的主要健全性测试之一是让它自己编译，然后使用生成的新编译器再次编译自己。生成的两个编译器应该是相同的模时间戳。

Answer 5

概括

好的，所以我同意一些答案，但我认为人们低估了编译器在转换和优化中的严格和保守程度。长话短说 - 尽管优化代码生成确实是一种魔法，并且 99% 的时间都使用启发式而不是证明（有人谈到了Denali超级优化器），但正确的代码生成实际上在数学上是合理的，而且它是经过设计的是这样。存在错误的事实是由于编译器代码库的巨大复杂性。作为一个侧节点，自动定理证明器可能有错误，即使它的每个部分在数学上都是合理的，所以编译器有错误的事实并不意味着它们是重写规则的随机集合。

现在，依次回答您的问题：

编译器程序员如何知道何时可以交换循环？

编译器理论的一个子领域称为依赖分析，它处理这样的问题。关于该主题有整本书，但对于您的特定问题：编译器将自动计算循环的迭代空间（如果边界是可计算的，请参阅底部的NB），它将计算出指令之间的依赖关系循环（有不同类型的依赖关系），它将计算循环的距离和方向向量，然后确定进行交换是否合法。维基百科关于此的文章只是给出了不同类型的依赖关系，但有指向其他子主题的链接，并且还引用了我提到的书。

而且，一般来说，他们是否使用数学证明来证明结论？

不，一般不会。还取决于我们所说的证明的含义-您是说使用定理证明器吗？例如，Denali论文使用 SAT 求解器。由 Microsoft Research @ Cambridge 开发的Dafny编译器和语言通过源级语言注释来验证您的代码。编译器会验证您的代码的正确性，尽管使用注释非常困难（我在大学的一个项目中与 Dafny 一起摆弄过，我根据经验发言）。另外，“一般不”是指不在gcc，llvm我和家人怀疑（但我没有检查）英特尔的icc. 再一次，我们在这里谈论的是类似 C 的源代码到机器级编译，没有什么比这更有趣的了。

编译器程序员如何知道他们的编译器会生成正确的代码？他们如何检验他们的结论？他们是否必须编写一个运行编译器的测试套件，并检查生成的代码是否正确？

其他答案广泛涵盖了这一点，因此无需多说。我想我可以补充一点，因为编译器在复杂性方面确实是野兽，所以对它们进行广泛的测试至关重要。另外，我想重申，即使在一段数学上合理的代码中（如果我们假设我们已经正式定义了这样的概念），处理该代码的基础设施中也可能存在错误，因此测试总是很重要的。

判决

编译器非常复杂。它们需要快速以启用无缝的编辑-编译-调试开发人员循环，并且还需要正确的 . 编译器对他们生成的代码的正确性是一种“本地数学上合理的”——编译器所做的每个转换都必须保留原始程序的语义。速度的提高是由启发式算法驱动的，这些算法是黑艺术技术的好例子，因为它们不能证明生成的代码会更快。他们也没有正式证明它是正确的，但是每个转换都旨在产生正确的语义保留代码。最后，编译器最热门的趋势（我猜现在计算机科学中的其他地方一样）是使用machine learning进行优化，所以我们将有更多的旋钮来调整 :) 耶

注意

编译器“后端”中的几乎所有东西，即代码生成器，要么是 NP 完全的，要么是不可判定的。特别是，无法确定循环交换是否合法，因为循环边界可以是任意表达式（比如函数调用）。但是，如果边界是可计算的（比如整数或简单的东西），那么这就是依赖分析开始的地方。