目前,约束求解作为符号执行的重要组成部分,已在软件验证、程序分析等领域得到了广泛应用,其在并发程序分析领域的贡献尤为突出.并发程序以计算速度快且资源利用率高为特点,在当今多核架构广泛应用的硬并发时代,其应用越发普遍.因此,针对并发软件的自动缺陷检测技术研究具有重大意义,其研究成果有助于快速有效的检测出各类并发缺陷,以保证并发软件的质量和可靠性.

并发程序的测试和验证面临的主要挑战是线程交织(Thread Interleaving)空间爆炸问题,即可能的线程交织数量随着线程数量和程序执行时间的增加而呈指数级增长,使并发缺陷难以被检测.解决线程交织爆炸的关键是识别冗余的线程交织.现有工作将探索并发程序状态空间的问题转换成约束求解问题,稳定高效地检测并发缺陷.然而异常庞大的并发程序状态空间会导致现有工作为事件添加的约束极其严格且复杂,复杂的约束构建易产生大量冗余甚至存在冲突的约束,严重影响并发缺陷检测效率.

针对上述问题,本文以最大因果约减算法中的约束为研究对象,通过过滤冲突约束并约减冗余约束,以提高并发缺陷检测的效率,最终设计了一种基于有向图构建约束的并发缺陷检测方法GC-MCR(Directed Graph-based Concurrent Constraint Maximal Causality Reduction).GC-MCR通过对冲突约束进行过滤,并约减冗余约束的表达式,有效降低单次约束的求解时间甚至减少约束求解器的调用次数,因此能够保证并发缺陷的检测能力,并提高并发缺陷效率.

本篇工作被收录于软件学报2023年第34卷第8期 .