proof - 证明程序的等效性

Question

优化编译器的最终目的是在程序空间中搜索与原始程序等效但速度更快的程序。这已在实践中针对非常小的基本块完成:https://en.wikipedia.org/wiki/Superoptimization

听起来困难的部分是搜索空间的指数性质，但实际上并非如此；困难的部分是，假设你找到了你要找的东西，你如何证明新的、更快的程序真的等同于原始程序？

上次我研究它时，在证明某些上下文中程序的某些属性方面取得了一些进展，特别是在讨论标量变量或小的固定位向量时在很小的范围内，但在证明程序的等效性方面并没有真正取得进展当您谈论复杂的数据结构时，规模更大。

有没有人想出一种方法来做到这一点，甚至“模解决这个我们还不知道如何解决的 NP 难搜索问题”？

编辑:是的，我们都知道停机问题。它是根据一般情况定义的。人类是一个存在证明，这可以用于许多感兴趣的实际案例。

Answer 1

你问的是一个相当广泛的问题，但让我看看我是否能让你继续前进。

John Regehr 在调查一些关于 super 优化器的相关论文方面做得非常好:https://blog.regehr.org/archives/923

问题是你真的不需要为这些类型的优化证明整个程序的等效性。相反，您只需要证明给定 CPU 处于特定状态，2 个代码序列以相同的方式修改 CPU 状态。为了在许多优化(即大规模)中证明这一点，通常您可能首先在两个序列中抛出一些随机输入。如果它们不是等效的代码位，那么您可能会很幸运并很快地展示这一点(反证法)，然后您可以继续前进。如果您没有发现矛盾，您现在可以尝试通过计算成本高昂的 SAT 求解器来证明等效性。 (顺便说一句，如果您对 super 优化器感兴趣，Regehr 提到的 STOKE 论文特别有趣。)

现在看看整个程序的语义等效性，这里的一种方法是 CompCert 编译器使用的方法。本质上，编译器正在证明这个定理:

如果 CompCert 能够将 C 代码 X 转换为汇编代码 Y，则 X 和 Y 在语义上是等效的。

此外，CompCert 确实应用了一些编译器优化，实际上这些优化通常是传统编译器出错的地方。也许像 CompCert 这样的东西就是你所追求的，在这种情况下，编译器通过一系列细化过程来处理事情，它证明如果每次通过成功，结果在语义上等同于前一次通过。