CAREER: Semantics, Abstractions, and Tools for a Pragmatic Verified LLVM Compiler

职业生涯：语义、抽象和实用验证LLVM编译器的工具编译器是计算生态系统的关键组成部分。它们可以将用多种语言（如C/ c++ /Java）编写的源程序转换为多种目标体系结构（如x86/ARM）。然而，编译器错误会破坏源程序级别强制执行的属性，并可能导致意外的应用程序行为和安全关键领域的灾难。这个项目旨在开发实用的、轻量级的形式化技术，使主流编译器健壮，并且编译器开发人员可以很容易地采用这种方式。这个项目在智力上的优点是开发了真实世界的编译器验证环境，它受到了编程语言、体系结构和并发性等多个领域的影响。该项目更广泛的意义和重要性是：(1)通过提高编译器的健壮性来提高大量软件项目的质量，(2)通过构建正确的大型系统（特别是编译器）来灌输形式化推理，以及(3)教育高中生、本科生和研究生使用轻量级形式化方法开发软件。该项目旨在构建新的技术和工具，可以在开发人员的帮助下检查优化的正确性。该项目通过(1)为主流LLVM编译器的各个组件设计数学精确的语义，(2)设计用于编写和指定LLVM优化的特定领域语言，不仅可以检查优化的正确性，还可以生成高效的c++实现，(3)设计构建精确翻译验证器的技术，在编译器开发人员的帮助下比较源代码和目标代码。本研究开发的技术不仅可以提高编译器的可靠性，还可以提高其他依赖于正确编译的大型软件系统的可靠性。

Title: : CAREER: Semantics, Abstractions, and Tools for a Pragmatic Verified LLVM CompilerCompilers are crucial components of the computing ecosystem. They can transform source programs written in multiple languages (e.g, C/C++/Java) into multiple target architectures (e.g, x86/ARM). Compiler bugs, however, break properties enforced at the level of source programs and can lead to unintended application behavior and disasters in safety-critical domains. This project aims to develop pragmatic and lightweight formal techniques for making mainstream compilers robust, in a manner that can be easily adopted by compiler developers. The intellectual merit of this project is the development of real-world compiler verification environments drawing influence from multiple areas like programming languages, architecture, and concurrency. The project's broader significance and importance are: (1) improving the quality of a large number of software projects by improving the robustness of the compiler, (2) inculcating formal reasoning for building large systems (compilers in particular) that are correct by construction, and (3) educating high school students, undergraduates, and graduate students for developing software with lightweight formal methods.This project aims to build new techniques and tools that can check the correctness of optimizations with the help of the developer. The project achieves this by (1) designing mathematically-precise semantics for various components of the mainstream LLVM compiler, (2) designing domain specific languages for writing and specifying LLVM optimizations, which not only check optimizations for correctness but also generate efficient C++ implementations, (3) designing techniques to build precise translation validators, which compare the source and the target code with assistance from the compiler developer. Technology developed by this research will not only improve the reliability of compilers but also the reliability of other large software systems which depend on correct compilation.