rjxb
软件学报
Journal of Software
1000-9825
软件学报编辑部
中国北京
6618
8c371350fea406f7f848ac3073df329717ac6125866d9e354f8bebd7bbdb1ec1
10.13328/j.cnki.jos.006618
基于Petri网展开的多线程程序数据竞争检测与重演
Data Race Detection and Replay of Multi-threaded Programs Based on Petri Net Unfolding
鲁
法明
LU
Fa-Ming
鲁法明(1981-), 男, 博士, 副教授, 博士生导师, CCF专业会员, 主要研究领域为Petri网, 并行程序验证, 过程挖掘
fm_lu@163.com 1
黄
莹
HUANG
Ying
黄莹(1998-), 女, 硕士生, CCF学生会员, 主要研究领域为并行程序验证, 机器学习
ds00hy@163.com 1 2 *
曾
庆田
ZENG
Qing-Tian
曾庆田(1976-), 男, 博士, 教授, CCF高级会员, 主要研究领域为Petri网, 人工智能
qtzeng@163.com 1
包
云霞
BAO
Yun-Xia
包云霞(1979-), 女, 副教授, 主要研究领域为Petri网, 并行程序分析与验证
baoyunxia98@163.com 1 *
唐
梦凡
TANG
Meng-Fan
唐梦凡(1998-), 女, 硕士生, 主要研究领域为并行程序验证
tangmf0220@163.com 1
1
山东科技大学 计算机科学与工程学院, 山东 青岛 266590
College of Computer Science and Engineering, Shandong University of Science and Technology, Qingdao 266590, China
2
中国科学院 深圳先进技术研究院, 广东 深圳 518055
Shenzhen Institutes of Advanced Technology, Chinese Academy of Sciences, Shenzhen 518055, China
黄莹, E-mail:
ds00hy@163.com
包云霞, E-mail:
baoyunxia98@163.com
24
4
2023
28
1
2022
34
8
3726
3744
5
9
2021
10
1
2022
14
10
2021
版权所有©《软件学报》编辑部 2023
Copyright ©2023 Journal of Software. All rights reserved.
2023
鲁法明, 黄莹, 曾庆田, 包云霞, 唐梦凡. 基于Petri网展开的多线程程序数据竞争检测与重演. 软件学报, 2023, 34(8): 3726–3744
Lu FM, Huang Y, Zeng QT, Bao YX, Tang MF. Data Race Detection and Replay of Multi-threaded Programs Based on Petri Net Unfolding. Ruan Jian Xue Bao/Journal of Software, 2023, 34(8): 3726–3744 (in Chinese)
数据竞争是多线程程序的常见漏洞之一, 传统的数据竞争分析方法在查全率和准确率方面难以两全, 而且所生成检测报告难以定位漏洞的根源. 鉴于Petri网在并发系统建模和分析方面具有行为描述精确、分析工具丰富的优点, 提出一种基于Petri网展开的新型数据竞争检测方法. 首先, 对程序的某一运行轨迹进行分析和挖掘, 构建程序的一个Petri网模型, 它由单一轨迹挖掘得到, 却可隐含程序的多个不同运行轨迹, 由此可在保证效率的同时降低传统动态分析方法的漏报率; 其次, 提出基于Petri网展开的潜在数据竞争检测方法, 相比静态分析方法在有效性上有较大提升, 而且能明确给出数据竞争的产生路径; 最后, 对上一阶段检测到的潜在数据竞争, 给出基于CalFuzzer平台的潜在死锁重演调度方法, 可剔除误报, 保证数据竞争检测结果的真实性. 开发相应的原型系统, 结合公开的程序实例验证了所提方法的有效性.
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网
网展开
动态程序分析
data race
Petri net
net unfolding
dynamic program analysis
国家自然科学基金(61602279); 山东省泰山学者工程专项基金(ts20190936); 山东省高等学校青创科技支持计划(2019KJN024); 山东省博士后创新专项基金 (201603056); 国家海洋局海洋遥测工程技术研究中心开放基金(2018002); 山东科技大学教学名师培育计划(MS20211102)
大数据时代, 随着对计算性能要求的不断提高, 云计算和多线程程序等并行计算技术越来越受到人们的重视[1 ,2 ] . 在多线程程序中, 由于线程调度的时序不确定性以及共享内存空间访问控制的复杂性, 如果设计不当, 程序会存在诸多并发缺陷, 进而导致运算结果出错甚至程序崩溃[3 ] . 这些并发缺陷的检测和排除是多线程程序设计的一大挑战, 而数据竞争[4 ] 就是引起广泛关注的并发缺陷之一.
数据竞争是指对同一块内存空间存在并发访问, 并且至少有一个访问是写操作. 数据竞争通常会对程序的正确性产生恶劣影响. 但是, 数据竞争的产生场景往往难以检测, 不仅需要特定的输入, 还需要特定的线程调度顺序, 这造成了数据竞争检测的困难. 当前, 数据竞争检测方法一般分为静态检测、动态检测和动静结合的数据竞争检测方法3类[5 ] .
静态检测方法针对程序源代码进行分析, 主要结合锁集对潜在的数据竞争缺陷进行检测, 常见的静态检测工具包括RacerX[6 ] 、RELAY[7 ] 和locksmith[8 ] 等. 该类方法通过静态代码分析程序的完整行为, 存在查全率高的优点. 不过, 由于静态分析方法不实际执行程序, 它以源代码为输入直接进行程序分析, 难以准确获取程序的运行时信息, 从而导致了较高的误报率. 此外, 对程序全部行为进行分析使得静态分析方法时间效率偏低.
动态检测方法监视程序执行过程中的行为, 收集必要的信息来判断哪些操作构成数据竞争. 常见的动态数据竞争检测算法分为基于lockset 的算法[9 -11 ] , 基于happens-before 关系的算法[12 -17 ] , 以及两者混合的hybrid 算法[18 -20 ] 这3种. 基于lockset的方法维护程序执行过程中每个线程的当前持有锁信息, 同时更新共享变量持有的锁信息, 当共享变量不再受到锁保护的时候, 报告数据竞争; 基于happens-before 关系的方法借助逻辑时钟识别两个操作之间因为同属于一个线程、因为锁的释放和申请, 以及因为线程的fork或join而导致的因果关系, 将不具备上述因果关系的两个操作识别为并发. 如果同一个共享变量的读写/写写操作之间是并发的, 则认定两者构成数据竞争; hybrid算法通常先基于lockset找到可疑的数据竞争, 然后借助逻辑时钟等方法对可疑竞争的真实性进行验证. 受限于线程执行交错的不确定性以及所收集信息的不完整性, 动态竞争方法会有较多的漏检, 但是数据竞争的动态分析方法一般比静态方法有更高的准确度.
动静结合的数据竞争检测方法通常先通过静态方法检测潜在的数据竞争, 然后, 在程序动态执行过程中对线程的调度进行干预, 以此增加数据竞争发生的概率, 重演成功的数据竞争均为真实的并发缺陷. 例如, 文献[21 ]从一个已有的动态分析技术中获得的潜在数据竞争的相关信息, 并据此控制线程的随机调度程序, 以提高真实数据竞争发生条件的出现概率, 以此提高数据竞争重演成功的概率; 文献[22 ]首先使用静态分析方法识别潜在的并发错误, 然后使用静态程序切片来针对潜在的并发错误获取较小的程序, 最后, 动态控制线程的调度以便多个线程同时访问同一内存位置, 以此验证并发错误是否会导致程序失败. 文献[23 ]以有害数据竞争的检测为目标, 首先综合考虑happens-before关系与ad-hoc类型的同步来精简需验证的数据竞争数量, 然后, 将相互之间不存在干扰的潜在数据竞争划分到同一组中, 再借助线程调度器以组为单位对潜在数据竞争进行重演. 动静结合的数据竞争检测方法综合两种方法的优点, 在数据竞争的查全率、准确度方面均有一定保证, 不过, 前期静态分析仍然耗时, 后期动态重演通常是一些随机性的调度方法, 重演成功率有待进一步提高.
综上所述, 目前的数据竞争检测方法在查全率、准确率方面难以两全, 而且数据竞争检测的效率也有待提高. 此外, 如文献[5 ]所述, 现有方法所产生的数据竞争报告使得开发者难以理解并据此追溯漏洞产生根源. 针对上述问题, 考虑到Petri网在并发系统建模和行为分析方面的优点, 本文拟提出一种基于Petri网展开[24 -30 ] 的新型数据竞争检测方法. 首先, 与动态检测方法类似, 所提方法也是从多线程程序某次具体的运行轨迹出发进行分析, 不过, 从该轨迹出发, 本文能构造出一个蕴含多种运行轨迹的程序Petri网模型, 从该模型出发进行数据竞争检测能降低传统动态分析方法的漏报率, 提高查全率; 然后, 与静态分析方法类似, 通过对前述程序Petri网模型的分析检测潜在的数据竞争缺陷, 本文将数据竞争检测问题转化为Petri网展开[30 ] 中共享变量访问操作的并发关系识别, 可有效提高数据竞争的检测效率; 与此同时, 潜在数据竞争对应的出现网片段可以很好地展示数据竞争产生的根源和具体路径; 最后, 由于程序运行轨迹中捕获的程序行为信息不够完备, 由此挖掘到的Petri网模型可能与源程序在行为上不一致, 从而导致数据竞争误报的现象, 为解决此问题, 本文给出一种数据竞争重演方法, 重演成功的数据竞争可保证真实性, 从而可提高检测准确率. 就性能而言, 本文从单一运行轨迹出发构造仅包含程序部分行为的Petri网模型, 相比静态分析方法构造反映程序全部行为的模型而言, 所提方法简化了模型构建和分析的复杂度, 在一定程度上可提升数据竞争检测方法的效率.
1
实例与动机分析
与经典的数据竞争动态分析方法类似, 本文假设程序由有限个线程构成, 这些线程通过共享对象的加锁/解锁以及读写进行同步和交互. 在程序的一次运行过程中, 将线程的启动/终止/阻塞、锁的获取和释放, 以及共享对象读写等操作所构成的操作序列称为一条多线程程序运行轨迹, 其形式化定义如下.
定义1 . 多线程程序运行轨迹. 多线程程序的运行轨迹, 记作
\begin{document}$ \alpha $\end{document}
, 是满足如下条件的一个操作序列:
\begin{document}$ \alpha \in Trace:: = Operation* $ \end{document}
\begin{document}$ \begin{gathered} Operation:: = c:{\rm{fork}}(u, v)|c:{\rm{join}}(u, v)|c:{\rm{stop}}(u)|c:{\rm{acq}}(u, l)| c:{\rm{rel}}(u, l)|c:{\rm{rd}}(u, x)|c:{\rm{wr}}(u, x) \\ \end{gathered} $ \end{document}
其中,
● u , v 表示线程, l 表示锁, x 表示一个共享变量, c 表示程序语句的标签(例如行号、列号等);
●
\begin{document}${\rm{fork}}(u, v)$\end{document}
表示线程u 启动线程v ;
●
\begin{document}${\rm{join}}(u, v)$\end{document}
表示线程u 阻塞直到线程v 终止;
●
\begin{document}${\rm{stop}}(u)$\end{document}
表示线程u 停止;
●
\begin{document}${\rm{acq}}(u, l)$\end{document}
表示线程u 获取锁l ;
●
\begin{document}${\rm{rel}}(u, l)$\end{document}
表示线程u 释放锁l ;
●
\begin{document}${\rm{rd}}(u, x)$\end{document}
表示线程u 读共享变量x ;
●
\begin{document}${\rm{wr}}(u, x)$\end{document}
表示线程u 写共享变量x .
以图1 中的Java多线程程序为例, 它包括主线程、threadA和threadB这3个线程、两个共享变量x 与flag 、一个锁对象lock . 主线程首先为共享变量flag 指派一个随机值, 然后依次启动线程threadA和theadB; 待两个线程都结束后, 主线程终止. 线程threadA启动后, 首先将共享变量x 的值设置为1, 然后尝试获取锁对象lock ; 获取lock 成功后将共享变量flag 的值设置为true. 线程threadB启动后, 首先尝试获取锁对象lock , 获取成功后读取共享变量flag 并将其值赋予私有变量new_flag ; 若new_flag 之后的取值为true则将x 的取值设置为2.
1
多线程程序实例 Program 1
程序Program 1存在两处关于共享变量x 的数据竞争. 具体而言, 若线程threadB首先获得lock 的使用权, 当主线程为flag 指派的初值为true时, 第22行threadB对x 的写操作与threadA对x 的写操作构成数据竞争; 当主线程为flag 指派的初值为false时, 第24行threadB对x 的写操作与threadA对x 的写操作构成数据竞争.
然而, 程序Program 1也存在一些运行轨迹不会呈现上述并发缺陷, 例如表1 中的操作序列. 当中, 线程threadA首先获得锁对象lock 的使用权, 并将共享变量flag 的值设为true; 然后, 线程threadB获得lock 使用权, 并将共享变量x 的取值最终设置为2. 若程序按照表1 中的轨迹执行, 则前述数据竞争不会触发.
1
程序Program 1的一个可能的操作执行序列
序号
主线程mainThread
线程threadA
线程threadB
1
6: wr(mainThread, flag )
2
27: fork(mainThread, threadA)
3
28: fork(mainThread, threadB)
4
9: wr(threadA, x )
5
10: acq(threadA, lock )
6
11: wr(threadA, flag )
7
12: rel(threadA, lock )
8
18: acq(threadB, lock )
9
19: rd(threadB, flag )
10
20: rel(threadB, lock )
11
22: wr(threadB, x )
12
29: join(mainThread, threadA)
13
30: join(mainThread, threadB)
14
31: rd(mainThread, x )
15
32: stop(mainThread)
对于图1 中的Program 1, 首先, 基于lockset的数据竞争检测方法[19 ] 不适用, 因为该方法要求所有的共享变量在执行读写操作时都必须通过锁来保护, 而Program 1对共享变量x 的访问操作均未加锁保护; 其次, 基于happens-before关系的数据竞争检测方法, 若以表1 中的运行轨迹为输入进行检测, 也无法检测到实际存在的竞争. 以得到广泛认可的VerifiedFT[17 ] 数据竞争检测算法为例, 基于happens-before关系的数据竞争方法认为运行轨迹中一个锁释放操作与其后首次执行的该锁的申请操作间存在必然的因果关系. 例如, 表1 的执行轨迹中, 由于线程threadA释放锁对象lock 的操作后, threadB首次申请lock , 故VerifiedFT等基于happens-before关系的方法会假设在锁对象lock 的使用权上, 线程threadA一定先于threadB, 从而在两个操作之间加上一个错误的时序约束关系. 而原本的程序行为并不存在这一约束, 线程threadB完全可以先获得lock 的使用权, 然后对变量x 进行写操作, 进而导致与threadA写x 时的数据竞争. 由此可见, 传统的happens-before关系对程序行为人为添加了更多的约束, 从而导致数据竞争的漏报. lockset与happens-before两者混合的hybrid 算法同时存在上述两个问题.
为解决上述问题, 本文不对共享变量的访问做锁保护的限定, 并从给定的程序运行轨迹出发挖掘能尽量准确反映程序行为的Petri网模型. 所挖掘模型中, 仅在如下情况下建立操作语句之间的因果关系: (1)同一线程内相继执行的两个操作语句; (2)线程的启动操作fork与被启动线程的第1个操作语句; (3)线程的join操作与等待线程的最后一个语句. 此外, 对于锁对象竞争导致的运行轨迹多样化的问题, 本文通过Petri网中的冲突结构来刻画这种行为的多样性. 如此一来, 前述动态分析方法中错误添加的因果关系便可以消除, 而且, 所挖掘模型中蕴含了多种潜在的程序运行轨迹, 这为本文方法更准确地、检测出更多的潜在数据竞争缺陷提供了可能.
此外, 由于定义1中的程序运行轨迹捕获的程序行为有限, 由此导致由其挖掘得到的Petri网模型对程序行为的刻画并不完全准确, 而且Petri网的运行原理与并发程序的执行语义不完全一致, 这导致网模型可能蕴含一些虚假的可执行操作序列, 进而导致数据竞争的误报. 针对这一问题, 本文将给出潜在数据竞争的重演方法, 以此保证本文方法所检测数据竞争的真实性.
最后, 需要指出的是, 由于动态分析以程序的运行轨迹为漏洞检测依据, 而线程执行交错的不确定性和程序控制逻辑与数据流交互的复杂性使得程序各类不同的运行轨迹难以完整捕获, 丢失的运行轨迹可能会导致数据竞争动态检测的漏报. 以图1 中的程序为例, 若仅以表1 中的运行轨迹为检测依据, 包括本文方法在内的动态分析方法无法检测到第9行对x 的写语句与第24行对x 的写语句间存在的数据竞争, 因为该轨迹中第24行语句对应的操作并未出现. 解决这一问题的关键在于生成尽量多的测试用例以尽可能地覆盖程序执行路径, 文献[31 ]提出了一种用于多线程程序数据竞争检测的测试用例自动生成技术, 其生成的测试用例覆盖率经评估可达94%, 虽然能覆盖大多数程序执行路径, 但丢失的路径信息都可能导致数据竞争的漏报.
2
基于运行轨迹的多线程程序Petri网模型挖掘
Petri网[24 ,25 ] 是一种广泛应用于并发系统建模和分析的工具, 其相关定义如下.
定义2 . Petri网. Petri网是一个四元组
\begin{document}$ \Sigma = (P, T; F, {M_0}) $\end{document}
, 其中,
\begin{document}$ P = \{ {p_1}, {p_2}, \ldots ,{p_n}{{\} }} $\end{document}
为库所集,
\begin{document}$ T = \{ {t_1}, {t_2}, \ldots , {t_m}{{\} }} $\end{document}
为变迁集,
\begin{document}$P \cap T = \varnothing$\end{document}
并且
\begin{document}$P \cup T \ne \varnothing$\end{document}
,
\begin{document}$ F \subseteq (P \times T) \cup (T \times P) $\end{document}
称为网的流关系,
\begin{document}$ {M_0}:P \to \{ 0, 1, 2, \ldots \} $\end{document}
为
\begin{document}$ \Sigma $\end{document}
的初始标识.
定义3 . 变迁使能与执行规则. 对
\begin{document}$ \forall x \in P \cup T $\end{document}
, 称
\begin{document}$ {}^ \bullet x \in \{ y \in P \cup T|(y, x) \in F\} $\end{document}
为x 的前集,
\begin{document}$ {x^ \bullet } \in \{ y \in P \cup T|(x, y) \in F\} $\end{document}
为x 的后集. 在标识M 下, 若变迁t 的每个前驱中都含有至少一个标记, 则称t 是使能的. 使能的变迁可以执行从而引发系统状态标识发生改变. T 执行后的标识M' 满足如下条件, 并记之为
\begin{document}$ M[t > M' $\end{document}
.
\begin{document}$ M'(p) = \left\{ {\begin{array}{*{20}{l}} {M(p) - 1,\quad \text{if}\;p \in {}^ \bullet t - {t^ \bullet }} \\ {M(p) + 1,\quad \text{if}\;p \in {t^ \bullet } - {}^ \bullet t} \\ {M(p),\quad\quad\; \text{otherwise}} \end{array}} \right. .$ \end{document}
对
\begin{document}$ \forall \sigma \in {T^ * } $\end{document}
, 若
\begin{document}$ {M_0}[{\sigma _1} > {M_1}[{\sigma _2} > {M_2}[{\sigma _3} > \ldots > {M_{k - 1}}[{\sigma _k} > M $\end{document}
, 则
\begin{document}$ \sigma $\end{document}
称为一个可引发变迁序列, 并称M 为系统的一个可达标识,
\begin{document}$ \Sigma $\end{document}
的所有可达标识的集合记为
\begin{document}$ R(\Sigma ) $\end{document}
.
进行系统建模时, Petri网的库所通常表示某种状态或者资源, 变迁通常表示某种动作, 流关系通常用以刻画动作执行的前提条件和导致的后继状态, 标识用于建模网系统的状态. 本文使用Petri网对多线程程序的行为进行建模时, 每个变迁对应程序执行过程中的一个操作; 库所分为两类, 控制库所用于建模线程的控制流状态, 资源库所用于建模程序中的锁对象; Petri网中的标识表示程序的运行状态. 程序运行之初, 仅有主线程的初始控制流库所和各个锁对象对应的资源库所含有一个标记, 其余库所标记数为0.
图2 就是根据表1 的程序运行轨迹挖掘到的一个能反映图1 程序部分行为的Petri网模型(具体挖掘方法稍后给出). 模型中, 每个变迁(用小矩形表示)对应一个程序操作, 变迁同时标注了其变迁ID和对应的程序操作; 黑色边线的库所(用圆表示)为某个线程的控制库所, 建模控制流状态; 红色边线的库所为一个资源库所, 建模一个锁对象. 控制流库所中的token (用黑点表示)表示线程的当前控制流状态处于激活态, 资源库所中的token表示当前锁对象处于可用状态. 初始状态下主线程的就绪态被激活, 各个锁对象可用, 故它们对应的库所各自有一个token, 相应地, 图2 中的系统初始标识满足
\begin{document}$ {M_0}({p_0}) = 1\, \; \wedge {M_0}({p_{lock}}) = 1\; \wedge \;\forall p \in P - \{ {p_0}, {p_{lock}}\} :{M_0}(p) = 0 $\end{document}
, 当中p 0 是一个控制流库所, 对应主线程的就绪状态; p lock 是一个资源库所, 对应程序中的锁对象lock .
2
由表1运行轨迹挖掘得到的程序Petri网模型
就程序Petri网模型的挖掘方法而言, 当给定多线程程序的某个运行轨迹后, 可以按照表2 所示的网模型构建规则构造程序本次运行对应的Petri网模型.
2
程序锁对象、初始状态以及操作所对应的Petri网模型
程序对象及其操作
对应的Petri网模型片段
说明
主线程就绪状态
该库所表示主线程的就绪状态, 初始标识下它包含一个token, 表示初始状态下主线程处于就绪状态
锁对象
该库所对应一个锁对象, 初始标识它包含一个token, 表示初始状态下锁对象处于可用状态
\begin{document}${\rm{fork}}\left(u, v\right)$\end{document}
变迁t 1 对应fork操作, 其前驱库所p 1 表示线程u 中fork操作的前驱控制流状态, 后继库所p 2 表示线程u 中fork操作的后继控制流状态, 后继库所p v0 表示线程v 的就绪状态
\begin{document}${\rm{join}}\left(u, v\right)$\end{document}
变迁t 1 对应join操作, 其前驱库所p 1 表示线程u 中join操作的前驱控制流状态, 前驱库所p v1 表示线程v 的结束状态; 后继库所p 2 表示线程u 中join操作的后继控制流状态
\begin{document}${\rm{acq}}\left(u, l\right)$\end{document}
变迁t 1 对应锁对象l 的acq操作, 其前驱库所p 1 表示线程u 中acq操作的前驱控制流状态, 前驱库所p l 表示锁对象l ; 后继库所p 2 表示线程u 中acq操作的后继控制流状态
\begin{document}${\rm{rel}}\left(u, l\right)$\end{document}
变迁t 1 对应锁对象l 的rel操作, 其前驱库所p 1 表示线程u 中rel操作的前驱控制流状态; 后继库所p 2 表示线程u 中rel操作的后继控制流状态, 后继库所p l 表示锁对象l
\begin{document}${\rm{rd}}\left(u, x\right)$\end{document}
变迁t 1 对应共享变量x 的读操作, 其前驱库所p 1 表示线程u 中该操作的前驱控制流状态; 后继库所p 2 表示线程u 中该操作的后继控制流状态. 红色圆圈表示的是一个共享变量, 它不属于Petri网的元素, 仅用来描述此操作执行了某个变量的读操作
\begin{document}${\rm{wr}}\left(u, x\right)$\end{document}
变迁t 1 对应共享变量x 的写操作, 其前驱库所p 1 表示线程u 中该操作的前驱控制流状态; 后继库所p 2 表示线程u 中该操作的后继控制流状态. 红色圆圈表示的是一个共享变量, 它不属于Petri网的元素, 仅用来描述此操作执行了某个变量的写操作
\begin{document}${\rm{stop}}\left(u\right)$\end{document}
变迁t 1 对应线程u 的终止操作, 其前驱库所p 1 表示线程u 中该操作的前驱控制流状态; 后继库所p 2 表示线程u 中该操作的后继控制流状态
具体而言, 首先为主线程的就绪状态和各个锁对象分别构建一个含有token的库所; 然后, 针对运行轨迹中各个操作的种类, 按照表2 中给出的规则添加相应的变迁及其输入、输出库所和流关系即可. 具体地说, 每个共享变量的读/写操作所对应变迁仅有唯一的前驱库所和唯一的后继库所, 分别对应该操作所属线程的两个控制流状态; 每个线程fork操作所对应变迁有一个输入库所对应该操作所在线程的上一个控制流状态, 两个输出库所分别对应该操作所在线程的下一个控制流状态, 以及被启动线程的就绪状态; 每个线程join操作所对应变迁有两个输入库所分别对应该操作所在线程的上一个控制流状态, 以及被join线程的结束状态, 有唯一的输出库所对应该操作所在线程的下一个控制流状态; 对于锁对象的获取操作而言, 它对应的变迁有两个输入库所, 其一对应该操作的前驱控制流状态, 另一个对应申请访问的锁对象; 对于锁对象的释放操作而言, 它对应变迁有两个输出库所, 其一对应该操作的后继控制流状态, 另一个对应释放的锁对象. 此外, 为直观起见, 表2 为每个共享变量的读写操作额外添加了共享对量对应的一个红色圆圈, 需要指出, 该元素并不属于Petri网的库所, 仅起到对共享变量读写的提示作用, 进行Petri网行为分析时完全可以忽略这些变量标记. 图2 中的Petri网就省略了这些变量标记.
以表1 中程序Program 1的运行轨迹为例, 结合前述Petri网模型挖掘方法和表2 中的Petri网模型构造规则, 可得图2 所示的Petri网模型. 初始标识下, 该模型仅有变迁t 0 可以执行, 它对应源程序中主线程的首条可执行语句, 即对共享变量flag 的写操作; t 0 执行完毕后, 状态库所p 1 被输入一个token, 代表主线程的下一个控制流状态被激活; 在这一新的状态下, 变迁t 1 使能, 代表启动线程threadA的操作可以执行; t 1 的执行将同时向库所p 2 和p A0 各输入一个token以激活他们, 前者对应主线程该操作执行后的后继状态, 后者对应线程threadA的就绪状态, 之后的操作依次类推. 实际上, 表1 中的程序运行轨迹对应着图2 Petri网的可执行变迁序列
\begin{document}$ \sigma {\text{ = }}{t_0}{t_1}{t_2}{t_{{\text{A0}}}}{t_{{\text{A}}1}}{t_{{\text{A}}2}}{t_{{\text{A3}}}} {t_{{\text{B0}}}}{t_{{\text{B1}}}}{t_{{\text{B}}2}}{t_{{\text{B3}}}} {t_3}{t_4}{t_5}{t_6} $\end{document}
, 该变迁序列执行完毕后, 主线程的终止状态库所和锁对象lock 对应的库所各自含有一个token, 这对应着程序Program 1的终止状态.
需要强调的是, 虽然上述Petri网是由程序的单一运行轨迹挖掘得到, 但它实际隐含了原程序多个不同的可执行操作序列. 究其原因, 虽然某个具体的程序运行轨迹中, 不同线程的锁获取操作对同一个锁对象有固定的先后顺序, 但根据运行轨迹构造Petri网模型时并没有强加上这种因果依赖关系.
仍然以图2 中的Petri网为例, 锁对象lock 对应的资源库所p lock 有两个后继变迁t A1 与t B0 , 它们构成一种冲突结构, 从而带来了多种不同的可执行变迁序列: 一种情景是变迁t A0 先引发, 对应着线程threaA首先获得锁对象lock 的使用权; 另一种情景是变迁t B1 先引发, 对应着线程threaB首先获得锁对象lock 的使用权. 具体来说, 当网系统在初始状态执行完毕变迁序列t 0 t 1 t 2 后, Petri网的标识为
\begin{document}$ {{M}} = {\text{\{ }}{p_3}{\text{, }}\, {p_{{\text{A}}0}}, \, {p_{{\text{B}}0}}, \, {p_{lock}}{\text{\} }} $\end{document}
当前状态下, 若t A1 先执行则得到前述可执行变迁序列
\begin{document}$ \sigma $\end{document}
, 它对应表1 中的程序运行轨迹; 若t B0 先执行, 则得到另一个可执行变迁
\begin{document}$ \sigma '{\text{ = }} {t_0}{t_1}{t_2}{t_{{\text{B0}}}}{t_{{\text{B1}}}}{t_{{\text{B}}2}}{t_{{\text{B3}}}}{t_{{\text{A0}}}}{t_{{\text{A}}1}}{t_{{\text{A}}2}}{t_{{\text{A3}}}}{t_3}{t_4}{t_5}{t_6} $\end{document}
, 它对应着表3 中的程序运行轨迹. 显然, 表1 的运行轨迹未触发数据竞争, 而表3 中第7、8行的两个操作则触发了数据竞争. 接下来借助网展开等Petri网分析工具对不同执行情景下共享变量读写操作之间可能的并发关系进行检测, 每个可能并发的共享变量读写操作都对应着源程序的一个潜在数据竞争.
3
程序Program 1的另一个操作执行序列
序号
主线程
线程threadA
线程threadB
1
6: wr(mainThread, flag)
2
27: fork(mainThread, threadA)
3
28: fork(mainThread, threadB)
4
18: acq(threadB, lock )
5
19: rd(threadB, flag )
6
20: rel(threadB, lock )
7
22: wr(threadB, x )
8
9: wr(threadA, x )
9
10: acq(threadA, lock )
10
11: wr(threadA, flag )
11
12: rel(threadA, lock )
12
29: join(mainThread, threadA)
13
30: join(mainThread, threadB)
14
31: rd(mainThread, x )
15
32: stop(mainThread)
3
基于Petri网展开的潜在数据竞争检测
要检测源程序中某共享变量的读写/写写操作间是否存在数据竞争, 实际只需分析前述所挖掘Petri网模型中这两个操作对应的变迁间是否可并发即可. 在诸多Petri网分析工具中, Petri网的展开技术[24 ,30 ] 可以对变迁之间是否存在并发作出有效判断, 为此, 本文将基于Petri网的展开进行程序潜在数据竞争的检测. Petri网展开技术基于出现网对系统行为进行分析, 下面简单介绍相关概念, 更多内容见文献[24 ,26 ,30 ].
首先, 对于无标识网
\begin{document}$ N = (P, T;F) $\end{document}
中的任意节点
\begin{document}$ y, y' \in P \cup T $\end{document}
, 若存在变迁
\begin{document}$ t, t' \in T $\end{document}
使得
\begin{document}${}^ \bullet t \cap {}^ \bullet t' \ne \phi \wedge (t, y) \in {F^ * } \wedge (t', y') \in {F^ * }$\end{document}
(当中,
\begin{document}$F^* $\end{document}
指流关系F 的自反传递闭包), 则称节点y 与
\begin{document}$ y' $\end{document}
冲突, 记作
\begin{document}$ y\# y' $\end{document}
; 若
\begin{document}$ (y, y') \in {F^ + } $\end{document}
则称y 与
\begin{document}$ y' $\end{document}
具有因果关系, 记作
\begin{document}$ y \prec y' $\end{document}
; 若
\begin{document}$ (y, y') \notin {F^ * } \wedge (y, y') \notin {({F^{ - 1}})^ * } \wedge \neg (y\# y') $\end{document}
, 则称y 与
\begin{document}$ y' $\end{document}
并发, 记作
\begin{document}$ y||y' $\end{document}
. 例如, 若忽略图2 中的token, 将其视作一个网, 则我们有
\begin{document}$ {t_{B0}}\# {t_{A1}} $\end{document}
、
\begin{document}$ {t_2}{\text{||}}{t_{A0}} $\end{document}
特殊的, 节点自身与自身冲突的情况称为自冲突, 如
\begin{document}$ {t_4}\# {t_4} $\end{document}
.
出现网(本文出现网的定义与文献[25 ]不同. 文献[25 ]要求
\begin{document}$ \forall b \in B:\left.\right|^{*} b \mid \leqslant 1 $\end{document}
, 这意味着网中不允许有冲突, 本文允许不同节点间存在冲突)是一个三元组
\begin{document}$ ON = (B, E;G) $\end{document}
, 当中B 为库所集, 又称条件集; E 为变迁集, 又称事件集, 它们满足(1)
\begin{document}$ \forall b \in B:|{}^*b| \leqslant 1 $\end{document}
; (2)
\begin{document}${{{G}}^ + } \cap {({{{G}}^{ - 1}})^ + } = \phi$\end{document}
, 即网中不含有向圈; (3)
\begin{document}$ \forall y \in B \cup E:\;\neg (y\# y) $\end{document}
, 即网中不存在自冲突; (4)
\begin{document}$ \forall y \in B \cup E $\end{document}
, 集合
\begin{document}$ \{ x|x \in B \cup E \wedge (x, y) \in {G^{\text{ + }}}\} $\end{document}
是有限的, 即任意节点的前驱节点都是有限的.
Petri网展开利用出现网描述系统行为的基本思想如下: 用出现网中的一个事件表示Petri网系统中某个变迁的一次执行, 用出现网中的一个条件表示网系统运行中涉及的某个token, 出现网中的流关系用以刻画原始Petri网中变迁执行对token的消耗和产生情况, Petri网初始标识下的各个token分别对应出现网中一个没有前驱的条件. 例如, 图3 中的出现网就是图2 Petri网系统的一个有限展开. 当中, 各节点旁标有两个标签, 节点内部的标签是出现网中该节点的唯一ID, 节点外的标签是该节点对应的原Petri网系统中库所或者变迁节点的ID, 双边框表示的事件为截断事件. Petri网的展开中, 一个事件e 的局部配置定义为
\begin{document}$[e]-\left\{e{'} \mid\left(e'_{2} e\right) \in G^*\right\} $\end{document}
, 局部配置对应的Petri网可达标识是指从初始状态执行[e ]中各个事件后到达的原Petri网系统标识. 若事件e 局部配置对应的可达标识与某已经存在之事件局部配置对应的可达标识相等, 则称e 为截断事件. 例如, 图3 给出的就是一个出现网, 它用以描述图2 中Petri网的行为.
3
图2中程序Petri网模型的展开
文献[30 ]已指出, 对于任意一个有界的Petri网系统, 可以构造一个有限的出现网来刻画网系统的行为, 称该出现网为原Petri网的有限完全展开. 例如, 图3 所示的Petri网展开中, 前驱为空的条件集合为
\begin{document}$ \{ {c_0}, {c_1}\} $\end{document}
, 它对应原Petri网的初始标识
\begin{document}$ \{ {p_0}, {p_{lock}}\} $\end{document}
. 事件e 6 和e 13 对应原Petri网中变迁t B0 两次不同场景下的执行. 具体而言, e 6 对应锁对象lock 先授权给线程threadB、后授权给线程threadA这一场景下t B0 的一次执行, 而e 13 对应lock 先授权给线程threadA、后授权给线程threadB这一场景下t B0 的一次执行. 条件c 1 、c 12 、c 14 、c 22 和c 25 均对应原Petri网库所p lock 中的一个token. c 1 对应的是Petri网初始标识下p lock 中的token, c 12 对应的是lock 先授权给线程threadB、后授权给线程threadA这一场景下锁释放操作t B 2 执行完毕后产生的p lock 中的token, 其余类似可得. 事件e 11 对应的是lock 先授权给线程threadB、后授权给线程threadA这一场景下, 线程threadB对变量x 的写操作t B3 的一次执行. 而lock 先授权给线程threadA、后授权给线程threadB这一场景下t B 3 的执行则因为截断事件e 18 的存在而被省略. e 18 之所以是截断事件, 是因为该事件的局部配置
\begin{document}$ \{ {c_{24}}, {c_{25}}, {c_{13}}, {c_7}\} $\end{document}
与事件e 17 的局部配置{c 22 , c 23 , c 15 , c 7 }对应着原Petri网的同一个标识
\begin{document}$ \{ {p_{B3}}, {p_{lock}}, {p_{A4}}, {p_3}\} $\end{document}
.
事件e 11 对应线程threadB对变量x 的写操作t B3 的一次执行, 事件e 3 对应线程threadA对变量x 的写操作t A0 的一次执行. 在图3 的展开中, 两者满足
\begin{document}$ {e_3}||{e_{11}} $\end{document}
, 两个事件具有并发关系, 这意味着原Petri网中变迁t B3 与t A0 存在并发的可能, 这就得到了关于共享变量x 的一个写冲突, 亦即一个潜在的数据竞争缺陷.
生成Petri网展开的算法有多种, 本文基于Esparza等人在文献[30 ]中提出的展开方法进行前述多线程程序Petri网模型的展开, 具体展开算法见算法1. 在算法实现过程中, 鉴于本文得到的Petri网模型满足1-safe性质, 而且本文目的是进行共享变量读写(或者写写)操作之间的并发关系检测, 本文使用优先队列和哈希函数的方法对文献[30 ]给出的展开算法进行了性能优化, 具体优化措施包括: (1)使用优先队列按照
\begin{document}$ \prec $\end{document}
关系动态维护展开中产生的事件; (2)按照序关系
\begin{document}$ \prec $\end{document}
弹出优先队列中最小的e ; (3)根据哈希函数判断e 是否为截断事件.
算法1 . 满足1-safe性质的Petri网模型的展开算法.
输入: 由程序运行轨迹挖掘到的Petri网
\begin{document}$ \Sigma = (P, T;F, {M_0}) $\end{document}
;
输出: Petri网模型的展开
\begin{document}$ \pi = (ON, h) $\end{document}
, 中
\begin{document}$ON = (B, E;G)$\end{document}
是一个出现网,
\begin{document}$ h $\end{document}
是将
\begin{document}$ ON $\end{document}
中的条件/事件映射到
\begin{document}$ \Sigma $\end{document}
中库所/变迁的函数.
步骤:
1.
\begin{document}$B: = \varnothing , E: = \varnothing , G: = \varnothing$\end{document}
2. FOREACH (
\begin{document}$ p \in P $\end{document}
)
3. IF (
\begin{document}$ {M_0}(p) \ne 0 $\end{document}
)
4. 向B 中添加一个新的条件b , 并令
\begin{document}$ h(b): = p $\end{document}
;
5. 计算当前展开片段
\begin{document}$ \pi $\end{document}
的候选扩展集合PE , 每个候选扩展是一个二元组
\begin{document}$ < t, {B_t} > $\end{document}
, 当中
\begin{document}$ t \in T $\end{document}
,
\begin{document}$ {B_t} \subseteq B $\end{document}
且
\begin{document}$ h\left( {{B_t}} \right){ = ^ \bullet }t $\end{document}
;
6. 初始化截断事件的集合Cur-Off 为
\begin{document}$\varnothing$\end{document}
;
7. WHILE (
\begin{document}$PE \ne \varnothing$\end{document}
) {
8. 在PE 中选择扩展
\begin{document}$ < t, {B_t} > $\end{document}
使得据其添加的事件
\begin{document}$ e: = < t, {B_t} > $\end{document}
按照第3节定义的关系
\begin{document}$ \prec $\end{document}
最小;
9. 在E 中添加事件e , 并令
\begin{document}$ h\left( e \right): = t $\end{document}
,
\begin{document}$ G: = G \cup \left\{ { < b, e > \left| {b \in {B_t}} \right.} \right\} $\end{document}
;
10. FOREACH (
\begin{document}$ p \in {t^ \bullet } $\end{document}
)
11. 向B 中添加一个新的条件b , 并令
\begin{document}$ h(b): = p $\end{document}
;
\begin{document}$ G: = G \cup \left\{ { < e, b > } \right\} $\end{document}
;
12. 从PE 中删除
\begin{document}$ < t, {B_t} > $\end{document}
;
12. IF (e 不是截断事件)
13. 根据新添加的条件b 重新计算并更新
\begin{document}$ \pi $\end{document}
的候选扩展集合PE
14. ELSE
15. 向cut-off 中添加事件e
16. }//WHILE
17. RETURN
\begin{document}$ \pi = (ON, h) $\end{document}
, 当中
\begin{document}$ ON = (B, E;G) $\end{document}
在上述Petri网的展开过程中, 为便于进行数据竞争检测, 对于每个共享变量的读写事件均会计算与其并发的所有其他读写事件, 然后判断这些并发的读写事件之间是否存在针对同一个共享变量的读写/写写冲突. 若存在, 则输出冲突事件及其全部前驱节点构成的Petri网展开的一个前缀, 该前缀就对应着原始程序一个潜在的数据竞争, 称其为该数据竞争伴随的Petri网展开前缀, 可记之为一个四元组
\begin{document}$ DR\_ON = (B', E';G', h') $\end{document}
, 当中
\begin{document}$ (B', E';F') $\end{document}
为该展开前缀对应的出现网,
\begin{document}$ {h{'}} $\end{document}
是将各个条件库所和变迁映射到源程序Petri网模型中一个锁对象库所、控制流状态库所或者程序操作变迁的映射函数.
以图3 中的Petri网展开为例, 当得到事件e 11 并检测到
\begin{document}$ {e_3}||{e_{11}} $\end{document}
时, 我们会导出图4 所示的Petri网展开前缀(为方便理解, 该图中给出了各个节点对应的程序元素, 同时加入了共享变量节点), 它对应的就是第2节所述的程序Program 1中存在的数据竞争.
4
Program 1中潜在数据竞争所伴随的Petri网展开前缀
4
基于网展开前缀的数据竞争重演
第2节所定义的程序运行轨迹忽略了很多可能影响数据竞争出现与否的同步原语, 比如wait、notify、suspend、LockSupport.park等, 这有可能导致前文所得Petri网模型的可执行变迁序列中隐含着原始程序中无法执行的操作序列, 进而会导致一些数据竞争的误报. 幸运的是, 上节所得Petri网展开前缀隐含了各个潜在数据竞争的产生根源和具体发生路径, 本节将据此给出控制源程序运行的一种确定性调度方法, 以此重演潜在的数据竞争, 重演成功的数据竞争方为真实的并发漏洞.
为此, 首先对上节所得潜在数据竞争对应的Petri网展开前缀进行分析, 计算其中出现的各个锁对象的授权线程序列. 具体见算法2, 基本思想是, 展开前缀中对关联着一个锁对象且无前驱的条件库所必然对应着这个锁对象的初始可用状态, 找到这些条件库所后, 只需沿该条件库所的后继节点追踪这个锁对象的使用线程, 一旦持有该锁对象的线程发生一次改变则将该线程ID追加到锁对象的授权线程序列中即可, 具体过程见算法1. 算法2的时间复杂度为
\begin{document}${\text{O}}(|\mathit{Locks}| \times \;(|B'| + |E'|))$\end{document}
, 当中
\begin{document}$|\mathit{Locks}|$\end{document}
为数据竞争伴随Petri网展开前缀中出现的锁对象数量,
\begin{document}$ |B'| $\end{document}
为前缀中条件库所的个数,
\begin{document}$ |E'| $\end{document}
为前缀中事件的个数.
以图4 所示的展开前缀为例, 当中仅仅出现了一个锁对象lock , 而且该对象仅在执行变迁t B0 时被授权给了线程threadB, 故lock 的授权线程序列为
\begin{document}$ \delta (lock) = < {\rm{threadB }} > $\end{document}
.
算法2 . 由潜在数据竞争伴随的Petri网展开前缀计算各个锁对象的授权线程序列.
输入: 某潜在数据竞争伴随的Petri网展开前缀
\begin{document}$ DR\_ON = (B', E';G', h') $\end{document}
;
输出: 展开前缀中出现的锁对象的集合LockSet , 以及一个为其中每个锁对象指定一个授权线程序列的函数
\begin{document}$ \delta $\end{document}
.
步骤:
1. 在DR_ON 中寻找前驱节点为空且h' (x )对应一个锁对象的条件库所x , 计入集合C_Lock ;
2. FOREACH (
\begin{document}$ c \in C\_Lock $\end{document}
) {
3. 设o 为 h' (c ) 所对应的锁对象的ID;
4. 初始化
\begin{document}$ \delta (o) $\end{document}
为一个空序列;
5. WHILE (c 在DR_ON 中存在后继节点){
6. 记e 为c 的后继事件, 并记
\begin{document}$ {\# _{{rm{ThreadID}}}}(e) $\end{document}
为h' (e )所对应操作隶属的线程ID;
7. IF (h' (e )是一个针对锁对象o 的锁获取操作){
8. 令
\begin{document}$\delta (o): = \delta (o) \circ {{\#} _{\rm{ThreadID}}}(e)$\end{document}
, 其中
\begin{document}$ \circ $\end{document}
表示序列的拼接操作;
9. 重置c 为e 的后继条件库所(该库所是唯一的, 因为每个锁获取操作后只有一个控制流库所为其后继);
10. }
11. ELSEIF (h' (e )是一个针对锁对象o 的锁释放操作)
12. 此时h' (e )会有一个控制流状态库所和一个资源库所为其后继条件, 令c 为资源库所对应的条件;
13. ELSEIF (h' (e )是一个线程的fork、join或stop操作, 或者是某共享变量的读写操作)
14. 此时h' (e )的后继库所中存在一个库所描述线程
\begin{document}$ {\# _{{\text{ThreadID}}}}(e) $\end{document}
的控制流状态, 重置 c 为该库所对应的条件;
15. } //WHILE
16. 将锁对象o 并入集合LockSet , 上述过程得到的
\begin{document}$ \delta (o) $\end{document}
即为其授权线程序列;
17. }//FOREACH
18. RETURN LockSet 与函数
\begin{document}$ \delta $\end{document}
.
此外, 基于数据竞争伴随的Petri网展开前缀, 从主线程就绪态对应的条件库所出发, 遍历整个前缀, 易得潜在数据竞争的发生位置(即哪2个线程第几次读/写哪个共享变量时发生了冲突). 以图4 为例, 潜在数据竞争对应的是事件e 3 与e 11 对共享变量x 的写操作冲突, 遍历前缀不难发现它们分别对应线程threadA对x 的第m =1次写操作、线程threadB对x 的第n =1次写操作.
得到各个锁对象的授权线程序列
\begin{document}$ \mathrm{\delta } $\end{document}
, 以及数据竞争的位置信息(假设潜在数据竞争由线程t 1 第m 次对共享变量x 的读/写操作、线程t 2 第n 次对x 的读/写操作构成)后, 基于CalFuzzer[32 ] 或其他的多线程程序主动调试平台[33 ,34 ] 再次运行原程序, 运行过程中按如下调度规则干预其执行过程.
● 调度规则Rule 1. 每当有线程t 尝试执行锁对象lock 的获取操作时, 分如下3种情况.
(1)若lock 的授权线程序列
\begin{document}$ \delta (lock) $\end{document}
当前非空、且尝试获取lock 的线程t 不是
\begin{document}$ \delta (lock) $\end{document}
的首元素, 则在CalFuzzer提供的lockBefore函数接口中阻塞线程t , 将其加入lock 关联的一个阻塞线程池.
(2)若lock 的授权线程序列
\begin{document}$ \delta (lock) $\end{document}
当前非空、且尝试获取lock的线程t 是
\begin{document}$ \delta (lock) $\end{document}
的首元素, 则直接执行该锁授权操作, 并在CalFuzzer提供的lockAfter函数接口中删除
\begin{document}$ \delta (lock) $\end{document}
的首元素, 再通过Calfuzzer的 unblock函数唤醒之前因为访问lock 访问而被阻塞的各个线程.
(3)若lock 的授权线程序列
\begin{document}$ \delta (lock) $\end{document}
当前为空, 则在CalFuzzer提供的lockBefore函数接口中阻塞尝试获取锁lock 的线程.
以程序Program 1为例, 按照图4 中展开前缀导出的锁授权线程序列为
\begin{document}$ \delta (lock) = < {\rm{ threadB}} > $\end{document}
. 重演阶段调度Program 1的运行时, 若threadA首先尝试获取lock , 则应通过block函数阻塞线程threadA; 若首次尝试获取lock 的线程是threadB, 则将锁lock 授权给threadB, 并删除
\begin{document}$ \delta (lock) $\end{document}
的首元素、更新其为空; 若threadA首先尝试获取lock 被阻塞, 而threadB之后尝试获取锁lock , 则将lock 授权给threadB并删除
\begin{document}$ \delta (lock) $\end{document}
的首元素后, 还应唤醒被阻塞的线程threadA.
● 调度规则Rule 2. 当线程t 1 尝试执行潜在数据竞争对应的对共享变量x 的第m 次读/写时, 在CalFuzzer提供的writeBefore函数接口中阻塞该线程, 同时设置变量t 1 _x 为true; 类似地, 当t 2 尝试执行潜在数据竞争对应的对共享变量x 的第n 次读/写时, 在CalFuzzer提供的writeBefore函数接口中也阻塞该线程, 同时设置变量t 2 _x 为true. 一旦t 1 _x 和t 2 _x 均为true, 则说明这2个共享变量的读/写操作在Calfuzzer的调度下同时处于了可执行状态, 数据竞争重演成功.
以前文Program 1为例, 假设基于Calfuzzer对该程序进行调度运行时, 原始程序仍然尝试按照表1 的轨迹运行, 按照上述调度策略则会执行表4 所示的各种调度措施, 最终会重演出我们想要的数据竞争缺陷. 需要指出的是, 这一并发缺陷按照表1 的原始轨迹运行时不会出现, 而且FastTrack[15 ] 、VerifiedFT[17 ] 等传统的动态分析方法也无法检测到该缺陷.
4
程序Program 1的一个数据竞争重演过程
序号
主线程
线程A
线程B
操作执行前后CalFuzzer的干预措施
1
6: wr(mainThread, flag )
writeBefore: 无干预
writeAfter: 无干预
2
27: fork(mainThread, threadA)
startBefore: 无干预
3
28: fork(mainThread, threadB)
startBefore: 无干预
4
9: wr(threadA, x )
writeBefore: (1) 阻塞threadA; (2) 设置threadA_ x 为true;
writeAfter: 无干预
5
18: acq(threadB, lock )
lockBefore: 无干预
lockAfter: 删除
\begin{document}$ \delta (lock) $\end{document}
的首元素
6
19: rd(threadB, flag )
readBefore: 无干预
readAfter: 无干预
7
20: rel(threadB, lock )
unlockAfter: 无干预
8
22: wr(threadB, x )
writeBefore: (1) 阻塞threadB; (2) 设置threadB_ x 为true; (3) 因threadA_ x 与threadB_ x 同时为true, 输出e 11 与e 3 所对应的程序第9行与第22行代码存在数据竞争
最后, 需要说明的是, 本文所提数据竞争检测和重演方法是一个两阶段的数据竞争分析方法, 需要运行源程序2次. 第1阶段, 通过CalFuzzer[32 ] 或RoadRunner[33 ] 等程序运行跟踪平台捕获程序首次运行时产生的运行轨迹, 构造本次运行对应的程序Petri网模型, 并借助Petri网的展开分析程序中潜在的数据竞争错误, 获取各个潜在数据竞争对应的锁对象授权线程序列以及数据竞争的位置信息; 第2阶段, 通过 CalFuzzer或其他程序主动调试平台, 在锁的授权操作或共享变量的读写操作前后, 执行特定的干预操作, 以此实现数据竞争的重演. 然而, 众所周知, 即使是同一个程序中同一个线程、同一个锁或者共享变量对象, 它们在两次不同的运行过程中可能会分配不同的ID. 按照本节方法进行数据竞争重演的前提是要在同一对象的不同ID之间建立映射关系. 解决方案如下: (1)就线程ID的对应而言, 两次运行中的第一个启动的线程必然是主线程, 由此可建立主线程之间的ID对应关系. 进而, 即使在两次不同的程序运行中, 主线程依次启动的子线程序列是一致的, 由此可以在这些子线程ID之间建立一一映射关系. 类似的道理, 根据各个子线程启动的线程序列又可建立其他线程ID之间的对应关系, 最终可完成线程ID之间的一一对应; (2)由于每个线程依次申请的锁对象序列是一致的, 据此可以在建立锁对象ID之间的对应关系; (3)每个线程依次访问的共享变量序列也是一致的, 据此可以得到共享变量ID之间的一一映射关系.
5
原型系统与实验评估
5.1
原型系统
基于Java多线程程序主动调试的开源平台CalFuzzer[32 ] 研发了相应的数据竞争动态检测和重演工具. 基于该工具, 用户只需输入一个多线程程序, 工具便会调用CalFuzzer的程序事件流自动生成功能捕获程序的运行轨迹, 之后根据捕获的轨迹构建程序的Petri网模型, 再基于Petri网展开算法对程序Petri网模型中蕴含的潜在数据竞争进行检测, 对于每个潜在数据竞争生成相应的Petri网展开前缀; 最后, 根据各个潜在数据竞争对应的Petri网展开前缀, 生成锁对象的授权线程序列用作程序运行的调度方案, 进而, 调用CalFuzzer平台提供的writeBefore、writeAfter、readBefore、readAfter、startBefore、startAfter、lockBefore、lockAfter、unlockAfter等函数进行程序执行的调度和数据竞争的重演. 所开发工具的架构和运行界面分别见图5 、图6 所示.
5
数据竞争检测与重演原型系统架构
6
原型系统运行界面截图
原型系统架构分为线程控制层、数据分析层、结果界面层3部分(如图5 所示). 最底层的线程控制层基于CalFuzzer内置API实现: 在线程事件捕捉模块中, 使用SOOT分析并修改程序的字节码, 在与并发相关的语句处插入回调函数, 在一次真实执行中捕捉多线程程序运行时的相关动作; 在线程调度控制模块中, 针对每个潜在的数据竞争, 根据上层数据竞争分析层得到的锁授权线程序列进行程序调度以重演数据竞争. 中间层为数据竞争分析层, 模型挖掘模块依据程序运行轨迹建立程序的Petri网模型, 并基于算法1对程序的Petri网模型进行展开; 数据竞争分析模块根据程序Petri网模型的展开分析读写冲突、检测潜在数据竞争, 为每一个潜在数据竞争生成一个展开前缀, 并据此计算锁对象的授权线程序列用作数据竞争重演的程序调度方案; 最终, 结合重演结果生成数据竞争分析报告. 最上层为系统界面层, 向用户展示挖掘得到的程序Petri网模型、Petri网模型的展开、所检测到的数据竞争对应的Petri网展开前缀, 同时给出数据竞争报告(如图6 所示).
图6 给出的是所开发原型系统的部分界面截图, 图6 (a)是根据程序运行轨迹挖掘和构建的多线程程序Petri网模型, 图6 (b)为Petri网展开的界面, 图6 (c)展示了一个潜在数据竞争对应的Petri网展开前缀和数据竞争检测结果, 图6 (c)中的提示信息Thread 1 write test/TestRace.java#41 address=4294967299(22)表示代码TestRace.java中在41行22列线程1中地址为4294967299的共享变量x 的写操作, 与代码49行26列线程2中该共享变量的写操作存在数据竞争.
5.2
实验评估与相关工作比较
就相关工作比较而言, 第2节结合程序Program 1从原理上说明了本文方法相比VerifiedFT等经典动态分析方法的优势, 即本文方法虽然是从单一运行轨迹挖掘得到程序的Petri网模型, 但是这个模型可以隐含多条潜在的程序运行轨迹, 从而可以减少数据竞争的漏报现象. 与此同时, 由于动态分析方法均依赖程序运行轨迹进行漏洞检测, 而完整的覆盖各种可能的程序执行路径难以获得, 丢失的路径中可能隐含着数据竞争, 故包括本文方法在内的数据竞争检测均可能存在一定漏报, 具体漏报率依赖于测试用例对程序执行路径的覆盖情况. 除此之外, 结合CalFuzzer软件平台[12 ] 中公开的多个Java多线程程序实例进行了实验评估和对比, 实验对比结果见表5 .
5
数据竞争检测试验结果
程序实例
实际数据竞争数量
本文方法的
检测结果
Calfuzzer集成方法HybridAnalysis+
Racefuzzer的检测结果
本文方法运行时间 (s)
CalFuzzer集成方法
HybridAnalysis+
Racefuzzer的单次运行时间 (s)
Test1
3
无漏报和误报
无漏报和误报
4
2.2
Test2
0
无漏报和误报
无漏报和误报
3.1
1.1
Test3
3
无漏报和误报
有一定概率发生漏报 (单次运行概率大, 运行次数增加概率逐渐变小), 无误报
3.2
2.1
Test4
6
无漏报和误报
有一定概率发生漏报(单次运行概率大, 运行次数增加概率逐渐变小), 无误报
6
4.2
Test5
0
无漏报和误报
无漏报和误报
3.1
1.3
Test6
3
无漏报和误报
有一定概率发生漏报(单次运行概率大, 运行次数增加概率逐渐变小), 无误报
4
2.1
Test7
0
无漏报和误报
无漏报和误报
3
1.3
Test8
0
无漏报和误报
无漏报和误报
10
3
Test9
0
无漏报和误报
无漏报和误报
6.4
2.1
Test10
3
无漏报和误报
有一定概率发生漏报(单次运行概率大, 运行次数增加概率逐渐变小), 无误报
5.4
3
Test11
3
无漏报和误报
有一定概率发生漏报(单次运行概率大, 运行次数增加概率逐渐变小), 无误报
4
2.3
Test12
2
无漏报和误报
有一定概率发生漏报(单次运行概率大, 运行次数增加概率逐渐变小), 无误报
10
11
本文实例Program1
2
有一定概率发生一个漏报(运行次数增加概率逐渐变小). 仅以表1 中的轨迹为依据发生1个漏报. 无误报
有一定概率发生两个或一个漏报(单次运行概率大, 运行次数增加概率逐渐变小). 仅以表1 中的轨迹为输入发生2个漏报. 无误报
3.1
2.7
对于程序实例Test1, 由于程序中不存在锁对象或锁的竞争, 任意一条程序运行轨迹中均能呈现出程序中存在的数据竞争漏洞, 故本文方法和CalFuzzer中集成的基于HybridAnalysis与RaceFuzzer的数据检测方法均能完整、准确的检测出程序的数据竞争缺陷; 对于程序实例Test3–6、Test10–12, 程序中存在锁对象的竞争等复杂的并发操作与程序行为, 有的运行轨迹能呈现出程序中的数据竞争缺陷, 而有的运行轨迹则无法直接呈现. 此时, CalFuzzer中集成的方法通常需要多次运行、分析多条执行轨迹方能完整的检测出程序中存在的数据竞争(实验表明, 单次运行通常会出现漏报, 运行3次以上通常能检测出所有的数据竞争), 而本文所提方法只需基于单条运行轨迹就可准确作出检测, 没有任何漏报现象; 其余程序实例本身不存在数据竞争缺陷, 所以两类方法均无漏报. 此外, 由于本文方法和CalFuzzer集成的方法均进行了数据竞争重演, 故所有的程序实例均没有误报.
从时间性能来看, 本文所提数据竞争检测方法的时间消耗大部分情况下高于CalFuzzer中集成的方法, 原因在于本文挖掘到的Petri网模型可能蕴含有多条运行轨迹, 对该Petri网进行展开时通常会消耗更多的时间. 而且, 程序中存在的线程数量和并发行为越多, 本文方法消耗的时间越多. 为进行时间测试, 设计了不同规模的多个多线程程序实例进行了性能测试. 具体而言, 每个测试程序设置两个共享变量进行自增操作, 设置两把锁分别进行获取和释放, 然后不断增加线程规模, 测试结果见表6 . 由测试结果可见, 当线程数目较少时, 我们的方法具有比较好的性能表现, 但当线程数量增加到10个以上时, 运行时间会以指数形式增加, 这主要是由于Petri网展开规模的快速增长. 不过, 这种时间上的损失带来的好处是漏报现象的减少.
6
Petri网展开的性能测试结果
线程数
库所数
变迁数
条件数
事件数
截断事件数
运行时间 (ms)
2
16
14
20
15
0
6
4
42
38
142
113
5
101
6
68
62
821
654
17
250
8
94
86
86
3490
321
2293
10
120
110
22176
17557
1793
13988
12
146
134
107556
85015
9217
216820
在对大规模并发程序进行数据竞争检测时, 为提高效率, 一个可能的方法是先基于lockset等效率高但是准确性不足的方法定位潜在的数据竞争, 然后, 以每组潜在的数据竞争为对象, 有针对性的进行程序Petri网模型的展开和数据竞争检测. 实际上, 文献[26 ]提出的Petri网反向展开算法可用于解决此问题. 不过, 文献[26 ]将Petri网的反向展开用于程序的静态分析, 它根据程序源码构造程序的Petri网模型、进而借助反向展开检测数据竞争. 但是, 当中需要用户人为给出一组可能存在竞争的共享变量读写操作, 之后进行针对性的检测. 而且, 静态分析方法在大规模程序分析时同样存在效率问题, 误报率较高. 后续工作中, 作者将尝试将本文方法与文献[26 ]中的方法进行结合, 在提高效率的同时降低误报率.
最后, 传统的数据竞争检测方法只会指出存在数据竞争的语句位置, 而本文方法所得数据竞争锁伴随的Petri网展开前缀可以直观展现这种缺陷的发生场景. 而且, 根据这种Petri网展开前缀可以有效地进行思索的重演, 以此保证潜在数据竞争的真实性. 不过, 本文方法也存在很多不足, 比如, 本文未考虑wait、notify等对数据竞争检测可能带来影响的其他同步原语.
6
总结与分析
本文提出了一种基于Petri网展开的多线程程序数据竞争检测和重演方法, 其主要的检测步骤和特色如下: 首先, 通过对程序某次运行轨迹的分析构建程序的Petri网模型, 该模型虽由单一运行轨迹挖掘得到, 但可能隐含着多个不同的程序可执行操作序列, 从而可降低传统数据竞争动态检测方法的漏报率; 之后, 将程序的数据竞争检测问题转换为Petri网模型中共享变量读写/写写操作的并发关系识别问题, 并借助Petri网展开技术完成了程序中潜在数据竞争的检测; 最后, 基于各个潜在数据竞争伴随的Petri网展开前缀给出了潜在数据竞争的触发路径, 并以此为基础, 借助CalFuzzer平台实现了数据竞争的重演, 保证了数据竞争检测真实性. 此外, 相比数据竞争的静态检测方法而言, 本文仅分析单一运行轨迹对应的Petri网模型, 这有效缩减了问题的复杂度, 而且能保证数据竞争检测的真实性. 相比传统的数据竞争动态检测方法而言, 本文从单一运行轨迹挖掘得到的Petri网模型可以蕴含多条不同的程序运行轨迹, 可以减少数据竞争的漏报现象.
不过, 目前所提方法仍然存在诸多不足. 比如, 本文未考虑wait、notify等对数据竞争检测可能带来影响的其他同步原语, 对大规模程序进行分析时的性能有待优化等. 此外, 在进行数据竞争重演的过程中, 程序在如下两种情况下可能出现死锁: 其一, 被检测程序本身存在死锁, 在重演过程中该死锁被触发了; 其二, 被检测程序本身不存在死锁, 但是拟重演的潜在数据竞争是一个误报, 此时本文给出的程序调度和重演算法可能会导致死锁. 上述两种情况均会导致数据竞争重演的失败, 使得算法无法判定潜在数据竞争的真伪. 针对这一问题, 可以在重演的过程中借助死锁的动态检测方法[35 ,36 ] 进行死锁分析, 一旦检测到死锁的发生, 则对当时的锁图和相关的程序运行状态进行分析, 分析死锁产生的根源, 据此开展后续的程序漏洞修复或者开展进一步的数据竞争分析工作, 相关研究将在后续工作中展开.
References
[
]1
苏小红, 禹振, 王甜甜, 马培军
并发缺陷暴露、检测与规避研究综述
计算机学报
2015
38
11
2215
2233
10.11897/SP.J.1016.2015.02215
苏小红, 禹振, 王甜甜, 马培军. 并发缺陷暴露、检测与规避研究综述. 计算机学报, 2015, 38(11): 2215–2233. [doi: 10.11897/SP.J.1016.2015.02215]
Su XH, Yu Z, Wang TT, Ma PJ
A survey on exposing, detecting and avoiding concurrency bugs
Chinese Journal of Computers
2015
38
11
2215
2233
10.11897/SP.J.1016.2015.02215
Su XH, Yu Z, Wang TT, Ma PJ. A survey on exposing, detecting and avoiding concurrency bugs. Chinese Journal of Computers, 2015, 38(11): 2215–2233 (in Chinese with English abstract). [doi: 10.11897/SP.J.1016.2015.02215]
[
]2
关守平, 王梁
云控制系统不确定性分析与控制器设计方法
自动化学报
2022
48
11
2677
2687
10.16383/j.aas.c190529
关守平, 王梁. 云控制系统不确定性分析与控制器设计方法. 自动化学报, 2022, 48(11): 2677−2687. [doi: 10.16383/j.aas.c190529]
Guan SP, Wang L
Uncertainty analysis of clouded control system with its controller design
Acta Automatica Sinica
2022
48
11
2677
2687
10.16383/j.aas.c190529
Guan SP, Wang L. Uncertainty analysis of clouded control system with its controller design. Acta Automatica Sinica, 2022, 48(11): 2677−2687. (in Chinese with English abstract).
[
]3
王彩璐, 陶跃钢, 杨鹏, 刘作军, 周颖
云控制系统并行任务分配优化算法与并联控制
自动化学报
2017
43
11
1973
1983
10.16383/j.aas.2017.c160504
王彩璐, 陶跃钢, 杨鹏, 刘作军, 周颖. 云控制系统并行任务分配优化算法与并联控制. 自动化学报, 2017, 43(11): 1973–1983. [doi: 10.16383/j.aas.2017.c160504]
Wang CL, Tao YG, Yang P, Liu ZJ, Zhou Y
Parallel task assignment optimization algorithm and parallel control for cloud control systems
Acta Automatica Sinica
2017
43
11
1973
1983
10.16383/j.aas.2017.c160504
Wang CL, Tao YG, Yang P, Liu ZJ, Zhou Y. Parallel task assignment optimization algorithm and parallel control for cloud control systems. Acta Automatica Sinica, 2017, 43(11): 1973–1983 (in Chinese with English abstract). [doi: 10.16383/j.aas.2017.c160504]
[
]4
Netaer RHB, Miller BP
What are race conditions? Some issues and formalizations
ACM Letters on Programming Languages and Systems
1992
1
1
74
88
10.1145/130616.130623
Netaer RHB, Miller BP. What are race conditions?: Some issues and formalizations. ACM Letters on Programming Languages and Systems, 1992, 1(1): 74–88. [doi: 10.1145/130616.130623]
[
]5
禹振, 杨振, 苏小红, 王甜甜
多线程程序数据竞争检测和验证方法研究综述
智能计算机与应用
2017
7
3
123
126, 129
10.3969/j.issn.2095-2163.2017.03.034
禹振, 杨振, 苏小红, 王甜甜. 多线程程序数据竞争检测和验证方法研究综述. 智能计算机与应用, 2017, 7(3): 123–126, 129.
Yu Z, Yang Z, Su XH, Wang TT
A survey on methods of data race detection and verification on multithreaded program
Intelligent Computer and Applications
2017
7
3
123
126, 129
10.3969/j.issn.2095-2163.2017.03.034
Yu Z, Yang Z, Su XH, Wang TT. A survey on methods of data race detection and verification on multithreaded program. Intelligent Computer and Applications, 2017, 7(3): 123–126, 129 (in Chinese).
[
]6
[
]7
[
]8
Pratikakis P, Foster JS, Hicks M
LOCKSMITH: Context-sensitive correlation analysis for race detection
ACM SIGPLAN Notices
2006
41
6
320
331
10.1145/1133255.1134019
Pratikakis P, Foster JS, Hicks M. LOCKSMITH: Context-sensitive correlation analysis for race detection. ACM Sigplan Notices, 2006, 41(6): 320–331. [doi: 10.1145/1133255.1134019]
[
]9
Savage S, Burrows M, Nelson G, Sobalvarro PG, Anderson TE
Eraser: A dynamic data race detector for multithreaded programs
ACM Trans. on Computer Systems
1997
15
4
391
411
10.1145/265924.265927
Savage S, Burrows M, Nelson G, Sobalvarro PG, Anderson TE. Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 1997, 15(4): 391–411. [doi: 10.1145/265924.265927]
[
]10
Von Praun C, Gross TR
Object race detection
ACM SIGPLAN Notices
2001
36
11
70
82
10.1145/504311.504288
Von Praun C, Gross TR. Object race detection. ACM Sigplan Notices, 2001, 36(11): 70–82. [doi: 10.1145/504311.504288]
[
]11
[
]12
[
]13
Perkovic D, Keleher PJ
Online data-race detection via coherency guarantees
ACM SIGOPS Operating Systems Review
1996
30
SI
47
57
10.1145/248155.238760
Perkovic D, Keleher PJ. Online data-race detection via coherency guarantees. ACM SIGOPS Operating Systems Review, 1996, 30(SI): 47–57. [doi: 10.1145/248155.238760]
[
]14
ItzkovitzA, Schuster A, Zeev-Ben-Mordehai O
Toward integration of data race detection in DSM systems
Journal of Parallel & Distributed Computing
1999
59
2
180
203
10.1006/jpdc.1999.1574
ItzkovitzA , Schuster A , Zeev-Ben-Mordehai O. Toward integration of data race detection in DSM systems. Journal of Parallel & Distributed Computing, 1999, 59(2):180-203. [doi:10.1006/jpdc.1999.1574 ]
[
]15
Flanagan C, Freund SN
FastTrack: Efficient and precise dynamic race detection
ACM SIGPLAN Notices
2009
44
6
121
133
10.1145/1543135.1542490
Flanagan C, Freund SN. FastTrack: Efficient and precise dynamic race detection. ACM SIGPLAN Notices, 2009, 44(6): 121–133. [doi: 10.1145/1543135.1542490]
[
]16
Ha OK, Jun YK
An efficient algorithm for on-the-fly data race detection using an epoch-based technique
Scientific Programming
2015
2015
13
10.1155/2015/205827
Ha OK, Jun YK. An efficient algorithm for on-the-fly data race detection using an epoch-based technique. Scientific Programming, 2015, 2015: 13. [doi: 10.1155/2015/205827]
[
]17
Wilcox JR, Flanagan C, Freund SN
VERIFIED FT: A verified, high-performance precise dynamic race detector
ACM SIGPLAN Notices
2018
53
1
354
367
10.1145/3200691.3178514
Wilcox JR, Flanagan C, Freund SN. VERIFIED FT: A verified, high-performance precise dynamic race detector. ACM SIGPLAN Notices, 2018, 53(1): 354–367. [doi: 10.1145/3200691.3178514]
[
]18
Pozniansky E, Schuster A
MultiRace: Efficient on-the-fly data race detection in multithreaded C++ programs
Concurrency and Computation: Practice and Experience
2007
19
3
327
340
10.1002/cpe.1064
Pozniansky E, Schuster A. MultiRace: Efficient on-the-fly data race detection in multithreaded C++ programs. Concurrency and Computation: Practice and Experience, 2007, 19(3): 327–340. [doi: 10.1002/cpe.1064]
[
]19
Xie XW, Xue JL, Zhang J
ACCULOCK : Accurate and efficient detection of data races
Software: Practice and Experience
2013
43
5
543
576
10.1002/spe.2121
Xie XW, Xue JL, Zhang J. ACCULOCK : Accurate and efficient detection of data races. Software: Practice and Experience, 2013, 43(5): 543–576. [doi: 10.1002/spe.2121]
[
]20
Yu MS, Bae DH
Simplelock+ : Fast and accurate hybrid data race detection
The Computer Journal
2016
59
6
793
809
10.1093/comjnl/bxu119
Yu MS, Bae DH. Simplelock+ : Fast and accurate hybrid data race detection. The Computer Journal, 2016, 59(6): 793–809. [doi: 10.1093/comjnl/bxu119]
[
]21
[
]22
Wu ZD, Lu K, Wang XP, Zhou X
Collaborative technique for concurrency bug detection
Int’l Journal of Parallel Programming
2015
43
2
260
285
10.1007/s10766-014-0304-y
Wu ZD, Lu K, Wang XP, Zhou X. Collaborative technique for concurrency bug detection. International Journal of Parallel Programming, 2015, 43(2): 260–285. [doi: 10.1007/s10766-014-0304-y]
[
]23
[
]24
[
]25
[
]26
http://www.jos.org.cn/1000-9825/6240.htm]]>
http://www.jos.org.cn/1000-9825/6240.htm]]>
[
]27
庞善臣, 蒋昌俊, 孙萍, 周长红
共享合成Petri网的性质分析
自动化学报
2004
30
6
944
948
10.16383/j.aas.2004.06.019
庞善臣, 蒋昌俊, 孙萍, 周长红. 共享合成Petri网的性质分析. 自动化学报, 2004, 30(6): 944–948. [doi: 10.16383/j.aas.2004.06.019]
Pang SC, Jiang CJ, Sun P, Zhou CH
Property analysis of shared composition Petri nets
Acta Automatica Sinica
2004
30
6
944
948
10.16383/j.aas.2004.06.019
Pang SC, Jiang CJ, Sun P, Zhou CH. Property analysis of shared composition Petri nets. Acta Automatica Sinica, 2004, 30(6): 944–948 (in Chinese). [doi: 10.16383/j.aas.2004.06.019]
[
]28
尤丹, 王寿光, 周孟初
信标可控性定义及问题
自动化学报
2014
40
12
2687
2696
10.3724/SP.J.1004.2014.02687
尤丹, 王寿光, 周孟初. 信标可控性定义及问题. 自动化学报, 2014, 40(12): 2687–2696.
You D, Wang SG, Zhou MC
Siphon controllability definitions and issues
Acta Automatica Sinica
2014
40
12
2687
2696
10.3724/SP.J.1004.2014.02687
You D, Wang SG, Zhou MC. Siphon controllability definitions and issues. Acta Automatica Sinica, 2014, 40(12): 2687–2696 (in Chinese).
[
]29
[
]30
[
]31
[
]32
[
]33
[
]34
[
]35
http://www.jos.org.cn/1000-9825/6244.htm]]>
http://www.jos.org.cn/1000-9825/6244.htm]]>
[
]36
鲁法明, 崔明浩, 包云霞, 曾庆田, 段华
基于程序运行轨迹Petri网模型挖掘的死锁检测方法
计算机集成制造系统
2021
27
9
2611
2624
10.13196/j.cims.2021.09.014
鲁法明, 崔明浩, 包云霞, 曾庆田, 段华. 基于程序运行轨迹Petri网模型挖掘的死锁检测方法. 计算机集成制造系统, 2021, 27(9): 2611–2624. [doi: 10.13196/j.cims.2021.09.014]
Lu FM, Cui MH, Bao YX, Zeng QT, Duan H
Deadlock detection method based on petri net mining of program trajectory
Computer Integrated Manufacturing Systems
2021
27
9
2611
2624
10.13196/j.cims.2021.09.014
Lu FM, Cui MH, Bao YX, Zeng QT, Duan H. Deadlock detection method based on petri net mining of program trajectory. Computer Integrated Manufacturing Systems, 2021, 27(9): 2611–2624 (in Chinese). [doi:10.13196/j.cims.2021.09.014]