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.