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).

翻译：开放模块（即功能依赖于其他模块的模块）的验证编译为当代软件中普遍存在的模块化程序的端到端验证提供了基础。然而，尽管该课题已历经数十年深入研究，现有方法仍难以在实践中应用，因为它们依赖于编译器内部工作机制的假设，使得外部用户难以使用验证结果。我们提出一种无需此类假设的已验证组合式编译方法，该方法适用于支持全局内存和指针的一阶语言编写的异构模块的验证编译。我们的方法基于CompCert的内存模型，并发现具有内存保护概念的Kripke关系可作为编译器通路的统一可组合语义接口。通过将编译器所有通路关于内存演化的依赖-保证条件吸收到该Kripke内存关系中，并将编译器优化需求附加于其上，我们得到了实用优化编译器的组合式正确性定理——这些定理是直接关联开放模块原生语义且对中间编译过程透明的精化关系。这种直接精化支持开放模块验证编译所必需的所有组合性和充分性属性。我们已将该方法应用于完整CompCert编译链及其Clight源语言，通过可自由相互调用（例如互递归）的非平凡异构模块的端到端验证，证明我们的编译器正确性定理具有开放组合性、直观易用性，并能降低验证复杂度。