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

作者简介:

鲁法明(1981-),男,博士,副教授,博士生导师,CCF专业会员,主要研究领域为Petri网,并行程序验证,过程挖掘;黄莹(1998-),女,硕士生,CCF学生会员,主要研究领域为并行程序验证,机器学习;曾庆田(1976-),男,博士,教授,CCF高级会员,主要研究领域为Petri网,人工智能;包云霞(1979-),女,副教授,主要研究领域为Petri网,并行程序分析与验证;唐梦凡(1998-),女,硕士生,主要研究领域为并行程序验证

通讯作者:

黄莹,E-mail:ds00hy@163.com;包云霞,E-mail:baoyunxia98@163.com

中图分类号:

TP311

基金项目:

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


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

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    数据竞争是多线程程序的常见漏洞之一, 传统的数据竞争分析方法在查全率和准确率方面难以两全, 而且所生成检测报告难以定位漏洞的根源. 鉴于Petri网在并发系统建模和分析方面具有行为描述精确、分析工具丰富的优点, 提出一种基于Petri网展开的新型数据竞争检测方法. 首先, 对程序的某一运行轨迹进行分析和挖掘, 构建程序的一个Petri网模型, 它由单一轨迹挖掘得到, 却可隐含程序的多个不同运行轨迹, 由此可在保证效率的同时降低传统动态分析方法的漏报率; 其次, 提出基于Petri网展开的潜在数据竞争检测方法, 相比静态分析方法在有效性上有较大提升, 而且能明确给出数据竞争的产生路径; 最后, 对上一阶段检测到的潜在数据竞争, 给出基于CalFuzzer平台的潜在死锁重演调度方法, 可剔除误报, 保证数据竞争检测结果的真实性. 开发相应的原型系统, 结合公开的程序实例验证了所提方法的有效性.

    Abstract:

    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网展开的多线程程序数据竞争检测与重演.软件学报,2023,34(8):3726-3744

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期: 2023-08-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号