Authors
Ling Zhang
Yuting Wang
Jinhua Wu
Jérémie Koenig
Zhong Shao
Abstract
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).
Published
In
Proc. 51st
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL'24), London, UK, January 2024.
Published as
Proceedings of the ACM on Programming Languages (PACMPL), Volume 8, Number POPL, Article 72 (January 2024), 31 pages.