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.

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