并发程序验证的Petri网方法

1、第九章 并发程序验证的Petri网方法9.1 引言由于并发程序所具有的并发特性，使得程序语义具有不确定性，从而使并行程序正确性验证研究较顺序程序要困难得多，因此，相关的程序规范、设计、分析与验证方法业已成为计算机理论界研究的重点与热点问题之一。近年来，许多学者利用并发分析工具Petri网对并发程序进行建模和分析1，特别是对于Ada任务程序的构造与分析23。其中，基于可达性的分析方法受到了广泛的关注，原因有三：（1）Petri网的动态性质与并发程序的性质具有相似性，如：死锁、活性等，而利用Petri网的可达图，可以很好的分析这些性质。（2）Petri网串语言的顺序语义与我们讨论并发程序所假设的语

2、义都是交错语义，即“事件并行发生的效果和以任一顺序串行发生的效果一样”，这使得基于可达性的分析方法在描述并发程序时不会改变原程序的语义，而且基于可达性的分析方法由于实际上是给出了系统的运行轨迹和各可达状态，因此，它可以支持系统多种性质的分析验证，包括安全性和活性（与Petri网的安全性和活性不同）。（3）基于可达性的分析手段很容易结合其他分析方法，如时序逻辑、进程代数等，提供更为有效的分析和验证方法。然而，不幸的是基于可达性的分析方法受到了状态爆炸的限制，已经证明，Ada任务程序的可达状态随任务的数目而成指数增长，这就造成了我们利用可达性分析手段进行分析与验证的困难。为了解决状态爆炸问题，一些

3、用于改善基于可达性分析方法的复杂性理论已经提出。4利用网化简理论，删除或结合一些不必要的库所或变迁，仅保留反映程序性质的重要库所和变迁，从而减少可达状态的数目，5着重讨论程序中的并发部分，而避免探讨全部状态，从而降低了分析的复杂性。6通过网分解理论，将较复杂的网系统通过分解，拆分成若干子网，分别加以讨论，最终得到原网系统的性质。7则结合上述各种方法，进行网化简，并认为各种方法的结合使用能够更有效的降低分析复杂性。8对上述网化简方法进行了总结及评估，并给出了相关的测试数据。在文6中，借助同步合成运算，将一个复杂的Ada网分解成若干个易于分析的子网，然后构造了分层可达图HRG：具有根节点（原网可达

4、图）、若干叶子节点（经过化简后的子网可达图）及其它非叶子节点（合成运算）的树状结构。可以完整表示原网可达图 与子网可达图的构造关系，并利用分层可达图HRG进行了可达性分析和死锁检测。下面借鉴上述思想，利用Petri网的同步合成运算，将一个复杂的Ada网分解成若干个易于分析的子网，并利用子网可达图及同步合成运算的性质，求出原Ada网的可达图。并据此求出网语言，再通过其对程序性质进行分析。显然，求解网语言与求解可达图是等价的，但二者的内涵不同，状态图侧重于表述系统的运行效果，而网语言则反映了系统的运行轨迹，刻画了系统的行为动作，更有利于描述系统的动态行为。这对于分析并发程序性质是有帮助的。另外，利

5、用网语言分析程序性质的工作鲜见论述，本文期盼在这方面能够做出一些有益的探索。9.2 同步合成运算的概念及性质近年来，组合化的设计思想日益得到人们的重视，尤其是对复杂系统的设计与分析，更能体现这一思想的重要性。文12-14引入了同步合成运算，并研究了同步合成运算对Petri网的动态不变性，深入探讨了同步合成的动态性质：行为不变性和行为相关性，并应用于实际系统的分析与设计中。文27对PVM程序进行建模，并利用同步合成运算，通过子程序耦合出大的程序，并分析其相关性质。在前面的章节中，仅讨论了两个网的同步合成运算，而对于复杂的系统，往往需要多个网的同步合成运算。这里，我们将推广至n个子网的同步合成运算

6、。定义9.1 n-同步合成 设Ni=(Pi,Ti;Fi),i=1,2, ,n是n个网，N=(P,T;F)为网N1,N2, ,Nn的n-同步合成网，当且仅当（1）P=P1P2 Pn,i,j,ij,PiPj=;（2）T=T1T2 Tn,i,至少存在一个j.，ij,有TiTj;（3）F=F1F2 Fn。设M0i是网Ni的初始标识，相应的Petri网记为PNi=(Ni,M0i),i=1,2,.,n。若M0(p)=M0i(p),pPi，则称PN=(N,M0)为n-同步合成Petri网。定义9.2（R-图） 一个R-图是一五元组(V,E,T,L,v0)，其中，(V,E)是一带标号的有限有向图，v0为根节点

