Page 49 - 《软件学报》2021年第6期

郝宗寅 等:Petri 网的反向展开及其在程序数据竞争检测的应用 1623

测试用例,包含 directed unfolding 的 358 组用例以及我们自己构造的 57 组用例,且所有用例均可覆盖.其中,Petri
网的变迁数量从 6~9462 不等,共计 261694 个变迁.实验环境为 AMD Ryzen 7 4800U,16GB RAM.源码及测试用
例可通过文献[31]获取.
Table 2 Example of concurrent program data race detection
表 2 并发程序数据竞争检测实例
反向展开流程 RExt RUnf

{rext1=(t4,{c1}),rext2=(t8,{c2})}
{rext2=(t8,{c2}),rext3=(t1,{c3})}
step 0. 初始 RUnf 中只有 c1,c2. {rext3=(t1,{c3}),rext4=(t15,{c4}),
step 1. 随机选择 rext1 进行扩展,创建 e1,c3. rext5=(t16,{c4}),rext6=(ts,{c4}),
step 3. 选择 rext2 进行扩展,创建 e2,c4,c5. rext7=(t3,{c5})}
step 4. 选择 rext7 进行扩展,创建 e3,c6. {rext3=(t1,{c3}),rext4=(t15,{c4}),
step 5. 选择 rext9 进行扩展,创建 e4,c7.新增扩展(t16,{c7}), rext5=(t16,{c4}),rext6=(ts,{c4}),
(t16,{c4,c7}),由 RExt 的条件删除(t16,{c7})以及 rext5. rext8=(t6,{c6}),rext9=(t5,{c6})}
step 6. 选择 rext10 进行扩展,创建 e5,c8. {rext3=(t1,{c3}),rext4=(t15,{c4}),
step 7. 选择 rext11 进行扩展,创建 e6.由反向截断事件的 rext6=(ts,{c4}),rext8=(t6,{c6}),
rext10=(t16,{c4,c7})}
定义,e6 会因 RUnf 的初始标识而截断,此次扩展中断. {rext3=(t1,{c3}),rext4=(t15,{c4}),
step 8. 选择 rext8 进行扩展,创建 e7,c9.新增扩展(t1,{c9}), rext6=(ts,{c4}),rext8=(t6,{c6}),
(t1,{c3,c9}),由 RExt 的条件删除(t1,{c9}). rext11=(t11,{c8})}
step 9. 选择 rext12 进行扩展,创建 e8,c10.新增扩展(ts,{c10}), {rext3=(t1,{c3}),rext4=(t15,{c4}),
(ts,{c4,c10}),由 RExt 的条件删除(ts,{c10})以及 rext6. rext6=(ts,{c4}),rext8=(t6,{c6})}
step 10. 选择 rext13 进行扩展,创建 e9,c11. {rext3=(t1,{c3}),rext4=(t15,{c4}),
此时目标标识可覆盖,算法结束. rext6=(ts,{c4}),rext12=(t1,{c3,c9})}
{rext3=(t1,{c3}),rext4=(t15,{c4}),
rext13=(ts,{c4,c10})}

4.1 无启发式策略时反向展开与正向展开的对比

由于启发式策略对算法效率有很大影响,不利于直观地体现反向展开在性质上的优势.因此,本文首先采用
基础的广度优先和深度优先策略对比两种算法(正向展开参考文献[18]).实验所用的用例集 randomtree 随机构
建了 37 个树状结构的 Petri 网,树中每个节点都是类似图 8(d)的循环模型,并随机选择叶节点中的标识进行可覆
盖性判定.规定算法的最大扩展次数为 10 000 次,最大运行时间为 35s.实验结果见表 3.
结果表明:在 randomtree 上,基于深度优先策略的反向展开效果最佳,在全部 37 组用例上,|E|的规模均最优;
同时,无论采用深度优先策略还是广度优先策略,反向展开的效率均优于正向展开.这是因为 randomtree 具备树
状结构.正向展开隐含刻画了系统的完整行为,涵盖了树结构的每个分支.而反向展开仅刻画与可覆盖性判定相
关的系统状态,只涵盖树的一条分支.
4.2 含启发式策略时反向展开与正向展开的对比

本节将对比启发式反向展开与 directed unfolding 在 Petri 网可覆盖性问题上的效率.在实现 directed
unfolding 时,本文采用了文献[17]中的启发式策略 hmax,hsum 以及文献[18]中扩展顺序可以与截断事件的偏序
分离这一性质;在实现反向展开时,本文采用了第 2.3 节中的启发式策略 block,hmax,hsum,并在实现细节上尽可
能保证二者一致.为便于比较,每组实验仅选择 directed unfolding 与反向展开中最优的启发式策略进行对比.相
关实验如下.
(1) randomtree
第 4.1 节中仅对比了无启发式策略下正向展开与反向展开的效率,这里为二者配备启发式技术进行比较.
规定算法的最大扩展次数为 10 000 次,最大运行时间为 35s.实验结果如表 4 与图 10(a)所示.