大规模并发程序运行时验证技术

1. 成果简介

并发技术已成为现代计算基础设施的核心组成部分。然而，并发缺陷由于其非确定性和难以重现等特性，对程序正确性构成了严峻挑战。运行时验证技术能够利用运行时信息精准预测并验证并发缺陷，该类技术通过定义“可行性约束”——即描述并发程序应满足的执行条件——基于已有程序执行轨迹，在不重新执行程序的前提下，通过调整线程调度顺序预测其他可能的执行行为，并借助偏序算法或约束求解等技术，判断这些预测执行是否满足可行性约束。

图 1 并发程序运行时验证技术

运行时验证技术自 Leslie Lamport 于1978年提出 Happens-before 偏序理论以来，在约束放宽和验证算法方面持续发展。然而，现有方法通常基于强假设，对读写关系、控制流和数据流施加了过多限制，不仅制约了验证覆盖范围，还在大规模并发程序中面临效率瓶颈。

一方面，为保证准确性，现有技术往往要求预测执行必须完全保持原始执行中的读写关系，导致验证过程中引入大量非必要约束，限制了缺陷检测覆盖率。针对该问题，课题组提出 ReconP 技术，引入程序静态信息，结合动静态混合分析精准界定并高效计算必要的读写约束，过滤冗余约束。实验表明，ReconP 能显著提升并发缺陷验证覆盖率，相关工作发表于 ICSE 2025。

图 2ReconP技术

另一方面，现有方法对控制流一致性施加了严格限制，要求预测执行的控制流必须与已有执行完全一致，限制了可验证的程序状态空间。课题组提出 SeqCheck 和 ToccRace 技术，放宽了对控制流的约束，基于程序局部不变行为为预测执行构建等价执行，通过验证后者间接推断前者的可行性。这一方法首次在运行时验证中兼容控制流变化，大幅提升了缺陷检测能力，相关工作发表于 FSE 2021 和 ICSE 2023。

图 3 间接验证技术（兼容控制流变化）

此外，某些类型的并发缺陷（如 UAF、DF 等内存漏洞）高度依赖数据流，现有方法因未考虑数据流变化而无法检测此类缺陷。课题组提出 Eagle 方法，在运行时验证中引入指针数据流分析，兼容指针别名导致的并发缺陷，成功在大规模开源软件中检出多项并发缺陷，并获得多个 CNVD 漏洞编号，该项工作发表于 ICSE 2024。

图 4 指针流分析与轨迹重排

运行时验证的时间复杂度与执行轨迹中的指令频次相关，覆盖高的方法往往具有指数或多项式复杂度，难以应用于大规模并发程序。课题组基于并发缺陷的行为特征，在验证过程中过滤无效信息，降低待验证指令的数量，从而将验证效率提升两个数量级，显著增强了该类技术在大规模并发程序上的实用性。这一优化技术已应用于 ReconP、SeqCheck、ToccRace 和 Eagle。

2. 技术先进性

该项技术的先进性主要体现在以下方面：

（1）ReconP：整合动静态信息，对必要约束进行边界界定和高效计算。

（2）SeqCheck和ToccRace：基于程序不变行为的控制流约束宽松处理，及精确的间接验证技术。

（3）Eagle：验证中引入指针数据流分析，兼容指针别名导致的并发缺陷。

（4）优化技术：基于并发缺陷的行为特征，过滤无效信息，降低验证时间开销。

3. 技术成熟度

相关软件已全部完成小试阶段，部分技术已进入产品化阶段，例如在华为5G基站软件中应用。

4. 可应用领域

该技术可应用于基础软件与中间件（操作系统内核、数据库等）、嵌入式与实时系统、网络与通信软件、大型互联网服务与后端系统（Web服务器、应用服务器等）、云计算与分布式计算框架、人工智能基础设施等领域

5. 联系人

蔡彦，yancai@ios.ac.cn，15010619808