CAREER: Automatically Generating and Processing Program Analyses and Optimizations
CAREER: Automatically Generating and Processing Program Analyses and Optimizations
批准号:
0644306
负责人:
Sorin Lerner
金额:
$40.0万
依托单位国家:
美国
项目类别:
Continuing Grant
财政年份:
2007
资助国家:
美国
项目状态:
已结题
起止时间:
2007-04-15 至 2012-03-31
中文摘要
开发高效、可伸缩、正确和精确的程序分析器和优化器是困难的。在一个新的优化编译器成熟到能够广泛使用之前,需要很长的时间,通常长达十年。这些困难阻碍了新语言和新体系结构的开发,还可能阻碍最终用户程序员使用特定于域的检查器或优化器来扩展编译器。将研究从非常高级别的规范自动生成高效、可伸缩、正确和精确的数据流分析器和优化器的技术。最重要的主题是理解设计程序分析和优化背后的基本原则,并利用这一理解尽可能地自动化分析器和优化器的编写过程。尝试自动化编写分析器和优化器的过程可以为编译器提供许多新的使用模型,包括:允许最终用户程序员使用特定于域的检查器或优化器轻松地扩展编译器;允许最终用户程序员基于额外的输入-输出示例连续训练编译器,即使在部署之后也是如此;以及当优化器发现需要新的数据流信息时自动生成额外的分析,并在执行时将这些新的分析链接到优化器。
英文摘要
Developing efficient, scalable, correct, and precise program analyzers and optimizers is difficult. There is a long time, often up to a decade, before a new optimizing compiler is mature enough to be widely used. These difficulties hinder the development of new languages and new architectures, and can also discourage end-user programmers from extending compilers with domain-specific checkers or optimizers.Techniques will be investigated for automatically generating efficient, scalable, correct, and precise dataflow analyzers and optimizers from a very high-level specification. The overarching theme is to understand the underlying principles behind designing program analyses and optimizations, and use this understanding to automate as much as possible the analyzer- and optimizer-writing process. Attempting to automate the process of writing analyzers and optimizers enables many new kinds of usage models for compilers, including: allowing end-user programmers to easily extend the compiler with domain-specific checkers or optimizers; allowing end-user programmers to continuously train the compiler, even after it is deployed, based on additional input-output examples; and automatically generating additional analyses when the optimizer discovers the need for new dataflow information, and linking these new analyses into the optimizer while in execution.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
Collaborative Research: SHF: Small: Data-Driven Lemma Synthesis for Interactive Proofs
-
批准号:2220892
-
项目类别:Standard Grant
-
资助金额:$25.0万
-
财政年份:2022
-
负责人:Sorin Lerner
-
依托单位:
SHF: Medium: Generating Correctness Proofs with Neural Networks
-
批准号:1955457
-
项目类别:Standard Grant
-
资助金额:$120.0万
-
财政年份:2020
-
负责人:Sorin Lerner
-
依托单位:
CPS: Synergy: Towards Foundational Verification of Cyber-Physical Systems
-
批准号:1544757
-
项目类别:Standard Grant
-
资助金额:$70.0万
-
财政年份:2015
-
负责人:Sorin Lerner
-
依托单位:
TWC: Medium: Towards a Formally Verified Web Browser
-
批准号:1228967
-
项目类别:Standard Grant
-
资助金额:$111.0万
-
财政年份:2012
-
负责人:Sorin Lerner
-
依托单位:
SHF:Small: Bringing Extensibility and Performance to Verified Compilers
-
批准号:1219172
-
项目类别:Standard Grant
-
资助金额:$40.0万
-
财政年份:2012
-
负责人:Sorin Lerner
-
依托单位:
SHF: Small: Application Shrinking for Reducing Energy Consumption
-
批准号:1018632
-
项目类别:Standard Grant
-
资助金额:$50.0万
-
财政年份:2010
-
负责人:Sorin Lerner
-
依托单位:
CPA-CPL: Scalable Analysis for Concurrent Programs
-
批准号:0811512
-
项目类别:Standard Grant
-
资助金额:$35.0万
-
财政年份:2008
-
负责人:Sorin Lerner
-
依托单位:
海外基金