7、，有向图的每一条边用变迁集合中的元素作为标号，映射L:ET。显然，Petri网的可达图是一个R-图。若干个R-图可以合并为一个R-图。定义9.3（G-合并） 设RG1,RG2, ,RGn是n个R-图，其中RGi=(Vi,Ei,Ti,Li,v0i)，i=1, ,n，则n个R-图RG1,RG2, ,RGn的G-合并（RG1,RG2, ,RGn）仍然是一个R-图RG=(V,E,T,L,v0)，其中，V,E,T,L,v0分别定义如下：1）VV1V2 Vn. 2）T=T1T2 Tn. 3）v0=(v01,v02, ,v0n) 4）V,E,L递归定义如下： a) v0V.', ,vn')V

8、1V2 Vn.若存在v=(v1,v2, ,vn)V，且存b)对于(v1',v2在tT1T2 Tn,使得对任意的i1,2, ,n,(vi,vi'),有Li(vi,vi')=t,或', ,vn')V,(v,v')E,L(v,v')=t。 者(tTi)(vi=vi')，那么，v'=(v1',v2c) V,E,L不含除a)、b)所得的其他任意元素。例9.1 设RGi=(Vi,Ei,Ti,Li,v0i),i=1,2是两个R-图（见图9.1（1）, 图9.1（2），其中t0T1T2,则其G-合并（RG1,RG2, ,RGn）是

