提升循环优化验证：新规则REDUCE与VALIDATE扩展

验证更多循环优化是理论计算机科学中的一个重要议题，特别是在编译器和翻译器的设计与验证领域。本论文由Benjamin Goldberg和Amir Pnueli，两位来自纽约大学计算机科学系的研究者撰写，他们关注于提升翻译验证的有效性，这是一种确保编译器正确翻译源代码的技术。由于完全验证整个编译器的难度，翻译验证倾向于在每次编译器运行时进行，通过生成验证条件来证明翻译的正确性。 之前的工作主要集中在循环转换的验证上，如PERMUTE规则用于验证循环重排变换，而VALIDATE规则则用于验证结构保持变换。然而，这些规则在处理某些优化编译器执行的复杂转换时显得不足，比如当循环中涉及变量递增并可能被替换为乘法操作时。论文指出，这表明现有的验证方法存在局限性，需要更为精细的循环缩减变换规则来适应这种情况。 新提出的REDUCEtions规则旨在解决这个问题，它扩展了早期的VALIDATE规则，使其能够处理更多复杂的循环转换。论文作者不仅介绍了这些新规则，还讨论了如何在他们的编译器验证工具TVOC（Translation Verification Oriented Compiler）中实现这些改进，包括以往的理论工作成果。这不仅涉及到理论层面的探讨，也涉及到了实际的工具应用，以提高编译器的正确性和效率。 该论文对翻译验证的理论框架进行了深化，并提出了一种新的实践方法，这对于确保现代优化编译器的正确性具有重要意义。通过引入REDUCEtions和改进的VALIDATE规则，研究者希望能够提升编译器在处理循环优化时的验证能力，从而为用户提供更可靠的结果。