It is a long-standing open problem to support verified compilation of
multi-threaded programs \emph{compositionally} when
sharing of stack data between threads is allowed.
%
Although certain solutions exist on paper, none of them is
completely formalized because of the difficulty in
simultaneously enabling sharing and forbidding modification of
stack memory in presence of arbitrary memory operations (e.g., pointer
arithmetic).
%
We present a compiler verification framework that solves this open
problem in the setting of \emph{cooperative multi-threading}. To
address the challenges of sharing stack data, we introduce
\emph{threaded Kripke memory relations} (TKMR) to support both
protection and sharing of stacks in a multi-stack memory model. We
further introduce \emph{threaded forward simulations} parameterized by
TKMR to capture semantics preservation for compiling program modules
in multi-threaded contexts. We show that threaded forward simulations
are both \emph{horizontally composable}—thereby enabling the
compositional verification of open threads and heterogeneous
modules—and \emph{vertically composable}—thereby enabling
composition of compiler correctness for multiple compiler passes. Furthermore,
threaded forward simulations can be converted into backward simulations.
%
We apply this framework to 18 passes of CompCert to get CompCertOC, the
first optimizing verified compiler that supports compositional
verification of cooperative multi-threaded programs with shared stacks.