Maude实现的并行函数式语言操作语义研究

106 浏览量更新于2024-01-14 收藏 763KB PDF 举报

身份认证购VIP最低享 7 折!

领优惠券(最高得80元）

理论计算机科学电子笔记174（2007）119-137www.elsevier.com/locate/entcs使用Maude及其策略定义分析Eden语义的梅塞德斯·伊达尔戈-埃雷罗a AlbertoVerdejobYolandaOrtega-Mall'enbaDepartameDida'cticdelasMatema'ticas，UivsidadCompluttenseddeMa dridbDepartametodeSisema s在计算中，未发现数据包摘要Eden是函数式语言Haskell的并行扩展。为了实现并行性，Eden超越了Haskell的纯惰性方法，将非严格的函数式应用程序与渴望的进程创建和渴望的通信结合起来。我们希望研究伊甸园的替代语义，以分析在语言设计过程中采取的一些决定的后果。在本文中，我们将展示如何在Maude中实现Eden的操作语义，以便可以轻松修改语义规则。此外，其他语义特征可以通过参数化模块来实现，该参数化模块允许以不同的方式实例化语义的几个参数，但不修改语义规则。关键词：操作语义，并行函数式语言，伊甸园，重写逻辑，莫德，重写策略。1介绍众所周知，函数式语言为并行编程提供了很大的可能性[10]，范围从完全隐式并行（例如自动并行化）到显式并行（程序员将计算分配给一组通信进程，甚至可以由程序员自己定位在指定的处理器上）。并行语言Eden更接近于后一种方法，扩展了Haskell [15]的协调功能，用于创建基于流的通信进程。Haskell是一种懒惰的语言，即它采用正常顺序求值，通过共享约简来避免重复计算。懒惰方法限制了并行性的开发，因为表达式只在需要时才计算。因此，Eden覆盖了纯惰性方法，结合了一个非严格的函数式1 研究由MCyT西班牙项目MIDAS（TIC200301000）支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.051120M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119具有急切的过程创建和急切的通信价值评估的应用这可能会产生推测性计算，即可能永远不会使用的结果的计算。Eden程序评估期间产生的推测计算量是可变的，取决于处理器的数量，基本操作的速度等。这种懒惰和渴望之间的相互作用正是由Eden的操作语义建立的此外，这种语义定义了两种极端程度的推测计算：最小和最大。虽然在GlasgowHaskell编译器（GHC）[4]之上存在Eden [8，17]的稳定实现，但我们希望研究Eden的替代为此目的，拥有一个框架是非常有用的，在这个框架中，Eden重写逻辑[14]和Maude [3]是实现这一目标的优秀候选人。首先，Eden的语法可以从字面上表示。其次，Eden的操作语义规则在大多数情况下可以在Maude中完全按字面表示，因此保持尽可能短的表示距离。第三，由于Maude规范是可执行的，因此我们直接获得Eden的实现，其中可以执行程序示例和分析最后，最近为Maude提出的策略语言[13]可以是用于以各种所需的方式控制语义规则的应用。在本文中，我们展示了如何在Maude中实现Eden的操作语义，以实现两个主要目标：（1）语义规则可以以简单的方式修改，以便在不久的将来我们可以研究不同的可能性，以及（2）几种措施-并行性，推测计算，通信等。可以通过改变语义的一些参数（在参数化模块中定义）而无需修改语义规则。从Eden的角度来看，这是迈向一个框架的第一步，在这个框架中，Eden表达式可以根据不同的语义进行评估，以便进行比较和分析。从在Maude中实现操作语义的角度来看，这项工作构成了继续进行的另一个步骤，以表示更复杂的语言的语义。我们考虑过的最简单的这不是我们在[ 16 ]中处理的Cardelli和Gordon的环境演算的情况然而，在后者中使用的策略解决的问题不同，我们认为在本文中，我们考虑到伊甸园本文的其余部分组织如下。首先，我们提出了一个简短的介绍莫德;一个完整的治疗，我们建议读者到莫德手册[3]。第3节给出了Eden的概述并实现了其内核语法，而第4节则致力于操作语义及其在Maude中的实现在第5节中，我们扩展了我们的框架，以便能够从计算中获得度量。最后一节提出了我们的结论和展望M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119121工作2访问Maude在Maude中，一个系统的状态通过一个等式的形式化被指定为一个代数数据类型。 Maude使用了一种非常有表现力的等式逻辑，即隶属等式逻辑[2]。在这种类型的规范中，我们可以定义新的类型（通过关键字排序）;子类型关系是-补间类型（子排序）;用于构建这些类型的值的运算符（op），它们的参数和结果的类型，并且其可以具有例如关联（ associative）或交换（commutative）的属性;标识用这些运算符构建的项的等式（eq）;以及声明项t具有排序s的成员资格（mb）t：s。方程和成员资格都可以是有条件的。条件由方程和成员的结合（写作/\）形成。假设方程是连续的和终止的，也就是说，我们可以使用方程从左到右将项t简化为等价于t的唯一（对运算符属性取模为结合性、交换性和恒等式）标准形式tJ，即它们表示相同的值。系统的动态行为由重写规则指定，重写规则的形式如下：如果t=0，则（我i=i（J2016 - 05 -2200：01：01Kpk−→qk）描述系统的本地并发转换。也就是说，当系统的一部分匹配模式t并且满足条件时，它可以被转换为模式tJ的相应实例。Maude模可以用一个或多个参数来参数化，每个参数都用一个理论来表示，该理论定义了模的接口，即实际参数所需的结构和性质。重写规则既不需要是连续的，也不需要是终止的。这种理论上的通用性要求在规范成为可执行时进行一些控制，因为必须确保重写过程不会朝着不希望的方向进行。我们已经为Maude定义了一种策略语言，可以用来控制规则如何”[13]这句话的意思是：最简单的策略是常量idle，它总是通过什么都不做而成功，而fail，它总是失败。基本策略包括应用规则（由相应的规则标签）到给定的术语，并具有为规则中的变量提供替换的可能性。在这种情况下，规则被应用于术语中任何它匹配满足其条件的地方。当所应用的规则是在条件中具有重写的条件规则时，策略语言允许通过搜索表达式来控制如何解决重写条件一个操作顶部，将规则的应用仅限于术语的顶部也被提供。巴-SIC策略然后被组合，使得策略被应用于执行路径。一些策略组合子是典型的正则表达式结构： concatenation （ ; ）、 union （ | ），以及 diteration（*for0ormoreiterations，+for1ormore，还有！对于“重复直到结束”迭代）。另一个策略组合子是122M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119典型的if-then-else，但一般化了，所以第一个参数也是一个策略。该语言提供了一个（x）matchrew组合子，允许将一个项拆分为子项，并指定如何重写这些子项3快速游览伊甸园Eden [11]扩展了非严格函数式语言Haskell的一组协调功能，以控制进程的并行计算。Eden中的协调基于两个主要概念：进程的显式定义和隐式的基于流的通信，即没有发送和接收等通信原语。除了函数定义和函数应用之间的区别之外，Eden还包括流程抽象，即流程行为的抽象方案，以及实际创建流程的流程实例化。此外，在伊甸园中，非确定性是通过一个预定义的过程抽象来引入的，该过程抽象用于实例化非确定性过程，将输入流转换为单个输出流。为了本文的目的，我们只关注EdenI=当在进程p中计算表达式E1#E2时，会创建一个新的子进程q和两个通信通道。子进程的父进程p通过输入通道向子进程提供E2的值。过程q评估E1E2并经由输出通道返回结果（到其父节点）。下图说明了这一点：E1#E2 EpEE−→2v1 2Q该语言被规范化为受限语法，其中所有子表达式，除了λ-抽象的主体，都被let-表达式中定义的变量替换。这保证子表达式是共享的，并且最多计算一次。我们还假设变量的通用重命名，以避免表达式计算期间的名称冲突。pE：：=x识别器| λx.Eλ-抽象| 第一季第二集应用|E1#E2| let {x i= E i}n进程创建1inE本地声明M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119123例如，以下表达式的求值设x0=x1#x1，x1=λx.x，x2= 1，x3=x4x0，x4=x5x2，x5= λy。（λz.z）英寸x3给进程创建一个位置：主进程计算x3，而子进程计算应用程序x1x1。为了做到这一点，子进程需要两次x1(i) 为了获得λ-抽象：将定义复制到子堆，(ii) 获取参数：父代将值传递给子代。在应用程序评估结束时，结果值被发送回父进程。3.1在Maude的我们在Maude中定义了上面给出的Eden内核的语法。我们用类和子类来表示不同的句法范畴及其关系。有不同的排序允许我们通过使用最合适排序的（Maude）变量我们有普通变量（Std），通道（Cha）和两个集合的并集（Var）的排序我们也使用两种排序用于区分弱头范式（Whnf）的表达式而那些没有的，两者都是伊甸园表达式（Exp）。排序标准ChaVarWhnf NonWhnf ExpLetBind LetBind。子分类StdCha Std.opc：String -> Cha.执行部分：标准实验->Whnf. op：Exp Exp->NonWhnf.操作let_in_：LetBinds Exp->NonWhnf. op _#_：Exp Exp-> NonWhnf.op _=_：Std Exp -> LetBind.op nil：-> LetBinds。op ：LetBindsLetBinds-> LetBinds。124M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119›→4操作语义在本节中，我们描述了[1]风格的操作语义，这反过来又基于Launchbury我们的目的只是描述语义的结构，并提出一些转移规则，重点是它们如何在Maude中实现对于Eden语义的更详细的概述正确性证明，示例和应用程序收集在[5]中。4.1两级过渡系统一个过程由一对p，H表示，其中p是一个过程标识符，H是收集变量到表达式的绑定的堆，这些绑定对与流程计算状态相对应的闭包进行建模。每个绑定都被认为是可用处理器执行的潜在线程，因此标签指示该线程状态：xαE，其中α：：= I|一|B对应于非活动（或者尚未要求或已完全评估）、活动（或要求）和阻止（要求但等待另一绑定的值）。通道标识符可以出现在绑定的任何一侧：在左手边，它们表示输出;而在右手边，它们表示输入。在下文中，我们将使用x， y，z∈Std 表示普通变量，c∈Chan表示通道，θ∈Var=StdChan，W∈Whnf表示弱头规范形，p和q表示过程标识符。评价模型由一系列系统来表示--系统是一组并行的过程--由转换规则来调节。堆中的一些绑定是并行执行的，共享相应进程的数据;但不同进程中的绑定只能通过进程通信共享信息语义需要小步过渡，以同步的方式建模并行性，在这个意义上说，单一的减少是本地的，独立地在每个过程中进行，然后在进行下一步之前组合。语义反映了构成Eden的两个子语言（计算和协调）之间的区别4.2在Maude一个线程是用一个变量、一个线程状态（排序为TState）和一个表达式构建的。堆是一组线程：none表示空堆，线程表示单例堆，子线程堆，堆的union_+_构建它们。联合构造函数被声明为关联的、可交换的，并且与空堆作为标识元素;模式匹配将以这些为模进行M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119125特性.最后，进程构造函数有四个参数：一个对应于进程标识符的字符串;一个堆;和两个计数器：一个表示这个进程的子进程的数量，另一个表示用于构建新变量的最大数量（当由于生成新变量而需要重命名时增加）。还有一个用于构建系统的union操作符（语法为空）。排序TState线程堆处理系统。子排序线程<堆。subsort进程<系统。操作A/B：-> TState。操作_|-_->_：变量TState Exp ->Thread。op none：-> Heap.op _+_：Heap Heap -> Heap [aspheroidid：none].op<_，_>：String Heap Nat Nat -> Process.opempty：-> System.op ：System System -> System [aslogid：empty]。我们定义了语义所需的几个辅助操作：替换、堆中变量的重命名、规范化等。它们在结构上是通过方程和使用owise（否则）Maude属性来定义的。对于完整的Maude代码，我们请读者参考[7]。4.3局部过程演化局部转换表示单个进程上下文中活动线程的减少。这个内部活动只影响相应的堆。表达式的求值在达到whnf值（W∈Whnf）时终止。当地T_（1/2）=H_（1/2）=θ→AE−→HJ，读作“对活动阈值和θ→A对于H+{θ→AE}转换为HJ“。图1中我们示出了表达惰性评估如何在需求下进行的局部规则。我们避免编写多个类似的过渡规则，允许绑定出现几个标签，对应于规则所允许的不同可能因此，x−<$IA→BE在规则（需求）的等式中，以及xA−A→BE在规则的等式中，手侧意味着对应于闭包x<$→E的线程变为活动的在这种情况下，它是不活动的，否则保持活动或被阻止。在Maude中，我们将语义规则表示为重写规则。有几种方法可以将推理系统映射到重写逻辑[12]。在结构操作语义学的情况下，判断通常具有状态之间的某种转换P→Q的形式，因此直接映射这种转换关系是有意义的将状态之间的关系转换为表示状态的项之间的重写关系。因此，形式P1→ Q1.. . Pn→ QnP0→Q0成为一个条件重写规则的形式P0−→ Q0如果 P1−→ Q1. Pn−→ Qn。通过这种方式，语义规则变成了（条件）重写规则：126M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119›−→›→›−→›→›→›→H+{x→I W}：θ→Ax−→H+{x→IW， θ→AW}（值）ifE∈/Whnf，H+{xIABE}：θAx−→H+{xAABE，θBx}（需求）H：xAx−→H+{xBx}（黑洞）ifE∈/Whnf，H+{xI−A→BE}：θ→Ax y−→H+{xA−<$A→BE，θ→Bxy}（应用需求）H+{x→I λz。E}：θ→Ax y−→H+{x→Iλz。E，θ→AE[y/z]}（β-还原）H：θA令{xi=Ei}在x−→H+{yi我Eiσ}n+{θAσ（x）}（let）›→›→i=1›→其中fresh（yi）（1 ≤ i ≤ n）和σ：=[yi/x1，. ，yn/xn]Fig. 1. 局部转移规则结论中的转换成为规则的主要重写，前提中的转换成为重写条件[18]。局部转换规则（如图1所示）的翻译相当文学。我们引入了两个新的构造器来表示堆。第一个，_：_已在语义规则中使用，以便分隔前导线程- 那些将要进化的东西-从剩下的堆里。第二个，__，是在重写规则的右侧使用，以便将修改的线程与未修改的线程分开，因为这种分离稍后会很有用。实际上，规则（需求）将三个转换规则放在一起，每个转换规则对应于在堆中查询的线程下面给出的重写规则要求表示通过使用排序为TState的变量T，以及用于检测线程是否被修改的辅助操作。注意如何使用排序NonWhnf的变量NW来确保语义规则中的条件E/∈Whnf。规则let还使用辅助操作来构建右侧的新堆。此规则重写进程而不仅仅是堆，因为重命名时，第四个参数必须递增。rl[值]：H + X|-I-> W：Theta|-A-> X=> H + X|-I-> W&θ|-A-> Wrl[demand]：H + X|-T -> NW：Theta|-A-> X=> H + nmd（X|-T -> NW）&md（X|-T -> NW）+ Theta|-B-> X。rl [黑洞]：H：X|-A-> X=>H&X|-B->X。rl[app-demand]：H + X|-T -> NW：Theta|-A-> X Y=>H + nmd（X|-T-> NW）&md（X|-T-> NW）+Theta|-B-> X Y。rl [β-还原]：H + X|-I->\Z. E：Theta|-A->X Y=> H + X|-I->\Z. 的&e0|-A-> E [Y/Z]。rl [let]：令X，N，M中的 L B S >=>.4.4局部并行性局部演化-对应于局部过渡规则-被认为是同时发生的，在一个并行的步骤。图2中给出的规则表示进程内并行线程的演化，其中ET（S）是系统S中允许演化的活动线程的集合H（i，1）是在应用相应的局部规则期间保持不变的H的部分，而K（i，2）包含了H（i，2）的修改后的绑定。它保证了本地转换之间没有干扰。定义ET（S）有几种可能性，取决于可用处理器的数量、允许的推测计算程度、赋予某些线程的优先级等。然后比较不同的调度策略，我们将在4.6节中看到。规则（本地并行）是相当“抽象”的。首先，它具有可变数量的前提，这取决于ET（S）返回的线程数量;其次，它使堆的分离区分修改的线程和未修改的线程。对于它的实现，我们已经通过使用__操作符修改局部规则的右侧来解决第二个问题。为了处理第一个问题，我们设计了几种方法;我们在这里展示了一种方法，它代表了前提的分解，以及通过重写规则逐步我们之所以选择这种形式，是因为它类似于数学表达，简化了所需的策略，而且更有效。我们考虑以下三个重写规则作为实现（局部并行）规则的算法的基本步骤。规则扩展为进程添加了三个参数：第一个是与必须进化的线程相关的变量集（新变量VS，下面解释），第二个表示未修改线程的交集（最初是整个堆）的（部分）求值，第三个表示修改线程的并集（最初是空堆）的（部分）求值。规则并行步骤执行算法，每次解决一个前提这是一个条件重写规则：第一个两个条件（其为匹配等式）从堆H提取对应于变量θ的线程，且第三（重写）条件表示对应于变量θ的前提in（局部并行）。这最后一个条件必须通过使用本地转换规则之一来解决注意到128M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119ppp堆H保持未修改，因为它用于每个前提的解析，并且变量Theta从集合VS中删除。最后，规则契约从进程中删除额外的参数，并执行堆的最终联合rl[延伸]： =>。crl [平行步骤]：E：=查找（Theta，H）/\H1-2：=过滤器（Theta，H）/\

E，N，M>=> 。rl [合同]： => p，H' + K，N，M >。必须控制这三条规则的应用。首先，通过提供变量VS的具体值来应用规则扩展，即ET（S）WLP中的变量，其中P是被重写的进程，S是整个进程系统2;然后，规则并行步骤被应用尽可能多的次数，即，对于ET（S）PARP中的每个线程一次;并且最后，规则契约必须被应用。下面的策略-par->接收一组变量作为参数，corre-par对规则的这种具体应用表示赞同。它表示−→S的关系，语义（在图2中定义）。sop -par->：VarSet。seq -par->（ActVS：VarSet）= extend[VS：VarSet- ActVS：VarSet];（平行步！）;合约。par实现关系−→S的另一种方法将使更多的控制在该策略中，使其遍历可演化变量的集合，并将局部规则应用于这些变量中的每一个（通过其他策略）。虽然在这种情况下，规则并行步骤将被简化，但之前提出的方法已被证明是更有效的，因为重写规则更强大，并简化了策略。4.5全球系统演化在上层，我们定义了由过程集表示的过程系统之间的全局转换。全球转型的一般形式是：S=o{p，HJ}SJpHp∈S其中每个堆Hp（与系统S中的进程p相关联）被变换为HJ，同时可以创建新的进程（在SJ中）。菱形标记是规则名称的占位符。4.5.1平行现在我们考虑系统S内过程的并行演化：（平行） {Hppar−→S HJ}p，H∈SJ段S=<${p，Hp<$}<$p，Hp <$∈S这个规则有可变数量的前提，系统S. 每一个前提都使得相应的过程精确地进化一次2这个交集是在从strategy=par=> below调用策略-par->时计算的M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119129（S，θp，H+{θ→αx#y} θ）pc（S，θp，H+{θ→Bc， c→Ay} θ，−→1 2q，η（nh（x，H））+{cAη（x）z，zBc}1›→ifnf（x，H+{θ→αx#y}）=0›→2q，z，c1，c2是新的标识符，代入η用新的变量图三. （进程创建）规则过渡par−→S。我们通过strategy=par=>来它将策略-par->应用于系统中的每个进程。这一战略是递归，当系统的其余部分（由下面的变量 S ： System 表示）为空时终止strategy=par=>接收与应用于整体的函数ET返回的线程相对应的变量作为参数。系统Strategy-par->是用进程P的可演化变量集调用的，由函数inters计算。sop =par=>：VarSet。seq =par=>（VS：VarSet）=if（match empty）thenidle else（matchrew P：Process S：SystembyP：Process using -par->（inters（P：Process，VS：VarSet）），S：System using =par=>（VS：VarSet））fi.4.5.2多步规则在每个进程内部演化之后，必须在系统级完成以下任务一般来说，这些任务意味着多个单一步骤，每个步骤最多涉及两个过程。设S是一个过程系统，一个规则的名称（kipar），对于每个单步规则S−o→SJ，我们定义一个多步规则规则S=oSJsatisfyingg：S−→o 因此，如果Sj−→oSJJ，则该值为noSJ。THE在某些进程中将单步规则REQ应用于某些绑定可以使得能够将相同的规则REQ应用于相同或其它进程中的其它绑定，但是它永远不能禁用在前一应用之前启用的规则REQ的应用单步规则在Maude中实现为重写规则，而关系==在以后的工作中，通过更多的策略。4.5.3进程创建子进程的初始堆包含进程体中依赖变量求值所需的所有绑定;这些绑定通过函数nh（needed heap）从父进程复制到子进程堆：nh（x，H）收集所有H中从x可到达的绑定。一个新变量的重命名ηPC是为了避免名称冲突。流程创建（参见图3中的−→规则）是如果对必须传递的值有某种依赖性，则会阻止。函数nf（needed free）收集从自由变量派生的依赖关系。让我们再次考虑第3节中作为例子给出的表达式。在应用（let）局部规则之后，产生的堆如左图所示130M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119下图的右侧;（流程创建）规则生成右侧的结构：=其中c7是子进程的输入，而c8是输出;两者都是内部变量，程序员没有定义，因为Eden中的通信是隐式的。PC下面的规则在Maude中实现了−→规则。它使用辅助功能重命名复制到子堆中的堆，并构建新的变量和通道。crl[pc]： X # Y，N，M >=> c1 + c2|-A-> Y，N +1，M +1>（searchVar（X，VVL）Z）+ Z|-B-> c2，0，M'>如果nf（X，H +θ|-T->X# Y）=无/\q：= childName（p，N）/\c2：= c（newvar（p，M））/\c1：= c（newvar（q，0））/\（1）求new var（q，1）的值 I I.seq =pc=> = pc！ .4.5.4通信流程之间的值通信规则如图5所示。当要传递的值对应于一个抽象时，必须复制- 从生产者的堆到消费者的堆-在抽象中评估依赖变量所需的所有绑定。同样，只有当抽象不依赖于挂起的通信时（对应于图4中第一列的讨论也可以应用于这种情况），重命名替换（η）被应用于转移的堆，绑定变量被新变量替换时，才能发生尽管一次通信可能会启用其他通信，但这永远不会导致无限次通信（在一个系统步骤中）。此外，通信的顺序是不相关的，因为已经绑定到值的变量不受通信的影132M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119响。因此，相应的多个图像的图像-st eprule=conm，其中，cicarriesuteveyponicomu nicat iconisweldef i ned。在Maude中很容易实现价值沟通的规则：[com]：M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119133›→›→WHNF解锁：一BxwUnblA Ax（S，θp，H+{x<$→W，θ<$→EB}<$）−→（S，θp，H+{x<$→W，θ<$→EB}<$）WHNF失活：（S，θp，H+{θAW}θ）德ACTI−→（S，θp，H+{θ<$→W} θ）阻塞进程创建：IA（S，θp，H+{θ›→x#y}θ）BPCB−→（S，θp，H+{θ<$→x#y} θ）要求高的流程创建：BpcdB A（S，θp，H+{θ<$→x1#x2} θ）−→（S，θp，H+{θ<$→x1#x2，y<$→E} θ）我如果y<$→E∈nf（x，H）要求沟通：（S，P，H+{cIW}P）vComdI−→（S，p，H+{c<$→W，x<$→E}）我如果x<$→E∈nf（W，H）见图6。日程安排规则 W，N，M> ch，N ' ， M' >=>p，Hp，N，M>（msubs（W '，VVL ））， N' ，N2 >如果nf（W，Hp）=无/\<：= renL（W，c，N'）.当传递一个值时，必须从生产者的堆复制到消费者的堆中，复制所有计算值中的依赖变量所需的绑定。只有在价值不取决于待决通信时，才能进行此复制。4.5.5调度完成所有启用的流程创建和通信后，必须完成以下任务• 同时根据绑定到whnf值的变量解除绑定（wUnbl）。• 在whnf（deact）中取消绑定到值。• 阻止无法执行的进程创建（bpc）。• 挂起进程创建和/或通信（pcd和vComd）所需的苛刻绑定。相应的规则如图6所示，在Maude实现中很容易阅读：crl[wUnbl]： W + θ|-B-> E，N，M>=> W + θ|-A-> E，N，M>如果X= blockedOn（E）。rl[deact]： W，N，M>=> W，N，M>。134M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119crl [bpc]：X# Y，N，M >=> X # Y，N，M>如果T=/=B。crl[pcd]： X # Y，N，M>=> X #Y + Z|-A-> E，N，M > 如果Z|-I-> E + H '：= nf（X，H）。crl[vComd]： W，N，M>=>>最大值W+X|-A->E，N，M>如果X|-I-> E +H' ： = n f （ W ， H ）。由于新的工作负载规则=不确定性=，因此，wUnbl deactbpc pcdvComd=;=，与解释sysUnbling在获得全局转换之前=战略定义了这两种关系：sop =unbl=>.=;=; =。下一篇Maudeseq =unbl=> = =wUnbl=>;=deact=>;=bpc=>;=pcd=>;=vComd=>。sop=sys=>.seq =sys=> = =com=>;=pc=>;=unbl=>。4.5.6过渡系统步骤parsys最后，系统的每一个过渡步骤被定义为=;=。在莫德，下面的策略允许计算转换步长。它将被应用于正在进化的整个系统S，首先它通过传递ET（S）返回的可进化线程集作为参数来应用strategy=par=>。sop ==>.seq ==>=（matchrew S：System by S：System using =par=>（ET（S：System）））;=sys=>.4.6推测并行在任何具体的实现中，对Eden程序的评估都可能导致不同的计算。推测并行性的确切数量取决于可用处理器的数量、调度器决策和基本指令的速度。因此，程序的执行范围可以从将推测减少到最小-仅计算有效要求的内容将其扩展到最大值-执行所有推测计算。虽然前者相当于在单个处理器上执行程序，调度程序优先考虑由主线程发起的需求，但后者相当于拥有无限的处理器集合来评估每个生成的进程的输出。在语义中，也可以反映有限数量的处理器在活动线程之间的分布遵循不同的规则，例如：在线程之间随机分布，或在线程之间公平地分布处理器，或甚至优先考虑主线程的需求并在其他线程之间分布其余的处理器再一次，Maude的设施和模块化使我们能够生产一个简单的-M. Hidalgo-Herrero等人理论计算机科学电子笔记174（2007）119135通过选择函数nf和ET的适当定义来实验不同的替代方案。这些函数可以用不同的方式定义，从而获得不同的Eden语义。在本实现中，我们将每个定义放在不同的Maude模块中。通过实例化定义语义规则的模块，使用具有nf和模块与ET的具体定义，我们得到一个完整的规范伊甸园。5计算措施在本节中，我们将展示如何扩展我们的框架，以便对计算进行测量，例如完成的工作，并行度，通信量等。模块化，特别是规则和策略之间的分离，再次成为有用的工具，因为必要的更改并不意味着修改已经实现的语义规则。首先，重写的术语被扩展为测量的实际值。一种可能的方法是使用一组属性及其值。其中一个属性包含Eden系统（Sys），它将被前面部分中所示的语义规则重写。这里我们展示一些属性的例子。排序属性属性集。子排序属性<属性集。op nilAS：->AttrSet.op ：AttrSet AttrSet -> AttrSet [aslogid：nilAS]。操作系统：系统->属性Work：December2009- 演化的活动线程数opNumProc：Nat -> Attr.- 进程数op MaxPar：Nat -> Attr.- AvPar：Nat -> Attr.-Average thread parallelism op AvProcPar：Nat -> Attr. -平均进程并行度然后，必须定义重写规则来描述这些度量的修改。例如，下面的规则addPC将进程数递增1，规则addET更新已完成的总工作以及最大线程并行度。这些更新由将由策略实例化的变量CardETrl [addPC]：NumProc（N）=> NumProc（N+1）。rl[addET]：MaxPar（Max）Work（W）=>MaxPar（max（Max，CardET））Work（W + CardET）.最后，我们需要修改策略，以便将这些规则与语义规则一起应用。我们在下面展示了其中两种新的改进策略。Strategy=pc=>现在在应用规则pc（进程创建）后应用规则addPC。strategy ==>使用由表达式大小计算的可演化线程数（ET（S：System））更新度量MaxPar和Work的值。se