学术研究报告：CompCertOC——支持共享栈的多线程程序验证组合编译

一、 研究团队、期刊与发表信息

本研究的主要作者为上海交通大学的张凌、王宇霆（通讯作者）、梁亚伦，以及来自美国耶鲁大学的邵中。该研究以题为“CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks”的论文形式，于2025年6月发表在《Proceedings of the ACM on Programming Languages》（Proc. ACM Program. Lang.）期刊的PLDI特刊上。

二、 学术背景与研究动机

本研究属于形式化方法、编程语言理论和编译器验证的交叉领域，具体聚焦于验证的组合编译（Verified Compositional Compilation, VCC）这一研究方向。VCC的目标是能够对由不同语言编写的异构模块分别验证其编译器的正确性，然后将这些正确性定理组合起来，从而保证整个编译后程序的正确性。这一方向在过去十年中取得了显著进展，并主要基于最先进的验证编译器CompCert进行构建。

然而，一个长期存在的公开难题是：在允许线程间共享栈数据的情况下，如何支持多线程程序的验证组合编译？ 尽管已有一些理论上的解决方案，但由于在存在任意内存操作（如指针运算）时，同时允许栈共享和禁止栈内存修改的复杂性，没有一个方案被完全形式化。现有的VCC工作（如Thread-Safe CompCertX和CasCompCert）为了保持组合性，通常禁止一个线程的栈内存被另一个线程访问和修改。这偏离了像POSIX线程API这样的常见编程实践（允许将栈变量地址传递给其他线程），也无法支持诸如Rust中的作用域线程等现代编程范式。

因此，本研究旨在解决这一开放性问题，提出并形式化一个编译器验证框架，使得在协作式多线程（cooperative multi-threading）的设定下，能够实现支持栈共享的、组合式的验证编译。研究目标包括：1）设计新的形式化机制来同时支持栈的保护与共享；2）定义能够捕获多线程上下文下模块编译语义保持性的模拟关系；3）证明该模拟关系具备水平和垂直组合性，从而支持异构模块和跨编译器阶段的组合验证；4）将该框架应用于CompCert的多个编译阶段，构建一个名为CompCertOC的已验证优化编译器。

三、 研究详细工作流程

本研究是一项理论构建与形式化验证工作，其“工作流程”并非传统意义上的实验步骤，而是概念提出、形式化定义、性质证明和工具实现的过程。主要流程可分为以下几个核心阶段：

