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

1620 Journal of Software 软件学报 Vol.32, No.6, June 2021

2.3 反向展开算法的启发式优化
扩展顺序对目标标识可覆盖性验证的效率有着关键影响,为此,本文基于实践总结并参考文献[17]提出了 3
种启发式技术:
(1) block 策略.
•
•
在反向扩展 rext=(t,C)中,C 到 t 可以不满足满射关系.然而实践表明:C 到 t 不满足满射时往往意味着 rext
产生得过早,相应的条件还没来得及产生,此时由其引导的扩展都将会是冗余扩展.为了尽可能避免这种情况发
生,将不满足满射关系的 rext 加入阻塞队列,优先选择满足满射关系的反向扩展.仅当所有反向扩展都不满足满
射关系时,才会在阻塞队列中选择一个 rext 激活.实践中,block 策略通常会配合其他启发式策略共同使用.
(2) hmax 策略.
hmax 策略是 Bonet 在文献[17]中提出的一种基于距离的启发式策略.定义 d(M,M′)为标识 M 到 M′间的距离.
i
hmax 将 M 到变迁 t 的距离定义为 max ( dM ,{ })p ,将 M 到库所 p 的距离定义为1min+ ( dM , ),t 如此递推.
p∈ i t t∈ i p
计算 d(M,M′)时,只需求 M 到 M′中每个库所的最大距离,即计算 max p∈M′ d(M,{p}).
上述过程可总结为
⎧ 0, M′ ⊆
⎪ ⎪ M
( dM M′ , ) = 1 min i ( d M t = { } p .
i
, ), M′
+ ⎨
⎪ t∈ p
,{ }), otherwise
⎪ ⎩ max pM ′ ( dM p
∈
(3) hsum 策略.
hsum 与 hmax 十分相似,不同的是:hsum 将 M 到变迁 t 的距离定义为 ∑ ( dM ,{ }),p 与之对应,计算 d(M,M′)
p∈ i t
时,统计 M 到 M′中每个库所的距离总和,即计算 ∑ ( dM ,{ }).p
pM∈ ′
上述过程可总结为
⎧ 0, M′ ⊆
⎪ M
, ), M′
( dM M′ , ) = ⎪ 1 min i ( d M t = { } .
i
p
+ ⎨
⎪ t∈ p
⎪∑ p∈ i t ( dM p
,{ }), otherwise
⎩
hmax 策略与 hsum 策略在使用时会结合配置大小.具体而言:对于两个反向扩展 rext 1 =(t 1 ,C 1 ),rext 2 =(t 2 ,C 2 ),
若有|[rext 1 ]|+d(M 0 ,Mark([rext 1 ]))<|[rext 2 ]|+d(M 0 ,Mark([rext 2 ])),则优先选择 rext 1 进行扩展.
3 基于反向展开的数据竞争检测
由于线程调度的不确定性,多线程程序往往伴随着数据竞争.数据竞争是指在非线程安全的情况下,多个线
程对同一内存地址空间进行访问.数据竞争会影响程序的运行结果,甚至会导致系统崩溃.由于数据竞争通常只
在一些特定的线程轨迹中出现,这给开发人员检测数据竞争带来了极大的挑战.历史上几起严重的事故,如
Therac-25 放射治疗设备事故 [20] 、2003 年北美的大规模停电 [21] 以及纳斯达克的 FaceBook 故障 [22] 都与数据竞
争有关.数据竞争检测主要分为静态检测 [23−25] 与动态检测 [26−28] 两类.本节将基于 Petri 网的反向展开对 Java 并
发程序中的数据竞争进行静态检测.
3.1 程序Petri网模型的构建

Krishna [29] 针对 C-Pthread 程序提出了其同步原语、流程控制语句的 Petri 网模型构建方法.本文将这些建
模方法应用到 Java 并发程序上,主要考虑以下 4 种语句的模型构建.
(1) 线程启动与合并:Java 中,线程 t 的启动与合并分别对应 t.start(⋅),t.join(⋅).调用 t.start(⋅)后,线程 t 的状态
变为 Runnable,在得到 CPU 调度后,变为 Running 状态正式运行.调用 t.join(⋅)后,当前线程的状态变为
Blocked,直到线程 t 执行完毕后才会变为 Runnable 状态,重新等待 CPU 调度.线程的启动与合并对应