权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Translation Validation of Advanced Compiler Optimizations

高级编译器优化的翻译验证

基本信息

批准号：
0098299
负责人：
Lenore Zuck
金额：
$ 24万
依托单位：
New York University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2001
资助国家：
美国
起止时间：
2001-07-01 至 2003-06-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=0098299&HistoricalAwards=false
关键词：
Translation Validation Advanced Compiler Optimizations

项目摘要

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.

标题：高级编译器优化的翻译验证 PI：Lenore Zuck 提案编号：CCR-0098299 这项研究的目标是推进最先进的技术，确保在存在广泛优化的情况下确保编译的正确性。这将通过使用翻译验证来实现，其中不是验证编译器本身，而是构建一个工具来正式确认编译器每次运行生成的目标代码是源程序的正确翻译。正在开发的方法将处理现代体系结构的广泛优化，范围从显着改变程序结构的高级循环优化到低级机器相关优化（例如指令调度）。该研究将首先发展正确翻译的理论。将特别注意获得现代架构的硬件因素特征的最大程度的忠实表示，例如指令延迟、CPU 资源等。首选（通常是强制性）方法是验证器工具应通过仔细分析源和目标来自动导出所有这些信息。该提案第二部分的一个主要组成部分将致力于开发启发式和分析技术，通过这些技术可以完成这项任务。