基于petrinet分析并发控制

《基于petrinet分析并发控制》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、基于petri网分析并发控制刘云峰，2012年7月5日1.简介petri网是用来分析并发行为的一种形式模型。举例来说，一个进程创建两个线程，然后等待它们结束，如下图：Figure1：开始进程T2:创建；T3:合并；T1和T0为各自线程的操作。P5为起始控制点，其中的黑点儿为token，表示拥有控制权。经过T2以后，P5失去控制权，P0与P3获得控制权，如下图。Figure2：创建线程如此运行，最后token到达P6，进程结束，见Figure3。注意P4和P2都有token时，T3才能激活。这个图里边，所有的P的token都不超过1，是有界的，这代表一种合理

2、性。Figure3：线程合并与进程终结值得一提的是，如果是一个进程fork出两个进程，这个图依然有效。在设计过程中，对并行过程建立petri网模型，比较容易验证所期望的性质。以下对几种同步控制方法和并行设计模式进行分析。1.同步控制方法互斥锁Figure4：临界资源访问T0和T1两个操作访问了临界资源，为了保证互斥性，引入了P5，同时又需要保证对方进入，需要在T2和T3释放token。这个方案可以保证P2和P4不同时包含token，或者说T0和T1随机互斥发生。事实上，这个P5就是互斥锁的模型。在程序中，P5的出边实现为T0和T1之前的加锁操作，P5的入边

3、实现为T2和T3之后的解锁操作。此时P5中token的个数，解释为资源量。读写锁读写锁指的是读锁和写锁，除了读与读可并行以外，其它组合都只能互斥完成。这里用权重为2的变换T4、T5表示“写”操作。这个模型里，所有的P有界。而且除了P2和P4可以同时有token，其它组合只能是P2，P4，P8，P9单独有token。此时P5的2出边实现为加写锁操作，1出边实现为加读锁操作，所有入边都实现为解锁操作。Figure5：读写锁模型条件变量条件变量在petri网中不需要显式地表达，因为每个变换都自动判断在P中的前提条件。·单入多出的变换：发送/广播信号，需要下一级变

4、换等待·多入单出的变换：等待·多入多出的变换：视情况而定1.并行设计模式最简单的并行行为是模块之间没有数据交互，基本不需要验证。下面讲述的是有数据交互并行行为生产者-消费者这种行为中，消费者是依赖于生产者的，有一种实现方案见Figure6。Figure6：生产者-消费者设计1T4为生产过程，T2为消费过程。两个过程的连接关系保证了先后次序。然而这种方式P1和P2不满足有界性，比如可能有无限个token累积在P1，在现实中表现为生产的产品未及时消费，产生库存溢出。此时要改变设计，用P2（消费完毕）作为生产的条件，可以保证P的有界性，见Figure7。系统实现

5、的时候，P1和P2解释为两个条件变量，生产者等待在P2上，执行完毕之后发信号给P1；消费者等待在P1上，执行完毕之后发信号给P2。系统启动时，发送信号给P2。值得注意的是，对于多个生产者-消费者的情况，程序的结构不发生变化，只是条件变量的等待/唤醒条件发生变化。Figure7：生产者-消费者设计2流水线模式流水线是多级的生产者消费者模式老板-工人模式其实Figure1就是这种模式，创建者为老板，被创建者为工人。1.总结在petri网中可以准确地描述并发行为，并且可以根据petri网的性质推断现实系统的行为特征，提供自动化的模型检查与验证。