基于锁增广分段图的多线程程序死锁检测
作者:
作者简介:

鲁法明(1981-),男,博士,副教授,博士生导师,CCF专业会员,主要研究领域为Petri网理论与应用,并发系统建模与分析,业务过程管理与决策支持.
曾庆田(1976-),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为Petri网理论与应用,并发系统建模与分析,业务过程管理与决策支持.
郑佳静(1996-),女,硕士生,CCF学生会员,主要研究领域为软件形式化方法,并行程序验证.
段华(1976-),女,博士,副教授,主要研究领域为形式化方法,Petri网.
包云霞(1979-),女,讲师,主要研究领域为形式化方法,Petri网.
王晓宇(1999-),男,本科生,主要研究领域为软件形式化方法,并行程序验证.

通讯作者:

鲁法明,fm_lu@163.com

基金项目:

国家自然科学基金(61602279,61472229);国家重点研发计划(2016YFC0801406);山东省泰山学者工程专项基金(ts20190936);山东省高等学校青创科技支持计划(2019KJN024);山东省自然科学基金智慧计算联合基金(ZL2019LZh001);山东省博士后创新专项基金(201603056);国家海洋局海洋遥测工程技术研究中心开放基金(2018002);山东科技大学领军人才与优秀科研创新团队项目(2015TDJH102)


Deadlock Detection of Multithreaded Programs Based on Lock-augmented Segmentation Graph
Author:
Fund Project:

