CompCertOC: Verified Compositional Compilation of Multi-Threaded Programs with Shared Stacks
Last modified: Mon Jun 9 14:20:54 2025 GMT.
Authors
Ling ZhangYuting Wang
Yalun Liang
Zhong Shao
Abstract
Sharing of stack data between threads is a common practice in multi-threaded programming (e.g., scoped threads in C++ and Rust). It is a long-standing open problem to support verified compilation of multi-threaded programs compositionally in presence of stack-data sharing. Although certain solutions exist on paper, none of them is completely formalized because of the difficulty in simultaneously enabling the sharing and forbidding the 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. 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.
