证明程序的等效性

Question

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

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

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

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

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

Answer 1

你问的是一个相当广泛的问题，但让我看看是否可以让你继续下去。

John Regehr 非常出色地调查了一些有关超级优化器的相关论文： https: //blog.regehr.org/archives/923

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

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

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

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