理论计算机科学电子笔记128（2005）19-34www.elsevier.com/locate/entcs负载平衡并行显式状态模型检测Rahul Kumar1 和埃里克·G Mercer2验证与确认实验室杨百翰大学美国普罗沃摘要本文首先确定了一些关于并行模型检查技术和算法的关键问题;特别是，静态分区算法中负载平衡和大队列大小的固有问题本文提出了一种负载平衡算法，以提高分布式模型检测的运行时性能，减少最大队列大小，并减少错误发现前扩展的状态数负载均衡算法是基于广义维交换（GDE）。本文对基于GDE的负载平衡算法在分布式内存集群、工作站网络（NOW）和共享内存机器三种不同超级计算体系结构上的性能进行了实证分析分析表明，提高了加速比，降低最大队列大小和更少的总状态探索错误发现之前的最后，本文提出了一个研究的通信开销所产生的使用负载平衡算法，虽然显着，并不妨碍性能增益。关键词：模型检测，并行，分布式，负载平衡，GDE，队列大小，错误检测，通信1介绍显式状态模型检查是一种通过可达性分析来验证设计中的属性的方法然而，模型检验的实际应用受到状态爆炸问题的阻碍[5]。状态爆炸是使用交织枚举并发系统的状态空间1电子邮件：rahul@cs.byu.edu2电子邮件：egm@cs.byu.edu1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.01620R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）19语义，其中在任何给定状态中必须分别考虑每个并发启用的转换存在几种技术来解决状态爆炸问题的各个方面。对称性和偏序约简利用结构和并发性来减少可达状态空间中必须探索以完成模型检查问题的状态数量[3][6]。位状态散列（超迹）和散列压缩降低了可达状态空间中存储状态的成本[7][13]。所有这些技术都可以验证更大的问题，但最终，它们仅限于单个工作站上可以存储的状态数量。如果模型检查算法在验证问题完成之前耗尽了它运行的工作站上的资源，那么必须以某种方式改变问题，以减少其可达状态空间的大小，直到它可以适应可用资源。分布式模型检测的目标是将多个处理器的内存和计算资源结合起来，以提高状态生成和存储能力。Stern和Dill提出的分布式模型检查的开创性工作在执行期间创建了可达状态空间的静态分区[14]。作为时间和每个处理器上的通信开销的函数而观察到的工作负载关键取决于在验证过程之间如何划分状态过去已经探索了几种技术，如缓存（兄弟和状态），偏序约简，对称约简，不同的分区函数和动态分区，以减少通信开销并创建完美的状态分布[11][10]。即使使用上述技术，为任何给定的问题创建一个完美的分区，同时保持同等负载的处理器需要状态空间的先验知识，这正是我们试图解决的问题。本文提出了一个实证研究的种子静态分区出租显示的负载不平衡的水平，无论选择的静态分区，存在于不同的超级计算平台上的进程之间。这种不平衡导致多个处理器的空闲时间很长，搜索队列也非常大。高空闲时间表明许多处理器没有对状态枚举做出贡献，并且大的搜索队列通过耗尽存储器资源而导致过早终止。此外，分区中的不平衡减慢了错误发现，因为导致错误的状态可能被深埋在搜索队列中。本文进一步提出了一种基于广义维交换（GDE）的负载均衡算法负载平衡的状态划分算法提高了分布式模型检测的加速比，尽管增加了通信。此外，它还减少了R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）1921最大队列大小增加了10倍，并且平均减少了错误发现之前这些结果在三种不同的超级计算体系结构上的实验研究中得到了展示：工作站网络（NOW）、集群和共享存储器体系结构。2模型和平台对这项工作进行了实证分析，以更好地理解静态分区算法和其他使用park-mur方法的技术的性能 [9]。在以下平台上完成测试并收集结果：(i) IBM 1350 Linux集群，具有128个高速互连的双处理器节点;(ii) 具有100 Mbps互连的工作站网络;(iii) Marylou 10 IBM pSeries 690 64 Power 4+处理器@1.7 GHz 64 GB总内存。测试的主要部分使用位于[1]中模型数据库中的模型进行之所以选择这些模型，是因为它们提供了一个大型的、可控的、有趣的和多样化的测试集。所选模型并不能代表所有类型的问题，但它们有效地捕捉了我们在研究几个问题时的一般观察结果。3分布式模型检测技术分析本节将首先分析静态分区算法，并提出使用静态分区算法时遇到的问题，在分析之后，我们讨论解决这些问题的两种示例技术。我们的研究结果表明，这些技术不是很有效的模型和基准测试我们使用。3.1队列不平衡和空闲时间静态分区算法可以使用多个处理器以更快的速度验证更大的模型。我们对算法的进一步研究支持这样的结论，即分布式验证期间的空闲时间很高，并且参与处理器的队列中的状态分布高度不平衡，导致过早终止，降级的错误发现和大队列大小。图1（a）显示了在NOW架构上使用32个处理器进行验证的整个期间内，以1秒间隔对所有处理器进行采样的队列的22R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）19百分比x 104732个节点660550440330220110000 20 40 60 80 100 120 140时间（秒）静态划分算法CPU SG空闲功能(a)（b）第（1）款Fig. 1.该图显示了使用NOW架构的主要功能的时间和时间分布的高度队列不平衡。(a)使用32个处理器的jordon模型的队列大小。(b)所有处理器用于验证中的主要功能的总时间显示大量空闲时间。间隔采样是使用大多数基于UNIX的系统上可用的报警和信号实用程序来实现的。横轴表示时间，纵轴表示给定处理器队列中的状态数该图显示了队列大小的不平衡，许多处理器仅在验证的早期部分有有用的工作要做。在验证的后半部分，只有20%的处理器处于活动状态。这些结果与Behrmann最近的工作一致[2]，其中观察到相同的不平衡。图1（b）显示了在验证Atomix模型期间，花费在主要复合函数上的时间的总百分比。主要的复合功能是CPU、状态生成（SG）和空闲。CPU是执行I/O操作和通信所花费的时间。状态生成时间被定义为处理队列中的状态并生成其后继状态所花费的时间。空闲时间是由于处理器搜索队列为空而等待接收新状态在此状态下，验证处理器仍在处理消息。然而，消息中的状态被丢弃，因为它们先前已被添加到散列表中。该图表明，在通信之后，空闲时间占主导地位。事实上，几乎三分之一的总时间都花在了空闲上。对于不同大小和形状的其他模型也观察到类似的结果3.2配分函数空闲时间是负载不平衡的直接结果这可以在各种哈希函数的实验中看到，以及它们对加速的影响我们研究了配分函数对状态分布的影响，通过使用各种散列函数实现配分函数，其中包括国R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）19234.543.532.521.510.50x 1040 20 40 60 80 100 120140时间（秒）3.532.521.510.50x 1040 20 40 60 80 100 120 140时间（秒）(a)（b）第（1）款图二、在NOW架构上使用64个处理器和两个来自Spin的不同散列函数的Atomix模型的队列不平衡SPIN[8].图2（a）显示了NOW架构上使用SPIN的单比特前向散列函数的64个队列的队列分布。虽然与图1（a）相比，更多的处理器在整个验证运行期间保持活动状态，但仍有相当数量的处理器处于空闲状态，并且在验证过程的一半以上运行时间内保持空闲状态图2（b）显示了相同的队列分布，使用不同的位掩码用于来自SPIN的相同散列函数。尽管两个实验的所有其他参数都保持不变，但分布非常不同。类似的结果已经注意到其他散列函数，如Jenkins前向散列函数和我们使用的动态分区算法[10]。 这些结果表明，要在所有处理器的队列中创建一个完美的状态分布，然后在整个验证过程中保持这种分布，需要状态空间的先验知识这正是我们首先要解决的问题3.3状态高速缓存一种提高分布式模型检查性能的技术是使用状态缓存来减少消息和哈希查找的数量。以前关于状态缓存的工作，以提高性能已经在[11][4]中提出。我们的分析表明，在相同的消息或不同的消息发送到其他处理器的重复状态的存在。这是因为模型的状态空间中的许多状态可以通过不同的路径和从不同的状态到达。为了避免这种情况，在每个处理器上分配一个内存块作为直接映射状态缓存。只有缓存中不存在的状态才会被转发到它们所属的处理器。国国24R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）19使用Cache相对于静态分区算法的加速比1.121.11.081.061.041.0210.980.960.940 5 10 15 20 25 30 35处理器图三.在IBM 1350群集上使用大小为1 MB的缓存获得的相对于静态分区算法的加速比。对状态缓存的进一步研究表明，一旦缓存大小超过1 KB，尽管占用率很高，但消息数量的减少并不显著这是由于在并行验证中使用大量处理器时的低转换局部性。通过使用缓存观察到的平均加速是恒定的，但不是很高。相对于静态分区算法，在1.05的区域中获得了加速比。图3显示了在IBM 1350集群上使用1 MB缓存实现的加速。由于高速缓存而实现的加速由在直接映射状态高速缓存中查找状态所花费的时间以及将状态插入到高速缓存中所花费的时间来确定这导致缓存在加速、队列大小或错误发现方面没有显著的改进。4方法在分布式模型检测中，我们引入了队列负载均衡的概念来减少总空闲时间。[12]中的工作描述了一种全局负载平衡技术，其中所有参与状态空间生成的处理器都试图达到完美的平衡状态。在均衡中，所有处理器在队列中具有相等数量的状态，以消除不平衡。状态生成的短周期之后是处理器通过交换队列信息和队列中的额外状态来彼此平衡队列的周期。这种方法有几个缺点。首先，在并行模型检测问题中引入了太多的通信开销，而并行模型检测问题本身是非常通信密集的。乔丹·阿加速比R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）1925n = 0P0n = 3n = 1P0P1P4P5均p0P0P1P7n = 2P2P 3P2P 3见图4。 1到8个处理器的超立方体结构。如果模型或处理器数量显著增加，这将导致算法无法扩展。其次，用户/验证者负责指定迭代次数，在此之后负载平衡周期应该发生（频率）。如果选择的值非常小（高频），则通信开销非常高，有效加速非常低。另一方面，如果选择的值较大（低频），则不会发生有效的负载平衡，并且并行验证过程的行为方式与静态分区算法相同。全局负载平衡算法的另一个问题是等待所有处理器同步负载平衡所需的时间。考虑4个处理器P0、P1、P2和P3的场景。 假设P1，P2，P3已准备好进行负载平衡，并且已经启动了负载平衡-的阶段。如果在这种情况下，P0恰好是非常重的负载，将状态插入到其队列中，则P0将无法与其他处理器同时进入负载平衡阶段，导致其他处理器等待，直到P0完成处理状态/消息并进入负载平衡阶段。我们使用广义维度交换（GDE）进行负载平衡，它通过让每个处理器与每个维度邻居均衡其工作负载来在所涉及的处理器之间执行迭代负载平衡[15][16]。维度邻居是根据为处理器选择的拓扑计算的。我们的GDE方法将验证过程中的处理器分组为超立方体结构。图4显示了1到8个处理器的超立方体的结构以及在每种情况下创建的维数GDE算法设置类似于边着色问题，其中没有两个边可以被分配相同的颜色;因此，如果超立方体结构中的处理器使用与P1P626R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）19210001000算法：GDEBalanceExceles（）1：/在每个处理器上，每个输入都由BFS/DFS进行检查/2：对于所有的邻居，第三章：n：=getN extractionalN eighborID（）第四章：q：=getLocalDataSize（）5：s：=sendDataSize （ n， q ） 6 ：return图五. 发送端GDE负载均衡算法。边着色问题，会有[log（N）]|颜色，其中N是处理器的数量。每种颜色都可以被认为是一个维度，处理器的子集属于特定的维度。这网络结构使我们能够以优雅的方式查看处理器，并实现在通信方面更有效的算法。在GDE负载平衡方案中，每个节点与其维度邻居平衡工作负载（队列中的状态数）。在8个处理器的网络中，处理器P0与处理器P1、P2和P4平衡。在平衡阶段，每个处理器可以选择完全平衡工作负载，以便两个队列中的每个队列具有相同的工作量，或者它们可以选择平衡到其他点。交换参数被定义为在执行负载平衡操作时在两个处理器之间共享的工作负载量。[16]中的工作证明了在尽可能少的迭代中创建平衡状态的最佳值是1。图5和图6显示了该算法的伪代码。每i次迭代，其中i是用户设置的平衡频率，处理器将其当前队列大小发送到其维度邻居。在接收侧，一旦处理器从维度邻居接收到队列大小，处理器就执行图6所示的算法。如果本地队列上的工作负载高于邻居上的工作负载，则将状态发送到邻居。另一方面，如果工作负载不是更高，则不采取任何动作，并且执行返回到状态生成和通信过程。从其他处理器接收状态是隐式发生的，不会发生阻塞。为了我们的测试目的，我们将交换参数设置为一半，而bal-频率为1states. 平衡频率为1意味着负载在已经从处理器的队列处理了1000个状态之后，或者如果处理器的队列为空，则启动平衡由于队列中的每个状态仅在检查哈希表之后添加，因此将队列状态直接传输到其他处理器队列不会删除访问状态集;因此，不会导致不同处理器上的相同状态的多个副本。R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）1927算法：HandleM消息（M，ID）1：/如果从ID中接收到一个队列大小，则需要将其删除/2：/确定相邻消息或来自消息M的队列大小/3：qn=getSize（M）4：ql：=getLocalTimeSize（）5：如果ql> qn，则6：sendStates（（ql−qn）/2，ID）7：其他8：/在一个非blocking时装店发生的Reeivehappens/9：receiveStates（（qn−ql）/2，ID）10：返回见图6。 接收端的GDE负载均衡算法。5结果图7显示了使用IBM 1350 Linux集群的atomix和jordon模型的GDE负载平衡方案相对于静态分区算法（没有缓存）的相对加速除了更高的加速比之外，我们还可以看到加速比曲线随着处理器数量的增加而向上移动这是由于网络拓扑的N维超立方体所创建的高效通信模式。图8显示了NOW架构上GDE方案的加速。我们可以看到，实现的加速比在图7的分布式内存集群架构上实现的加速要高。图9显示了在前面描述的共享内存机器上的相同模型和方案的加速。这里的加速比似乎低于其他两个架构上实现的加速比。总的趋势似乎是，处理器之间的互连越慢，GDE负载平衡方案越有效;因此，对于互连最快的共享存储器架构，我们可以看到负载平衡是最不有效的，以至于它是有害的。然而，对于分布式存储器体系结构，互连比NOW体系结构快，但比共享存储器体系结构慢：因此，它为GDE方案提供了提高性能和效率的机会。另一方面，NOW架构提供了最慢的互连和最佳的加速结果，如图8所示。观察到的行为和加速模式是未来研究和学习的领域28R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）19相对于静态分区算法的1.41.351.31.251.21.151.10 5 10 15 20 25 30 35处理器见图7。GDE方案相对于IBM 1350 Linux集群上的静态分区算法的加速。相对于静态分区算法的2.42.221.81.61.41.210 2 4 6 8 10 12 14 16处理器见图8。GDE方案相对于NOW架构上的静态划分算法的加速。图10（a）显示了在IBM集群上使用32个处理器时应用GDE负载平衡算法后每秒的队列状态。与图1（a）相比，使用GDE负载平衡算法有很大的不同。更多的处理器在整个验证过程中有状态要扩展。此外，每种情况下拍摄的快照数量表明，验证模型只需要一半的时间约旦原子Atomix密集缓存315142女王8加速比加速比R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）1929相对于静态分区算法的1.81.71.61.51.41.31.21.110.90.80 10 20 30 40 50 60 70处理器见图9。GDE方案相对于共享内存架构上的静态分区算法的加速。32个节点中平衡队列的队列占用率12000100008000600040002000GDE负载均衡算法的聚合次数706050403020100 10 20 30 40 50 60 70 80 900时间（秒）（一）CPUSG功能（b）第（1）款空闲见图10。此图显示了jordon模型在模型检查期间每个函数的队列不平衡和聚合时间（a）负载平衡后使用32个处理器的jordon模型的队列大小，显示了平衡的队列（b）实现GDE负载平衡方案后每个函数的聚合时间，显示了低空闲时间。彻底图10（b）显示了并行模型检查器中主要模块所花费的时间百分比。与图1（b）相比，我们可以看到，由于负载平衡，空闲时间从总时间的35%减少到几乎没有，并且由于额外的通信以提高性能，CPU时间增加了。约旦原子国加速比百分比030R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）19排队状态x 10568个节点的每个节点的队列占用率x 10468个节点的负载均衡队列占用率5 54 43 32 21 10020040060080010001200140016001800时间（秒）00 200 400 600 800 1000 1200时间（秒）(a)（b）第（1）款见图11。NOW架构上的jordon模型的平衡和不平衡队列（a）负载平衡之前使用8个处理器的jordon模型的队列大小。(b)使用8个处理器的jordon模型在负载平衡后的队列大小，显示高度平衡的队列。图11（a）示出了负载平衡之前的队列状态，图11（b）示出了NOW架构上负载平衡之后的队列状态。对于该特定示例，使用更高的平衡频率来实现更好的平衡。从图中可以看出，使用更高的频率在参与队列中创建了近乎完美的状态分布。在这种情况下，实现了1.6的加速比。并行验证算法的搜索顺序被显著修改。使用静态分区算法，涉及到一定程度的确定性，因为特定的状态保证在特定的进程上处理，并且每个错误状态或死锁状态总是在同一个处理器上发现。由于GDE将队列中的状态从一个进程转移到另一个进程，因此最初在特定队列中的状态可以转移到另一个队列;因此，与静态分区算法相比，它会导致错误和死锁状态在不同的处理器上被发现，并且顺序不同。结果是，平均而言，状态的shuing导致错误状态和死锁状态比静态分区算法更早地被发现。此外，如果错误状态恰好位于一个非常不显眼的位置，在队列中shu标记状态可以帮助并行算法更早地发现错误。表1显示了在使用8个处理器的有错误的模型上运行负载平衡算法和静态分区算法所收集的结果。在发现错误状态之前，报告每个算法生成的状态数。ratio列是静态分区算法中保存的状态数与使用GDE保存的状态数排队状态R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）1931表1在发现错误状态之前生成的状态的平均数模型静态分隔GDE算法比queens8-deadlock2254650045.09adash12121765085002.08Jordon660038601.71queens 8-错误15050869623431.56仲裁员4441633001.34疏浅31640626258668031.22atomix215068819835501.08两颗钻石228037621569131.06算法一个包含不明显错误的模型的明显例子是皇后问题。8皇后问题是指在棋盘上放置8个皇后，使得没有一个皇后会威胁到其他皇后。错误状态是以所述方式成功放置所有皇后。静态划分算法的性能优于串行算法，但GDE负载均衡算法优于这两种算法。即使在其他模型中，我们也可以看到负载平衡算法的性能比静态分区算法高出一个显著的因子，最坏情况下的性能只比静态分区算法略好静态分区算法的一个主要挑战是由于单个处理器的队列中缺乏可用空间而导致验证的在具有高分支因子的超大型密集模型中，每个处理状态都会生成大量必须保存在队列中的后继状态。如果队列没有分配足够的内存来容纳这些状态，则必须中断验证过程，并且验证无法完成。由于处理器的队列中的高负载不平衡，也会出现队列中的大量状态。通过主动调度使排队系统处于平衡状态. GDE负载平衡算法，它隐式地使队列更小，更易于管理;因此，它减少了每个处理器对队列的繁重内存需求。表2显示了在验证中使用8个处理器的各种模型的每个算法的最大队列大小，以及静态分区和GDE负载平衡算法的每个处理器上的最大队列大小内的标准差。从表中我们可以看出，静态分区算法和GDE负载平衡算法之间存在很大的差异。对于负载均衡算法，最大队列大小几乎比静态划分算法的最大队列大小小一个数量级，32R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）19表2最大队列长度和最大队列长度的标准差模型最大队列大小比标准偏差静态分隔GDE静态分隔GDE密集3522263082411.43139137575Jordon511934543879.41183442249两颗钻石389792483518.06118165149疏浅377491804164.69117099855atomix239938622613.8576428319女王815878764185893.792353352679高速缓存315142289803974922.9799843579用于队列分配器的内存的比例相同。每个算法的最大队列大小的标准偏差显示在表2的最后两列中。对于静态分区算法，我们可以看到，与最大队列大小相比，标准差非常大。 相比之下，GDE负载平衡方案提供低得多的标准偏差，表明队列处于平衡状态。使用GDE作为负载平衡技术会产生通信开销表3比较了使用静态分区算法（状态缓存为100k）和优化负载平衡算法（状态缓存为100k）进行验证时，任意两个处理器之间发送的平均消息数从表中我们观察到，对于模型缓存，atomix和dense，在负载平衡版本中发送的消息数量少于静态分区算法中交换的消息数量。这是由于状态缓存。对于其他情况，在负载平衡版本中发送的消息数量更大，但数量级相同。最后一列以相对于发送的较高邮件数的百分比形式显示差异我们可以看到，在最坏的情况下，只有多发送10%的消息才能实现1.6倍的加速。这种通信开销是可以接受的，因为它为我们提供了平衡的队列，更小的队列，并提高了模型检查器的错误检测能力。6结论和今后的工作从上面的讨论中，我们可以突出一些主要的兴趣点。使用静态划分算法的并行模型检查器由于主要与划分功能和通信方案相关的各种因素而具有一定的不确定性。我们已经证明，使用静态分区算法，每个进程上的队列是高度不平衡的R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）1933表3两个处理器模型静态分隔GDE算法百分比atomix276751.41254148.7-8.17密集324927.66320916.58-1.23高速缓存315142350984.19349259.3-0.49Jordon621258.95632280.921.74稀疏浅层993826.051032035.143.7女王8242680.2254276.524.56两颗钻石994516.561112782.9710.63并且验证期间的有效处理器数量是实际参与验证的处理器数量的一半。我们还表明，使用状态缓存在静态分区算法的加速方面使用负载平衡技术，如GDE，我们已经成功地平衡了所有处理器上的队列，并减少了在我们的基准测试套件中验证模型的时间。由于GDE负载平衡算法的不确定性，我们还改变了搜索顺序，使我们的模型中的错误状态可以更早地被发现，并通过探索更少的状态。使用GDE负载平衡算法，我们还表明，最大队列大小已减少了一个数量级相比，在静态分区算法中获得的最大队列大小，我们使用的模型和基准套件。我们还表明，使用状态缓存时，通信开销不会抵消GDE负载平衡在这一研究领域的未来工作将涉及创建完全独立于任何用户输入有关的频率负载平衡的负载平衡方案。处理器应该能够避免没有有用的工作要做的情况一个更详细的研究GDE计划相对于一对处理器之间完成的负载平衡量也很重要。其他动态负载平衡方案也提供了进一步研究的有趣领域。引用[1] 验证与确认实验室模型数据库。http://vv.cs.byu.edu网站。[2] G.贝尔曼 分布式时间自动机可达性分析之效能研究。 在电子笔记在理论计算机科学，卷68。 Elsevier，2002年。[3] E. M. Clarke，T. Filkorn和S. Jha.时序逻辑模型检验中的对称性利用。34R. Kumar，E.G.Mercer/Electronic Notes in Theoretical Computer Science 128（2005）19在第五届计算机辅助验证国际会议的会议记录中，第450- 459462. Springer-Verlag，1993.[4] C.德马丁尼河Iosif和R.西斯托dSPIN：SPIN的动态扩展。在SPIN，第261[5] O. 格伦贝格湾M. 小克拉克和D.A. 佩尔德。模型检查。第9[6] P. Godefroid和P. Wolper。使用偏序来有效验证死锁自由和安全属性。第三届计算机辅助验证国际研讨会论文集，第332-342页。Springer-Verlag，1992.[7] G. J. Holzmann 。 位状 态散 列分 析。 在 Proc. 15th Int. Confon Protocol Specification ，Testing，and Verification，INWG/IFIP，pages 301-314，Warsaw，Poland，1995中。查普曼和霍尔。[8] G. J. Holzmann。 模型检查器旋转。 IEEE Trans. Softw. Eng. ，23（5）：279[9] M.琼斯，E。Mercer，T.鲍河，巴西-地Kumar和P. Lamborn。对显式状态并行模型检查器进行基准测试。在理论计算机科学电子笔记，第89卷。Elsevier，2003年。[10] R.库马尔，M。Jones，J. Lesuer，and E.默瑟探索料斗中的动态分区方案。技术报告3，验证和确认实验室，计算机科学系，杨百翰大学，犹他州普罗沃，2003年9月。[11] F. Lerda和W.维瑟解决程序模型检查的动态问题。 计算机科学讲义，2057：80[12] D. M. Nicol和G. Ciardo.离散状态空间生成的自动并行化。Journal of Parallel and Distributed Computing，47（2）：153[13] 联合Stern和D. L.迪尔通过Hash Compaction改进概率验证。在Correct Hardware Design andVerification Methods，第987卷，第206史普林格出版社[14] 联合Stern和D. L.迪尔 对Murphi验证器进行验证。 第256-278页[15] M. H. Willebeek-LeMair和A. P·里夫斯高度并行计算机上的动态负载平衡策略。IEEETrans.并行分布系统，4（9）：979[16] C. Xu和F.刘 多机系统中的迭代动态负载平衡
我的内容管理
展开
