一句话：提出线程化 Kripke 内存关系与前向模拟，实现共享栈多线程程序的组合式编译验证，构建 CompCertOC。
在允许线程间共享栈数据时，多线程程序的组合式验证编译长期是开放问题：需在任意内存操作（如指针算术）下同时允许共享又禁止修改栈内存，此前没有完全形式化的方案。本文在协作式多线程设定下提出编译器验证框架，核心是 threaded Kripke memory relations（TKMR），在多栈内存模型中支持栈的保护与共享；并引入以 TKMR 参数化的 threaded forward simulations，刻画多线程上下文中模块编译的语义保持。作者证明该模拟水平可组合（支持开放线程与异构模块的组合验证）、垂直可组合（支持多趟编译的正确性组合），且可转换为后向模拟。框架应用于 CompCert 的 18 个 pass，得到 CompCertOC——首个支持共享栈协作式多线程程序组合验证的优化验证编译器。
It is a long-standing open problem to support verified compilation of multi-threaded programs 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 cooperative multi-threading. To address the challenges of sharing stack data, we introduce threaded Kripke memory relations (TKMR) to support both protection and sharing of stacks in a multi-stack memory model. We further introduce 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 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. 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.
@article{paperbot3131,
title = {CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks},
author = {Ling Zhang and Yuting Wang and Yalun Liang and Zhong Shao},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729276}
}