9、一个R-图RG=(V,E,T,L,v0)（见图9.1（3）。图9.1显然，上述定义及例9.1所采取的“分而治之”策略可以有效的降低求解可达图的复杂性，在这里我们正是利用上述方法求解Ada网的可达图的。对于n-同步合成Petri网的性质及语言，总可以通过两个子网的同步合成运算逐步迭代得出。下面，我们将刻画n-同步合成Petri网的语言性质，同时，通过该定理的证明展示如何利用两个子网的同步合成运算迭代得到n-同步合成Petri网性质的。定理9.1设PNi=(Pi,Ti;Fi,M0i),i=1,2, ,n是n个Petri网，则n-同步合成Petri网=(P,T;F,M0)的语言有L(PN)=T1T(

10、L(PN1)T2T(L(PN2) TnT(L(PNn)。-1-1-1证明 利用归纳法证明。-11 设n=2时，有定理3.4知，L(PN)=T-1(L(PN)(L(PN2)，即归1TTT2212纳基础成立。2 假设n=k时，结论成立，即设PNi=(Si,Ti;Fi,M0i),i=1,2,.,k是k个Petri网，则k-同步合成Petri网PNTk=(Sk,Tk;Fk,M0k)的语言有L(PNT)=TTk(L(PN1)T1n-1-12Tk(L(PN2) T-1kTk(L(PNk)下面需要证明n=k+1时，结论成立。根据假设知k-同步合成Petri网PNTk的语言为L(PNTk)，k+1子网语言是L

11、(PNk+1)，则利用定理3.4知，k+1-同步合成Petri网PNTk+1的语言为L(PNTk+1)=T-1Tkk+1(L(PNT)Tk-1k+1Tk+1(L(PNk+1)-1k=T-1Tkk+1(TTk(L(PN1)T1k+1-1-12Tk(L(PN2) TTk(L(PNk)T-1=T-1T1k+1T(L(PNk+1)-12k+1(L(PN1)Tk+1Tk+1(L(PN2) T-1kTk+1(L(PNk)T-1k+1T(L(PNk+1)即n=k+1时，结论成立。 综合1，2，结论得证。9.3 Ada程序的Petri网模型文1定义了Ada网，所谓Ada网，即指利用一系列转换规则将Ada任务程

12、序转换成的Petri网模型。一个Ada网模型模拟了若干个通信有限状态自动机。Ada任务中的通信是建立在汇聚机制之上的，每个状态表示一个任务的局部控制流，而通讯的交互过程则通过连接不同状态机的节点来表示。同时， if-else、case和loop等控制流结构也用网结构加以模拟并反映其对通信的影响。产生Ada网的转换规则主要是一系列对应Ada任务程序语句的Petri网模板，关于转换的细节，请参阅文1-3。这里仅介绍其中的通讯部分的转换规则，而对于Ada网的同步合成运算也正是基于该转换规则。图9.2（1）是一个Ada任务入口请求的Petri网模板，表示一个请求者执行entry语句调用的过程，根据入口

13、调用语句的语义知，其执行结果为本进程挂起，等待服务者的响应，以完成汇聚。图9.2（2）是一个Ada任务接受语句的Petri网模板，描述了服务者执行accept语句的过程，在服务者执行到自己的接受语句时，若请求者还没有发出对应的入口调用，那么，服务者任务挂起，等待入口调用的发出。图9.2（3）则反映了Ada任务的汇聚机制：一个任务中的入口请求语句与另一任务中的接受语句共同完成。从图9.2中可以看出，Ada任务程序的汇聚机制是通过外部库所ack-entry、entry-ex、ack-accept和变迁accept、accept-done，在两个任务之间进行通讯而实现的。其中，变迁accept、ac

14、cept-done其到了同步的作用，准确的表达了Ada程序汇聚机制的语义。我们对Ada网进行的同步合成运算，也正是将这两个变迁作为共享变迁进行操作的。 图9.2下面，我们就对文4, 7-8中所引用的自动加油站问题进行Ada网模型建模，其源程序及Ada网模型（图9.3）如下：例9.2 自动加油站问题1 task body Customer is 10 task body Pump is 20 task body Operator is 2 begin 11 begin 21 begin3 loop 12 loop 22 loop4 Operator.Prepay; 13 accept Activ

15、ate; 23 select 5 Pump.Start;6 Pump.Finish;7 accept Change;8 end loop9 end Customer14 accept Start; 15 accept Finish do 16 Operator.Charge; 17 end Finish 18 end loop 24 accept Prepay do 25 Pump.Activate; 26 end Prepay; 27 or 28 accept Charge do 29 Customer.Charge; 30 end Charge; 31 end select; 32 end

16、 loop;图9.3 源程序的Ada网模型研究Ada网本身的特性，可以更好地把握并发程序的性质，并简化网分析的复杂性，在文献1-4中均有讨论，归纳起来，其性质有如下几条：1. Ada网是安全的Petri网。2. Ada网中对应着程序语句的节点（库所和变迁）至多为线性数量个。 3. Ada网的初始标识仅在表示任务开始的库所中含有托肯。 4. if、 case等确定性语句，在网结构中表现为分支结构。5. 任务内部局部控制流中的确定性语句，若不含通讯语句，则不反映在Ada网中。 综上所述，在Ada任务程序中，任务内部的局部控制流实际上对应着一段顺序程序，其性质的分析和验证可用传统的顺序程序分析方法进

17、行解决。而Ada任务程序执行语义的不确定性，是由于多个进程的并发执行和任务间的消息传递的不确定性引起的。通过后继章节的讨论将知道：汇聚机制的同步起到了关键作用，反映在Ada网中，即相关的同步变迁accept、accept-done。9.4 Ada网的同步合成运算及其可达图求解图9.4（1）和图9.4（2）是对图9.2（3）进行同步合成运算所得到的两个子网。图 9.4事实上，通过同步合成运算，我们将通讯部分分解为隶属于两个子网（任务）的顺序流，因此，利用同步合成运算进行网分解后所得到的各个子网，分别对应着源程序中的各个任务。这样，通过独立地考察各个子网的可达图和性质，也即对各个任务的局部控制流进

18、行分析，考察相关性质，然后再利用同步合成运算的性质，对原Ada网进行分析。图9.5就是对图9.3所描绘的Ada网模型进行同步合成运算后所得的三个子网模型。图9.6所表示的就是三个子网的可达图，其中，我们进行了简单的化简，即将可达图上的连通分支（不包含共享变迁）约简为一个节点和一条边，很明显，这种化简不会改变原网的语言，但可以有效的缩减可达状态，进一步降低求解可达图的复杂性。具体示例参见图9.6。图9.6根据图9.6的三个子图，利用定义9.4及例9.1所叙述的方法，我们可以求出原Ada网的可达图来（见图9.7）。网语言中的每一元素在可达图RG(PN)中表现为从初始标识M0起始的有向路上所对应的变

19、迁引发序列。基于这点，我们能够利用表达式MiMj表示存在有向路径由Mi至Mj，其中路径上标号为。由此，我们可以借用类似自动机产生语言的方法推导出网语言的形式来。推导过程为:M=s1M1+s5s1M2+(s5s4s1+s4(s1s5+s5s1)t23M4M1=s5M2+s4s5t23M4综合（1）、（2）式，有M=(s1s5+s5s1)M2+(s5s4s1+s1s4s5+s4(s1s5+s5s1)t23M4又因为M2=t23M3+s4t23M4M3=s4M4+t24s4M5M4=t24M5结合（3）及上述各式，得到MM=(s1s5+s5s1)t23s4t24+(s1s5+s5s1)s4+s5s4

20、s1+s1s4s5+s4(s1s5+s5s1)t23t24M=(s1s5+s5s1)s4+s5s4s1+s1s4s5+s4(s1s5+s5s1)t23t24M5 +(s1s5+s5s1)t23s4t24M5=(s1s5)t23s4t24+(s1s4s5)t23t24)M5，5同理，可知M5=t13t25t26(s2s6)M10M10=(t14s5)M12 M12=s3t15t16t28t29M17综合上式，得M=(s1s5)t23s4t24+(s1s4s5)t23t24) t13t25t26(s2s6)(t14s5)s3t15t16t28t29M17将si用相应的变迁序列代替，我们就可得到M=

21、(t1t2t3t20t21)t23t11t12t24+(t1t2t3t11t12t20t21)t23t24) t13t25t26(t4t5t32t33)(t14t20t21)t6t7t15t16t28t29M17由此，我们可以得到原Ada网语言。定理9.2 设Ada网PN=(S,T;F,M0)，如图9.4所示。其中M0(S')=1并且对任意的sS'，有M0(s)=0，S'=begin-2-Customer,begin-11-Pump,begin-21-Operator,则网语言L(PN)为：L(PN)=(t1t2t3t20t21)t23t11t12t24+(t1t2t3

22、t11t12t20t21)t23t24)t13t25t26(t4t5t32t33)(t14t20t21)t6t7t15t16t28t29以上，我们通过网的同步合成运算和子网可达图化简方法，有效地缩减可达状态，降低求解原网可达图的复杂性，并根据原网可达图形式化地得到了原网语言。下面，将利用网语言分析和验证系统性质。9.5 基于Petri网语言的Ada程序分析正如我们所熟知的，网语言能够准确刻划实际系统的动态行为，模拟系统的动作，给出了一个网的语言，也就等于得到了实际系统的运行轨迹，从而可以有效的分析系统性质。目前，较多采用的分析方法是利用网的可达图进行系统分析，但由于其侧重的是描述系统的可达状态

23、，因此，无法直接利用其分析系统的动态性质，特别是系统的活性性质（不同于Petri网的活性），所以，现在利用可达图分析并发程序的性质，主要集中于程序的死锁分析。但较少涉及程序的活性性质。这一节利用网语言不仅可以有效的分析死锁等的安全性质，同时，可利用其分析程序的活性性质。9.5.1 Ada程序的安全性所谓安全性，是指某些状态永远不能发生，即，程序永远不能进入不期望进入的状态。程序的安全性是第一位的，它关心的是可能性问题，要求所有可能的状态均满足一定的性质。在安全的前提下才能讨论活性。定义9.511 若一个Ada任务程序成为静态可执行的，当切仅当其对应的Ada网是弱活的。满足定义9.5的程序总会执

24、行某些语句，而不会停止下来，这就避免了死锁的发生。因此，程序的静态可执行性质属于安全性的范畴，当然，这也并不能保证所有的语句都能被执行，即程序仅反复执行某一部分语句，而无法得到进展，这也就是所谓的活锁。这将在后面叙述。在第三章中讨论了基于Petri网语言的活性刻画。下面我们应用有关结果讨论程序静态可执行性质的判据。根据定理3.1，则有下面结论：定理9.3 设Ada任务程序所对应的Ada网PN=(S,T;F,M0)，其中，M0(S')=1并且对任意的sS'，有M0(s)=0，则Ada任务程序是静态可执行的充分必要条件是L(PN)=spref(L(PN)。当然，程序的静态可执行性质

25、条件要比程序的无死锁性强的多，一个正常终止的程序是不满足静态可执行性质的。因此，有必要讨论程序发生死锁的条件，便于我们分析程序的性质。这里需要强调的事，任何并发程序与顺序程序一样，都是单出口的，只是由于对于实时相应程序，如上面所提的自动加油站问题，终止性不具备任何意义，才在建模中没有描述单出口语句，这并不代表其不是单出口的。同时，在Ada网语义中，变迁描述了语句的运行，因此，我们有下述定理。定理9.4 设Ada任务程序所对应的Ada网PN=(S,T;F,M0)，其中，M0(S')=1并且对任意的sS'，有M0(s)=0，则Ada任务程序发生死锁的充分必要条件是：其中，='

26、;' t'，有 'L(PN)，并且若tend，有tteL(PN)，nd，tend表示单出口语句。证明 结论是显然的，='' t'，有 'L(PN)，并且若tend，有ttend，表明程序执行有限步后，非正常的终止下来，即发生死锁。反之亦然。定理9.2所描述的语言满足定理9.4的条件，即该语言中的元素（变迁序列）均为有限长度，利用定理9.4，易见例9.2的Ada任务程序发生了死锁。基于定理9.4，Ada任务程序的死锁分析算法描述如下：算法9.1 死锁分析输入：L(PN)，并且'，有 'L(PN)输出：若是发生死锁的序列，则输

27、出False，否则，输出True。（1） begin（2） while（3） 读入的一个字符t（4） if t=tend then 程序执行了单出口语句，正常终止（5） 输出True；并跳出循环。（6） elseif t为空字符 then 程序执行了有限步后，非正常终止，即发生死锁（7） 输出False，并跳出循环。（8） endif（9） enddo（10） endbegin利用可达图的分析方法一般是利用发生死锁时的可达标识，判断程序发生死锁时的执行情况，由于可达标识是各库所所含托肯的向量集，因此，判断起来稍嫌繁琐。这里，我们直接利用网语言及其同步合成运算性质进行判断，仅需找出发生死锁的变迁

28、发生序列中分属各个子网变迁集合中顺序运行的最后一个变迁，就能了解程序发生死锁时的运行状态。对于例9.2，根据定理9.2，可以知道变迁t7,t16,t29是分属各个子网变迁集合中顺序运行的最后一个变迁，即网执行了上述变迁后，进入死锁状态。根据Ada网的语义，易知此时任务Customer执行了Pump.Finish语句（加油完毕），等待响应，而任务Pump为了接受Finish调用，需要执行Operator.Charge语句（要求柜员机找零），同样，任务Operator为了接受Charge调用, 需要执行Customer.Charge语句（要求顾客能够接受找零），而若接受该调用，则需执行任务Cust

29、omer的接收语句，但其在Pump.Finish语句的后面，因此，程序发生了死锁。无法进展。安全性虽然是第一位的，但这只是一种保障，而一个系统总是具有一定功能，解决一定问题的，一般地，这些是属于活性的范畴。对于并发程序，也不例外。9.5.2 活性所谓活性，是指某些好的状态最终会进入，即，程序最终能进入期望中的状态。对于顺序程序而言，程序终止性和完全正确性是较多被讨论的活性性质。然而，在并发程序中，活性的内涵拓宽了，包括：（1）每一个服务请求都最终得到响应。（2）一个消息最终能达到其目的地。（3）一个进程最终会进入临界区。定义9.611 一个Ada任务程序是并发正确的，当且仅当其对应的Ada网是

30、活的。 基于定理3.2，则有下面结论：M0(S')=1定理9.5 设Ada任务程序所对应的Ada网PN=(S,T;F,M0)，其中，并且对任意的sS'，有M0(s)=0，则Ada任务程序是并发正确的充分必要条件是L(PN)=stpref(L(PN)。程序的活锁一直是并发程序研究的重点和难点，并发正确性对应着程序无活锁性和响应性等重要性质。所谓无活锁性：即各进程不会进入循环等待状态： 仅仅执行程序局部一些无意义的指令，而无法实现进展性。定理9.6 设Ada任务程序所对应的Ada网PN=(S,T;F,M0)，其中，M0(S')=1并且对任意的sS'，有M0(s)=0

31、，则Ada任务程序发生活锁的充分必要条件是L(PN)，其中，= * tT,使得t&()'，有 'L(PN)。证明 结论是显然的，L(PN)，其中，= *tT,使得进入局部循环，并且无t&()'，有 'L(PN)表明程序在执行有限步后，法跳转出来。执行后继语句。即进入活锁。反之亦然。基于定理9.6，Ada任务程序的活锁分析算法描述如下：算法9.2 活锁分析输入：L(PN)，并且'，有 'L(PN)输出：若是发生活锁的序列，则输出False，否则，输出True。（1） begin（2） if 中不存在如的子串 then 程序序列无循环

32、，故不会发生活锁（3） 输出True。（4） else（5） for i =1 to Length() do（6） 读入的一个字符t（7） if tT then T=T-t；从变迁集中去掉元素t（8） endfor（9） if T then 变迁集T不为空，即，程序在局部循环中有未执行的语句， 故存在局部死循环(10) 输出False(11) else 变迁集T为空，即，程序在局部循环中执行了全部语句，为正常循环(12) 输出True(13) endif(14) endif(15) endbegin本节首先利用网的同步合成运算，求解Ada网的可达图，并在保证语言不变的前提下，对子网可达图进行了

33、化简，通过采用上述方法，有效降低了求解可达图的算法复杂性。并保证了语言的不变性。其次，借用自动机作为语言产生器的方法，我们通过可达图形式化地产生了网语言。最终利用网语言分析了Ada任务程序的安全性和活性性质，给出了判断程序死锁和活锁的语言判据，定义了静态可执行性和并发正确性两个重要的反映程序特性的概念，并给出了其语言判据。事实上，网语言作为描述网动态性质的重要工具，反映了系统的运行轨迹，刻画了系统的行为动作，更有利于描述系统的动态行为。特别地，网语言的语义和并发程序的语义是相同的，因此，可以准确的表述并发程序的动态行为，适于反映和分析系统的动态性质。但这方面的研究一直未能开展起来。本节在网语言

34、的求解和利用网语言分析并发程序的性质方面进行了有益的探索，体现了网语言的独特优势。9.6 PVM程序的Petri网模型前面，我们讨论了Ada程序的验证与分析方法，接下来我们将在PVM并行环境下，用户经常出错的现象抽取为Petri网特征，并对此给出检验算法，帮助用户消除这些错误。对于PVM环境下，基于子进程(选出几种典型语句及常用通讯库函数为例)我们建立相应的Petri网模型如下：(1) 条件判断if . then . else . (2) 循环一 for (i=0; i<n; i+) =循环二(3) while . =(4) 与通讯无关的计算语句块 =(5) 发送消息 =(6) 接收消息

35、 =或 或(7) 广播消息 =(8) 障碍同步 =(9) 开始子进程 = .图9.8 PVM环境下基本子进程的Petri网模型9.7 PVM程序到Petri网模型的转换这一节中，我们除了讨论利用Petri网结构验证一些静态特性外，还将讨论利用可达图验证重要的动态性质。为保证可达图不至太大而难以进行，我们期望用安全Petri网作为验证模型，这一点在一定程度上是能够做到的。下面来说明这一点。应该说，真实地反映应该PVM程序可能是一个带抑制弧的无界Petri，如下面的程序段：read(n,m); if (me=0) for (i=0, i<n, i+) send(.) else for (j=

36、0, j<m, j+) recv(.) 图9.9 PN1它都有的Petri网PN1如图9.9所示，显然这是一个带抑制弧的无界Petri网，用它的覆盖图很难, 甚至不能分析相应的死锁, 活锁等现象。实际上，我们对此网进行适当地 处理，便可方便地进行抑制。我们抑制的目的主要是看该程序段是否含有潜在的死锁或活锁，为此，将此网改造为如图9.10所示的安全网PN2。图9.10 PN2（1）PN1中引发变迁还是或还是是受n(或m)控制的，而n(或m)是变量，它随读入多少而变化。图9.10中的2，引发还是或是是不确定的。可以认为2是反映着PN1中n, m可变的情况下，该程序段的固有特征，也就是说PN1

37、中n, m给定不合理会导致死锁(如m>n时)，或者说PN1潜在地存在死锁，而PN2正反映着存在死锁。（2）PN1 中引发分次数不少于引发次数，PN2引引发一次交替进行。这种限制不影响死锁的存在性。直观地理解，PN2反映着PN1的固有逻辑特征。而分析PN2比分析PN1要容易得多。进一步地，将PN2转化为相应的闭网PN3(如图9.11)。图 9.11 PN3PN3显然是一个安全网。尽管一般Petri网的可达图是指数规模，但对于安全网，实际规模要小得多，通常是可以容忍的，而且不会遗漏原网的死锁特征。这就是我们为什么要改造为安全网的缘故。下面我们给出具体的建模步骤：Step1. 确定总的进程个数

38、，对每个进程按基本子进程(语句或库函数)的顺序序列依次对于地写相应的进程Petri网；Step2. 都有进程之间的特性，按照相应的对于关系连接握手位置。如：进程i中send 发送消息给进程j中recvx接收，则操作如下：1 2: : : :=图 9.12Step3. 若得到的Petri网模型不是安全网，则做适当地改造。原则是：当send,recv 嵌入在各自的循环体中，则添加互补位置，将受控网改造为相应的安全网； Step4. 添加“空操作”，每一进程的出口位置到有一条有向弧(注：对于每一个条件判断语句的两出口位置，将其合并成一个位置。)；Step5. 将网中的位置统一编号为：p1 , p2

39、, . , pm，将网中的变迁统一编号为：t1 , t2 , . , tn。这样得到的Petri网PN = (P, T; F, M0)正是我们要原则的模型。根据PVM程序中经常出错的现象及在相应Petri网中的表现，我们给出如下结论，在此之前需要引入一个概念。定义9.7 设G = (V, E)是一有向图，Gs = (Vs, Es)是G的子图，Vs 且Vs V。若 vVs, vV-Vs，使得(v,v)E，则称Gs的出度为0，记作：degout (Gs) = 0。特别地当Vs=v时，记作：degout (v) = 0。根据PVM程序的异常现象与Petri网模型的关系，我们有如下结论：结论一. 通讯

40、中出现孤儿消息当且仅当相应的Petri网模型PN = (P, T; F, M0)中存在位置pP,使得p = ；(注：p =t | (tT) (p,t)F)。结论二. 通讯中出现缺发消息当且仅当相应的Petri网模型PN = (P, T; F, M0)中存在位置pP, 使得p = ；(注：p = t | (tT) (t,p)F)。结论三. 通讯中出现发送消息与接收消息的逻辑关系不匹配而处于无限等待当且仅当, 相应的Petri网模型PN = (P, T; F, M0)中存在死锁，当且仅当PN的可达图RMG()=(V, E, f)中存在MV，使得degout (M) = 0。结论四. 通讯中出现消息

41、循环等待，当且仅当相应的Petri网模型PN = (P, T; F, M0)中存在活锁，当且仅当PN的可达图RMG(PN)=(V, E, f)中存在强连通分支RMG(PNs)=(Vs, Es, f s)，使得degout (RMG(PNs) = 0且fs(Es) = f (Es) T。结论五. s 由RMG(PNs)唯一确定。9.8 PVM程序验证算法基于前面的结论，我们分别给出检验算法如下：算法 9.3 检验孤儿信息和缺发消息输入: P(T), (T)P /* P(T)是以p为表头结点存储(p,t)弧的邻接链表, (T)P是以p为表头结点存储(t,p)弧的邻接链表 */输出: SS, SR

42、/* SS为孤儿信息源集合，SR缺发消息源集合。*/for (i=0, i<m, i+) /* m为P集合中元素的个数 */if (P(T)i = “NIL”) /* pi = */Q(T)Pi; /* Q为指针，将(T)P表中第i个表头结点放到Q中。*/while (Q<>NIL) DOSSSSQ.data;QQ.linkfor (i=0, i<m, i+)if (T)Pi = “NIL”) /* pi = */QP(T)i; /* Q为指针，将P(T)表中第i个表头结点放到Q中。*/while (Q<>NIL) DOSRSRQ.data;QQ.link算

43、法9.4 求RMG(PN)和死锁集合输入: PN, A /*A是Petri网PN的关联矩阵 */输出: RMG(PN), SD /* RMG(PN)=(V,E,f)为Petri网PN的可达图，SD为死锁集合 */ VM0, E, b(M0)0, SD; /* b是标号函数 */10: if (MV: b(M)=1)结束else取MV且b(M)0;求EN(M)T, 使得tEN(M): Mt >if (EN(M)=)SDSDM;b(M)1else20: 取tEN(M);EN(M)EN(M)-t;求M，使得Mt >Mif (MV)VVM;b(M)0EE(M,M);f(M,M)“t”;if

44、 (EN(M)=)b(M)1;goto 10else goto 20算法9.5 求活锁集合输入: RMG(PN).输出: SL /* SL为PN的活锁集合 */ SL;for (V中每个结点M)N(M)0, b(M)0;N1;while (存在一个编号为0的结点M) N(M)N;NN+1;L(M)N(M);M进栈S；10: while (有一条未处理的边(top,M)关联于top) if (N(M)=0) /* M还不在这棵树中 */N(M)N;NN+1;L(M)N(M)M进栈Selseif (b(M)=0) /* M还未处理 */L(top)minL(top), N(M)if (L(top)

45、=N(top) /* 找到了一个强连通分支 */ b(top)1;M0stop;Vstop;while (SC栈顶的结点M: N(M)>N(top) b(M)1;VsVs M;退栈SCM0s进栈SSM0s进行标记;while (SS)while (有一个邻接于top而未标记的Vs中的结点M) Es Es (top, M);Ts Ts f(top, M);对M进行标记;M进入栈SS中退栈SSif (Vs>1且degout(Vs)=0且TsT) SLSL(M0s,Vs,Es,fs) /* fs为在Es上的投影函数 */else将top推进栈SC中栈顶的M”S上第二个结点; /* 从to

46、p起 */ L(M”)minL(M”), L(top)退栈S; /*从top返回到M”, 即新的top */ if (S)goto 10算法9.6(求活锁子网集)输入: SL.输出: S(PNs). /* S(PNs)为活锁子网集 */* 对每个RMG(PNs), 用邻接链表存储，每个链结点含有data, flag, link三个域。其中data为结点标号，flag为弧上旁标域，link为指针域。*/ while (SL)取RMG(PNs)SL;SLSL-RMG(PNs);for (k=0, k<x-1, i+)Pvk;while (P)vP.data;MMv - Mvk;tp.flag

47、;TsTs t;for (i=0, i<n, i+)if (M(i)>0)Ps Ps ps;Fs Fs (t,ps)elseif (M(i)<0)Ps Ps ps;Fs Fs (ps,t)P P.linkS(PNs)S(PNs)(Ps,Ts;Fs,M0s).9.9 举例说明下面程序段的Petri网模型如图9.13所示，它的可达状态图如图9.14所示。从图9.14中容易看出存在两个死锁状态p6, p9, p12, p14h p6, p10，而且从初始状态到p6, p9, p12, p14的任何路径上的旁标均含有t3。这说明4中2里的token无论引发t2(即条件成立CT)还是引

48、发t3(即条件不成立CF)，都将导致死锁状态。也就是说条件语句中无论条件真假都将出现死锁，故此出现有错。.if (me=0) read(x) if (x>0) send1(.)else recv2(.)send3(.) else Ssend2(.) recv3(.) recv1(.) 图 9.13 PN4.p1,pt1 7 2,p7 p1,p8t2 t3 t1 ,p7 4,p7 p2,p8 p19,p12 7 2 t3 1 p6,p7,p14 p3,p8 p4,p8 p2,p9,p12 7 8 t3 p612 p4,p912 t5 p5,p9 t6图9.14 RMG(PN4)将上述程序修

49、改为图9.15所示，它对于的Petri网模型为PN5，PN5的可达图如图9.16所示。不难看出RMG(PN5)中有一死锁状态p6, p9, p12，从p1 ,p7到p6, p9, p12的任何路径的旁标中均含t2，不含t3，这说明PN5中p2里的token引发t2(条件成立时)必将导致死锁，引发t3(条件不成立时)将不会出现死锁。也就是说，在改正后的出现中，只要我们的条件控制得当(使得条件不成立)就不会死锁，条件控制不当(使得条件成立)必将出现死锁。.if (me=0) read(x) if (x>0) send1(.) recv2(.) send3(.) else S send2(.)

50、recv3(.) recv1(.) .图9.15 PN5p4 5913691314610136,p11 t6 t9 t10图9.16 RMG(PN5)在这一节中，我们基于Petri网，针对PVM出现中孤儿信息，缺发信息，死(活)锁现象，给出相应的验证方法，所得结果为PVM程序的正确设计与调试起到指导作用。 9.10 本章小结在这一章中，我们基于前面讨论的Petri网行为分析理论，探讨了并行程序验证问题。首先介绍了Ada程序的Petri网模型，Ada程序的安全性与活性含义以及Petri网语言刻划，基于Petri网语言的行为分析理论给出了安全性与活性（注意：这里的安全性与活性不同于Petri网中安

51、全性与活性的含义）问题的验证分析算法，并通过一些例子说明了验证分析过程。接着，讨论了PVM并行环境下，程序的Petri网模型，以及几种异常现象（死锁性、活锁性、孤儿消息和缺发消息）的Petri网描述，基于Petri网可达图提出这些异常现象的验证分析方法，最后通过例子说明了验证分析过程。应该说Petri网的行为分析方法对于验证分析并行程序的动态行为机理十分重要，将为并行处理提供一种理论分析工具。进一步可研究的工作应该是探讨更为实用和有效的行为分析算法。参考文献1 S.M.shatz W.K.cheng “A Petri Net Framework for Automated Static Ana

52、lysis of Ada TaskBehavior” J.Syst.Software. vol 8.1988: 343-359.2 T.Murata B.Shenker S.M.Shatz “Detection of Ada Static Deadlocks Using Petri NetInvariants” IEEE Transactions on Software Engineering. vol.15 , no 3.1989: 314-326.3 S.M.Shatz K.Mai C.Black and S.Tu “design and Implementation of a Petri

53、 Net-basedTookit for Ada Tasking Analysis” IEEE Trans.Parallel and Distributed System.,vol 1, no 4, 1990: 424-441.4 S.M.Shatz Shengru Tu T.Murata “An Application of Petri Net Reduction for Ada TaskingDeadlock analysis” IEEE Transactions on Parallel and Distributed Systems, vol.7, no 12, 1996: 1307-1

54、3225 P.Godefroid P.Wolper “Using Partial Orders for the Efficient Verification of DeadlockFreedom and Safety Properties.” In Formal Methods in System Design. .Kluwer. Academic Publisher. vol 2.no 2.1993: 149-164.6 M.Notomi T.Murata “Hierarchical Reachability Graph of Bounded Petri Nets forConcurrent