基于BDD的Petri网可达图的GPU并行计算

作     者：马树城 

作者单位：西安电子科技大学 

学位级别：硕士

导师姓名：刘鼎;吴启俊

授予年度：2021年

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：Petri网 可达图 CUDA BDD Cuckoo哈希 

摘      要：随着社会数字化经济的不断发展,越来越多的工业嵌入式软件和互联网基础设施,采用分布式并发系统的组织架构。此类复杂系统,常会因并发使用共享资源不当而产生死锁问题,这不仅会降低生产率,有时甚至会导致整个系统的崩溃。为了避免死锁现象发生,系统运行过程分析和状态预测就成为设计该类系统的关键因素。Petri网作为分析流程的标准数学工具,可针对存在共享资源行为且由事件驱动的一类并发系统,做精确建模。在Petri网的相关理论中,基于可达图的分析方法是实现模型行为与状态分析的重要手段,是预测和避免死锁的重要基础。然而,随着网结构复杂程度与初始标识模长的增加,Petri网模型的可达状态数目会呈现指数增长,甚至会产生状态爆炸问题。本文针对Petri网可达图计算开展研究,主要进行了以下工作:1、作为并行计算可达图的基础,分析循环解耦、派生/汇集和分而治之等常用并行模式,总结串行计算并行化的重构原理。基于CUDA（统一计算设备架构,compute unified device architecture）,本文提出了一种以GPU（图形处理器,graphics processing unit）为主要运算平台的并行计算方法。为了计算性能最大化,以组成GPU基本单位SM（流处理器簇,stream multiprocessor）的硬件结构为研究起点,对与之配套的线程组织和内存管理等编程模型的实现,进行了总结。2、分化计算Petri网可达图的串行算法步骤,深入研究每次迭代中变迁使能发射和添加新合法标识等关键环节。具体工作包括:a)针对上述关键环节进行串行循环解耦,本文提出了一种链表插入式哈希的可达图并行算法。该算法基于哈希值对标识进行存储,目的是在索引组织多线程进行状态转移计算时,防止线程间耦合导致并行运算退化为串行运算。然而,该并行算法存在线程竞争激烈、时间和空间复杂度高等问题。b)为了解决线程竞争和时间复杂度问题,本文提出了一种降低线程间冲突几率和提升搜索速度的并行计算方法。该算法以具有多重位置选择集和驱逐特性的Cuckoo哈希作为主体框架,且包含一种专门存储驱逐上限元素的自平衡二叉搜索树（也称红黑树）。c)针对运行空间复杂度高导致的内存溢出问题,基于BDD（二元决策图,binary decision diagram）可以优化布尔函数表示新可达状态的性质,本文提出了一种在哈希桶下添加ROBDD（约简有序二元决策图,restrict ordered binary decision diagram）节点的算法,该算法通过可达状态的压缩形式减小了GPU的内存使用率。为了多角度对比三种并行算法的绝对加速比和可达状态数量的运算上限,本文计算了不同规模Petri网的可达图,并对计算结果进行了分析,指出了当前依然存在的问题,为后续研究提供参考。