Verified compilation of C programs with a nominal memory model
Verified compilation of C programs with a nominal memory model
复制标题
DOI：
10.1145/3498686
复制
发表时间：
2022-01
影响因子：
--
通讯作者：
Yuting Wang;Ling Zhang;Zhong Shao;Jérémie Koenig
中科院分区：
文献类型：
--
作者：
Yuting Wang;Ling Zhang;Zhong Shao;Jérémie Koenig
内存模型在验证命令编程语言的汇编中起着重要作用。代表性的是CompCert的基于块的内存模型 - 最新的经过验证的C编译器。尽管取得了成功，但Compcert的存储器模型提供的记忆空间的抽象仍然是原始且僵化的。从本质上讲，它使用固定表示形式来识别全局内存空间中的内存块，并使用全球共享状态来区分使用和未使用的块。因此，关于内存的任何推理都必须在全球内存中统一工作。不可能单独推理内存的不同子区域（即堆栈和全局定义）。这不仅会在编译器验证中产生不必要的复杂性，而且在支持需要与上下文内存一起使用的开放或并发程序的验证汇编方面构成了重大困难，这在以前的CompCert的许多扩展中表现出来。为了消除上述局限性，我们根据名义技术提出对基于块的内存模型的增强。我们称其为标称内存模型。通过采用名义技术的关键概念，例如原子名称和支持以建模内存空间，我们能够1）将内存块的表示形式推广到满足原子名称属性的任何类型，以及2）删除用于管理的全局约束。内存块，为开放和并发程序启用灵活的内存结构。为了证明名义记忆模型的有效性，我们基于IT开发了一系列compcert的扩展。这些扩展表明，标称内存模型1）支持用于验证C程序的一般框架，2）在部分内存上实现编译器转换的直观推理； 3）启用有关与上下文内存一起工作的程序的模块化推理。我们还证明，这些扩展需要对原始组件进行有限的更改，从而基于易于采用的标称内存模型进行验证技术。
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.