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

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

concurrent programs, and the data race detection problem is converted into the coverability problem of a specific state in 1-safe Petri nets.
The experiment compares the efficiency between forward unfolding and reverse unfolding in the coverability problem of Petri net. The
results show that when the Petri net has more forward branches than backward branches, reverse unfolding is more efficient than forward
unfolding. Finally, the key factors influencing the efficiency of reverse unfolding are analyzed.
Key words: Petri net; coverability determination; reverse unfolding; heuristic optimization; data race detection

Petri 网作为一种分布式并发系统的建模和分析工具,在柔性制造系统 [1,2,] 、业务过程管理系统 [3,4] 、并发程
序形式化验证 [5,6] 等方面得到了广泛使用.然而,状态爆炸问题妨碍了 Petri 网在大规模并发系统分析中的应用.
[7]
[8]
为此,McMillan 首次提出利用网的展开描述系统行为,并通过分支进程 与偏序技术构造展开网的有限完备
前缀,有效缓解了 Petri 网性质分析中的状态爆炸问题,由此受到了研究者们的广泛关注.
[9]
Esparza 等人 指出,McMillan 定义的偏序关系在某些情况下会导致有限完备前缀的规模呈指数级增长,并
针对安全 Petri 网提出了一种全序关系,最小化有限完备前缀的规模.Khomenko 等人 [10] 规范了展开的定义,并对
展开进行参数化配置.Heljanko 等人 [11] 将展开技术并行化,提高了展开的效率.Benito 等人 [12] 将展开技术扩展到
[5]
时间 Petri 网.Schwarick 等人 [13] 将展开技术扩展到于颜色 Petri 网.在 Petri 网展开技术的应用方面,Lu 等人 针
[6]
对网系统的死锁检测提出一种无界 Petri 网的有限展开技术.Xiang 等人 基于展开技术对并发系统中的数据不
一致问题进行检测.Dong 等人 [14] 基于 Petri 网的可达图对 CTL 进行验证.Liu 等人 [15] 借助分支进程技术检测工
作流的健壮性.在 Petri 网的性质分析方面,Chatain 等人 [16] 针对 Petri 网的可覆盖性问题设计了一种目标导向的
展 开技术 , 通过 分析内 部因 果关系 对冗 余变迁 进行 剪枝 .Bonet 等人 [17] 结合 启发式 技术 提出了 一 种
semi-adequate ordering,提升了展开技术在 Petri 网可覆盖性分析上的效率,并在后续的论文 [18] 中证明扩展顺序
可以与截断事件的偏序分离,拓宽了启发式展开技术在 Petri 网性质分析中的应用.
网的展开通过分支进程与偏序技术可在一定程度上缓解 Petri 网性质分析中的状态爆炸问题.但展开网中
仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态标识的可覆盖性进行判定,以此为目标有
望对网系统的展开进行化简.为此,本文针对安全 Petri 网的可覆盖性判定问题提出了一种目标导向的反向展开
算法.反向展开从需要做出可覆盖性判定的目标标识出发,仅刻画与可覆盖性判定相关的系统状态,并结合启发
式技术缩减展开的规模,以此提高目标标识可覆盖判定的效率.进而,将反向展开算法应用于并发程序的形式化
验证,将并发程序的数据竞争检测问题转换为 Petri 网特定标识的可覆盖性判定问题.实验对比了启发式反向展
开与 directed unfolding [17] (一种同样采用了启发式技术的正向展开)在 Petri 网可覆盖性问题上的效率,结果表
明:在 415 组测试数据中,反向展开的规模在 85 组数据上优于 directed unfolding,在 26 组数据上与 directed
unfolding 持平.最后,本文对影响反向展开效率的关键因素做了分析与总结.
本文第 1 节围绕 Petri 网的可覆盖性判定问题,分别分析正向展开与反向展开的适用场景,并结合实例说明
反向展开相比正向展开的优势.第 2 节介绍 Petri 网的反向展开算法,包括相关概念的形式化定义、算法流程以
及启发式优化策略.第 3 节将反向展开应用于并发程序的数据竞争检测.第 4 节结合实验评估正向展开与反向
展开在 Petri 网可覆盖性判定问题上的效率.第 5 节对本文所做的工作进行总结与展望.

1 实例与动机分析

本节首先在 Petri 网的可覆盖性判定问题上分别论述正向展开与反向展开的适用场景.之后,将通过一个实
例说明反向展开相比正向展开的优势.
先来看两个简单的例子.图 1(a)中 Petri 网的初始标识为{ps},需验证目标标识{pt}的可覆盖性.为了便于表
述,将图 1(a)左侧的路径称为 path1,右侧的路径称为 path2.在这个例子中,正向展开从初始标识{ps}出发,难以在
path1 与 path2 间做出选择,若不慎选择了 path2,将会做很多冗余的扩展.与正向展开不同,反向展开从目标标识
{pt}出发,仅需要沿着 path1 反向扩展,很容易找到与初始标识{ps}间的可达路径.
图 1(b)可以看作图 1(a)的“倒置”.在这个例子中,反向展开从目标标识{pt}出发,难以在 path1 与 path2 间做
出选择.而正向展开从初始标识{ps}出发,很容易沿着 path1 到达目标标识{pt}.