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

浩劫项目的目标是提供(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.