National Natural Science Foundation of China (61602279, 61472229); National Key Research and Development Plan (2016YFC0801406); Taishan Scholars Program of Shandong Province (ts20190936); Excellent Youth Innovation Team Foundation of Shandong Higher School (2019KJN024); Smart Computing Joint Fund of Shandong Provincial Natural Science Foundation (ZL2019LZh001); Postdoctoral Innovation Foundation of Shandong Province (201603056); Open Foundation of First Institute of Oceanography, MNR (2018002); Shandong University of Science and Technology Research Fund (2015TDJH102)

  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [39]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    死锁是并行程序常见的缺陷之一,动态死锁分析方法根据程序运行轨迹构建锁图、分段图等模型来检测死锁.然而,锁图及其现有的各种变型无法区分同一循环中锁授权语句的多次执行,扩展锁图中记录的锁集无法捕捉线程曾经持有而又随后释放的锁信息,分段图无法刻画锁的获取和释放操作与线程启动操作耦合而导致的段间依赖关系.上述问题导致了多种死锁的误报.为解决上述问题,对已有的锁图和分段图模型进行改进,在锁图基础上扩充语句的执行时序信息,在分段图的基础上扩充锁的获取和释放信息,对段进行更细粒度的划分以建模锁对象导致的段间依赖关系;最终,在上述锁增广分段图与时序增广锁图的基础上,提出一种新的死锁检测方法.所提方法能够有效消除前述各种误报,从而提高死锁检测的准确率.文中开发相应的原型系统,并结合多个程序实例对所提方法的有效性进行评估验证.

    Abstract:

    Deadlocks are a common defect of parallel programs. To detect deadlocks, dynamic deadlock analysis methods build models such as lock graphs and segment graphs according to program running traces. However, a lock graph and its existing variants cannot distinguish different executions of one lock acquisition statement in a loop structure. The lock set used in extended lock graphs cannot capture those locks which were once held and then released. A segmentation graph cannot model the inter-segment dependencies caused by the coupling of lock release/acquisition operation and thread start operation. The above problems have led to a variety of false positives. To address this issue, existing lock graph and segment graph models are improved. Specifically, a lock graph is extended with statement execution order information. A segmentation graph is expanded with lock acquisition and release information. Furthermore, segments in a segmentation graph are more finely divided in the improved model to capture the inter-segment dependencies caused by lock objects. Eventually, based on the improved models, a new deadlock detection method is proposed. It can eliminate the aforementioned false alarms effectively and improve deadlock detection accuracy. A corresponding prototype system is developed for experimental evaluation. The validity of the proposed method is verified through experiments.

    参考文献
    [1] Su XH, Yu Z, Wang TT, Ma PJ. A survey on exposing, detecting and avoiding concurrency bugs. Chinese Journal of Computers, 2015,395(11):93-111(in Chinese with English abstract).[doi:10.11897/SP.J.1016.2015.02215]
    [2] Zhang J, Zhang C, Xuan JF, Xiong YF, Wang QX, Liang B, Li L, Dou WS, Chen ZB, Chen LQ, Cai Y. Recent progress in program analysis. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):80-109(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5651.htm[doi:10.13328/j.cnki.jos.005651]
    [3] Lu S, Park S, Seo E, Zhou YY. Learning from mistakes-A comprehensive study on real world concurrency bug characteristics. Computer Architecture News, 2008,36(1):329-339.
    [4] Bensalem S, Griesmayer A, Legay A, Nguyen TH, Peled D. Efficient deadlock detection for concurrent systems. In:Proc. of the 9th ACM/IEEE Int'l Conf. on Formal Methods and Models for Codesign. IEEE Computer Society, 2011. 119-129. https://doi.org/10.1109/MEMCOD.2011.5970518
    [5] Sun J, Liu Y, Dong JS, Liu Y, Shi L, Andre E. Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans. on Software Engineering and Methodology, 2013,22(1):1-29.[doi:10.1145/2430536.2430537]
    [6] Artho C, Biere A. Applying static analysis to large-scale, multi-threaded Java programs. In:Proc. of the 13th Australian Conf. on Software Engineering. IEEE Computer Society, 2001. 68-75.
    [7] Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R. Extended static checking for Java. ACM SIGPLAN Notices, 2002,37(5):234-245. https://doi.org/10.1145/543552.512558
    [8] Engler D, Ashcraft K. RacerX:Effective, static detection of race conditions and deadlocks. ACM SIGOPS Operating Systems Review, 2003,37(5):237-252. https://doi.org/10.1145/1165389.945468
    [9] Williams A, Thies W, Ernst MD. Static deadlock detection for Java libraries. In:Proc. of the 19th European Conf. on Object-Oriented Programming. Berlin, Heidelberg:Springer-Verlag, 2005. 602-629. https://doi.org/10.1007/11531142_26
    [10] Naik M, Park CS, Sen K, Gay D. Effective static deadlock detection. In:Proc. of the 31st Int'l Conf. on Software Engineering. IEEE, 2009. 386-396. https://doi.org/10.1109/ICSE.2009.5070538
    [11] Harrow J. Runtime checking of multithreaded applications with visual threads. In:Proc. of the 7th Int'l SPIN Workshop on SPIN Model Checking and Software Verification. Berlin, Heidelberg:Springer-Verlag, 2000. 331-342.[doi:10.1007/10722468_20]
    [12] Havelund K. Using runtime analysis to guide model checking of Java programs. In:Proc. of the 7th Int'l SPIN Workshop on SPIN Model Checking and Software Verification. Berlin, Heidelberg:Springer-Verlag, 2001. 245-264.[doi:10.1007/10722468_15]
    [13] Agarwal R, Wang LQ, Stoller SD. Detecting potential deadlocks with static analysis and run-time monitoring. In:Proc. of the 1st Haifa Int'l Conf. on Hardware and Software Verification and Testing. Berlin, Heidelberg:Springer-Verlag, 2005. 191-207.[doi:10.1007/11678779_14]
    [14] Joshi P, Park CS, Sen K, Naik M. A randomized dynamic program analysis technique for detecting real deadlocks. ACM SIGPLAN Notices, 2009,44(6):110-120.[doi:10.1145/1543135.1542489]
    [15] Cai Y, Chan WK. Magiclock:Scalable detection of potential deadlocks in large-scale multithreaded programs. IEEE Trans. on Software Engineering, 2014,44(3):266-281. https://doi.org/10.1145/512529.512558
    [16] Bensalem S, Havelund K. Scalable dynamic deadlock analysis of multi-threaded programs. In:Proc. of the Parallel and Distributed Systems:Testing and Debugging (PADTAD-3), IBM Verification Conf. Springer, Berlin, Heidelberg. 2005.[doi:10.1007/11678779_15]
    [17] Agarwal R, Bensalem S, Farchi E, Havelund K, Nir-Buchbinder Y, Stoller SD, Ur S, Wang LQ. Detection of deadlock potentials in multithreaded programs. IBM Journal of Research and Development, 2010,54(5):3:1-3:15.[doi:10.1147/JRD.2010.2060276]
    [18] Samak M, Ramanathan MK. Trace driven dynamic deadlock detection and reproduction. ACM SIGPLAN Notices, 2014, 49(8):29-42. https://doi.org/10.1145/2555243.2555262
    [19] Cai Y, Zhai K, Wu SR, Chan WK. Teamwork:Synchronizing threads globally to detect real deadlocks for multithreaded programs. ACM SIGPLAN Notices, 2013,48(8):311-312. https://doi.org/10.1145/2442516.2442560
    [20] Burckhardt S, Kothari P, Musuvathi M, Nagarakatte S. A randomized scheduler with probabilistic guarantees of finding bugs. ACM SIGARCH Computer Architecture News, 2010,38(1):167-178.[doi:10.1145/1735970.1736040]
    [21] Cai Y, Lu Q. Dynamic testing for deadlocks via constraints. IEEE Trans. on Software Engineering, 2016,42(9):825-842.[doi:10.1109/TSE.2016.2537335]
    [22] Cadar C, Dunbar D, Engler D. KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs. In:Proc. of the 8th USENIX Conf. on Operating Systems Design and Implementation. USENIX Association, 2008. 209-224.
    [23] Cai Y, Chan WK. MagicFuzzer:Scalable deadlock detection for large-scale applications. In:Proc. of the 34th Int'l Conf. on Software Engineering. IEEE, 2012. 606-616.[doi:10.1109/ICSE.2012.6227156]
    [24] Cai Y, Jia CJ, Wu SR, Zhai K, Chan WK. ASN:A dynamic barrier-based approach to confirmation of deadlocks from warnings for large-scale multithreaded programs. IEEE Trans. on Parallel and Distributed Systems, 2015,26(1):13-23.[doi:10.1109/TPDS.2014. 2307864]
    [25] Cai Y, Wu SR, Chan WK. ConLock:A constraint-based approach to dynamic checking on deadlocks in multithreaded programs. In:Proc. of the 36th Int'l Conf. on Software Engineering. ACM, 2014. 491-502. https://doi.org/10.1145/2568225.2568312
    [26] Joshi P, Naik M, Park CS, Sen K. CalFuzzer:An extensible active testing framework for concurrent programs. In:Proc. of the 21st Int'l Conf. on Computer Aided Verification. Berlin Heidelberg:Springer-Verlag, 2009. 675-681. https://doi.org/10.1007/978-3-642-02658-4_54
    [27] Gao J, Yang X, Jiang Y, Liu H, Ying WL, Sun WT, Gu M. Managing concurrent testing of data race with ComRaDe. In:Proc. of the 27th ACM SIGSOFT Int'l Symp. on Software Testing and Analysis. ACM, 2018. 364-367. https://doi.org/10.1145/3213846.3229502
    [28] Yuan YH, Li Y, Wang ZG. A matrix algorithm for enumerating all circuits of a graph. Journal of Northwestern Polytechnical University, 1992,10(2):204-210(in Chinese with English abstract).
    [29] Li B, He YP, Ma HT. Automatic program repair:Key problems and technologies. Ruan Jian Xue Bao/Journal of Software, 2019, 30(2):244-265(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5657.htm[doi:10.13328/j.cnki.jos.005657]
    [30] Wei HM, Gao J, Qing P, Yu K, Fang YF, Li ML. MPI-RCDD:A framework for MPI runtime communication deadlock detection. Journal of Computer Science and Technology, 2020,35(2):395-411.[doi:10.1007/s11390-020-9701-4]
    [31] Lu FM, Tao RR, Du YY, Zeng QT, Bao YX. Deadlock detection-oriented unfolding of unbounded Petri nets. Information Sciences, 2019,497:1-22. https://doi.org/10.1016/j.ins.2019.05.021
    [32] Lu FM, Zeng QT, Zhou MC, Bao YX, Duan H. Complex reachability trees and their application to deadlock detection for unbounded Petri nets. IEEE Trans. on Systems, Man and Cybernetics:Systems, 2019,49(6):1164-1174.[doi:10.1109/TSMC.2017. 2692262]
    [33] Zhu JQ, Sun HZ, Huang YX, Liu M. Delay satisfied route selection and real-time update scheduling in software defined networking. Ruan Jian Xue Bao/Journal of Software, 2019,30(11):3440-3456(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5655.htm[doi:10.13328/j.cnki.jos.005655]
    附中文参考文献:
    [1] 苏小红,禹振,王甜甜,马培军.并发缺陷暴露、检测与规避研究综述.计算机学报,2015,395(11):93-111.[doi:10.11897/SP.J.1016. 2015.02215]
    [2] 张健,张超,玄跻峰,熊英飞,王千祥,梁彬,李炼,窦文生,陈振邦,陈立前,蔡彦.程序分析研究进展.软件学报,2019,30(1):80-109. http://www.jos.org.cn/1000-9825/5651.htm[doi:10.13328/j.cnki.jos.005651]
    [28] 袁亚华,李泳,王自果.一种求网络所有回路的矩阵方法.西北工业大学学报,1992,10(2):204-210.
    [29] 李斌,贺也平,马恒太.程序自动修复:关键问题及技术.软件学报,2019,30(2):244-265. http://www.jos.org.cn/1000-9825/5657.htm[doi:10.13328/j.cnki.jos.005657]
    [33] 朱金奇,孙华志,黄永鑫,刘明.软件定义网络中延迟满足的路由选择与实时调度更新.软件学报,2019,30(11):3440-3456. http://www.jos.org.cn/1000-9825/5655.htm[doi:10.13328/j.cnki.jos.005655]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

鲁法明,郑佳静,包云霞,曾庆田,段华,王晓宇.基于锁增广分段图的多线程程序死锁检测.软件学报,2021,32(6):1682-1700

复制
相关视频

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

京公网安备 11040202500063号