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

Concurrency bug test for a class of multithreaded software

作　　者：朱承丞[1] 董利达[1,2] 

机构地区：[1]浙江大学电子电路与信息系统研究所,浙江杭州310027 [2]杭州师范大学国际服务工程学院,浙江杭州311121

出　　处：《西安电子科技大学学报》2015年第2期167-173,212,共8页Journal of Xidian University

基　　金：国家自然科学基金资助项目(61071062);浙江省自然科学基金资助项目(Y12F02030)

摘　　要：多线程软件由于进程间共享使用资源而极易发生死锁这一严重的并发漏洞.通过Petri网模型对多线程软件进行建模,并利用混合整数规划技术检测其漏洞.目前,使用互斥锁的多线程软件可通过Gadara网建模和检测.而使用信号量的多线程软件,虽可用S*PR网建模,但是尚未有理论支撑混合整数规划用于其漏洞检测.定义了S*PR网的一个子类——SEM-S*PR网,它允许资源库所初始标志大于1且分支可对称地使用资源,进而可建模一类使用信号量的多线程软件.依据结构特点,证明了该网保持活性的充分必要条件是网运行过程中所有信标始终非空.此结论是混合整数规划用于SEM-S*PR网建模的多线程软件的并发漏洞检测的理论基础.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＊PR nets,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＊PR nets,i.e.,SEM-S＊PR nets.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＊PR net 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＊ PR nets.Finally,two concurrency bug test examples are introduced,and the results show the validity of this work.

关 键 词：多线程软件 PETRI网 S＊PR网 死锁检测 混合整数规划 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]