证明程序的等价性

Question

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

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

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

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

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

Answer 1

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

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

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

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

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

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