基于petri网分析并发控制

1.     简介

petri网是用来分析并发行为的一种形式模型。举例来说,一个进程创建两个线程,然后等待它们结束,如下图:

Figure 1:开始进程

T2: 创建; T3: 合并;T1和T2为各自线程的操作。

P5为起始控制点,其中的黑点儿为token,表示拥有控制权。经过T2以后,P5失去控制权,P0与P3获得控制权,如下图。

Figure 2:创建线程

如此运行,最后token到达P6,进程结束,见Figure 3。这个图里边,所有的P的token都不超过1,是有界的,这代表一种合理性。

Figure 3:线程合并与进程终结

值得一提的是,如果是一个进程fork出两个进程,这个图依然有效。

在设计过程中,对并行过程建立petri网模型,比较容易验证所期望的性质。以下对几种并行设计模式和同步控制方法进行分析。

2.     并行设计模式

最简单的并行行为是模块之间没有数据交互,基本不需要验证。下面讲述的是有数据交互并行行为

生产者-消费者

这种行为中,消费者是依赖于生产者的,有一种实现方案见Figure 4。

Figure 4:生产者-消费者设计1

T4为生产过程,T2为消费过程。两个过程的连接关系保证了先后次序。然而这种方式P1和P2不满足有界性,比如可能有无限个token累积在P1,在现实中表现为生产的产品未及时消费产生库存溢出。

此时要改变设计,用P2(消费完毕)作为生产的条件,可以保证P的有界性,见Figure 5。

Figure 5:生产者-消费者设计2

流水线模式

流水线是多级的生产者消费者模式

老板-工人模式

其实Figure 1就是这种模式,创建者为老板,被创建者为工人。

3.     同步控制方法

互斥锁

Figure 6:临界资源访问

T0和T1两个操作访问了临界资源,为了保证互斥性,引入了P5,同时又需要保证对方进入,需要在T2和T3释放token。这个方案可以保证P2和P4不同时包含token。事实上,这个P5就是互斥锁的模型。

读写锁

读写锁指的是读锁和写锁,除了读与读可并行以外,其它组合都只能互斥完成。这里用权重为2的变换T4、t5表示“写”操作,T6和T7释放写锁。这个模型里,所有的P有界。而且除了P2和P4可以同时有token,其它组合只能是P2,P4,P8,P9单独有token。

Figure 7:读写锁模型

条件变量

条件变量在petri网中不需要显式地表达,因为每个变换都自动判断在P中的前提条件。

4.     总结

在petri网中可以准确地描述并发行为,并且可以根据petri网的性质推断现实系统的行为特征,提供自动化的模型检查与验证。

原文地址:https://www.cnblogs.com/liuyunfeng/p/2578061.html