该文档属于类型a，是一篇关于多线程程序验证中调度约束抽象的原创研究论文。以下是针对该研究的学术报告：

多线程程序验证中的调度约束抽象方法研究

1. 作者与发表信息

本文由Liangze Yin、Wei Dong、Wanwei Liu（国防科技大学复杂系统软件工程实验室）和Ji Wang（国防科技大学高性能计算国家重点实验室）合作完成，发表于IEEE Transactions on Software Engineering期刊，2020年5月第46卷第5期。论文标题为《On Scheduling Constraint Abstraction for Multi-Threaded Program Verification》，是软件工程领域关于并发程序形式化验证的重要研究。

2. 学术背景

科学领域：研究属于形式化方法（Formal Methods）中的有界模型检测（Bounded Model Checking, BMC），聚焦多线程C程序的自动化验证。
研究动机：多线程程序因线程调度的非确定性导致行为编码复杂，传统BMC需精确编码所有可能的线程交错（thread interleaving），生成庞大公式，限制可扩展性。作者观察到，公式复杂性主要源于调度约束（scheduling constraint）的精确编码，因此提出通过抽象-精化（abstraction-refinement）方法弱化并逐步强化调度约束，以提升效率。
目标：设计一种兼具理论完备性和实践高效性的方法，避免直接编码复杂调度约束，同时通过事件顺序图（Event Order Graph, EOG）和约束求解技术实现精确验证。

3. 研究方法与流程

研究流程分为以下关键步骤：

（1）初始抽象构建
- 对象：多线程C程序，基于共享变量和顺序一致性（Sequential Consistency, SC）模型。
- 方法：忽略调度约束，构建初始抽象φ0 = finit ∧ R ∧ Z，其中finit编码初始状态，R编码线程内部逻辑，Z编码共享变量的读写关系。
- 创新：通过静态单赋值（Static Single Assignment, SSA）形式转换程序，简化约束规模，避免直接编码调度约束的立方级复杂度。

（2）反例验证与EOG构建
- 对象：抽象模型的反例（counterexample），对应潜在的执行路径。
- 方法：
- 事件顺序图（EOG）：将反例转化为有向图，节点为读写事件，边为程序顺序（≤ₚ）和读写链接（↦）。
- 图验证算法：通过三条规则推导隐式顺序（如传递性、读写冲突规则），检测图中环路以判定反例的不可行性（infeasibility）。
- 约束验证：若图验证无法判定，则通过SMT求解器编码所有顺序约束，进一步验证。

（3）精化约束生成
- 核心思想：从不可行反例中提取“核心原因（kernel reasons）”，生成精化约束K。
- 图基方法：分析EOG中的冲突环路，提取最小冲突子集（如读写链接与程序顺序的组合），生成简洁的CNF子句。
- 约束基方法：若图基方法失效，利用SMT求解器的不可满足核心（unsatisfiable core）生成精化约束。

（4）实验验证
- 数据集：SV-COMP 2017并发测试集的1,047个程序及两个真实服务器系统。
- 工具实现：基于CBMC工具链，集成图与约束验证算法。
- 对比工具：Lazy-CSeq-Abs、MU-CSeq、Threader等。

4. 主要结果

1. 性能优势：

   • 速度：在SV-COMP 2017中，Yogar-CBMC以1,550秒完成所有测试，比第二名Lazy-CSeq-Abs（9,820秒）快6.34倍。
     
   • 内存：峰值内存消耗43GB，仅为对比工具的41%。
     
   • 完备性：验证了所有案例（包括传统工具难以处理的复杂工业程序）。
     

2. 技术贡献：

   • EOG验证算法：92%的反例通过图基方法判定，避免昂贵的约束求解。
     
   • 精化效率：平均迭代80次内完成验证，精化约束规模仅为调度约束的1/1200。
     

3. 理论价值：

   • 完备性证明：结合图基与约束基方法，确保方法在给定循环展开深度下的完备性。
     

5. 结论与意义

• 科学价值：提出首个基于调度约束抽象的BMC方法，通过EOG和精化技术平衡效率与完备性，为并发程序验证提供新范式。
  
• 应用价值：工具Yogar-CBMC获SV-COMP 2017并发赛道金牌，适用于工业级代码（如Linux驱动）的验证。
  

6. 研究亮点

1. 创新方法：首创“事件顺序图”抽象与图基精化算法，显著降低约束规模。
   
2. 性能突破：在保持完备性前提下，效率超越所有已知工具。
   
3. 工业适用性：成功验证含复杂指针与数据结构的真实系统代码。
   

7. 其他价值

论文开源工具链（Yogar-CBMC）为后续研究提供可复现基准，其图基验证规则可扩展至其他形式化方法（如硬件模型检测）。