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

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

3.2 基于可覆盖性判定的数据竞争检测
程序中关于同一个共享变量的两条读/写或者写/写操作,如果它们在执行顺序上存在先后依赖关系,则不
会产生数据竞争;反之,若他们之间存在并发关系,则会导致数据竞争.由此一来,可以对程序的 Petri 网模型进行
分析,判别两个操作对应的变迁是否在某些状态下具有并发关系.实际上,对于任意的两个变迁 t 和 t′,我们只需
•
•
•
•
要判定是否存在一个可达标识 M,使得 M≥ t+ t′,即判定标识 t+ t′的可覆盖性.

Fig.9 Java source code (left) and its Petri net model (right)
图 9 Java 程序源码(左)与其对应的 Petri 网模型(右)
考虑图 9 所示的例子,其中,读共享变量 System.out.println(x)与写共享变量 x=2 之间未加同一把锁,会发生数
据竞争.共享变量 x 的写操作 x=2 对应变迁 t9,读操作 System.out.println(x)对应变迁 t11,判定数据竞争只需验证
目标标识{p8,p11}的可覆盖性.
程序 Petri 网模型的反向展开流程见表 2.
不难发现,Mark([e9])={ps},故目标标识{p8,p11}是可覆盖的,两个读写操作对应的变迁可以并发,程序存在
潜在的数据竞争.
本节构建了 Java 并发程序的 Petri 网模型,将数据竞争检测转化为验证相关变迁的可覆盖性,并结合实例展
示了反向展开算法在数据竞争检测上的应用.然而,本文仅给出了 Java 多线程程序的 Petri 网建模方法,并没有设
计实际的建模工具.在实际应用中,可以考虑使用 Soot [30] 对 Java 并发程序自动化建模.Soot 是一款 Java 字节码
分析优化框架,可以将 Java 源码转换为 Jimple 中间代码进行分析.比如:可以借助 JInvokeStmt 分析线程的启动
与合并,以及各种函数调用;借助 JEnterMonitorStmt 与 JExitMonitorStmt 分析锁的申请与释放;借助 JIfStmt 与
JGotoStmt 分析程序中的分支与循环.篇幅所限,我们将在后续工作对此展开研究.

4 实验评估

本节将通过实验对比启发式反向展开与 directed unfolding [17] (一种同样采用了启发式技术的正向展开)在
Petri 网可覆盖性问题上的效率.本文将通过事件总数及运行时间评估算法效率.实验所用的基准库包含 415 组