一句话：提出无需编译器内部假设的开放模块组合式验证编译，用Kripke内存关系建立直接精化并保证组合性与充分性。
验证开放模块的编译是模块化程序端到端验证的基础，但现有方法依赖编译器内部假设，难以复用。本文面向支持全局内存与指针的一阶异构模块，提出无需此类假设的组合式验证编译方法。其核心是基于CompCert内存模型，发现带内存保护的Kripke关系可作为各编译遍统一、可组合的语义接口；将内存演化的rely-guarantee条件与优化需求并入其中，得到直接关联开放模块原语语义、不暴露中间过程的精化式正确性定理，并支持组合性与充分性。作者在CompCert编译链上实现，通过可相互递归调用的异构模块端到端验证，表明定理可组合且降低验证复杂度。
Verified compilation of open modules (i.e., modules whose functionality depends on other modules) provides a foundation for end-to-end verification of modular programs ubiquitous in contemporary software. However, despite intensive investigation in this topic for decades, the proposed approaches are still difficult to use in practice as they rely on assumptions about the internal working of compilers which make it difficult for external users to apply the verification results. We propose an approach to verified compositional compilation without such assumptions in the setting of verifying compilation of heterogeneous modules written in first-order languages supporting global memory and pointers. Our approach is based on the memory model of CompCert and a new discovery that a Kripke relation with a notion of memory protection can serve as a uniform and composable semantic interface for the compiler passes. By absorbing the rely-guarantee conditions on memory evolution for all compiler passes into this Kripke Memory Relation and by piggybacking requirements on compiler optimizations onto it, we get compositional correctness theorems for realistic optimizing compilers as refinements that directly relate native semantics of open modules and that are ignorant of intermediate compilation processes. Such direct refinements support all the compositionality and adequacy properties essential for verified compilation of open modules. We have applied this approach to the full compilation chain of CompCert with its Clight source language and demonstrated that our compiler correctness theorem is open to composition and intuitive to use with reduced verification complexity through end-to-end verification of non-trivial heterogeneous modules that may freely invoke each other (e.g., mutually recursively).
@article{paperbot2622,
title = {Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules},
author = {Ling Zhang and Yuting Wang and Jinhua Wu and Jérémie Koenig and Zhong Shao},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632914}
}