Translation Validation of Advanced Compiler Optimizations

标题：高级编译器优化的翻译验证PI：Lenore ZuckProposal编号：CCR-0098299这项研究的目标是提高在存在广泛优化的情况下确保编译正确性的最新技术。这将通过使用翻译验证来实现，其中，不是验证编译器本身，而是构造正式确认由编译器的每次运行产生的目标代码是源程序的正确翻译的工具。正在开发的方法将处理现代体系结构的一组广泛的优化，从戏剧性地改变程序结构的高级循环优化到诸如指令调度之类的低级依赖于机器的优化。这项研究将首先发展正确翻译的理论。将特别注意获得现代体系结构的硬件因素特征的最大忠实表示，例如指令等待时间、CPU资源等。首选的(通常是强制的)方法是验证器工具应该通过仔细分析源和目标来自动获得所有这些信息。提案第二部分的一个主要组成部分将致力于开发可用来完成这项任务的试探法和分析技术。

Title: Translation Validation of Advanced Compiler Optimizations PI: Lenore ZuckProposal Number: CCR-0098299This goal of the research is to advance the state of the art in ensuring the correctness of compilation in the presence of extensive optimization. This will be achieved via the use of translation validation where, rather than verifying the compiler itself one constructs a tool that formally confirms that the target code produced by each run of the compiler is a correct translation of the source program. The methods being developed will handle an extensive set of optimizations for modern architectures, ranging from high level loop optimizations that dramaically change the structure of a program to low level machine dependent optimizations, such a instruction scheduling. The research will first develop the theory of a correct translation. Special care will be taken to obtain a maximally faithful representation of hardware factors characteristic of modern architectures, such as instruction latencies, CPU resources, etc.The preferred (and often mandatory) approach is that the validator tool should derive all of this information automatically by a carefully analysis of the source and the target. A major component of the secondpart of the proposal will be dedicated to the development of heuristics and analysis techniques by which this task can be accomplished.