一种多线程软件并发漏洞检测方法

doi:10.3969/j.issn.1001-2400.2015.02.028

J4 ›› 2015, Vol. 42 ›› Issue (2): 167-173+212.doi: 10.3969/j.issn.1001-2400.2015.02.028

一种多线程软件并发漏洞检测方法

朱承丞¹;董利达^1,2

(1. 浙江大学电子电路与信息系统研究所，浙江杭州 310027; 2. 杭州师范大学国际服务工程学院，浙江杭州 311121)

收稿日期:2013-12-12 修回日期:2014-03-10 出版日期:2015-04-20 发布日期:2015-04-14
通讯作者: 朱承丞
作者简介:朱承丞(1990-)，男，浙江大学硕士研究生，E-mail: zhuchengcheng@live.cn．
基金资助:
国家自然科学基金资助项目(61071062)；浙江省自然科学基金资助项目(Y12F02030)

Concurrency bug test for a class of multithreaded software

ZHU Chengcheng¹;DONG Lida^1,2

(1. Institute of Electronic Circuit and Information System, Zhejiang Univ., Hangzhou 310027, China; 2. Hangzhou Institute of Service Engineering, Hangzhou Normal Univ., Hangzhou 311121, China)

Received:2013-12-12 Revised:2014-03-10 Online:2015-04-20 Published:2015-04-14
Contact: ZHU Chengcheng

摘要/Abstract

摘要： 多线程软件由于进程间共享使用资源而极易发生死锁这一严重的并发漏洞．通过Petri网模型对多线程软件进行建模，并利用混合整数规划技术检测其漏洞．目前，使用互斥锁的多线程软件可通过Gadara网建模和检测．而使用信号量的多线程软件，虽可用S^*PR网建模，但是尚未有理论支撑混合整数规划用于其漏洞检测．定义了S^*PR网的一个子类——SEM-S^*PR网，它允许资源库所初始标志大于1且分支可对称地使用资源，进而可建模一类使用信号量的多线程软件．依据结构特点，证明了该网保持活性的充分必要条件是网运行过程中所有信标始终非空．此结论是混合整数规划用于SEM-S^*PR网建模的多线程软件的并发漏洞检测的理论基础．

关键词: 多线程软件, Petri网, S^*PR网, 死锁检测, 混合整数规划

Abstract: Due to the sharing of resources, the deadlocks often occur as concurrency bugs in multithreaded software. This paper utilizes the Petri net to model multithreaded software and use the mixed integer programming tool to test the concurrency bugs in it. Currently, multithreaded software using the mutex can be modeled and tested by the Gadara nets. Multithreaded software using semaphores can be modeled by S^*PRnets, but there is no theory to support the mixed integer programming-based concurrency bugs test method for them. This paper defines a subclass of S^*PRnets, i.e., SEM-S^*PRnets. The initial marking of resource places in it can be greater than 1 and branches can use resources symmetrically. Thus, it can model a class of multithreaded software using semaphores. By structural analysis, it can be proved that a SEM-S^*PRnet is live if and only if all its siphons are always marked during execution. This result ensures that the mixed integer programming techniques can also be applied for detecting concurrency bugs in multithreaded software modeled by SEM-S^*PRnets. Finally, two concurrency bug test examples are introduced, and the results show the validity of this work.

Key words: multithreaded software, petri nets, S^*PRnet, deadlock test, mixed integer programming

中图分类号:

TP301.1

朱承丞;董利达. 一种多线程软件并发漏洞检测方法 [J]. J4, 2015, 42(2): 167-173+212.

ZHU Chengcheng;DONG Lida. Concurrency bug test for a class of multithreaded software [J]. J4, 2015, 42(2): 167-173+212.

参考文献

