共享内存并行CTL*模型检测

理论计算机科学电子笔记128（2005）107-123www.elsevier.com/locate/entcs共享内存体系结构上的CTL* 模型检测Cornelia P. Inggs科妮莉亚·英格斯1，2 和霍华德·巴林杰3曼彻斯特大学计算机科学系英国摘要在本文中，我们提出了一个并行算法的CTL* 模型检测的虚拟共享内存的高性能并行机结构。该算法是自动机驱动的，并遵循一个游戏的方法，其中一个玩家获胜，如果自动机是空的，而其他玩家获胜，如果自动机是非空的。我们展示了如何使用动态负载平衡技术在处理器上划分工作，可以并行玩这个游戏。性能图说明了算法的实用性和有效加速比。保留字：模型检测，共享内存，并行化，自动机，博弈论1介绍模型检查是一种用于自动验证设计的成熟技术，现在被工业界采用来检查许多关键系统的正确性属性在过去的十年中，在开发专门的状态编码和算法以减少这种验证方式所固有的状态爆炸问题的负担方面取得了巨大的进步，这对这种工业采用至关重要即便如此，1这项工作得到了英国大学ORS奖、曼彻斯特大学计算机科学系奖学金和南非哈里·克罗斯利奖学金的全力支持。2inggscp@telkom.co.za3howard@cs.man.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.022108C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）107可验证的系统仍然受到时间和可用内存的严重限制，开发缓解状态爆炸问题的技术仍然是一个活跃的研究领域。最近引起极大兴趣的一种技术是模型检查的并行化。在20世纪80年代和90年代，有一些关于模型检查器并行化的独立出版物，然后Stern和Dill在过去的三到四年中，并行模型检测得到了相当大的兴趣。现有的研究主要集中在分布式网络上的实现和静态划分函数的开发上。静态分区函数依赖于状态，而不是工作负载的分布。据我们所知，使用动态分区函数的唯一算法是Heyman等人的符号算法[12]和基于Heyman等人的两种算法s article [3，11].在这些算法中，每当内存变得不平衡时，通过重新划分状态空间来保持内存平衡。最初只有安全检查是并行的，但在过去的几年里，活性检查的并行算法的发展增加了，检查LTL [2，6，16，15]，CTL [7]和μ-演算[5]的算法见[13]，为一个完整的参考书目。有效的活性检查并行算法的发展一直不如安全检查和非常少的并行算法检查活性和安全性能实现加速比。我们探索了共享内存多处理器计算机模型检查的并行化，特别是，显式状态上的并行化的模型检查的安全性和活性属性进行了研究，并导致CTL* 的并行模型检查器的发展。该研究表明了使用共享内存结构的模型检测的实用性和有效的加速并行算法的性能进行了评估，通过理论分析，也通过实验分析，使用了一些典型的模型，包括并行模型检查器本身的正确性属性。在我们早期的论文[14]中，我们提出了一种在共享内存架构上进行可达性分析的并行算法。在本文中，我们提出了一个并行模型检查算法的CTL*，使用动态负载平衡技术的并行可达性分析算法中描述的[14]。下一节将概述并行可达性分析算法接下来是描述串行自动机驱动的CTL*的博弈论算法及其在第3节和第4节中的并行化。C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）107109该算法的性能进行了分析和讨论，在第5节和结论在第6节。2并行可达性分析我们的并行可达性分析算法是在N个进程上执行的，每个进程（控制线程）在一个物理处理器上运行。所有N个进程共享一个存储器用于存储访问状态，每个进程都有自己的无界私有堆栈和有界共享堆栈用于存储未扩展状态。一个进程只能将状态添加到它自己的私有和共享堆栈中，但是当它自己的私有和共享堆栈为空时，它可以窃取一个状态，即，从另一个进程的共享堆栈中删除状态。1进程队列到达（initState）2开始平行3if（procid = 0） thennext：= initState;4elsenext：= EMPTY; endif;5做6if（next = EMPTY） thennext：= PopFromStack（）; endif;7if（next/=EMPTYt）hen8System. out. println（）;9其他10System. out. println（）;11结束;12while（i）;13端部平行;14结束过程Fig. 1.一种并行可达性分析算法图1给出了并行可达性分析的伪代码。每个参与进程在开始并行指令和结束并行指令之间执行代码的副本通过Dijkstra等人的低开销的基于令牌的算法和用于计算的伪代码来检测终止后继者，PopFromStack和PushOnStack在附录中给出每个共享堆栈都有一个锁来同步对它的读写访问，但是存储，一个哈希表，没有互斥锁来同步访问。当多个进程创建相同的状态时，这可能会导致重复工作，但由于可用的并行计算比自然并行任务多得多，执行冗余工作并不是一个显著的开销。然而，人们发现，很少有工作是重复的。例如，当模型的并行模型检测算法在本文中所描述的110C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）107×∈›→检查了8个处理器上的死锁自由度，访问了780多万个状态，只有6个状态重复。3AltMC：一个基于交替自动机和博弈论的模型检测问题可以表述为：给定Kripke结构K和时序逻辑公式φ，确定K| = φ。形式上，Kripke结构是一个四元组K=（S，R，s0，L），其中S是一个有限的状态集，RS×S是一个必须是全的转移关系（对于每个si∈S，至少存在一个sj，使得（si，sj）R），s0是初始状态，并且L：S2P将每个状态映射到一组原子命题，状态已经开发了几种方法来解决模型检测问题。本文描述的算法遵循自动机驱动的方法，该方法基于以下原则：公式φ可以转换为接受φ的模型集的自动机Aφ，并且Kripke结构K可以被视为自动机。 模型检查器然后构造乘积自动机AK，φ=K×Aφ，如果AK，φ非空，φ对K成立，否则不成立[18，4]。在我们的背景下，用犹豫交替自动机[4]表示分支时间时态逻辑CTL* 中的公式，并用一个称为非空性博弈的博弈公式化了乘积自动机Aφ的构造及其非空性检验[19]。作为简要介绍，有限树上的自动机（树自动机）运行在无符号标记的树上，其中符号是有限字母表。交替自动机A在树T上的游程r是这样一棵树，其根标记为（s0，q0），每隔一个节点标记为（N<$S）4的元素。每个r的节点对应于T的节点。r中的节点（x，q）对应于状态q中的自动机读取T中的节点x。注意，r中的许多节点可以对应于T中的同一个节点。节点及其后继节点的标签必须满足转移函数。如果游程r的所有无限路径都满足接受条件，则游程r是接受的。请注意，当在transition函数中读取true或false时，我们可以在树中获得表示运行的有限分支。在接受运行中，只有在有限分支的末尾才能找到true。不 同 类 型 的 交 替 自 动 机 有 不 同 的 接 受 条 件 。 在 犹 豫 变 换 自 动 机（HAAs）中，接受条件是一对状态（G，B），它们的满足取决于对转移的下列限制[4]在这 里，树被建模为N个N的子集，其中每个N的序列通过其路径名唯一地标识树的节点。C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）107111∈ ∈∈公司简介兰迪波特游戏达到一个假的游戏达到一个真正的在港口移动后，它在当前游戏中 处 于 一 个 位 置 ， 并 且 inf（play）G=在波特移动后，它在当前打法中的位置和f（play）中的位置是G/=在布兰迪的一次行动后，访问当前play中的一个位置，并且f（play）中的一个位置为B/=在布兰迪的一次行动后，访问当前游戏中的位置，并且inf（play）B=表1非空博弈中一局的获胜条件HAA的结构：HAA的集合可以划分为不相交的集合Si，并且集合之间存在偏序≤。 这些集合可以进一步分类为瞬时的、存在的或泛的，使得对于每个Si，以及对于所有s Si，a ∈ i，k ∈ i，（1）如果Si是瞬时的，则δ（s，a，k）（δ是HAA的转移函数）不包含来自Si的元素;（2）如果Si是存在的，则δ（s，a，k）仅包含析取的re-sort-sort-（3）如果Si是泛的，则δ（s，a，k）只包含Si的合取相关元. 从HAA的这种限制性结构可以得出，每一条无限路径π都会被困在一个存在集或全称集Si中。路径满足（G，B）当且仅当Si是存在的且inf（π）G= 或S i是泛函数且inf（π）B=，（inf（π）是在路径π上无限重复的状态集合）。检查HAAφ和Kripke结构K的乘积的非空性可以定义为一个两人博弈，其中参与者1（Brandy）试图表明交替自动机是空的，而参与者2（Port）试图确定它是非空的。博弈的一个过程是一个可能无限的位置序列（s0，q0），（s1，q1），. . ，其中每个位置是Kripke结构和公式的交替自动机的乘积（在下文中称为与或树）中的一个节点与或树的结构决定了哪一个玩家下一步行动。当在游戏中发现标记为真（Portwins）或假（Brandy wins）的节点时，或者当重新访问当前游戏中的位置时，即，当找到无限路径时，然后考虑接受条件以确定游戏的获胜者。病例总结见表1。串行实现使用深度优先搜索（DFS）算法和堆栈来存储当前路径。一条无限的道路，112C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）107在堆栈上的位置被重新访问的深度和堆栈的当前深度之间的元素。为了提高效率，存储库跟踪已经进行了所有移动的状态的结果，以便当重新访问这些结果时，可以重用这些结果，但是随后可能发生的是，错误的结果可能会被重新使用。因为每当位置被重新访问时，播放被截断。为了确保结果在存储时是正确的，一旦从该状态开始的所有移动都已经进行，则针对该状态进行新的游戏。这款新游戏使用了新的结果存储和堆栈，因此在上一次游戏中可能被截断的任何无限游戏现在都可以完成。新的博弈可以递归地进行，因此为了确保终止，新的博弈不会从已经在进行新博弈的状态进行。一旦一个州的新游戏完成，新游戏4PMC：一种基于交替自动机和博弈论的在串行算法中，非空博弈是沿着由串行可达性分析算法创建的DFS路径进行的。在并行算法中，使用第2节中描述的并行可达性分析算法进行非空博弈。后一种选择有两个后果。首先，在并行分析中，与或树不再像串行情况那样以深度优先的方式进行探索。相反，未展开的位置从堆栈中删除，因此可以是与或树中任何位置的随机位置。因此，在任何一点上，一组路径，每个在一个可能的不同阶段的代同时探索。第二，由于没有单一的堆栈，位置被添加到存储器中，当它们被生成时，这样其他进程就可以检测到访问过的位置。这意味着，当流程重新访问某个位置时，它仍然应该确定重新访问该位置是否关闭了一个周期。进一步的含义是，一个进程可以到达一个旧的位置，而另一个进程仍然忙于计算它的结果。当到达旧状态sold时，进程可以继续计算旧状态的结果，从而复制第一个到达sold的进程的工作，或者sold可以跟踪等待其结果的所有位置，并在确定获胜者后将结果转发给它们。我们实施了后者。我们需要考虑的另一个问题是重用游戏结果对最终获胜者的影响。回想一下，当到达真或假终端状态时，或者当重新访问当前路径上的位置时（找到无限次播放当一个进程到达C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）107113一个终端真或假状态，它可以立即存储结果，并将结果转发给该位置的前任。当一个进程重新访问一个位置，并且位置的结果未知时，算法必须首先确定它是否在无限次游戏中，如果是，则是Brandy还是Port在游戏中获胜。这两个目标都是通过从旧状态玩新游戏来实现的。为了避免重复工作，只有在没有其他进程正在从旧状态玩新游戏的情况下，才从该状态玩新游戏。当进程到达旧位置Sold，同时扩展位置Spre，并且另一进程当前正在玩来自Sold的新游戏，则将Spre添加到Sold然后，一旦新游戏完成，结果将被转发到spre。新的游戏是在一个处理器上本地进行的，因此可以进行第3节中描述的串行非空游戏。请注意，只有来自完成的本地新游戏或终端真或假状态的结果才被存储和重用。由于这些结果是正确的，因此不需要进一步的新游戏。在并行模型检测算法中，博弈逻辑嵌入在第3节中描述的并行可达性分析算法中。并行可达性分析算法分为三个步骤：（1）空闲-在平行的非空博弈中，除了两个例外，执行相同的步骤堆栈现在存储工作项而不是状态，并且在步骤（3）中执行的操作现在取决于工作项。有四个可能的工作项：Expand、Play、Result和除了第8行之外，并行非空博弈的主程序逻辑的伪代码与图1中的并行可达性分析算法相同。 在并行非空博弈中，程序ComputeSuccessors在第8行中，由Procedure ProcessWorkItem替换。的伪代码这些功能在附录中给出ProcessWorkItem对不同工作项执行的操作是：Expand Expand在交替自动机表中扩展表达式，该表达式对应于当前交替自动机状态和当前Kripke状态下的命题的真值;Play通过将新的交替自动机状态与当前Kripke状态的所有后继者组合来在乘积自动机中移动;Result存储当前乘积状态的结果，然后将结果转发给等待该状态结果的前导列表中的所有状态;在玩完新游戏之后，将创建一个Result工作项。114C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）1074.1正确性并行算法的正确性已通过首先建立串行和并行算法将构造同构的与或图来证明。然后证明了对于给定的Kripke结构和CTL* 公式，串行非空博弈和并行非空博弈将从HAA的初始位置确定相同的赢家，通过证明串行非空博弈和并行非空博弈将确定特定路径的相同赢家，串行非空博弈和并行非空博弈将确定与或树中特定位置的相同赢家，存储的结果可以重用，并且并行算法中的结果转发是正确的PMC的并行算法的其他属性，例如免于死锁，已经通过使用SPIN和PMC本身来验证[13]。5性能理想情况下，在一个处理器上以时间TS运行的算法将在P个处理器上以时间TP=TS/P运行。不幸的是，TP几乎总是大于TS/P，因为在多个处理器上执行代码涉及额外的开销更准确地说，TP=TS/P+θP，其中θP是开销项，是实际执行时间和理想执行时间之间的差异[1，8]。有几个并行化成本占开销。第一个是θIP，它是由于并行性不足而产生的开销。并行算法通常具有不能并行运行的顺序组件，例如算法的组合启动和整理时间。这种开销通常被称为Amdahl第二个成本θSched是调度开销;这是每个线程在并行部分开始时执行调度代码所需的时间。第三个成本θLI是负载不平衡的结果。第四个成本θSync是同步开销;例如，它考虑了获取或释放锁所需的时间。最终成本θUnknown是指在其他方面没有考虑的额外开销，例如内存访问时间。因此，算法在P个处理器上运行的时间可以给出为：TP=TS/P+θIP+θSched+θLI+θSync+θUnknown不同开销的值可以通过对1个进程执行可达性分析并使用高分辨率计时器来测量执行不同代码块所需的时间来测量。然后可以计算P= 1至16的TP值，以预测算法的性能。C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）107115Rithm。然后可以将其与实验期间的TP测量值进行比较。并行算法的性能可以通过绘制1/TP与进程数P的关系图来可视化。这些性能图的优点在于，它们提供了并行算法的可扩展性的可视化表示5.1理论与实验性能为了对并行可达性分析算法的理论性能进行建模，测量了并行算法的开销值，并考虑了两个不同的模型：模型A，其捕获算法的最佳可能行为，其中没有空闲时间;模型B，其捕获最坏情况的场景，其中状态的窃取必须与对同一共享堆栈的其他访问同步，并且每次进程想要窃取状态时，它必须等待所有其他进程获得并释放锁，然后才能访问共享堆栈。型号A和型号B的性能曲线如图所示凌晨2图2a中的第三个性能图显示了算法的真实性能;性能图是从实验结果中获得的，这些实验是在分支度为3的1亿个状态图上运行的，以确定可达性分析的时间。对于每个P值，可达性分析执行十次，图2a中标记为实数的性能图显示了每组十次运行的平均值。规则间隔的垂直线显示了在相应过程上运行十次期间获得的最快和最慢结果。取多次运行的平均值，因为存在许多影响运行时间的变量，例如，由高速缓存争用推断的高速缓存行使用的不可预测性，以及进程获得对共享堆栈的访问的对结果的分析表明，平均值已稳定在其十次运行内。并行算法的性能非常好，并且随着处理器数量的增加而扩展该实现需要approxi-100万个状态图上的一个进程和大约20秒的16个进程上完成的可达性分析分钟。模型B示出了与实现算法的实验结果类似的行为，如果其空闲开销被改变以模拟这样的场景，其中想要窃取状态的进程在其获得对共享栈的访问之前必须仅等待另一个进程完成对共享栈的单次访问。116C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）1070.070.060.050.040.030.020.01(a) MSMP：1亿个州1.210.80.60.40.2(b) 多个共享多个私有堆栈（63 423）02 4 6 8 10 12 1416数量的处理器02 4 6 8 10 12 14 16数量的处理器图二.（a）探索1亿个状态图的理论与实际性能（b）检查并行可达性分析算法的ESML模型5.2ESML模型的实验性能为了评估模型检查器在真实模型上的性能，PMC与ESML的状态生成器集成，ESML是一种类似Promela的建模语言[9]。图图2b示出了在第2节中描述的并行可达性分析算法的ESML模型的死锁检查性能，图3a示出了通信模型的活性属性EFAGp图7和图8给出了更多的图表。8 .第八条。对于使用并行模型检查器检查安全属性，有效地产生与并行可达性分析相同的加速。然而，这些属性通常在整个状态图被搜索之前被满足或被违反，并且也可以在不同路径上的不同深度处被满足。并行算法也倾向于找到比具有顺序DFS算法的模型检查器更短的路径。对于检查活性属性的结果有所不同，但当有一个加速活性检查也扩展以及处理器数量的增加。活性检查比安全检查需要更多的工作（更长的独立工作），但需要额外的同步来存储检查周期所需的信息然而，较长的独立作业的效果超过了额外同步的效果，并且通常比安全检查获得更好的加速进一步发现，活性检查性能的变化通常高于安全检查，因为访问州的顺序也与何时以及从哪个州进行本地游戏有关。在某些情况下，这种差异特别大。 作为示例，在图3b中描绘了当检查生产者-消费者模型的活性属性AGEFp例如，在六个处理器上，在最慢运行期间访问了4000个州（不包括在本地比赛期间访问的州）后，在36秒内检查了属性，房模型最恰当的模型最差1/时间1/时间C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）1071170.160.140.120.10.080.060.040.020(a) 通信模型：Checking EFAGP02 4 6 8 10 12 1416数量的处理器0.80.70.60.50.40.30.20.10(b) 生产者消费者模型：检查AGEFp02 4 6 8 10 12 14 16数量的处理器图三.检查（a）通信模型的EFAGp和（b）生产者-消费者模型的AGEFp在以最快速度访问了250个州之后。所玩的本地游戏的数量也对模型检查器的性能有影响，并且对于特定的活性属性，取决于所检查的模型。 通常，与为模型生成的有限状态机的状态总数相比，需要进行大量的局部博弈。这会导致一些进程忙于玩本地游戏，而另一些进程则没有工作，然后在玩本地游戏时长时间处于空闲状态;见图10。8d.6结论我们的第一个目标是评估并行模型检测在共享内存架构上的可行性加速比良好，动态负载平衡算法有效;除了当局部游戏的数量与全局状态的数量相比很高时，实际上不存在由于不平衡负载而导致的空闲时间。第二个目标是确定任何陷阱时，并行模型检查共享内存架构。发现的主要缺陷是同步开销和错误共享（见图9），当两个或多个处理器试图写入同一缓存行中的不同字时，会发生这种情况。为了提高效率，应该小心使用互斥锁，并且应该分配内存以避免错误共享对于未来的工作，我们计划实现一个改进的算法，重新使用本地游戏的所有中间结果，以避免冗余，并提供更快的工作。更一般地说，我们还确定了对基准模型的需求，并对串行状态空间缩减技术与并行算法的集成进行了全面调查1/时间1/时间118C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）107确认除了我们的赞助商之外，我们还要特别感谢计算机科学系的CNC（新计算中心），他们对并行化方法和实现进行了有益的讨论，并专门访问了他们的SGI Origin 3400机器。引用[1] M. K. Bane和G. D.莱利扩展的开销分析。计算机科学讲义，2400：162[2] J. 巴尔纳特湖 Br im，andJ. 是的。 D是S P IN中的DLTLmodel-checking。第八届SPIN软件模型检测国际研讨会论文集，计算机科学讲义第2057卷。Springer–Verlag, May[3] S. Ben-David，T. Heyman，O. Grumberg和A.舒斯特可扩展的分布式在线符号模型检查。第三届计算机辅助设计形式方法国际会议（FMCAD'00），第390-404页，德克萨斯州奥斯汀，2000年11月[4] O. 伯恩霍尔茨分支时间时序逻辑的模型检测。博士论文，以色列海法理工学院，1995年6月。[5] B. Bollig，M. Leucker和M.韦伯无交替μ演算的局部并行模型检验。在Proceedings of the 9thInternational SPIN Workshop on Model Checking of Software （ SPIN 2002 ） ， LectureNotes in Computer Science，Grenoble，France，April 2002。史普林格出版社[6] L. 布林岛 Cern'a，P. 克雷奇阿尔河。 Pel'an ek. D 是TRIBUTLMD-ChekingaseDonegativecycledetection.计算机科学讲义，2245，2001。[7] L. Brim，J.你好啊，还有K。 Y或V。使用大量的数据是非常困难的。在Proceedings of the1st International Workshop on Parallel and Distributed Model Checking（PDMC 2002），pages 80[8] J. M. Bull.并行程序中开销的一种层次分类。在重症杰利岛Gorton和P. Croll，编辑，第一届IFIPTC 10并行和分布式系统软件工程国际研讨会论文集，第208-219页。查普曼大厅，1996年。[9] P. J. A. de Villiers和W.维瑟并发系统的验证语言在第七届南部非洲计算机研讨会论文集，第59[10] I.福斯特设计和构建并行程序。Addison-Wesley，1995年。[11] O. Grumberg，T. Heyman和A.舒斯特分布式符号模型检验的μ演算。In G.贝里，H。Comon，和A. Finkel，编辑，Proceedings of the 13th International Conference on Computer AidedVerification（CAV 2001），卷2102计算机科学，第350[12] T. Heyman，D.盖斯特岛Grumberg和A.舒斯特在超大型电路的并行可达性分析中实现可扩展性。以. P. Sistla E. A. Emerson，编辑，Proceedings of the 12th International Conference onComputer Aided Verification（CAV 2000），卷1855计算机科学讲义，芝加哥，伊利诺伊州，2000年7月。[13] C. P·英格斯共享内存多处理器上的并行模型检测。博士论文，曼彻斯特大学，曼彻斯特，2004年1月。C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）107119[14] C. P. Inggs和H.巴林杰共享存储器体系结构上模型检查的有效状态探索。并行和分布式模型检查研讨会（PDMC'02），理论计算机科学电子笔记（ENTCS）第68卷，捷克共和国布尔诺，2002年[15] P. Krca'l.D是一种特殊的、有约束力的LT L模型。 在洛 Br imandDO. Grumberg，编辑，Proceedings of the 2nd International Workshop on Parallel and Distributed ModelChecking（PDMC 2003），第89卷，Electronic Notes in Theoretical Computer Science，Boulder，Colorado，2003年7月。爱思唯尔[16] A. L.拉丰特通过局部化循环简化分布式LTL模型检验。报告00176，In stititutfur？r In fourrm atik，Univerer sit？tFreiburg，2002年7月。[17] 联合Stern和D.迪尔将Murφ验证器标记化。号手术 Grumberg，编辑，Proceedings of the 9 thInternational Conference on Computer Aided Verification（CAV[18] M. Y. Vardi 和P. Wolper 。自动程序验证的自动机理论方法。 在Proceedings of the 1stSymposium on Logic in Computer Science，第322-331页，1986年。[19] W. Visser 和H. 巴林杰实际 CTL 模型 检查：是否应该SPIN 延长？Software Tools for Technology Transfer，2（4）：350120C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）1077附录1进程队列到达（initState）2开始平行3if（procid = 0） thennext：= initState;4elsenext：= EMPTY; endif;5做6if（next = EMPTY） thennext：= PopFromStack（）; endif;7if（next/=EMPTYt）hen8System. out. println（）;9其他10System. out. println（）;11结束;12while（i）;13端部平行;14结束过程1过程计算后继程序2对于所有的后继者tofs都是3如果（t是新的），则4return（t）;5如果（t是第一个后继者），则s：= t;6int n（t）;7结束;8endforall;9结束过程见图4。 过程EQUELREACH和EQUELREACH1步骤PopFromStack（s，id，privstack）2if（ notempty（privstack）） then3publicint findDuplicate（）;4结束;5if（s = EMPTY notempty（sharedstacks[id]））then6int n = nums（nums）;7sort：=sort（sort）;8return[id];9结束;10while（s = EMPTY more shared stacks to check）执行11id：= next processor;12如果notempty（sharedstacks[id]），则13int n = nums（nums）;14sort：=sort（sort）;15return[id];16结束;17最后;18结束过程1程序PushOnStack（s，id，privstack）2if（ notfull（sharedstack）） then3int n = nums（nums）;4Push（s）;5return[id];6其他7Push（s）;8结束;9结束过程1方法：initState（initState）2开始平行3if（procid = 0） thennext：= initState;4elsenext：= EMPTY; endif;5做6if（next = EMPTY） thennext：= PopFromStack（）;endif;7if（next/=EMPTYt）hen8System. out. println（）;9其他10System. out. println（）;11结束;12while（i）;13端部平行;14结束过程1程序ProcessWorkItem（下一个）2开关（下一个类型）3案例分析：4return next;5voidrun（）;6案例扩展：7int n =int n（int n）;8病例结果：9return next;10next：= EMPTY;11System. out. println（）12案例13System. out. println（next）;14终端开关;15结束过程图五.过程BELELGAME以及BELREACH和BELGAMEC.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）1071211函数SplitAndOr（parent，parentId，altState）2return.altState：=FormulaLeft（）;3int findDuplicate（int findDuplicate）;4return. results =ResultsRemoveFreeSlot（）;5下一个.idCopy：= next.result.id;6AddPredecessor（next，parent，parentId）;7next.result.pos：=ANDORPOS; 89cur.altState：=FormulaRight（altState）;10cur.type：= FormulaLeftQuant（altState）;11cur.idCopy：= cur.result.id;12int n =int nums（）;13int n（int n，int n）;14cur.result.pos：=ANDORPOS; 1516pushOnStack（cur）;17return next;18端函数1920函数Move（cur，next）21开关（下一个类型）22案例AND：23cur.result.resToGo：= 2;24cur.result.andOr：= AND;25next：=SplitAndOr（cur.result，cur.idCopy，cur.altState）;26deadlock：= 0;27病例OR：28/与AND大小写相同，但AND替换为OR/29caseAND−SUCC：30next.result.andOr：= AND31type：= EMPTY;32return（cur，next）;33案例OR−SUCC：34/n与AND −SUCC情况相同，但AND替换为OR −/35终端开关;36结束;37返回死锁;38端函数1Procedure ProcessResult（当前，下一个）2int：= cur.result;3return（int n）;4if（tmp.id = curState.idCopy） then5if（（tmp.andOr = OR Result（cur）= TRUE）6（tmp.andOr = ANDResult（cur）=7return 0;8其他9tmp.result.resToGo−−;10结束;11如果（tmp.result.resToGo≤0），则12if（tmp. po s/=ANDORPOS）t hen13System. out.println（）;14结束;15return TRUE;16结束;17endif;1819如果（向前），那么20if（cur = initial state） then21mcResult：=Result（cur）; terminate：= TRUE;22其他23而NotEmpty（tmp.predecessors）则24int n =int n（int n）;25int findDuplicate（int findDuplicate26if（ Empty（next）） thennext：= cur;27public intfindDuplicate（）;28最后;29网址：tmp.id ++;30结束;31结束;32int n = int n（int n）;33if（forward） then AddSlotToFreeList（tmp） endif;34结束过程见图6。 并行非空对策122C.P. Inggs，H.Barringer/Electronic Notes in Theoretical Computer Science 128（2005）10787.576.565.554.542(a) Gneiss通信模型（2 108个州）2 4 6 8 10 12 1416数量的处理器(c)Gneiss Global Model（55 144 states）21.510.500.05(b) 滑动窗口模型（46 840状态）2 4 6 8 10 12 14 16数量的处理器(d) 餐饮哲学家模型（1 270 080个州）1.510.50.040.030.020.0102 4 6 8 10 12 1416数量的处理器02 4 6 8 10 12 14 16数量的处理器见图7。对四个ESML模型中的每一个进行详尽的可达性分析;请参阅标题以了解每个模型的大小1/时间1/时间1/时间1/时间C.P. Inggs，H.Barringer/Electronic N