没有合适的资源?快使用搜索试试~ 我知道了~
《理论计算机科学电子札记》68卷第4期(2002年)URL:http://www.elsevier.nl/locate/entcs/volume 68. html20页sPetri网规范Alexander Bell和Boudewijn R.哈弗科特1计算机科学德国亚琛工业大学性能评估和分布式系统实验室摘要在本文中,我们提出的算法模型检查CTL的系统指定为Petri网。我们提出了顺序以及分布式模型检测算法。该算法依赖于系统状态空间的显式表示,但不要求转换关系显式可用;它在需要时重新计算。这种方法使我们能够以快速有效的方式对具有数亿个状态的非常大的系统进行模型检查。此外,我们的分布式算法扩展性非常好,因为它们显示出80%到100%的效率。1介绍在过去的十年中,模型检查已经成为一种非常强大的技术,可以自动验证正式指定的系统属性[14,9,13]。在本文中,我们重点使用计算树逻辑(CTL)[8]正式指定系统属性;此外,我们假设感兴趣的系统被描述为一个Petri网。后一种选择对我们的方法来说并不重要,尽管它确实对我们实现算法的方式有影响。当模型检查现实系统时,通常会遇到(至少)两个问题:被建模的系统的状态空间的大小是禁止的,并且检查即使是简单的逻辑属性所需的时间也非常大。虽然已经用符号状态空间表示获得了良好的结果,例如, 使用二元判定图,当与这种符号方法结合使用时,实际的模型检验算法通常变得更慢。 出于这个原因,我们坚持使用基于哈希表的显式状态空间表示;已经取得了非常好的结果。1电子邮件: albe@cs.rwth-achen.de,haverkort@cs.rwth-achen.de2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。贝尔和哈弗科特2”[12]这是他的座右铭 为了解决状态空间爆炸问题,使用多处理器系统或工作站集群也有帮助;这些系统通常拥有非常大的(分布式)主存。此外,这种系统的大计算能力也有助于有效地减少模型检查时间。最近已经报道了使用多处理器系统或工作站集群从高级系统描述生成状态空间(和转移关系)的分布式算法,例如,[15][16][17][19] 然而,所有这些论文都只关注状态空间的生成文献[3]研究了LTL的并行模型检测问题,这是一个不同类型的问题。 在本文中,我们扩展了我们以前的工作[12],并开发了有效的(在计算和通信方面)算法,用于以分布式方式对基于Petri网的模型进行模型检查CTL表达式。对几千万个状态的模型的实验结果表明,该方法可以获得很好的加速效果和效率。本文的其余部分组织如下。在第2节中,我们提出了关于Petri网的基本知识,它们的表示和后继状态和前趋然后,在第三节中,我们简要介绍了逻辑CTL,然后我们提出了顺序模型检测算法的CTL在Petri网在第四节。第5节然后提出了一些分布式算法,用于相同的目的。实验结果在第6节中报告,而第7节总结了论文。2Petri网模型2.1Petri网我们考虑一类简单的Petri网(PN),包括指数延迟转移,抑制弧,以及标记相关的速率和权重。 目前,我们不考虑标记依赖弧多重性,也不考虑立即跃迁;我们稍后再讨论这些。在这里,我们将遵循[11,第14章]。为了描述Petri网模型,我们使用Ciardo等人为工具SPNP定义的语言在本文中,我们没有使用Petri网的随机特性;这是留给未来的,我们将解决随机Petri网的CSL或CSRL的分布式模型检查[2,1]。我们的工具PARSECS(见下文)完全支持Petri网语言CSPL,并被用作在目前的文件中报告PARSECS是用C/C++编写的,并使用MPICH [18]库进行分布式计算。2.2状态空间与可达图生成使用简单的搜索算法,我们可以计算所有可达状态(状态空间S)以及转移关系。这些一起形成(有向)标记可达性图(RG)。我们使用PARSECS状态空间生成器贝尔和哈弗科特3−(ParState-spaceE xplorer and MarkovC hainS olver);它存在于串行和分布式版本中,并且可以在合理的时间内生成具有数亿个状态的状态空间关于这些的更多细节,请参见[12]。在本文的其余部分中,我们假设状态空间已经生成,并且在主存中可用。正如我们稍后将看到的,我们主要对搜索的可能性感兴趣对于一个国家来说,S。由于这个原因,我们决定使用哈希表,这使我们有可能在O(1)中找到一个状态。 给定状态空间S,我们将其存储在大小为N的哈希表中|S|= c·|S|对于一些C > 1。 当我们使用一种技术称为开放寻址的双哈希(参见[16],第6.4节)N|S|必须是一对孪生素数中较大的一 我们的实验表明,对于c = 1,我们可以使用平均不到3次的比较操作在哈希表中找到某个状态(或检查其存在)。2. 这种表示方法远远优于基于树结构的表示方法。2.3后继和前代计算我们可以生成的状态空间的大小受到可用于存储状态空间的内存量的限制转移关系(底层马尔可夫链的生成矩阵)在生成过程中以稀疏矩阵格式写入磁盘。这种转换关系通常比状态空间大得多,并且只允许计算状态的后继,而不允许计算需要矩阵转置的前导。为了节省存储空间,我们决定不使用状态空间生成器中的可达图信息,而是在必要时重新计算后继状态和前驱状态。继承国给定标记m的可能后继状态(标记2)可以通过考虑该标记中的启用转换的集合(通过检查所有转换的启用条件来确定)并且计算如果在标记m中出现的新标记MJ,从PN的语义容易地确定一个特定的变迁t∈T(T是Petri网中所有变迁的集合)火灾。该算法的伪代码在算法1中给出在我们描述计算后继状态的算法之前,让我们介绍以下符号。设ct,p是当转换t触发时,在位置p处的标记上的净效应显然,我们有ct,p=O(t,p)I(t,p),其中O(t,p)是当transitiont触发时在p中生成的令牌数(关联矩阵C=[ct,p]总结了这些值。如果et是一个零向量,在第t个位置有一个1,那么2我们使用状态(表示为s)和标记(表示为m)的术语可互换;当提到标记时,我们以某种方式强调它包括Petri网的所有位置中的标记的数量的事实,因此是贝尔和哈弗科特4∈∈联系我们JJt的触发改变了新标记mJ=m+C·et=m+ct中的标记m,其中ct是与转换t的触发相关联的C中的列。算法1(计算标记m的后继:Succ(m))0. givenm;Succ(m)<$;1. 对于所有t T2. 如果启用,则执行(t,m)3.然后Succ(m)← Succ(m)<${m+ct};4. od;5. intn(n);被继承国在许多应用中,重要的是具有在反向方向上探索转移关系的手段,即,想要知道给定状态m的所有(或一个)前驱状态。当以迭代的方式解决与SPN相关的马尔可夫链时,或者当模型检查下一个和直到操作时([14,8];见下文),会出现这种需求。考虑一个标记m;它是通过触发任何一个转移t∈T从另一个标记到达的。因 此 , 对 于 m的 可 能 的 前 驱 的 集 合 , 我 们 有 : PosPred ( m ) ={m-ct|t∈T}。 这一套可能也是大,有两个原因:(i)对于所有t和给定m,形式为“m-c t“的状态在t未被启用的情况下,使得m不能从它到达。因此,我们认为,我们必须算法2(计算标记m的前驱:Pred(m))0. givenm;Pred(m)<$;1. 对于所有的t∈T2. domJ←m−ct;/*mJ∈ PosPred(m)!* */3.ifmS/* hash table lookup whethermexists at all */4.然后,如果使能(t,mJ),则Pred(m)Pred(m)mJ;5. od;6. returnPred(m);请注意,这个过程几乎和寻找替代者的过程一样便宜。唯一的区别是,我们首先计算可能的前导,检查它们的存在,然后检查它们的启用,而对于寻找后继,我们首先检查启用,然后计算后继。请注意,与后继计算相反,我们需要在计算前导时知道完整的状态空间S贝尔和哈弗科特5∈⊆×2.4简单状态属性简单的状态属性在这里被非正式地定义为简单的逻辑比较。对数字表达式、位置标记和常量的依赖 作为一个例子,设{P1,P2,P3,P4}是给定Petri网中的库所集合,#Pi表示在Pi中的确定标记所对应的个数.简单态性质的例子是:#P1<3,#P2≥(2 × #P4)和(#P1/#P2)<3+2 ×(#P3−#P4)。没有其他理由限制这些简单的表达式,确保当只知道当前标记(状态)时,它们可以被评估为真或假。因此,简单表达式不需要关于后继或前趋状态的信息;它们的值可以被看作与每个状态相关联的原子命题。 我们用空间换取时间,并使用用于存储状态空间(N)的哈希表大小的位向量来存储满足简单表达式的状态集|S|).这意味着我们为每个哈希表条目分配所需的位数请注意,可以考虑专门的数据结构,特别是对于小集合(一些简单的表达式可能会基于树的集合或BDD似乎是合理的替代方案。目前,我们坚持使用位向量表示。3计算树逻辑3.1语法我们考虑CTL的以下语法(摘自[14,第3章])。设AP是原子属性的集合(由2.4节中定义的简单状态属性组成)pAP,则CTL-公式P被定义为(在BNF中):::=p| ¬ϕ|ϕ∨ϕ|EX-2000|E [U] |A [U].其他布尔运算符,如true(tt)、false(ff)和(f)或implica- tion(→),都像往常一样定义。3.2语义我们将检查CTL公式的模型是由高级Petri网描述定义的模型,也就是说,状态集是可达标记S的集合,转移关系RSS完全由Petri网的触发语义定义,并且对应于可达图中的(标记的)边。此外,与每个状态相关联的原子命题是简单表达式在每个状态下是否成立的指示。有关更多详细信息,请参阅第4节。贝尔和哈弗科特6然后,模型检查算法基本上验证以下满足关系|=(对于p∈ AP,CTL公式,s为状态):S|= pi p在s中计算为trueS|=<$i not(s |=)S| = 12i(s|=1)或(s |= 100)S| = EX isJ|对于某些(s,sJ)∈ R,S|=E[1U2]i对于某条路径(s=s(0),s(1),s(2), . . . )的情况下,[i≥0 |=j[0≤j j,那么我们可以将它插入到SatJ(j)中(通过将适当的位设置为true)而不是Snew,并且它的前导序列将在当前迭代中被检查在第6节中给出了该算法的简单和优化实现的结果4.6Modelchecking=A[1U2]对于对于m_n=A[n1U_n2]的m_n的m个单元的改进的计算,我们可以通过构造序列Sat0(n)|Sat1(n)|Sat2(n)|···来与前面类似地 注意到它并不意味着只考虑上一次迭代中新生成的状态;我们必须在每次迭代中重新考虑每个状态。此外,我们必须确保在(E [1] U [2 ])算法的步骤3-6中,仅添加所有后续状态从其导致以下状态的已知满足该性质。关于这个的伪代码,参见算法6。算法6(Backwardcomputationof=A[1U2])0. SatJ()←;Sat()← Sat(2);1. 当SatJ(k)/=Sat(k)时2.doSatJ()← Sat();3.对于所有的s∈Sat(n)4.do for allsJ∈Pred(s) <$Sat(<$)<$Sat(<$1)5.if(Succ(sJ)Sat())6.然后Sat()← Sat()<${sJ};7.f; od;8.od;9. returnSat();贝尔和哈弗科特10/→ {···}i=1步骤1中的集合SatJ(k)和Sat(k)的相等性检查不需要逐元素地进行我们可以只查看元素的数量,以检查Sat(k)是否在上一次迭代中增长在检查sJ的所有后继者是否都满足条件1之前,这是一个昂贵的测试,我们证明sJ不在Sat(条件1)中并且满足条件1。 人们可以看到为什么我们有在步骤5中重新考虑各国每当我们有新的元素在星期六(星期六),这个测试的结果可能会改变。5分布式实现5.1介绍在状态空间生成的分布式版本中,如[12]中详细描述的,使用散列过程将每个状态分配给特定的处理器;该散列函数表示为A:S一、,NoP((假设有NoP处理器)。这样,我们将状态空间存储为一个分区:S=NoPSi。通过选择在分区Si之间均等地分配状态的散列函数,我们同时分配工作要做得均匀。我们使用的哈希函数通常会产生最小和最大分区之间的差异低于5%的分区。产生更均匀的分区大小的分配函数是已知的,但会导致更多的交叉弧,即。例如,特定状态s的后继者sJ=Succ(s)不属于与s(A(sJ)=A(s))。在状态空间生成期间和模型检查期间,大量的R_n_m_e_r都需要通信在所选示例中(见第6节),交叉弧的比例低于30%。所获得的加速比(见第6.3节)表明,没有进一步的负载平衡的战略是必要的。有关状态空间划分的更多详细信息,请参见[4,12]。关于哈希表的大小,串行情况的条件现在对每个单独的处理器都成立在每个处理器中,散列表用于存储分配的状态(以及所有其他所需的信息),就像顺序情况一样。每当我们将状态从一个处理器发送到另一个处理器时,我们使用缓冲器。每个处理器都有一个输出缓冲器(大小在2到4 KB之间)用于其他处理器。一个缓冲器被关闭,即,如果它是满的或者已经达到某个超时值(通常为0.5-2.0s),则它存储的所有状态都被发送到接收处理器。从MPI对receive-function的所有调用都以非阻塞方式实现。这样,我们就消除了死锁的可能性贝尔和哈弗科特11∈5.2一阶逻辑表达式的模型检查简单表达式和一阶逻辑表达式在分布式实现中不构成任何问题,因为为此目的根本不需要通信。所有的处理器都像串行处理器一样,只在状态空间5.3模型检查=EX1对于下一个操作符,我们需要在完整的状态空间上进行一次遍历,在那里我们使用向后过程。原则上,所有NoP处理器都可以并行工作。然而,我们不能在本地计算集合Pred(sJ),因为sJ的前趋者不需要与sJ具有相同的处理器索引。同样,我们必须计算可能包含不存在的状态的集合PosPred(sJ)我们可以通过移除不存在的局部状态,以及可以从不变量或某个地方的已知最小/最大数量的标记中看到不存在的状态,来局部缩小这个集合不能在本地处理的剩余元素sPosPred(s,J)被发送到负责它们的处理器A(s)。如果处理器A(s)接收到一个状态s,它检查这个状态是否存在,也就是说,如果在处理器A(s)的本地哈希表中有一个针对s的条目,则应该设置与节点在此情况下,处理器A(s)不需要回复处理器A(s,J)案子因此,NoP处理器必须考虑与它们的Sat(Sat)部分相对应的它们的本地状态集,以及它们从其他处理器接收的请求。一旦所有处理器都处理完它们的局部集合Sat(n)并且它们的带有请求的输入队列为空,则过程结束。5.4Modelchecking=E[1U2]在评估exist-until-formula时,所有处理器再次自行操作状态空间的一部分当确定前趋状态时,对于下一公式可以发生相同的情况:计算的前趋sJ∈Pred(s)不必由当前前趋处理器处理d,更确切地说,如果A(s)i=A(sJ),处理器A甚至不能决定计算出的状态是否存在,没有因此,它将状态sJ发送给A(sJ),然后A(s j)决定是否存在。如果国家根本不存在,就不需要做任何进一步的事情。如果它exist,则应检查此状态是否是Sat(1)的成员;如果是,则应将其添加到集合Sat(1)中。为了避免无用的通信,如果从发送处理器接收潜在状态的处理器发现接收到的状态不存在,它可以通知发送处理器这个事实。如果那个特定的状态在模型检查过程的其余部分中重新出现,它可以在本地过滤掉。但是,请注意,这确实会消耗内存,贝尔和哈弗科特12当潜在状态在给定处理器中出现至少两次时,支付0。此外,它还需要额外的内存和通信。由于我们预计这一开销将大于节省,我们不进一步考虑这一点。检查某个状态是否存在的另一种解决方案是在每个处理器上使用它的一些隐式重新表示来额外存储完整的状态空间。这将导致这样的情况,即每个处理器可以本地决定每个潜在状态的存在。BDD和MDD表示都满足具有非常低的存储器需求以存储完整的状态空间并允许快速检查状态是否存在的要求。我们将在不久的将来研究这种方法。因此,处理器在集合Sat(k)上迭代,直到该集合不再改变。请注意,Sat(Sat1)的更改可能来自处理器本身,也可能来自其他处理器。如果对于所有处理器,传入队列都为空,并且本地生成的前置队列已被考虑,则程序结束。我们使用环检查来建立分布式终止检测。关于在Sat(Sat)中查找状态的各种实现步骤与下一个运算符相同。5.5Modelchecking=A[1U2]分布式for-all-until检查也基于串行版本。原则上,我们使用算法6,其中每个处理器在其自己的状态空间分区Si上操作,并且具有其自己的局部集合Sati(i),SatJi(i),Sati(i),Sati(Sat2),如算法7所示。终止检查由1号线的环形检查。分布式算法的主要变化位于第4-14行如前所述,我们不能在本地计算状态的前导,所以我们必须对状态s的可能前导进行遍历(第4行)(其中A(sJ)=i)。如果前任是本地州,即,A(sJ)=i,我们检查我们是否还不知道它,以及它是否满足1(第6行)。如果所有这些测试如果Sat(n)成立,我们必须检查是否所有sJ的后继者都属于Sat(n)。我们分两步来做,首先,我们检查是否所有本地后继都属于Sati(i)(第7行),只有当这是真的,我们才检查是否有任何远程后继(第8行)。如果没有远程后继者,我们可以将SJ添加到Sati(i)(第9行),否则我们进行分布式后继者检查(第11行),我们将在下面描述。请注意,我们只有在测试了我们可以在本地检查的所有内容之后才执行此分布式检查如果sJ不是一个本地状态,我们甚至不能检查这个状态是否存在,所以我们将它发送到相应的处理器(第13行),并带有消息标识符msg checkAU。每个处理器周期性地检查接收到的消息。通过消息标识符msg checkAU接收的状态贝尔和哈弗科特13∈∈←∅←联系我们⊆∅∈ ∧∈联系我们⊆∅∈∈ ∧∈∈Algorithm7(对于pr oc,(一)0. SatJi();Sati()Sati(2);1. while(not finished)/* 分布式环校验 */2.doSatJi()← Sati();3.for allsSati(星期六)4.对于所有sJ PosPred(s)5.do如果A(sJ)=i则/*sJ是局部状态 */6.如果(sJ/Sati(n)sJ/Sati(n1)),则7.如果local Succ(sJ)Sati(i),则8.如果remote Succ(sJ)=则9.Sati()Sati()sJ;10.其他11.Distr Succc Check(sJ);12.else/*sJ 不是本地状态 */13.send(A(sJ),sJ,msg checkAU);14.od;15.f; od;16.od;17. returninti(i);算法8中给出的程序这本质上与处理本地状态相同,但我们必须检查接收到的状态是否存在(第2行),而不是检查它是否是本地状态。算法8(处理接收状态-Recv msg checkAU())1. 对于所有sJ2. 如果sJ Si那么/* 这个状态存在吗?* */3.if(sJ/Sati(n)sJ/Sati(n1))4.则如果local Succ(sJ) Sati(k)5.那么如果remote Succ(sJ)=6.则Sati(n)Sati(n) sJ;7.int n= getN(N);到目前为止,构造k=A[k1U2]的离散算法与构造k =E[k1U2]的离散算法相比并不完全相同,但还没有考虑分布式后继校验因此,我们不能只发送状态(ME)-”““忘记他们。为了实现分布式检查,处理器i向负责某些后继的每个处理器j询问是否所有这些后继都是Satj(k)的元素。处理器j必须在每种情况下回答这个问题(真或假)。当处理器i接收到真实答案时,它可以从未回答问题的本地列表中删除相应的问题当去掉关于一个特定状态的最后一个开放问题时,我们知道我们只接收到真s,并且由此,我们可以将SJ添加到Sati(n)。如果我们得到一个false,所有关于原始状态sJ的问题都可以从列表中删除。 如果答案对应于没有问题贝尔和哈弗科特14exists被接收,我们可以把它丢弃,因为处理器i之前收到了一个错误的答案。6实验结果6.1硬件和测试模型我们在亚琛工业大学计算机科学系的集群上进行了实验,该集群由26个双Pentium III(500MHz)Linux工作站组成,每个工作站配备512MB主内存和40GB本地磁盘空间,通过交换式快速以太网(100Mbps)连接。作为案例研究,我们选择了一个取自[7]的看板系统的Petri网模型。该模型的图形表示如图1所示 该模型用初始标记中的四个子系统中的每一个中的令牌的数量N来参数化(在位置P看板i中,i = 1,.,4)。该模型有两种变体,一种是定时同步转换,另一种是即时同步转换(tsync1和tsync2)。 我们使用了定时同步的变体。 表1显示了给定的状态和弧(CTMC级别的转换)的数量N. 用于存储状态空间的哈希表的大小比状态空间的大小(N)大20|S|= 1。2·|S|).这是可能的,因为我们从状态空间生成步骤中知道状态的数量;如果我们不知道状态的数量,如果我们事先知道状态数,我们会分配一个主内存所允许的最大哈希表。注意,N= 8、 9的情况不能在单个节点上串行处理Fig. 1. Kanban模型6.2串行算法在本节中,我们提出了一些初步的结果,从我们的原型实现。表1显示了串行算法的一些基本时序。贝尔和哈弗科特15∧N|S||一|将军S读出S记忆APϕ1∧ϕ21160616 0:00.4零点零点二<1MB0:00.00:00.024 60028 120零点五零点零点二<1MB0:00.00:00.0358 400446 4000:02.50:00.41.5MB0:00.10:00.04454 4753 979 8500:21.10:00.64.5MB0:01.20:00.052 546 43224 460 0162:26.80:02.820MB0:06.5零点零点二611 261 376115 708 992十四分二十二点九0:14.089MB0:29.20:00.7741 644 800450 455 040五十一:十五点零0:50.7326MB1:48.00:02.78133 865 3251 507 898 700-----9383 933 6784 176 462 582-----表1看板模型的统计和基本序列测试(h:m:s.s)在第四列中,我们列出了生成状态空间所需我们将此时间作为参考,它包括将状态空间和可达性图写入磁盘的时间从磁盘读取状态空间并将其插入哈希表所需的时间显示在第五列中。模型检查器所需的内存显示在第六列中。这包括哈希表的内存,内部需要的位向量和13位的原子propo-itions或子公式在执行期间评估第七列显示了评估四个形式为#Pi>1的原子命题所需的时间。应该注意的是,这是一个昂贵的操作,因为我们的实现使用字符串比较来访问某个位置。最后一列显示了计算一个简单逻辑公式所需的时间,在本例中,构造一组标记,其中,101和102是原子命题。为了对时态运算符的算法进行基准测试,我们在这个模型上做了向后EX测试-B-EX:在此测试中,我们使用EX运算符(使用precedentary函数实现)进行了向后状态空间生成给定仅在初始标记s0中为真的公式Sats0和对于状态空间S中的每个状态为真的公式SatS,我们使用以下算法:1.Sat()← {s0};2.while(Sat(Sat)/=S)3.doSat()←EX Sat();贝尔和哈弗科特16这意味着我们在Pred(... Pred(Pred({s0})).. . ).贝尔和哈弗科特17最后,我们得到了完整的状态空间。前向EX测试-F-EX:这是与“B-EX”相同的测试简单的EU测试-S-EU:该测试再次通过询问可以从哪些状态读取初始标记的问题来进行向后状态空间生成;在CTL中:N=E[trueUSats0]。我们使用的是算法见第4.5节。注意,这测试了最坏情况的sce-nario for an E [. 联合]公式,因为我们从一个只包含一个元素的集合开始,最终得到完整的状态空间。优化的欧盟测试- O-EU:这是与“O-EU”相同的测试。然而,使用第4.5节中提到的EU算法的优化变体。我们在表2中列出了这些测试的结果所有模型检查测试都包括读取状态空间并将其插入哈希表所需的时间(参见表1,第5列)。 我们还列出了达到的fixpoint。请注意由于欧盟的优化而带来的改善算法由于时间限制,我们没有对NN测试B-EXF-EXS-EUO-EU时间iter。时间iter。时间iter。时间iter。1 零点零点二18 零点零点二15零点零点二19零点零点二820:02.4360:03.628 0:00.437 0:00.4930:47.7541:13.940 0:03.155 0:02.7124九分十八点九72十四分四十一点五530:25.673 0:22.01251:11:50.0901:50:22.065二点三十五点二91 2:09.11666:22:31.0108 十点三十四分十五秒78十二点二十七分一秒109九分五十六点九15727:51:34.0126--四十八点零八分半127三十七:三十二点五18表2看板模型的序列结果-时态运算符贝尔和哈弗科特18应当注意,对于合理的大模型(大于1百万个状态),向后状态空间生成(具有状态的知识space)via=E[trueU Sat({s0})]比原始状态空间生成器.使用配备2GB内存和两个1GHz Pentium III处理器的工作站,我们还能够生成状态空间(在1:26小时内),并对N= 8(近1.34亿个状态)的情况进行模型检查(优化的EU测试运行了1:08贝尔和哈弗科特19’generate’’simple-EU’绝对加速比6.3分布式算法为了简洁起见,我们跳过基本逻辑运算符和原子命题求值的结果,因为这些可以简单地并行化,并且所得到的加速仅取决于由分配函数A实现的状态空间划分的对称性。2到26个处理器的结果总是每个集群节点使用一个处理器,而52个处理器的结果每个节点使用两个处理器为一个处理器给出的时序取自串行算法。图2(a)显示了生成状态空间和运行N= 5的看板模型的简单和优化EU测试的挂钟时间这是计时给出任何合理结果的最小情况。正如人们所看到的,即使是小模型也可以实现很好的加速比;我们在所有测试中使用12-14个处理器实现了52个处理器的加速受到初始化时间的限制,与大约5-7秒的执行时间相比,初始化时间会导致显著的开销我们还运行了选定的1603614032120281002480201660124082040 0(a) 挂钟时间(b)绝对加速图二. N=5的看板模型的s-EU和o-EU结果(2 546 432个状态)图3和图4显示了N= 6、 7的看板模型实现的(绝对)加速和绝对效率,它们确实明显优于N= 5。从这个图可以看出,所获得的并行度不如我们的状态空间生成器高。这可能是由于我们还没有调优模型检查算法,而我们为状态空间生成做了调优对于分布式情况,达到固定点的迭代次数与EX测试的串行情况相同。对于EU测试,处理器之间的迭代次数不同-它甚至对于程序的不同执行都不相同,因为它取决于发送/接收定时。’generate’’simple-EU’时间[s]1020304050481216202428323640444852数量过程进程数贝尔和哈弗科特20’gen.speedup’’simple-EU.speedup’“线性”’generate’’simple-EU’绝对效率绝对效率×1.1481440.940360.8320.7280.6二十四点五200.4160.3120.2840.10481216202428323640444852进程数0481216202428323640444852进程数(a)绝对加速(b)绝对效率图三. N=6的看板模型的S-EU和O-EU的绝对加速比/效率(11 261 376个状态)1.1481440.940360.8320.7280.6二十四点五200.4160.3120.2840.10481216202428323640444852进程数0481216202428323640444852进程数(a)绝对加速(b)绝对效率见图4。N=7(41 644 800个状态)的看板模型的S-EU和O-EU的绝对加速比/效率对于N= 8,可以将我们的快速单工作站(Pentium III,1GHz,2GBRAM)的结果与使用226个处理器(Pentium III,500MHz,每2个处理器512MB RAM需要1:08小时连续运行的O-EU测试可以使用’gen.eff’’simple-EU.eff’’generate’’simple-EU’绝对加速比绝对加速比
下载后可阅读完整内容,剩余1页未读,立即下载
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功