第一阶段：核心概念与形式化模型的构建 1. 问题分析与关键洞察：研究首先通过一个典型的共享栈多线程程序（如图1所示，父线程将栈变量地址传递给子线程）揭示了现有VCC框架（特别是其基于Kripke内存关系（KMR）的依赖-保证条件）的不足。关键在于，现有的injp KMR为整个函数调用定义了内存保护条件，它要求被调用方不能修改调用方的任何私有内存。然而，在多线程上下文中，一个上下文切换（如yield）虽然被视为一个“外部调用”，但其内部执行（在切换回之前）实际上应该被允许修改当前线程自身的私有栈，只是不能修改其他线程的私有栈。将yield与普通函数调用混为一谈会导致过强的保护条件，使得编译正确性证明失败。 2. 引入线程化Kripke内存关系（TKMRS）：为了解决上述问题，研究者提出了线程化Kripke内存关系（Threaded Kripke Memory Relations, TKMRS）。TKMRS在传统KMR的基础上引入了两个新的可访问性关系： * 内部可访问性（{_i）：描述线程内部执行（如j++）所提供的内存保护保证。它允许当前线程修改自己的私有栈，但必须保证不修改其他线程的私有栈。 * 外部可访问性（{_e）：描述线程间交互（如函数调用、上下文切换）所依赖的内存保护条件。它放松了injp的限制，只要求当前线程的私有栈不被环境（其他线程或外部调用）修改，而允许环境修改其他线程的私有栈。 为了形式化地区分不同线程的栈内存，本研究采用了名义内存模型（Nominal Memory Model）。该模型将内存块标识符扩展为(线程ID, 块号)对，从而在内存状态中明确区分全局内存块和各线程的栈内存块，并能追踪当前正在执行的线程ID。这使得{_i和{_e的定义得以精确实现。 3. 定义线程化前向模拟（Threaded Forward Simulations）：基于TKMRS，研究者定义了线程化前向模拟作为编译器正确性的新概念。它是在协作式并发语义下、参数化于TKMRS的前向模拟关系。该模拟关系显式地利用{_i和{_e来刻画内部执行和外部交互的内存保护约束。其核心是维护一个模拟不变式，该不变式记录了初始调用时的世界（用于{_e保证）和最近一次进入模块时的内存世界（用于{_i保证），从而在证明中同时满足对外部环境的保证和对内部执行步骤的约束。

第二阶段：组合性定理的证明 1. 垂直组合性：研究者证明了线程化前向模拟在垂直方向上是可组合的。这意味着如果编译器阶段A将语言L1正确编译到L2（具有模拟关系R），阶段B将L2正确编译到L3（具有模拟关系S），那么可以通过组合R和S得到一个模拟关系R·S，进而证明整个编译链L1到L3的正确性。更重要的是，他们证明了对于特定的模拟约定（如ctinjp），存在精化关系R·S ⊑ R，使得组合后的关系可以精化到单个关系，从而得到直接的、不暴露中间语言的编译正确性定理。 2. 水平组合性：研究者证明了线程化前向模拟在水平方向上也是可组合的。这分为两个步骤： * 模块链接：如果两个模块（可能用不同语言编写）分别满足相对于某个公共接口的线程化前向模拟，那么它们链接后的组合语义也满足相同的模拟关系。这支持了异构模块的分别验证与组合。 * 线程链接：这是本研究的关键贡献。研究者定义了将开放语义（L: A ↠ A）转换为封闭的多线程语义的函数（如mt_c(L)）。然后证明，如果C语言开放语义L1和汇编语言开放语义L2之间存在线程化前向模拟（使用特定的约定c2a），那么将它们分别转换为多线程语义后，得到的封闭语义mt_c(L1)和mt_a(L2)之间也存在标准的前向模拟关系。该证明的核心在于利用线程化前向模拟中的内部保证（{_i）：当一个线程（如服务器线程）通过yield切换出去并执行内部代码时，其{_i保证确保了不会修改原线程（如客户端线程）的私有栈，从而满足了yield作为“外部调用”所依赖的{_e条件。这使得上下文切换能够像普通函数调用一样被安全地处理。

第三阶段：编译器实现与验证（构建CompCertOC） 1. 研究基础：本研究基于两个现有的CompCert扩展：Nominal CompCert（用于支持线程局部栈的名义内存模型）和CompCertO（用于支持VCC的开放语义框架）。 2. 验证流程：研究者将提出的线程化前向模拟框架应用于CompCert的编译通道。他们证明了CompCert总共20个通道中的18个都满足线程化前向模拟。这些通道涵盖了从Clight（C语言的简化形式）到汇编代码（ASM）的完整编译链，包括重要的优化通道如内联（inlining）、常量传播（constprop）、公共子表达式消除（cse）和死代码消除（deadcode）等。 3. 组合成器：通过垂直组合性，将这18个通道的线程化前向模拟组合起来，得到了一个从Clight到ASM的、整体的线程化前向模拟关系⩽_c2a。这个关系就是CompCertOC编译器的核心正确性定理。它表明，对于支持协作式并发且允许栈共享的开放程序模块，CompCertOC的编译能保持其语义。 4. 案例分析：为了展示框架的有效性，研究者将其应用于验证一个非平凡的多线程示例程序（图2）。该程序包含一个用C写的客户端线程和一个用C及汇编写的服务器线程，它们通过POSIX线程API（pthread_create, pthread_join）共享栈上的数组。通过使用CompCertOC分别编译各个模块，然后应用模块链接和线程链接定理，最终得到了整个多线程程序的、封闭的语义保持性定理（包括前向和后向模拟）。

四、 主要研究结果

1. 形式化模型的结果：成功定义了线程化Kripke内存关系（TKMRS）和线程化前向模拟。TKMRS通过区分{_i和{_e，精确刻画了多线程环境下栈内存共享与保护的微妙需求，为解决栈共享难题提供了理论基础。线程化前向模拟则提供了一个可操作的、适用于编译器验证的语义保持性定义。
2. 组合性证明的结果：严格证明了线程化前向模拟同时具备垂直组合性和水平组合性。垂直组合性支持多阶段编译器的验证；水平组合性，特别是线程链接定理，使得能够将分别验证的、运行于独立线程的模块正确性，组合成整个并发程序的正确性。这是实现支持栈共享的VCC最关键的一步。
3. 编译器验证的结果：成功构建了CompCertOC，这是第一个经过形式化验证的、支持协作式多线程程序栈共享的优化编译器。研究证明了CompCert中18个关键通道满足线程化前向模拟，并将它们组合成一个完整的、从Clight到汇编的验证编译链。所有形式化开发都在Coq证明助手中完成，基于CompCert 3.13版本。
4. 案例验证的结果：通过对一个结合了异构性（C和汇编模块）和栈共享（使用POSIX线程API在父子线程间共享栈数据）的示例程序进行成功验证，实证了CompCertOC框架的有效性和实用性。该案例展示了如何将编译正确性定理应用于具体的、符合常见编程习惯的多线程程序。

五、 研究结论与价值

本研究成功解决了“支持栈共享的多线程程序验证组合编译”这一长期存在的公开问题。其核心贡献在于提出了一个完整的形式化框架，该框架通过引入TKMRS和线程化前向模拟，首次在协作式多线程语义下，实现了对栈共享的严格支持，同时保证了编译器验证所必需的组合性质。

科学价值： 1. 理论创新：提出了TKMRS，为并发程序的内存推理提供了新的形式化工具，清晰地区分了线程内部和线程间的内存保护责任。 2. 方法论贡献：定义了线程化前向模拟及其组合性定理，为并发程序的模块化、组合式编译器验证建立了新的方法论。特别是线程链接定理，为将开放模块的语义正确性“提升”到封闭的并发系统语义提供了通用模式。 3. 桥梁作用：该框架将专注于单线程模块编译正确性的VCC研究与并发程序的整体语义连接起来，为后续在抢占式多线程等更复杂并发模型下的研究奠定了基础。

应用价值： 1. 实用验证编译器：产生了CompCertOC，一个可用的、验证过的编译器，能够编译现实世界中常见的、使用栈共享模式的多线程C程序。 2. 提升验证能力：使得对使用POSIX线程等标准库编写的、涉及栈数据共享的并发程序进行端到端的形式化验证成为可能，增强了验证工具在系统软件和安全关键软件领域的适用性。 3. 支持现代语言特性：为验证类似Rust作用域线程（scoped threads）等高级并发抽象提供了理论基础。

六、 研究亮点

1. 首创性：这是首个完全形式化的、支持多线程程序栈共享的验证组合编译框架和编译器实现，填补了该领域长期的空白。
2. 关键洞察：识别出现有VCC框架无法处理栈共享的根本原因在于将上下文切换与函数调用等同看待，并提出了通过区分内部/外部可访问性来放松保护条件这一巧妙解决方案。
3. 强大的组合性：不仅恢复了在栈共享下几乎丢失的水平组合性（模块/线程链接），还保持了垂直组合性，使得能够构建复杂的多阶段验证编译器。
4. 与现有生态集成：工作建立在成熟的CompCert、Nominal CompCert和CompCertO基础上，并成功验证了CompCert的大部分优化通道，表明其解决方案与实际的编译器优化实践是兼容的。
5. 完整的形式化与实现：所有理论定义、定理证明和编译器验证均在Coq中完成，保证了高度的可信性。生成的CompCertOC是一个可直接使用的工具。

七、 其他有价值的内容

研究者在讨论部分指出，CompCertOC的编译器正确性定理目前是针对协作式并发语义的。要连接到抢占式并发语义（如常见操作系统的线程模型），可以借鉴现有工作（如CasCompCert）的思路，利用DRF-SC（Data-Race Free - Sequential Consistency）等定理，在程序验证框架中将抢占式执行“规约”到协作式执行。这项工作更侧重于编译器验证而非程序验证，因此将抢占式语义的连接留作未来工作。这种清晰的界限划分体现了研究的专注性和可扩展性。