［1］ Li Z, Zhou M. Deadlock Resolution in Automated Manufacturing Systems: a Novel Petri Net Approach ［M］. Heidelberg: Springer, 2009. ［2］ Chao D Y. Max'-controlled Siphons for Liveness of S³PGR² ［J］. IET Control Theory ＆ Applications, 2007, 1(4): 933-936. ［3］ Wang S, Wang C, Zhou M. Design of Optimal Monitor-based Supervisors for a Class of Petri Nets With Uncontrollable Transitions ［J］. IEEE Transactions on Systems, Man, and Cybernetics: Systems, 2013, 43(5): 1248-1255. ［4］ Wu N, Zhou M, Li Z. Resource-oriented Petri Net for Deadlock Avoidance in Flexible Assembly Systems ［J］. IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans, 2008, 38(1): 56-69. ［5］ Murata T. Petri Nets: Properties, Analysis and Applications ［J］. Proceedings of the IEEE, 1989, 77(4): 541-580. ［6］ Liu G Y, Chao D Y, Uzam M. A Merging Method for the Siphon-based FMS Maximally Permissive Controllers with Simpler Structures ［DB/OL］. ［2014-01-04］. http://imamci.oxfordjournals.org/content/early/2013/08/21/8mamci.dnt029.short. ［7］ Chu F, Xie X L. Deadlock Analysis of Petri Nets Using Siphons and Mathematical Programming ［J］. IEEE Transactions on Robotics and Automation, 1997, 13(6): 793-804. ［8］ Tricas F, Garcia-Valles F, Colom J M, et al. A Petri Net Structure-based Deadlock Prevention Solution for Sequential Resource Allocation Systems［C］//Proceedings of IEEE International Conference on Robotics and Automation. Piscataway: IEEE, 2005: 271-277. ［9］ Ezpeleta J, Colom J M, Martinez J. A Petri Net Based Deadlock Prevention Policy for Flexible Manufacturing Systems ［J］. IEEE Transactions on Robotics and Automation, 1995, 11(2): 173-184. ［10］ Silva D J. Application and Theory of Petri Nets ［M］. Heidelberg: Springer, 1998: 64-83. ［11］ Li Z, Shpitalni M. Smart Deadlock Prevention Policy for Flexible Manufacturing Systems Using Petri Nets ［J］. IET Control Theory ＆ Applications, 2009, 3(3): 362-374. ［12］ Chou S-Y, Trappey A, Pokojski J, et al. Global Perspective for Competitive Enterprise, Economy and Ecology ［M］. Heidelberg: Springer, 2009: 41-52. ［13］ Liu G, LI Z. General Mixed Integer Programming-based Liveness Test for System of Sequential Systems with Shared Resources Nets ［J］. IET Control Theory ＆ Applications, 2010, 4(12): 2867-2878. ［14］ Liao H, Wang Y, Cho H K, et al. Concurrency Bugs in Multithreaded Software: Modeling and Analysis Using Petri Nets ［J］. Discrete Event Dynamic Systems, 2013, 21(6): 2067-2082. ［15］ Liao H, Lafortune S, Reveliotis S, et al. Optimal Liveness-enforcing Control for a Class of Petri Nets Arising in Multithreaded Software ［J］. IEEE Transactions on Automatic Control, 2013, 58(5): 1123-1138. ［16］王祺, 王安荣, 蒲绪强. 制造系统 Petri 网特殊标识求解算法［J］. 西安电子科技大学学报, 2013, 40(6): 86-91. Wang Qi, Wang Anrong, Pu Xuqiang. Computation of Special Markings of Petri Nets of Manufacturing Systems ［J］ Journal of Xidian University, 2013, 40(6): 86-91. ［17］ Ezpeleta J, Tricas F, Garcia-Valles F, et al. A Banker's Solution for Deadlock Avoidance in FMS with Flexible Routing and Multiresource States ［J］. IEEE Transactions on Robotics and Automation, 2002, 18(4): 621-625. ［18］ Lindo Systems Incorporated. LINGO ［CP/OL］. ［2013-08-12］. http://www.lindo.com/. ［19］ Chen Y, Li Z. Optimal Supervisory Control of Automated Manufacturing Systems ［M］. Boca Raton: CRC Press, 2013. ［20］ Hu H, Zhou M, Li Z, et al. An Optimization Approach to Improved Petri Net Controller Design for Automated Manufacturing Systems ［J］. IEEE Transactions on Automation Science and Engineering, 2013, 10(3): 772-782.

[1]	王祺;陈晓亮. 一种用于柔性制造系统混惑状态估计的算法[J]. 西安电子科技大学学报, 2017, 44(2): 69-74.
[2]	马子玥;童音. 采用基本标识图的Petri网控制策略[J]. 西安电子科技大学学报, 2016, 43(6): 68-73.
[3]	蒋忠远;张秀艳;马子玥. 智能电网中电能存储系统的容量优化[J]. J4, 2015, 42(6): 106-112.
[4]	张秀艳;钟春富;贾建援. S³PR网的可达标识集算法[J]. J4, 2015, 42(5): 105-109.
[5]	张丽;赵良煦;王寿光;汪成英. 针对α网的最优线性约束转换方法[J]. J4, 2015, 42(5): 183-187+212.
[6]	陈晓亮;蒋忠远;叶剑虹 . 工作流网的混或检测和预防策略 [J]. J4, 2015, 42(2): 77-83.
[7]	尤丹;刘苗;吴文慧;王寿光. S³PR网的严格极小信标计算方法[J]. J4, 2014, 41(4): 193-197+204.
[8]	洪良. S³PR网可达标识数的一种有效估算方法[J]. J4, 2014, 41(3): 169-173.
[9]	李晔;王映辉;于振华. 信息物理融合系统的面向对象Petri网建模[J]. J4, 2014, 41(2): 165-171.
[10]	王祺;王安荣;蒲绪强. 制造系统Petri网特殊标识求解算法[J]. J4, 2013, 40(6): 85-91.
[11]	张曼;段振华. 工作流网合成规则及其在流程设计中的应用[J]. J4, 2012, 39(2): 200-206.
[12]	陈玉峰;李志武. 安全Petri网事件分离状态的BDD算法[J]. J4, 2010, 37(1): 119-124+141.
[13]	郭金维;李志武. 一种时延Petri网的死锁预防方法[J]. J4, 2009, 36(5): 902-908.
[14]	朱森;李志武. 双航母编队C³I系统Petri网建模与分析研究[J]. J4, 2009, 36(4): 661-668.
[15]	陈胜;鲍亮;陈平;胡圣明;王萌. BPEL流程数据竞争和死锁检测算法研究 [J]. J4, 2008, 35(6): 1056-1062.

一种多线程软件并发漏洞检测方法

Concurrency bug test for a class of multithreaded software

PDF (PC)

赞

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

Metrics

本文评价

推荐阅读 0