CAREER: Multilayer Code Synthesis For Correctness and Performance

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

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.