基于Petri网展开的多线程程序数据竞争检测与重演  

Data Race Detection and Replay of Multi-threaded Programs Based on Petri Net Unfolding

作　　者：鲁法明 黄莹 曾庆田 包云霞 唐梦凡 LU Fa-Ming;HUANG Ying;ZENG Qing-Tian;BAO Yun-Xia;TANG Meng-Fan(College of Computer Science and Engineering,Shandong University of Science and Technology,Qingdao 266590,China;Shenzhen Institutes of Advanced Technology,Chinese Academy of Sciences,Shenzhen 518055,China)

机构地区：[1]山东科技大学计算机科学与工程学院,山东青岛266590 [2]中国科学院深圳先进技术研究院,广东深圳518055

出　　处：《软件学报》2023年第8期3726-3744,共19页Journal of Software

基　　金：国家自然科学基金(61602279);山东省泰山学者工程专项基金(ts20190936);山东省高等学校青创科技支持计划(2019KJN024);山东省博士后创新专项基金(201603056);国家海洋局海洋遥测工程技术研究中心开放基金(2018002);山东科技大学教学名师培育计划(MS20211102)。

摘　　要：数据竞争是多线程程序的常见漏洞之一,传统的数据竞争分析方法在查全率和准确率方面难以两全,而且所生成检测报告难以定位漏洞的根源.鉴于Petri网在并发系统建模和分析方面具有行为描述精确、分析工具丰富的优点,提出一种基于Petri网展开的新型数据竞争检测方法.首先,对程序的某一运行轨迹进行分析和挖掘,构建程序的一个Petri网模型,它由单一轨迹挖掘得到,却可隐含程序的多个不同运行轨迹,由此可在保证效率的同时降低传统动态分析方法的漏报率;其次,提出基于Petri网展开的潜在数据竞争检测方法,相比静态分析方法在有效性上有较大提升,而且能明确给出数据竞争的产生路径;最后,对上一阶段检测到的潜在数据竞争,给出基于CalFuzzer平台的潜在死锁重演调度方法,可剔除误报,保证数据竞争检测结果的真实性.开发相应的原型系统,结合公开的程序实例验证了所提方法的有效性.Data races are common defects in multi-threaded programs.Traditional data race analysis methods fail to achieve both recall and precision,and their detection reports cannot locate the root cause of defects.Due to the advantages of Petri nets in terms of accurate behavior description and rich analysis tools in the modeling and analysis of concurrent systems,this study proposes a new data race detection method based on Petri net unfolding technology.First,a Petri net model of the program is established by analyzing and mining a program running trace.The model implies different traces of the program even though it is mined from a single trace,which can reduce the false negative rate of traditional dynamic analysis methods while ensuring performance.After that,a Petri net unfolding-based detection method of program potential data races is proposed,which improves the efficiency significantly compared with static analysis methods and can clearly show the triggering path of data race defects.Finally,for the potential data race detected in the previous stage,a scheduling schema is designed to replay the defect based on the CalFuzzer platform,which can eliminate false positives and ensure the authenticity of detection results.In addition,the corresponding prototype system is developed,and the effectiveness of the proposed method is verified by open program instances.

关 键 词：数据竞争 PETRI网 网展开 动态程序分析 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]