SHF: Small: Havoc: Verified Compilation of Concurrent Managed Languages

Havoc项目的目标是提供（a）关于重要并发抽象（例如，锁、监视器、堆栈、队列、散列表等）（B）用于推理由共享存储器并发编程模型中的编译器执行的程序变换的正确性的精确存储器模型，沿着关于模型的设计对编译器变换和优化的影响的详细实验验证，以及（c）一种方法，用于正式推理应用程序线程和受管理组件（如现代垃圾收集器）之间的复杂并发交互。这项工作的主要工件将是正式认证的工具，特别是编译器和现代托管语言中的运行时组件，可用于取代现有的基础设施，以及新的语言级内存模型，这些模型在概念上更清晰，可以在经过验证的优化编译器框架内进行推理和部署。 这些工件将极大地改变安全关键型应用程序的环境，其中越来越多地包含并发组件，减轻了对源代码和二进制文件进行昂贵的手动检查的需要，并实现了更丰富的优化类别。 它们将极大地帮助工程师构建高保证、任务关键的软件系统，如航空电子设备、医疗系统和军事通信系统。拟议的研究重点将是从Java应用程序生成的Java字节码到低级中间表示的优化通道的规范和验证（寄存器传输语言），用于PI先前开发的CompcertTSO认证编译器。此外，该项目还将对突出的运行时组件进行形式化，包括内存管理和线程。 在Java内存模型之后，语言语义基础上的内存抽象将被仔细定制，以促进关于程序转换的机械化推理，并将认识到底层硬件的宽松内存特性。 该项目结合了基础设施工程和软件验证方面的科学进步。

The goals of the Havoc project are to provide (a) foundational results on verified compilation of important concurrency abstractions (e.g., locks, monitors, stacks, queues, hash-tables, etc.) into efficient non-blocking variants, (b) a precise memory model for reasoning about the correctness of program transformations performed by the compiler in a shared-memory concurrency programming model, along with detailed experimental validation on the impact of the model's design on compiler transformations and optimizations, and (c) a methodology to formally reason about complex concurrent interactions between application threads and managed components like modern garbage collectors. The primary artifacts of this effort will be formally certified tools, specifically, compilers, and runtime components found in modern managed languages that can be used to replace existing infrastructure, as well as new language-level memory models that are both conceptually cleaner to reason about and deploy within a verified optimizing compiler framework. These artifacts will dramatically change the safety-critical application landscape, which increasingly contains concurrent components, relieving the need for costly manual inspection of source and binary, and enabling a richer class of optimizations. They will greatly assist engineers in the task of constructing high-assurance, mission-critical software systems, such as avionics, medical systems, and military communications systems.The proposed research focus will be on the specification and verification of optimization passes from Java bytecodes generated from a Java application to a low-level intermediate representation (register transfer language), used in the CompcertTSO certified compiler previously developed by the PIs. In addition, the project will undertake the formalization of salient runtime components, including memory management and threads. While patterned after the Java memory model, the memory abstraction underlying the language semantics will be carefully tailored to facilitate mechanized reasoning about program transformations and will be cognizant of the relaxed memory features of the underlying hardware. This project combines infrastructure engineering and scientific advances in software verification.