Last modified: Tue Jul 8 19:43:30 2025 GMT.
We present a compiler verification framework that solves this open problem. To address the challenge of sharing stack data, we introduce threaded Kripke memory relations to support memory protection and stack-data sharing on a multi-stack memory model. We further introduce threaded direct refinements parameterized by the Kripke memory relations, which are capable of describing semantics preservation for compiling open modules in multi-threaded contexts. We show that threaded direct refinements are both horizontally composable---thereby enabling the compositional verification of open threads and heterogeneous modules---and vertically composable---thereby enabling composition of compiler correctness for multiple compiler passes.
We apply this framework to the full compilation chain of CompCert, resulting in CompCertOC, the first optimizing verified C compiler that supports compilation of multi-threaded modules with sharing of stack data and without any artificial restriction on compositionality. We demonstrate the capability of CompCertOC through compositional verification of multi-threaded heterogeneous programs (i.e., written in C and assembly) which mutually interact with each other by using standard POSIX thread primitives (e.g., dynamic thread creations and joining) while sharing stack data during their interaction.