FLC的模型检测问题及并行化算法在格拉斯哥并行Haskell中的性能评估

理论计算机科学电子笔记128（2005）125-138www.elsevier.com/locate/entcsChop1不动点逻辑的并行符号模型检验Martin Lange和Hans Wolfgang LoidlInstitutfuürInformatik，UniversityofMunich，GermanyEmail：{mlange，hwloidl}@ tcs.ifi.lmu.de摘要我们考虑FLC的模型检测问题，FLC是一种能够定义非正则性质的模态定点逻辑。本文提出了一个符号模型检验器的改进，并讨论了如何并行化这个算法它报告的原型实现的算法在格拉斯哥并行Haskell（GP H）和它的性能在一个集群的工作站。保留字：符号模型检查，函数式编程。1介绍目前，（时态）逻辑的模型检测被普遍认为是验证的关键方法之一。模型检验用于验证目的的有效性的一个主要限制是状态空间爆炸问题。为了解决这个问题，人们采用了符号方法[3]，这些方法直接作用于流程描述，并且通常在那里实现更好的性能在相关应用中，对效率的需求以及面对巨大的状态空间通常会导致使用具有很少表达能力的逻辑来进行模型检查任务。这有一个明显的缺点：如果一个期望的正确性属性在这个逻辑中是不可表达的这使得寻找（尽可能有效的）具有更高表达能力的逻辑的决策过程变得合理。1这项工作得到了欧盟委员会在FET全球计算主动倡议项目IST-2001-33149（MRG）下的部分支持1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.023126M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125FLC [9]的引入使时态逻辑在表达性阶梯上迈出了一大步，FLC是一种定点逻辑，它用一个用于顺序组合的运算符扩展了模态μ这使得FLC能够表达非正则性质，如本文在文献[5]中提出的顺序算法的基础上，提出了一种基于BDD的FLC符号模型检验算法，并讨论了如何通过并行化提高其效率。与模态微演算相反，公式的语义是一个函数，这为并行求值提供了新的机会，除了同时求值布尔连接词之外。例如，定点迭代需要测试两个函数在一组有限参数上的相等性，这可以并行完成。本文报告了第一个运行时结果，比较了符号模型检查器的顺序和par-analog版本我们使用Glasgow Parallel Haskell（GP H）作为编程语言有三个原因。首先，GP H提供了一种简单的方法，增加并行现有的顺序算法，delegate- gating的任务分配等决定的运行时系统。其次，使用一种将函数作为第一类公民的语言可以很容易地表达FLC公式的语义，这些公式只是函数（从状态集到状态集第三，Haskell请注意，由于语义存在于函数空间-局部算法现在是只计算函数中真正需要的那部分的算法。在最初意义上的全局性-计算所有具有某种属性的状态-是通过使用BDD给出的对于基本的BDD操作，我们使用调优的C库。我们利用GP H的以下语言特性：半显式并行性，便于表达并行执行;高阶函数，用于自然地将模型检查算法表达为函数; Haskell的外部函数接口（FFI）1.1相关工作[4]提出了一个分布式版本的符号模型检查器，用于模态微演算。通过对子公式的独立评估来获得并行性-正如我们所做的那样-并且这些任务使用状态空间切片显式分布。对子公式求值的唯象主义似乎是将模型检验任务分配给全模态微演算的唯一可能性，全模态微演算是一种涉及复杂定点公式的逻辑。M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125127在定点之间的限制性交替的情况下，采用了显式图形着色方法，该方法受益于模型检查图可以划分为可以单独处理的组件的事实。此方法由[1]用于μ-演算的无交替片段，[6]仅用于交替深度。[1]还报告了在Haskell中实现的具有显式消息传递的并行版本。然而，他们的显式消息传递并行化方法比我们在GP H中的实现更冗长。与他们的实现相反，我们使用了一个调优的基于C的BDD库来获得高顺序性能，这是[1]中纯Haskell实现中报告的问题。因此，我们的工作从可比的算法和实现，不仅通过处理更丰富的逻辑，但也通过使用内置的编译器支持的并行语言。因此，我们不必自己管理并行化任务。1.2组织本文件的结构如下。第2节介绍了带有斩波的定点逻辑（FLC），重点介绍了与模型检查算法并行化相关的属性。第三节描述了FLC的顺序符号模型检测算法。第四节介绍了Glasgow Parallel Haskell（GP H）的主要概念，并讨论了该算法的几种并行版本。第5节给出了在工作站集群上运行并行算法的经验数据，并总结了结果。2预赛令P ={tt，ff，q，q，. . }是在互补下闭的命题常数的集合，V ={Z，Y，. . }命题变量的集合，并且A ={a，b，. . }一组动作名称。标号转移系统是一个图一一T=（S，{−→ |a∈A}，L）其中S是s的集合，−→对于ea cha∈A是a关于状态的二元关系和L：S →2P标记状态，使得对于所有s∈ S：q∈L（s）i <$q/∈L（s），tt∈L（s），且ff/∈L（s）. 我们将使用fix符号s−→at表示传递关系。他的遗嘱是不能兑现的我们总是假设过渡系统是有限的。因此，它们可以使用BDD表示。关于BDD的正确介绍，请参见示例[2]。在[3]中，我们展示了如何使用BDD来进行一般的验证，以及如何使用Park和时态逻辑CTL来实现模态微演算的一个变体。在这样一个T，w.l.o.g.假设|S|≤2n，其中n∈N.那么每个状态都有一个介于0和2n- 1之间的唯一数，人们可以识别一个状态128M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125∨⎨不s的二进制表示为s1. Sn，si∈ B.T可以表示为|一|+的|P|2·n个变量上的BDD 我们把它们的名字和总顺序固定为x1y1<<. |〔一〕|ϕ ∨ ϕ |ϕ ∧ ϕ |µ Z. |V Z.|;其中q∈ P，Z∈ V，a∈ A。 我们将用σ代替μ或ν。 为了节省方括号，我们引入了 这样 的约 定：; binds strengthened than （ 约束力 强于 ） ; which bindsstrengthen than（约束力强于）。公式被假定为是良好命名的，因为每个绑定变量都是不同的。我们的主要兴趣是没有自由变量的公式，在这种情况下，有一个函数fp（）：V →FLC将每个变量映射到它的定义定点公式。子公式的集合Sub（σZ. σ）通常定义为Sub（σZ. σ）={σZ.<$}Sub（）。变量X在xl中最右边自由出现的尾部，tlX（xl）是– intuitively – everything that occurs behind this 从技术上讲，它被归纳定义为：tlX（;）：=如果X出现在X中，则X（X）{|j∈tlX（变量X的尾集tl（X）是所有tlX（X;n）的并集，其中fp（X）=σX. n，如果σ=v，则所有最右边的出现都被tt替换，否则被ff替换。一个环境ρ：V →（2S→2S）将变量映射到集到集的单调函数。 ρ[Z<$→f]是将Z映射到f的函数，并且符合p在所有其他参数上。FLC公式的语义[·]]T：2S→ 2S，相对于和ρ，是关于2S上的包含序的状态子集上的单调函数。这些函数连同偏序给出f±giXS：f（X）g（X）形成一个完全的格，有连接H和满足H。根据塔斯基-克纳斯特定理，泛函F：（2S→ 2S）→M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125129不.（2S→ 2S）存在。 它们被用来解释FLC的定点公式。为了简化符号，我们假设一个转移系统T是固定的，并将[·]]ρ写成[·]]ρ。[[q]] ρ：= λX。{s∈ S|q ∈ L（s）}[[Z]] ρ ：=ρ（Z）[[τ]]ρ：=λX.X[[;]]ρ：=[]]ρ[[]]ρ[[]]ρ：=[]]ρH[[]]ρ一[[]]ρ：=λ X。{s∈S|t∈X，s. t. s−→t}一[a]ρ：=λ X。{s∈S|<$t∈S， s−→t<$t∈X}[[μZ.]]ρ：={f：2S→2S|f单调，[Z]]ρ[Z<$→f]±f}与和νX.的情况类似。 一个状态s满足ρ下的一个公式，记作s| = ρε，i ε s∈ [[ε]]（S）.如果ε是一个封闭公式，那么ρ可以省略，我们写[ε]]（S）以及s| = 0。我们将给出几个FLC公式的例子。例2.1a）设A={a，b，c，d}，第1章：= 是的。[b];ff（[c][d]）;Y[a];（v Z. [b]（[c][d]）;Z[a];Z;Z）;（（[a];ff[b];ff）Y）公式B1表示子公式= νZ。[b]n（[c]n[d]）;Zn[a];Z;Z表示这可以通过展开定点公式来最好地理解，从而获得模态和变量的序列很容易看出，用a [b]替换Z会减少Z然后，[b];ff<$[a];n假定在开始时没有b是可能的，并且对于每个n个a-动作的序列，最多可以有n个b-动作。最后，Y11中的Y允许这样的序列在死锁状态下组合或完成。b）设τ3：= νX.τ τ [a]; X; τb（μY. [a];Y;[b][b];Y;[a]τ）;X.最 好把它看作是一个有交集的上下文无关文法。然后，内部最小定点公式在X之前生成偶数个[·]公式的序列，其中a的个数与b的个数一样多。与其他合取项一起，展开X创建任意公式的[c1];. ; [cn];[bn];. ;b其中b出现m次，n≥m，ci∈ {a，b}，所有i和m =|{我|ci= a}| −| {我|ci= b}|. 因此，在k-a-actions和l-b-actions之后，总是有可能再做另一个k-l- b-actions。130M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125|SSMC（ρ，ε）=情况εQτX〔一〕→→→→ψ0∨ψ1→ψ0∧ψ1→0;σX. σ→→λt.tqλt.t ρ（X）λt。一号... . yn.ta，yn/xn]λt。一号... . yn.ta→ t [y1/x1，.， yn/xn]λt. MC（ρ，ε0）（t）εMC（ρ，ε1）（t）λt. MC（ρ，ε0）（t）εMC（ρ，ε1）（t）λt. MC（ρ，ε0）（MC（ρ，ε1）（t））设X = λt。若σ=μ，则f=f，否则F=λf.MC（ρ[X<$→f]，λ），设T=tc，X，ρ（t），00fixPoint（T，F，X）fixPoint（T，F，g）=λt。设f=F（g），iff（tJ）=g（tJ）thenf（t）elsefixPoint（T，F，f）（t）Fig. 1. FLC的顺序和符号模型检测算法3顺序算法在[5]中提出了一种基于BDD的FLC顺序模型检测算法然而，这里给出的版本是不正确的。FLC公式的语义是单调函数格的元素。这个格子中的不动点使用通常的定点迭代方法计算。为了决定是否找到一个定点，我们必须在多个（可能是指数级的）参数上比较函数，而不仅仅是一个参数。因此，符号模型检测算法比以前预期的更昂贵，提高其性能成为一个更重要的问题。该算法在以下意义上是局部的。然而，为了确定对于给定的s和n，s=n是否成立，没有必要计算整个语义[n]。相反，它可以从[]]（）开始逐点计算底层状态集等。将此与局部模型检查算法的通常想法进行比较，该算法不计算满足给定公式的所有状态集。M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125131{|∈}图1所示的算法MC将环境ρ和FLC公式作为参数，并返回[]]ρ。因此，它在通常意义上是全球性的。函数式语言中的求值策略保证只计算[]] ρ中建立或反驳s所需的部分|= 0。算法MC调用函数fixPoint，该函数计算fixpoint迭代，直到达到稳定性。由于我们的局部性类型，函数不会对每个参数进行评估。这意味着定点迭代可以在给定参数上变得稳定，尽管函数空间中的定点尚未到达。因此，函数fixPoint必须对多个参数的fixpoint迭代进行求值。它近似于必要的（即表示状态集的BDD）使用函数tc，X（t），它采用FLC公式，自由变量X，环境ρ和BDDt，并首先计算{t}在函数[[]]ρtl（X）下的自反和传递闭包。这个集合包括所有需要作为参数的BDD的集合，以便计算函数空间中的定点4优化算法MC4.1Glasgow Parallel Haskell（GP H）G P H [11]是非严格的纯函数式编程语言Haskell 98 [10]的适度保守扩展，增加了一个用于并行组合的构造函数par（顺序seq组合子已经是Haskell 98的一部分）：x'par' e表示x和e的潜在并行执行。通常x是出现在e中的变量，但它可以是一个通用的Haskell表达式。表达式的结果是e的结果，因此语义上par是其第二个参数的投影。在操作上，这个表达式将x添加到潜在并行执行池中。是否真正并行执行x，以及如果是，在哪里执行它，是由运行时系统自动做出的。在G P H中，程序员使用par combinator将表达式注释为潜在并行，并将并行性的管理留给运行时系统 我们称之为半显式并行模型。GP H的实现模拟了一个虚拟共享堆，即所有程序变量都可以访问，就像驻留在同一个处理器上一样。如果不是这种情况，则运行时系统安排处理器之间的自动数据传输。虚拟共享堆促进了能够利用大量处理器的与体系结构无关的程序的开发。相比之下，物理共享内存机器中的处理器数量受到硬件约束，通常为几十个。对于只想利用少量并行性的应用程序，132M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125记忆可以使用。存在用于物理共享存储器机器的运行时系统的实验版本，但是当前在正常执行期间由于频繁的锁定（当分配新的数据结构时，频繁的锁定变得必要）而导致高 因此，我们最终希望通过尽可能优化物理共享内存情况下的通信例程，将共享内存机器集成到我们的模型中，但即使对于这些机器，也保留整体虚拟共享内存模型这个应用程序的一个重要语言特性是Haskell中提供的FFI接口。这使我们能够使用现有的，调优的C代码进行基本的BDD操作。然而，由于我们使用的Long BDD库[8]管理自己的堆，因此Haskell堆和C堆之间的交互是必要的。在Haskell方面，这意味着BDD被表示为For- eign Object，即在Haskell堆外部构造的数据结构。这个数据结构由一个指向C堆的指针和一个finaliser例程表示，一旦Haskell堆不再使用它，就会执行该例程为了提供更高层次的抽象，我们通常使用求值策略[11]来表示更复杂的Haskell程序中的并行性。这些策略是多态的高阶函数，表达了并行性、评价顺序和评价程度。策略是按照par和seq来制定的，并通过使用组合子 例如，对列表xs中的所有元素进行并行求值，将每个列表元素求值为标准形式，可以写成xs 'using' parList rnf。预定义的策略parList可以写成foldr par（）。 在本文中，我们将只使用重载策略rnf，它将数据结构评估为范式。4.2并行算法我们的算法MC的第一个并行版本PMC1（n），其中n表示在其执行中使用的处理器的数量，利用了结构并行性或并行性。两个分支的执行之间不存在依赖关系，从而产生了大量并行性的丰富资源。 这种并行算法的结构是分而治之。但是5.1节中的顺序分析表明，在这些构造上不受限制地使用并行性将产生太多的并行性，以至于效率低下。因此，我们将此版本与常用于分治并行的阈值机制相结合：在由模型检查算法生成的公式树中，并行性仅生成到某一深度或阈值。我们提供阈值作为算法的附加参数虽然这种并行性可以只用一个par组合子来描述，但我们还需要使用seq组合子指定求值顺序，M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125133评价度，采用归正规化评价策略rnf。此外，系统要求输入到并行线程的所有数据都存在于Haskell堆中。否则只有一个指向C堆的指针被发送到另一个处理器，在那里这个指针当然是无效的。因此，我们必须引入函数freezeBDD和thawBDD，它们将BDD从C复制到Haskell堆，反之亦然。函数fMC是MC的一个变体，它在这种“冻结”的BDD上工作算法中的并行分支的代码看起来像这样，描述-与评估线程的主线程并行地执行对线程的评估：然后fg->\ t->lett（in（rnf其中bAND将两个BDD与布尔型bDD组合。在tc，X，ρ的帮助下计算测试集T需要再次调用模型检查器MC（在更小的公式上）。这是因为X的尾需要转换成从BDD到BDD的函数，以便计算t在这些函数下的传递闭包。 这引起了布尔连接词的进一步评估。此外，一组函数上的传递闭包的计算可以并行化。算法PMC2通过与定点计算本身并行地计算测试集而从MC产生。这需要改变图1中σ情况的最内层let：lettxs' =（（map freezeBDD）. setToList。试验.thawBDD）t '测试集=（mkSet. 地图thawBDD）xs在（rnf同样，需要额外的代码来冻结和解冻潜在并行计算的输入和输出rnfxs'子句生成了测试集，它通过调用测试（对应于图1中的tc）来注意，计算xs'的线程t. 当后者需要数据结构由前者生产。这种并行源的主要优点是其粗粒度，将整个测试集生成转换为并行线程。这里使用的并行形式是生产者-消费者（或管道）并行，其中生产者和消费者在同一数据结构上并行工作这种并行性可以与版本PMC1中大量的分治并行性结合起来。此外，我们还可以并行计算测试集本身。这是可能的，因为有有限多个函数需要计算一组BDD的闭包。134M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125−−不∨∧∃∀不仅可以并行应用单个函数，还可以用单个函数并行化单个迭代，因为它需要应用于多个BDD。5经验测试数据在这一节中，我们将描述一个模型有界堆栈或计数器的过渡系统族设P={tt，ff}，A={push，pop，reset，idle}。一个N比特-计数器是T=（S，{-→a|a∈A}，L），其中hS={0， . . ，2N−1}，对于所有s，t∈S：s−−pu−s→h tit=s+1，s-p-o→p tit=s−1，s−−re−se→t tit=0，s−−id−l→e 不i=t.请注意，不计算模2N。相反，值0不能减少，2N 1不能增加。换句话说，N位计数器可以在值0和2N 1之间增加和减少，重置为0并且不做任何事情。根据第2节，一个N位计数器可以用4个BDD在2·N个变量上表示。算法MC、PMC1（1）和PMC1（4）已经在其顺序和并行版本中针对N的某些值在N位计数器上运行。下面的公式被用作输入：例2.1中的公式1和公式3，其中a：= push，b：= pop，c：= reset，d：= idle，以及公式2：= v X.τX;公式3：= push，要求无限长的push路径，公式4：= μX。[push];X.图2中给出了与N位计数器的大小2N相关的运行时间（以秒为单位）。所有的测量都是在一组具有1.6GHz AMD Athlon处理器、256kB缓存、512MB DDR SDRAM内存和9.5GB本地硬盘的SuSE 9.0 PC上运行的该网络是100 MB/s的快速以太网，在PVM 3.4.3下测量的延迟为120μ s我们使用GHC5.02.3进行编译，并对其运行时系统GUM进行并行扩展。5.1顺序配置文件按照我们开发并行程序的方法[7]，我们从分析顺序代码开始，以确定最耗时的组件。我们使用成本中心profiling来分类时间和堆消耗的程序点负责计算。在分析N= 4时的103的剖面结果时，最引人注目的是，结果是外部对象的finaliser例程的高开销：堆的47%和时间的23%。模型检查算法生成大量的外来对象：通过调用和 1700万通过运营，1.16亿通过BDD运营。为一类外来对象共享finnaliser例程，这些对象表示M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125135⟨ ⟩300020001000010005000SEC0 1 2 34SECϕ1×1000个州ϕ32000100006000400020000SEC0 2 46SECϕ2×100个州ϕ40 5 1015国0 510×100个州++MCPMC1（1）PMC1（4）图二. 顺序和并行运行时间。在这种情况下，BDD将提高顺序性能。虽然直接的时间消耗在[]和[]分支上的时间相当小，分别为1.3%和8.3%，但这些情况在[ ]和[]分支上启动了更大的计算，总共为25.9%，并且间接地通过定点计算。在整个计算过程中，整个堆驻留时间保持在较低水平，从未超过400kB。总之，虽然BDD操作相当便宜，但它们被频繁调用，从而增加了总成本。 这是具有不规则并行性的符号应用程序[7]的典型特征，并且与GP H中执行的并行性的动态管理很好地匹配。5.2并行运行时我们的性能结果表明，版本PMC1产生了非常细粒度的并行性，即生成的线程只有少量的工作要做。并行版本包含用于冻结和解冻BDD以及用于生成和管理大量线程的开销。因此，朴素和/或并行版本没有实现任何加速。当将和/或并行性与线程总数阈值结合时，产生的下降幅度很大：对于N =2和N= 7，从468下降到408.在4个处理器上运行这个版本，输入为1.28，N= 7，相对加速比为1.09，N= 8。对于这个公式，+++++++++++136M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125与顺序版本相比，1个处理器版本的平均值保持在2的因子内，但对于其他公式，它显著增加。特别是，版本产生更多的潜在并行执行堆之间的数据传输。对于其他公式，我们实现了高达1.071991年为1.13，1993年为1.13，1994年为1.12。 当保持阈值固定时，对于较大的输入，加速比下降。对于一个只有轻微调整的并行算法与高度不规则的并行lelism这样低的加速比是不足为奇的。显然，该算法不支持并行性不足。我们目前的工作集中在算法的粒度控制，使用阈值是朝着这个方向迈出的一步。然而，最佳阈值的选择通常取决于输入公式，我们目前正在探索自动选择此阈值的替代方案 性能对线程粒度公式101和N= 11的加速较差：0.98（a慢下来）。对于这个输入，总共生成了2062个线程，远远超过了2062个线程。当降低阈值时，性能会再次提高，从而限制并行性的数量以及与之相关的开销在我们设计的并行算法的一个重要目标是实现可扩展性，即，以确保更多的处理器比目前使用的可以利用不改变代码。不幸的是，这个属性也会触发堆之间不必要的数据传输。一个使用惰性来避免这些操作的实现，除非并行性被明确利用，否则应该会提高一个处理器的性能，但实现起来很棘手。将这种显式的求值顺序硬连接到代码中是其在其他简单的并行模型中复杂性的主要原因。因此，我们现在致力于一种方法，其中外部对象的结构用编组函数扩展，该编组函数将作为运行时系统使用的图打包算法的一部分自动启动，以在处理器之间传输计算。这确保了堆之间的数据传输仅在需要并行执行时进行，并从并行GP H代码中消除了这种复杂性。尽管PMC2版本避免了太细粒度的并行性问题，它只在执行的主线程之上创建一个并行线程。 第4节中讨论的代码生成了生产者-消费者并行性，利用了GP H的非严格语义：消费者甚至可以在中间数据结构（测试集）完全生成之前就开始处理它。然而，我们对这个版本的测量表明，测试集生成和定点迭代之间的数据依赖性太紧了以实现有用的并行量：大多数情况下，两个线程中的一个被阻塞，等待远程数据到达。例如，使用M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125137并且N= 7，在96%的时间期间，只有一个线程在运行，而另一个线程在尚未产生的数据上被阻塞，然而，在重叠这两个计算中实际上没有留下并行性。因此，PMC 2根本没有实现任何加速：对于N =1和N = 10，加速比为0。98，对于N =2和N = 7，加速比为0。99.对于更复杂的输入公式，可以在到达公式中的量化器之前，在最开始计算形式为σX.的子公式的测试集。本案中测试集的计算可以与模型检验公式的其他部分并行进行，所有测试集的计算也可以并行进行。然而，这可能会产生一些不必要的工作，而且这个版本的有效性在很大程度上取决于输入公式的结构5.3总结所提出的符号模型检查器生成高度不规则的并行性的形式深，不平衡的分治树，需要阈值来限制总的并行性和/或输入公式的并行性产生的。实现的加速比很小：在最好的情况下，N =2和N= 7，我们可以在4个处理器上报告1.2的绝对加速比，在最坏的情况下，我们得到相当大的减速。我们确定了转换的Haskell的数据结构和线程粒度太细是主要的限制。为了提高性能，我们需要一种更好地控制线程粒度的方法使用测试集的大小来指导是否在计算层次的一个子树中生成并行性的决定将是有希望的。测试集本身的并行计算被证明是不值得的，因为测试集的生产者和消费者之间的数据依赖性太紧密，以至于不允许这两个线程之间的大量并行执行。更一般地说，我们使用Haskell作为顺序和并行算法的顶级语言的经验是积极的。与早期基于Java的实现相比，该算法本身更接近于这里给出的高级表示[5]。 使用调优的BDD库在顺序情况下已经为我们提供了高性能，利用了Haskell的外部函数接口（FFI）。 G P H作为并行语言允许不同并行版本的快速原型化，这在传统并行语言中是不可能的。然而，使用外部BDD库，我们必须编写显式的编组代码来将C堆中的BDD转换为Haskell数据结构。目前，数据编组必须显式地控制在GP H码中，增加了并行算法的复杂度。在未来，我们计划将数据编组集成到用于传输计算的自动图打包算法中。为了写这封信-138M. Lange，H.W.Loidl/Electronic Notes in Theoretical Computer Science 128（2005）125µshalling代码是FFI之上的附加层，类似于GreenCard工具，将非常有用。引用[1] B. Bollig，M. Leucker和M.韦伯局部并行模型检验的无交替μ-演算。In S. Leue D. Bonaki，编辑，Proc.9th Int. SPIN软件模型检查研讨会，SPIN'02，LNCS第2318卷，第128-147页。施普林格，2002年。[2] R. E.布莱恩特基于图的布尔函数操作算法。 IEEE Transactions on Computers，35（8）：677[3] J. R. Burch，E. M. Clarke，K. L. McMillan，D. L. Dill和L.黄哲伦符号模型检查：1020个状态及以上。Information and Computation，98（2）：142[4] O. Grumberg，T. Heyman和A.舒斯特分布式符号模型检验的μ演算。In G.贝里，H。Comon，和A. Finkel，编辑，Proc.13th Conf. on Computer-Aided Verification，CAV'01，LNCS第2102卷，第350-362页。Springer，2001年7月。[5] M.兰格非正则性质的符号模型检验。In R. Alzheimer和D. Peled编辑，Proc.16th Conf. onComputer Aided Verification，CAV斯普林格。[6] M. 洛伊克河Somla和M.韦伯LTL、CTL和L2的并行模型检验.在L. Brim和O. Grumberg，编辑，第二届并行和分布式模型检查国际研讨会，PDMCElsevier，2003年。[7] H.- W. Loidl，P.W. Trinder，K. Hammond，S.B. Junaidu，R.G. Morgan和S.L.佩顿·琼斯。GPH中的并行符号程序设计。Concurrency - Practice and Experience，11：701[8] D.久了长BDD图书馆网页，2004年5月。http://www-2.cs.cmu.edu/~modelcheck/bdd.html网站。[9] M. 穆勒-奥姆。一种改进的固定点，在逻辑上与hhhop匹配。 我在C。 Mei n el and dS. Ti son，editor s，Proc. 第16届研讨会计算机科学的理论方面，STACS'99，LNCS的第1563卷，第510-520页，特里尔，德国，1999。斯普林格。[10] S.L. Peyton Jones ， J. Hughes 等 Haskell 98 ： ANon-strict ， Psychological FunctionalLanguage，1999.可在www.example.com上http://www.haskell.org/。[11] P.W. Trinder，K.哈蒙德，H.- W. Loidl和S.L.佩顿·琼斯。算法+策略=策略主义。J. ofFunctional Programming，8（1）：23-60，Jan. 1998年