验证程序的等价性

优化编译器的最终目的是在程序空间中搜索等价于原始程序但速度更快的程序。这已经在实践中用于非常小的基本块：https://en.wikipedia.org/wiki/Superoptimization 验证程序的等价性

听起来很难的部分是搜索空间的指数性质，但实际上它不是;最难的部分是，假设你找到了你想找的东西，你如何证明这个新的，更快的程序与原始程序真的是相同的？

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

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

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

2017-06-22 rwallace

可能是https://cstheory.stackexchange.com/或https://cs.stackexchange.com/？ – mustaccio

看起来你会再次遇到[停止问题]（https://en.wikipedia.org/wiki/Halting_problem）。但通过使用类似[B方法]（https://en.wikipedia.org/wiki/B-Method）的方法，可以证明两种算法都实现了相同的规范，因此可以认为它们具有足够的等效性，仍然不足以找到它们。 –

Julien是正确的 - 这个问题在一般情况下是无法解决的（至少不是图灵等价系统），如果你找到了一个oracle，你可以这样做，但在这种情况下，我建议你使用它来购买乐透券而不是优化代码）。 – Patrick87

你在问一个相当广泛的问题，但让我看看我能否让你走。

约翰·雷吉汉弗做了非常好的工作调查上superoptimizers一些相关论文：https://blog.regehr.org/archives/923

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

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

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

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

来源

2017-08-28 19:06:51 nightshade99

验证程序的等价性

回答

相关问题