基于程序运行轨迹Petri网模型挖掘的死锁检测方法
2021-10-11鲁法明崔明浩包云霞曾庆田
鲁法明，崔明浩，包云霞，曾庆田，段 华
(1.山东科技大学 计算机科学与工程学院，山东 青岛 266590;2.山东科技大学 数学与系统科学学院，山东 青岛 266590)
0 引言
随着多核处理器技术的快速发展，多线程程序被广泛应用，软件系统的运行效率得到显著提升。然而，由于程序调度的不确定性和执行空间的复杂性，多线程程序容易引发死锁和数据竞争等诸多并发缺陷[1]。死锁通常会导致系统运行不稳定，甚至造成严重后果，而且，据统计，约30%的并发缺陷与死锁有关[2]。因此，多线程程序的死锁检测具有重要意义。
常见的死锁检测方法分为3类[1,3-4]：模型检验[5]、静态分析[6-9]和动态分析[10-16]。模型检验借助形式化模型分析程序所有可能的行为，但其程序建模复杂，而且状态空间爆炸等问题也容易导致时间性能的降低，不适合大型软件程序的分析验证；静态分析通过对程序代码(而非执行代码)的静态分析来进行死锁检测，能较全面地发现潜在死锁，但同样存在效率低的问题。此外，由于缺乏程序运行时的诸多信息，静态分析通常会产生较多误报；动态分析[15]通过分析程序运行轨迹，研究锁授权顺序中存在的特定模式，并据此进行死锁检测。动态方法通常只针对某次或有限的几次运行轨迹对程序进行分析，故存在死锁漏报率高的不足。但是，同时具有动态分析效率高、可自动化进行的优点。而且，由于动态分析依赖的程序运行轨迹隐含了大量程序运行时的信息，因此存在误报率低的优点。鉴于误报率高严重影响死锁分析的实际应用(如，文献[5]对Sun JDK1.4进行分析时报告了100 000个潜在死锁，但仅有7个为真实死锁)，并且误报的排除费时费力，故本文着眼于对死锁的动态分析。
动态死锁分析方法对程序运行轨迹进行分析并构建能部分反映程序行为的锁图等模型，再基于这些模型研究锁授权顺序中存在的特定模式，并根据这些模式来检测死锁。例如，文献[7]首次基于锁图(将每个锁对象作为一个节点；当某线程在持有锁A并请求锁B时，在节点A到B间添加一有向弧，由此形成的图称为锁图。)给出了一个死锁的动态分析工具Visual Threads，它将锁图中每个环路视为一个潜在死锁。这种方法简单有效，但存在多种类型的误报。比如，单一线程访问锁对象时形成的环路、门锁保护的环路、具有因果关系的多个线程之间的锁授权操作导致的环路等，这些环路都会导致死锁误报。文献[11]提出基于锁树的GoodLock死锁检测算法，该算法能排除单线程环和门锁环导致的误报，但只能检测两个线程之间由于锁对象的持有和等待导致的死锁。文献[12-13]提出了环锁依赖链的概念，相比锁图，它相当于在锁图的有向弧上扩充了线程ID、当前持有的锁集等信息，能同时排除单线程环和门锁保护环导致的误报，而且对构成死锁的线程数量没有限制。文献[14-15]一方面基于线程之间的start和join操作对线程进行了分段，根据段之间的依赖关系提出了分段图的概念；另一方面，在锁图的基础上扩充线程ID、当前持有的锁集以及段号等信息，提出了分段锁图的概念；最终，提出一种基于分段图和分段锁图的死锁检测新方法，可以排除单线程环、门锁环和多线程间具有因果关系的段锁授权操作环导致的误报。然而，前述各种工具对多线程程序并发原语的建模能力有限，比如，无法对锁的授权/释放操作及其执行的场景进行准确刻画，从而仍然会导致一些误报现象(见1.1节案例分析)。在并行程序分析、业务过程管理[17-19]等分布式并发系统建模与分析领域，Petri网以其坚实的数学基础和直观的图形化表示被广泛应用[20-21]。鉴于此，本文拟采用Petri网对程序运行轨迹中蕴含的与死锁相关的多种并发原语进行建模，对锁的授权和释放、并发原语的每一次执行都采用独立的变迁来建模，这可以有效提高程序行为建模的精确度；之后，基于该Petri网模型的行为分析对多线程程序的潜在死锁进行检测。相比传统方法，本文所提方法能排除更多的误报。
对多线程程序而言，除各类并发原语，线程的循环等待、语句执行时间等也对死锁的产生具有重要影响。前述各种模型，包括本文拟采用的Petri网模型，很难完整建模所有死锁相关的信息，从而仍会导致一些误报现象。为保证所检测死锁的真实性，文献[22]提出一种多线程程序的随机调度方法，通过不同调度方案下程序的大量运行来尽量触发死锁，这可以保证所检测死锁的真实性。但是，该方法事先并不进行潜在死锁的检测，其调度是盲目的、完全随机的，加之死锁通常是低概率事件，这导致该方法在效率和可靠性方面存在较大不足。相比而言，文献[12,23-25]先进行潜在死锁的检测，之后针对每一个潜在死锁有针对性地生成程序调度方案以重演死锁，这提高了死锁重演成功的概率。具体而言，文献[12，23]提出一种启发式的死锁重演和程序调度策略，在线程到达潜在的死锁点时挂起线程，以此增加死锁触发的概率。不过，该方法本质上也是随机的，通常需要多次运行才能触发死锁，而且存在所谓的颠簸问题[12]，即使是一个真实的死锁也无法保证一定重演成功。文献[24-25]针对潜在死锁生成一组程序调度的约束集，当程序的运行不符合生成的约束时挂起线程的执行，该调度方案是确定性的。本文基于挖掘到的程序Petri网模型也可以生成一个确定性的程序调度方案来重演死锁。相比而言，文献[24-25]中的工作基于环锁依赖链检测潜在死锁，而本文方法检测到的潜在死锁误报更少、更准确。
总之，本文首先通过对Java多线程程序运行轨迹进行分析，挖掘一个能隐含尽量多程序行为信息的Petri网模型；之后，通过对该模型的动态行为分析检测潜在的程序死锁，并生成一个可用于死锁重演的确定性的程序调度方案。相比已有工作，本文方法有如下特点：
(1)基于程序运行轨迹挖掘一个更能精确建模程序行为的Petri网模型，该模型相比传统的锁图及其扩展模型能规避更多的死锁误报现象；与此同时，该模型虽由程序的单次运行轨迹重构而得，但它可以包含多条不同的程序运行轨迹，这为检测出更多的死锁提供了可能。
(2)在所得程序Petri网模型的基础上，对传统Petri网可达树技术进行扩充，进行程序死锁检测的同时可得到死锁重演的一种确定性调度方案，这为死锁的真实性奠定了基础。
1 动机与研究路线
1.1 实例分析
图1给出了一个多线程程序实例，包含3个线程(主线程、threadA和threadB)、3个锁对象(G、o1、o2)。主线程首先启动线程threadA，该线程在一个循环体中顺序获取锁G、o1和o2，然后逐个释放。第一次循环过程中，线程在获取锁G后会启动线程threadB，然后会先获取G，释放G后再依次获取o2和o1。threadA第二次执行循环体时不进行线程threadB的新建和启动。不难发现，“threadA第二次执行循环体时顺序获取锁o1和o2的操作”与“threadB释放G后顺序获取o2和o1”的操作会导致程序死锁的发生。而“threadA第一次执行循环体时顺序获取锁o1和o2的操作”与“threadB顺序获取o2和o1”的操作不会导致死锁，因为第一次循环执行过程中锁G始终被threadA持有，此时threadB因无法获得锁G而不会执行获取o2和o1的操作。
表1 多线程程序Program 1的一次运行轨迹
假设程序某次运行的轨迹如表1所示。表中：fork(u,v)表示线程u启动线程v的操作, acq(u,o)和rel(u,o)表示线程u获取和释放锁对象o，stop(u)表示线程u终止，join(u,v)表示线程u等待线程v终止后方执行后续操作。基于该运行轨迹，按文献[11-12]的方法可得如图2所示分段图和分段锁图。前者实际上将源程序每个线程执行的操作分为了多个段，每段对应一个唯一的段ID，段和段之间执行顺序上的先后关系通过分段图中的有向路径来建模；分段锁图是在传统锁图有向弧
基于锁图、环锁依赖链、分段图与分段锁图以及本文方法，对表1中的程序运行轨迹进行分析，得到表2所示的死锁检测结果。如前所述，表2第一行给出的潜在死锁实际是一种误报，因为threadA在第一次循环体执行过程中会始终持有锁G，此时threadB会被阻塞在第57行获取G的位置，从而无法执行后续操作。但是，如表2所示，基于锁图、环锁依赖链、分段图与分段锁图的已有方法均无法排除这一误报，究其原因，上述几种模型均无法区分threadA两次不同循环中获取锁的操作，而且由于上述模型没有显式建模锁对象的释放操作，threadB顺序获取o2和o1前需要曾经持有锁对象G的条件也因为G的及时释放而无法刻画。正是因为这些因素导致了误报的发生。
表2 不同方法对表1运行轨迹进行动态分析所得死锁检测结果
针对上述问题，本文拟利用Petri网对程序运行轨迹中蕴含的程序行为进行更精确的建模：分别对模型中锁的授权和释放进行建模，对线程的start/stop/join等并发原语也进行描述，而且同一并发原语的多次执行分别用多个独立的Petri网变迁刻画。这种建模粒度的细化以及更多程序信息的建模为提高死锁检测的准确性奠定了基础。此外，该模型通过资源库所的冲突结构，描述锁对象间的互斥竞争关系，通过变迁可执行序列中的操作先后关系，刻画同一线程各操作间的顺序关系，以及分段图所描述的不同线程操作间的顺序关系。这种模型隐含的程序行为信息超过了以往的锁图、环锁依赖链、分段图和分段锁图，其死锁检测能力理应更加准确。
利用本文方法可排除上述误报现象，并能准确检测出真实的死锁，从而证明了本文方法的有效性。此外，从该Petri网模型出发还可以方便地得到死锁重演的一种确定性调度方案。
1.2 研究路线
本文研究路线如图3所示。给定一个Java多线程程序实例，首先通过RoadRunner[注]RoadRunner是一个Java多线程程序的动态分析框架，它将事件流通信到后端分析，其中每个事件描述目标程序执行的需要关注的操作。[26]捕获程序某次运行时各并发原语构成的操作序列，包括锁的申请和释放、线程的start/stop/join等；之后，为每个并发原语构建相应的Petri网子模型，在此基础上，结合程序运行轨迹构建程序的Petri网模型；接下来，为进行程序死锁检测，构造程序Petri网的伴随网模型，并给出其死锁检测可达树的概念和构造方法；最后，基于死锁检测可达树，一方面给出潜在的程序死锁，另一方面为每个潜在死锁生成一个确定性的程序调度方案以用于死锁重演。下面对研究路线中的各项关键内容分别进行介绍。
2 程序运行轨迹的Petri网模型挖掘
2.1 多线程程序的运行轨迹
假设多线程程序由一组有限的线程组成，每个线程有一个唯一的线程标识符(如u或v)，程序运行轨迹α定义为程序运行过程中所执行的各类并发原语构成的序列，具体如下：
α∈Trace∷=SynOperation*，
op∈SynOperation∷=c:fork(u,v)|c:join(u,v)|c:stop(u)|c:acq(u,l)|c:rel(u,l)。 其中：
SynOperation表示各类并发操作的集合，SynOperation*为并发操作构成的序列全体；
u,v∈Tid表示线程，l∈Lock表示锁，c表示一个程序语句的标签；
fork(u,v)表示线程u派生并启动一个新线程v；
join(u,v)表示线程u等待线程v完成后，方能继续向下运行；
stop(u)表示线程u终止；
acq(u,l)和rel(u,l)表示线程u获取和释放锁l。
如表1所示即为Java多线程程序Program 1的一个运行轨迹，它描述了程序某次运行中各个并发原语的执行顺序等信息，后文将据此构建程序的Petri网模型。
2.2 并发原语与程序的Petri网模型构建
Petri网被广泛用于并发系统的建模和分析。一个Petri网对应一个4元组Σ=(P,T;F,M0)，其中：P和T分别是不相交的库所集和变迁集，F⊆(P×T)∪(T×P)是网Σ的流关系集，M0:P→{0,1,2,…}被称为Σ的初始标识，它描述系统的初始状态[27]。本文每个Petri网变迁用于刻画程序中一个并发原语的某次执行，库所分为控制流库所和资源库所两类，前者对各个线程的控制流状态进行建模，后者用来描述多个线程间共享的锁对象。
根据Petri网的执行规则与各个并发原语的操作语义，可得表3所示各类并发原语和程序状态对应的Petri网模型。模型中各库所、变迁所描述的程序含义见表3第3列。
基于RoadRunner或者其他程序运行分析平台捕获多线程程序的运行轨迹后，进而可根据表3给出的规则构建程序的Petri 网模型。具体而言，最初为主线程的就绪状态生成一个库所，并在其中添加一个token(表示主线程处于就绪状态)；同时为每个锁对象生成一个库所，也向其中添加一个token(表示初始状态下各个锁对象可用)；之后，对每一个捕获到的并发原语操作，按照表3的规则添加变迁、控制流库所和资源库所及相应的流关系。以表1的运行轨迹为例，按上述方法可得其对应的程序Petri网模型，如图4所示(红色矩形框对应的变迁及其关联的流关系不含在内)。
Σ1中的绿色圆圈为资源库所，对应锁对象；黑色圆圈为控制流库所，对应线程的控制流状态；黑色矩形为变迁，对应并发操作的一次执行。为便于理解，在每个变迁和资源库所旁用蓝色标签给出了其对应的程序含义，黑色标签是库所或变迁的ID。库所内的小黑点为token，控制流库所中的token表示相应的控制流状态被激活，资源库所中的token表示相应的锁对象可用。需要指出的是，由程序运行轨迹和表3规则所构造的Petri网模型是安全的，因为控制流库所或处于激活状态，或处于非激活状态；资源库所或对应锁对象的可用状态，或对应锁对象的不可用状态，这意味着在任意可达状态下，程序Petri网模型的各个库所中的token数量或为0，或为1，从而是安全的。
对于按上述方法构建的程序Petri网模型，原程序运行轨迹相对应的变迁序列显然是可引发的。例如，表1中的运行轨迹对应着图4中的变迁序列σ=t1t2t3t4t5t6t7t8t9t10t12t11t13t14t15t16t17t18t19t20t21t22t23t24，易验证该序列是可引发的。从初始标识出发，σ引发后到达的状态标识为{p26,p18,p27,p28,p29}。该标识是一个合法的程序终止状态(未被join的各线程的终止状态库所含有一个token，每个锁对象对应的资源库所含有一个token，其他库所均不含token。这意味着所有线程均正常终止，且所有的锁均被释放)。
表3 程序状态与并发原语的Petri网模型
续表3
然而，前述构造的程序Petri网模型除隐含原始的程序运行轨迹外，还可能包含许多其他的程序潜在运行轨迹。这是因为，前述构造原理保证了仅在以下情况下才会在Petri网中建立节点之间的因果关系(其他情况下被处理为并发或者冲突，由此导致了执行轨迹的多样性)：①同一线程中的两个操作依次执行，则在它们之间建立直接因果关系；②线程u执行fork(u,v)操作，此时在fork(u,v)和线程v的第一个操作之间建立直接因果关系；③线程u执行Join(u,v)操作，此时在线程v的最后一次操作stop(u)和Join(u,v)之间建立直接因果关系；④锁l对应的资源库所和acq(u,l)之间建立直接因果关系；⑤rel(u,l)和锁l对应的资源库所之间存在因果关系。对于任何其他情况，即使是运行轨迹中相继发生的两个操作，它们之间也不建立因果关系。例如，表1中第11步操作60:acq(threadB,o2)和第12步操作28:acq(threadA,G)，虽然他们之间在表1运行轨迹中紧邻发生，但不满足前述5种条件，故其在Petri网模型的可执行变迁序列中顺序是不确定的(t12与t11的引发次序多样化)。例如，σ′=t1t2t3t4t5t6t7t8t9t10t11t12t13t14t15t16t17t18t19t20t21t22t23t24也是Σ1中的一个可执行变迁序列。
程序Petri网模型隐含了多样化的程序运行轨迹，这为程序的死锁检测提供了可能。例如，σ″=t1t2t3t4t5t6t7t8t9t10t11t12t17也是Σ1的一个可执行变迁序列，该序列执行后到达一个死标识{p1,p14,p19}，该标识下没有任何一个变迁可执行，而且存在未正常终止的线程。这实际对应着源程序的一个死锁状态(threadA持有o1申请o2，threadB持有o2申请o1)，该变迁序列对应的程序运行轨迹如表4所示，表中加粗字体给出的操作由于threadA与threadB对锁对象o1和o2的持有等待导致了程序死锁。
表4 导致死锁的实例程序的运行轨迹
2.3 程序模型的伴随Petri网
对于2.2节由运行轨迹挖掘到的程序Petri网模型，无论是程序的合法结束状态，还是程序的死锁状态，均对应Petri网模型的一个死标识。为区分二者，在程序Petri网模型的基础上添加一个额外的变迁(对应图4中红色矩形框表示的recover变迁)，其作用是将程序的合法终止状态恢复为初始状态。如此一来，程序的合法终止状态在修改后的网模型中便不再是死标识，而程序的死锁状态仍将对应一个死标识。为达到这一目的，recover变迁的输入库所应设置为所有未被join的线程的终止态库所和所有锁对象对应的资源库所，其输出库所应设置为主线程的就绪态库所和所有锁对象对应的资源库所。称添加recover变迁后的网模型为原始程序Petri网模型的伴随网，其严格定义如下：
定义1程序模型的伴随Petri网给定一个由运行轨迹挖掘的程序Petri网模型Σ=(P,T;F,M0)，设PthreadStop是所有未被join的线程之终止状态库所的集合，Plock是所有锁对象对应的资源库所集合，p0是主线程就绪状态对应的库所。令P′=P，T′=T∪{recover}，其中recover是一个新添加的变迁，F′=F∪((PthreadStop∪Plock)×{recover})∪({recover}×({p0}∪Plock))，称Σ′=(P′,T′;F′,M0)为Σ的伴随Petri网。
例如，图4含有recover变迁完整模型就是Σ1的伴随Petri网。显然，源程序的合法终止状态不再是伴随Petri网的一个死标识，因为该状态下recover变迁可使能，并将系统状态恢复为程序的初始状态。而源程序的死锁状态仍然对应伴随Petri网的一个死标识(即{p1,p14,p19})，因为在死锁状态下，recover变迁和原来的所有变迁均不使能。因此，要检测多线程程序的潜在死锁，只需要对伴随Petri网进行死标识检测，下面给出检测方法。
3 多线程程序的死锁检测与重演
可达树[14]是进行Petri网可达性分析的重要工具，安全Petri网可达树的每个节点都关联着网模型的一个可达标识。树中的叶节点分为两类：①复制节点，它与可达树中之前出现的某个节点关联的标识相同；②终端节点，该节点关联的标识为死标识，死标识下不存在可使能的变迁。2.3节已经指出，伴随Petri网模型的每个死标识均对应源程序的一个潜在死锁。
已有不少工作基于可达树进行Petri网死标识的分析和检测[9,28-29]，本章在传统可达树构造算法的基础上，基于各个变迁所对应并发原语的含义，为每个死标识生成一个用于死锁重演的程序调度方案，并称包含该死锁重演调度信息的可达树为死锁检测可达树。
死锁检测可达树的构造思想如下：首先，构造伴随Petri网模型的可达树；之后，对于可达树中每个死标识对应的终端节点，求取根节点到终端节点的变迁序列对应的操作序列；最后，基于各个死标识对应的操作序列，计算序列中涉及的每个锁对象的授权线程序列。各个锁对象的授权线程序列就是后续重演的依据，据此可生成一个确定性的程序调度方案，具体方法如下：
对于可达树中某终端节点，假设从根节点到它的操作序列中出现了锁对象o，而且在操作序列中o被依次授权给了线程u1u2…uk，记δ(o)=
(1)每当有线程u尝试进入锁对象o的同步块(即尝试获取o)时，判断u是否为δ(o)的首元素。若u不是δ(o)的首元素，则在CalFuzzer提供的lockBefore函数中阻塞线程u，并将其加入到o所关联的一个阻塞线程池中；若u是δ(o)的首元素，则在CalFuzzer提供的lockAfter函数中删除δ(o)的首元素；
(2)每当有线程u退出锁对象o的同步块(即释放o)时，在CalFuzzer提供的unlockAfter函数中，将锁对象o阻塞线程池中的线程全部唤醒；
(3)lockAfter函数中，一旦所有锁对象的授权线程序列变为空，则唤醒所有阻塞线程池中的线程对象，后续不再对程序的运行作任何干预和调度；
(4)每次LockBefore函数被调用，都判断当前程序执行状态下是否已经触发死锁。若有程序死锁被触发，且各个锁对象的授权线程序列为空，则说明潜在死锁重演成功；若有死锁被触发，但存在锁对象的授权线程序列不空，则说明程序存在另一个真实死锁，本文试图重演的潜在死锁的真实性无法判定；若没有死锁被触发，而且程序正常终止，则说明潜在死锁是一个误报。
以图4中的伴随Petri网为例，其对应的死锁检测可达树如图5所示。树中存在两个终端节点(复制节点的标识采用绿色字体，终端节点用红色，蓝色标签为各个变迁对应的并发操作)，从根节点到他们的变迁序列分别为t1t2t3t4t5t6t7t8t9t10t11t17t12和t1t2t3t4t5t6t7t8t9t10t12t11t17。这两个变迁序列均涉及到锁对象G、o1和o2，而且两个序列中锁对象的授权序列也是一致的：锁对象G依次授权给threadA、threadB、threadA，锁对象o1依次授权给threadA、threadA，锁对象o2依次授权给threadA、threadB。进行重演时，假设源程序仍尝试按表1未触发死锁的操作序列运行。按前述调度规则，可得表5中的调度方案(表中13行第3列操作意味着线程尝试执行它时被阻塞，15行第3列的操作意味着被阻塞线程唤醒后又一次执行前面阻塞发生时的操作，加粗字体的操作构成触发死锁的操作集)。最终，潜在死锁会被触发，重演成功，验证了死锁的真实性。
表5 死锁重演过程实例
续表5
综上所述，基于本文所提方法，一方面对程序实例Program1的潜在死锁进行了更为准确的检测，相比传统基于锁图、环锁依赖链、分段图和分段锁图减少了死锁误报现象的发生；另一方面，给出了一种用于死锁重演的确定性程序调度方案生成方法与调度策略，相比传统的随机性调度方法，可以更为方便和有效地对潜在死锁进行重演和验证。
4 工作对比与实验评估
第1章结合程序1从原理上说明了本文方法相比iGoodlock等经典动态分析方法的优势，本章进一步结合CalFuzzer开源项目中公开的多个Java多线程程序实例[注]CalFuzzer项目及其程序实例链接https://github.com/ksen007/calfuzzer/tree/master/test/benchmarks/testcases,Demo2程序实例链接https://pan.baidu.com/s/1aRyD7jAEKWSS0EGkuZDFpg，提取码：bmv9。进行实验评估。实验对比结果如表6所示，实验时的机器配置为：Intel(R) Xeon(R) Platinum 8163 CPU @ 2.50 GHz、内存2 GB、操作系统为Ubuntu 5.4.0。(表中的CF代表Clafuzzer集成的死锁检测和重演方法)
就检测准确性而言，CalFuzzer中集成的是iGoodlock死锁检测方法，该方法使用环锁依赖链检测潜在死锁，如第1章所述，该方法相比本文方法会产生更多的死锁误报。表1中程序Demo2和本文实例就体现了这一点，iGoodlock算法报告的潜在死锁数更多，而且多出的死锁均为误报。对于每个检测到的潜在死锁，CalFuzzer基于DeadlockFuzzer进行死锁重演，其本质是一种随机的重演策略，而本文的调度方案是确定性的，由此导致的结果是：同一个真实死锁，DeadlockFuzzer通常需要运行多次方能触发成功，而本文基于锁授权线程序列只需一次重演即可(实验中，对于程序实例Test1a和Test1b，运行了3次以上方才重演成功)。
表6 程序死锁检测的实验结果对比
从时间性能来看，在潜在死锁的检测阶段，本文所提方法耗时更多，本质上是因为本文构建的程序模型包含了程序更多的行为信息，而且Petri网的死锁检测算法本身耗时较多，但这种时间性能的降低换来的是潜在死锁检测准确度的提高；在潜在死锁的重演阶段，本文所提的重演方法效率更高，因为本文给出的是一种确定性的程序调度方案，而CalFuzzer的调度方案是随机的、通常需要多次运行方能重演成功。
5 结束语
本文提出一种新型的多线程程序死锁检测和重演方法，首先捕获程序运行轨迹中各类并发原语对应的操作，据此构建程序的Petri网模型；之后，将程序的死锁检测问题转化为程序模型伴随Petri网的死标识检测问题；最后，在传统可达树的基础上，计算并扩充了可用于死锁重演的程序调度方案，给出了具体的程序调度规则，为潜在死锁的真实性判定奠定了基础。文中分析和程序实例表明，所提出的基于程序Petri网模型的死锁检测方法能排除更多的误报，而且给出的死锁重演方案简单易懂，相比过往随机性的程序调度方案可以更为有效地完成死锁重演。然而，本文方法也存在一定的不足，尤其是程序包含很多的并发行为时，所构建Petri网模型的可达树可能出现状态爆炸问题，后续将借助Petri网展开等方法来缓解该问题。
此外，本文仅给出了所提死锁检测和重演方法的基本原理，在开发具体的应用软件时还存在诸多技术问题。例如，在死锁检测和重演两个不同的阶段需分别运行程序，而程序中锁对象和线程对象在两次不同的运行中具有不同的ID，如何进行同一对象在两次运行中不同ID间的对应，这在以往工作中是一个难点。幸运的是，该问题基于本文方法是可以有效解决的，限于篇幅，具体解决方法在后续工作中给出。此外，影响死锁的并发原语还包括wait/notify等并发原语，如何对它们进行Petri网建模和分析也是后续工作需要解决的问题。
