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

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

的 Petri 网模型如图 8(a)所示;
(2) 锁的申请与释放:Java 中使用 synchronized 语句实现线程的互斥,包括同步方法和同步代码块,二者本
质上是相同的.当线程 t1 与线程 t2 同时访问同步代码块时,只有一个线程可获取访问权限.锁的申请
与释放对应的 Petri 网模型如图 8(b)所示;
(3) 分支:Java 程序中的分支在逻辑上都等价于 if,if-else 型分支.对应的 Petri 网模型如图 8(c)所示;
(4) 循环:Java 程序中的循环分为 for/while 型循环和 do-while 型循环,二者的结构相似,都由一个控制条件
和一个循环体构成.对应的 Petri 网模型如图 8(d)所示.

(a) 线程的启动与合并 (b) 锁的申请与释放

(c) 程序中的分支 (d) 程序中的循环

Fig.8 Petri net models of Java concurrent programs
图 8 Java 并发程序的 Petri 网模型
图 9 给出了一个 Java 多线程程序的实例以及由上述规则构造所得的程序 Petri 网模型,其中,带星号的变迁
对应程序语句,其余变迁仅用于表达程序结构.具体而言:
(1) 程序语句方面,t1 代表创建线程 t1,t6 代表创建线程 t2,t14 代表将线程 t1 合并到主线程.t7,t8 代表申请
锁 lock,t15,t16 代表释放锁 lock.t9 对应语句 x=2,t10 对应语句 x=1,t11 对应语句 System.out.println(x);
(2) 程序结构方面,t2,t4 代表进入 if 结构,t13,t17 代表退出 if 结构.t3 代表一轮循环的开始,t5 代表一轮循
环的结束,t12 代表退出循环.