论文部分内容阅读
资源分配系统是一种典型的离散事件系统。由于对有限的资源的竞争使用,资源分配系统的进程间极易产生对资源的循环等待,进而发生死锁,使得系统阻塞而无法继续执行。作为一种数学建模工具,Petri网由于其直观的图形表示和形式化的数学描述,被广泛应用于分析和解决资源分配系统的死锁问题。其中,S*PR网以其良好的建模能力,正逐渐受到学者们的重视,并被广泛应用于建模和分析资源分配系统的死锁问题。通过研究信标的活性条件,进而检测网系统活性并设计满足条件的活性保持控制器是基于S*PR网的死锁控制的主要研究方向之一。目前学术界对S*PR网活性条件的研究主要集中于它的一个普通网子类Gadara网。Gadara网可建模同种资源总量为1且进程的选择操作不使用任何资源的资源分配系统。然而经过研究发现,许多常见的资源分配系统并不能通过Gadara网建模,而需要通过S*PR网的其他子类建模和分析其特性。针对这一问题,本文对几种S*PR网子类活性条件及其应用展开了研究,完成的主要工作有:(1)提出了一类用于建模存在缓存区的资源分配系统的普通S*PR网模型,BS*PR网。同时证明了BS*PR网是活的当网中所有信标满足资源受控条件。进而提出了一个检测非资源受控信标的混合整数规划算法,该算法可用于BS*PR网的活性检测。在多线程程序和经典制造系统案例中的应用表明,该模型能够有效地建模和分析存在缓存区的资源分配系统。(2)提出了一类可用于建模进程选择操作对称使用资源的资源分配系统的普通S*PR网模型,SEM-S*PR网。该子类进程子网选择库所可对称地使用资源,并不再限制系统中使用的同种资源的总量为1。因而,Gadara网本质上是SEM-S*PR网的一个特例。同时证明了SEM-S*PR网是活的当且仅当网中所有信标始终非空,该结论为混合整数规划技术应用于SEM-S*PR网的活性检测提供了理论基础。进一步地,将SEM-S*PR网结论推广至选择操作对称使用资源的广义S*PR模型,OSC-S*PR网。在证明其保持活性的充分条件是网中所有信标Max’-Controlled的基础上,提出了一个基于混合整数规划的S*PR网非Max’-Controlled信标检测算法,该算法可用于检测该OSC-S*PR网的活性。更重要的是,通过将任意S*PR网转换为一个OSC-S*PR网,该算法也可推广应用于S*PR网的活性检测。在实际软件系统,经典制造系统以及哲学家模型中的实验结果表明,本文提出的几种S*PR网子类不但能够建模和分析Gadara网所建模系统中的死锁问题,还能够分别建模进程选择操作对称和存在缓存区的资源分配系统。同时,基于对应子类的活性条件,还可将混合整数规划技术应用于S*PR网的活性检测,进而保证了更高的计算效率。