一句话：提出基于名义技术的内存模型，突破 CompCert 块式内存模型限制，支持开放/并发程序的可验证编译。
CompCert 的块式内存模型对内存空间采用固定块表示和全局共享状态，无法对栈、全局定义等子区域分别推理，给编译器验证及开放或并发程序的可验证编译带来困难。本文提出名义内存模型：借助 nominal techniques 中的 atomic names 与 supports 来建模内存空间，将内存块表示泛化到满足原子名性质的任意类型，并移除管理内存块的全局约束，从而支持灵活的内存结构。作者基于该模型实现一系列 CompCert 扩展，表明其能支撑通用的 C 程序可验证编译框架、对部分内存上编译器变换的直观推理，以及对使用上下文内存的程序的模块化推理；且对原 CompCert 改动有限，便于采用。
Memory models play an important role in verified compilation of imperative programming languages. A representative one is the block-based memory model of CompCert---the state-of-the-art verified C compiler. Despite its success, the abstraction over memory space provided by CompCert's memory model is still primitive and inflexible. In essence, it uses a fixed representation for identifying memory blocks in a global memory space and uses a globally shared state for distinguishing between used and unused blocks. Therefore, any reasoning about memory must work uniformly for the global memory; it is impossible to individually reason about different sub-regions of memory (i.e., the stack and global definitions). This not only incurs unnecessary complexity in compiler verification, but also poses significant difficulty for supporting verified compilation of open or concurrent programs which need to work with contextual memory, as manifested in many previous extensions of CompCert. To remove the above limitations, we propose an enhancement to the block-based memory model based on nominal techniques; we call it the nominal memory model. By adopting the key concepts of nominal techniques such as atomic names and supports to model the memory space, we are able to 1) generalize the representation of memory blocks to any types satisfying the properties of atomic names and 2) remove the global constraints for managing memory blocks, enabling flexible memory structures for open and concurrent programs. To demonstrate the effectiveness of the nominal memory model, we develop a series of extensions of CompCert based on it. These extensions show that the nominal memory model 1) supports a general framework for verified compilation of C programs, 2) enables intuitive reasoning of compiler transformations on partial memory; and 3) enables modular reasoning about programs working with contextual memory. We also demonstrate that these extensions require limited changes to the original CompCert, making the verification techniques based on the nominal memory model easy to adopt.
@article{paperbot1590,
title = {Verified compilation of C programs with a nominal memory model},
author = {Yuting Wang and Ling Zhang and Zhong Shao and Jérémie Koenig},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498686}
}