CAJ | 학술논문

多线程软件由于进程间共享使用资源而极易发生死锁这一严重的并发漏洞。通过 Petri 网模型对多线程软件进行建模，并利用混合整数规划技术检测其漏洞。目前，使用互斥锁的多线程软件可通过 Gadara网建模和检测。而使用信号量的多线程软件，虽可用 S*PR 网建模，但是尚未有理论支撑混合整数规划用于其漏洞检测。定义了 S*PR网的一个子类———SEM-S*PR网，它允许资源库所初始标志大于1且分支可对称地使用资源，进而可建模一类使用信号量的多线程软件。依据结构特点，证明了该网保持活性的充分必要条件是网运行过程中所有信标始终非空。此结论是混合整数规划用于 SEM-S*PR网建模的多线程软件的并发漏洞检测的理论基础。
다선정연건유우진정간공향사용자원이겁역발생사쇄저일엄중적병발루동。통과 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.