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

点击翻译按钮获取中文摘要

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.