CAREER: Multilayer Code Synthesis For Correctness and Performance

职业：多层代码合成以确保正确性和性能

• 批准号: 1261811
• 负责人: Qing Yi
• 金额: $ 21.96万
• 依托单位: University of Colorado at Colorado Springs
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-08-13 至 2017-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1261811&HistoricalAwards=false
• 关键词: CAREER; Multilayer; Code; Synthesis; Correctness

Correctness and performance are two of the most fundamental concerns insoftware development. In particular, the increasing complexity of modern computing environment has made it extremely difficult for software applications to be both correct and efficient. Software programs are frequently found to be flawed, and existing technology has fallen behind in providing the necessary programming language and tool support to ensure high quality software development. This research develops programming language as well as compiler analysis and optimization techniques to support the automated translation of software from high-level design to low-level efficient implementations. This research develops a multilayer code synthesis framework that systematically produces high-quality software by effectively combining software verification techniques with program analysis and compiler optimization in a three-phase translation process. First, starting from the software design phase, the framework automatically translates formal software semantic specifications into object-oriented or procedural implementations based on strategies selected by programmers. Then, based on knowledge from the software-design phase, a sequence of domain-specific optimizations is applied to the implementation to improve algorithm efficiency. Finally, architecture-specific optimizations are applied to performance-critical routines, and the optimized routines are empirically tuned as the application is ported to different machines. Different design and programming languages may be used in each translation phase, and software verification technology will be used to ensure the correctness of each translation. The research focuses on scientific computing and system software applications, where both correctness and performance are of critical concern. The integrated research is expected to significantly improve both the trustworthiness and performance of existing software development.

正确性和性能是Insoftware开发的两个最根本问题。特别是，现代计算环境的复杂性日益增加，使软件应用程序变得非常正确且高效。软件程序经常被发现存在缺陷，现有技术在提供必要的编程语言和工具支持方面已落后，以确保高质量的软件开发。 这项研究开发了编程语言以及编译器分析和优化技术，以支持从高级设计到低级有效实现的软件自动翻译。这项研究开发了多层代码综合框架，该框架通过有效地将软件验证技术与程序分析和编译器优化在三相翻译过程中进行系统地生成高质量的软件。首先，从软件设计阶段开始，该框架会根据程序员选择的策略自动将正式的软件语义规格转换为面向对象或程序实现。然后，基于软件设计阶段的知识，将一系列特定的域特异性优化应用于实现，以提高算法效率。最后，将特定于架构的优化应用于性能至关重要的例程，并且在应用程序移植到不同机器时，对优化的例程进行了经验调整。在每个翻译阶段都可以使用不同的设计和编程语言，并且软件验证技术将用于确保每次翻译的正确性。该研究的重点是科学计算和系统软件应用程序，在这些应用程序中，正确性和性能都是至关重要的。预计综合研究将显着改善现有软件开发的可信度和性能。