M演算：新型分布式进程演算抽象机的形式描述

145《理论计算机科学电子札记》66卷第3期（2002年）网址：http://www.elsevier.nl/locate/entcs/volume66.html25页高阶分布过程演算Florence Germaina，Marc Lacostea和Jean-BernardStefaniba法国电信研发部，28，CheminduVieuxChe nee，38243Me ylanCede x，法国电子邮件：fflorence.germain，marc.lacosteg@rd.francetelecom.combINRIA Rho科隆-阿尔卑斯，655，Avenue deinrialpes.fr摘要本文给出了一种新的分布式进程演算M-演算的抽象机的形式描述。M演算可以理解为连接演算的扩展，它实现了以下特性的原始组合：可编程位置，高阶函数和进程，进程移动性和动态绑定。我们的抽象机器涵盖了这些不同的功能，并提出了一个模块化的结构，明确分离的顺序（功能）执行核心的评估机制，后者从基本的编组，位置和路由机制。1介绍对移动和分布式编程的形式化模型的探索仍在继续，这可以从最近的分布式进程演算中看出。这些演算的关键见解是由L。Cardelli在[3]中指出，基于WAN的分布式编程与LAN环境中的分布式编程有很大的不同因此，位置的概念出现在几个最近的过程计算中，例如Join演算[6，9]，Seal演算[17]，Nomadic Pictt [18，19]，D演算[20]，DiTyCo [10，11]，Klaim [13]以及Mobile Ambients [4]的不同变体，例如Safe Ambients [8]或Boxed Ambients[2]。这些演算中的每一个都引入了一个特定的局部性概念，其特征在于其交互协议。例如，在Join演算中，局部交互协议允许局部之间的远程通信和通过go构造的局部迁移。在Mobile Ambients中，交互协议对应于in、out和open能力，其允许环境移入和移出其他环境，并消除环境边界，重新激活。地方的交互协议旨在捕捉不同的方面c 2002年由Elsevier Science B出版。诉在CC BY-NC-ND许可下开放访问。杰曼，拉科斯特，还有史蒂芬妮146分布式系统中的计算：资源访问，进程移动性，访问控制，故障模式等。然而，在一个真正的分布式系统中，人们很可能会遇到不同形式的局部的组合因此，非常希望能够在同一演算中将不同形式的地点结合起来。例如，应该可以将局部故障模型与访问控制模型结合起来。这正是M-演算[16]的目的，它引入了称为细胞的可编程位置的想法。在M-演算中，每个单元包括两部分：负责实现局部交互协议的膜和在单元内执行的内容与Join演算和Ambients中一样，我们为位置命名，并为命名的单元格编写（P）[Q]a与膜P和含量Q。由于细胞膜是一个M演算过程，我们可以在演算中定义控制给定位置的相互作用协议。在分布式演算中，当涉及到结合通信和位置时，也存在许多替代方案。一个极端是Join演算的完全透明的通信模型，其中消息被直接路由到目标位置。在频谱的另一端，人们发现移动环境，其中通信纯粹是本地的环境和远程通信必须使用迁移原语和显式编码的路由来传递环境消息。Seal和Boxed Ambients位于这两个极端之间，提供了跨一个地区边界的通信能力。M-演算提供了一种在这些可能性之间进行权衡的形式。我们仍然提供透明的异步交互，但通信不是直接的。它包括一个基本的步骤，一次只穿过一个细胞膜，使用一个沉默的路由机制，允许每个膜过滤传入和传出的消息。人们可能会注意到，控制迁徙和控制交流之间有着惊人的相似之处。出于这个原因，为了合并这两个方面，我们在M演算中采用面向通信的方法，考虑高阶演算：在我们的设置中，迁移成为形实转换程序或钝化进程的通信。实际的分布式编程也需要某种形式的动态绑定，因为程序（进程）中的特定名称应该绑定到的确切资源直到运行时才需要知道，并且通常取决于该程序将执行的位置。因此，M演算支持一种形式的动态绑定，由此相同的资源名称可以访问不同单元中的这种功能的组合：可编程的地方，高阶进程，透明但可控1异步通信，和动态绑定，使M-演算一个有趣的候选人，一个现实的分布式和移动编程模型。然而，要成为一个现实的编程模型，M-1对于通用的分布式编程，演算表现出局部的默认行为，这允许它们被透明地使用。然而，特定的程序员需求可能需要更丰富的通信语义。因此，演算也使得这种默认行为能够被定制，从而允许显式地对位置交互协议进行编程。杰曼，拉科斯特，还有史蒂芬妮147微积分应该是有效的可实现的。在本文中，我们报告了一个初步的实现M-演算，一个直接实现分布式的ab-机的演算本文详细介绍了这一ab-机器的形式化规范，表明高阶特征，分布和移动性的组合实现也简洁而准确地描述。这项工作表明，即使M-演算构成了（分布式）连接演算的非平凡的高阶扩展，该演算仍然是可实现的，并且它的分布式抽象机实际上并不比连接演算的等价机更复杂。本文中描述的分布式抽象机本身就很有趣。它的模块化结构反映了演算的操作语义。它将标准的顺序功能评估部分与计算的其余部分分开，并确定了在存在移动性的情况下消息的分布式路由所需的关键结构。本文的结构如下。第二节简要介绍了M-演算及其操作语义.第3节形式化地给出了M-演算的抽象机.第4节描述了集中式设置中抽象机的具体实现。第五部分总结了本文的相关工作和未来的研究。2M-演算综述2.1语法图1和图2中给出的M-演算的语法是按值调用的混合-calculus和Join calculus。从前者，我们有抽象和功能应用。从后者中，我们有了带有连接模式和并行组合的资源定义。为此，我们添加单元构造a（P）[Q]，它扩展了Join演算局部构造，以及传递钝化运算符，一个简单名称模式匹配的条件测试[ =V]P; Q，和-演算限制n：P。M演算中的通信采用异步的点对点消息交换的形式，反映了当前大规模网络中的主要通信模式。消息采用应用程序的形式，可以分为两种：形式为rV的消息，其中r是资源名称（消息目标），V是值的元组（消息参数），是从不跨越单元边界的本地消息它们用于给定单元内进程之间的通信。形式为d：rV的消息可以用于不同小区之间的通信，其中d表示目标小区，r表示资源。如果d是表格A，（分别a）目标资源应位于膜内（分别）内容）的单元格名为a. 这些已编址的消息在杰曼，拉科斯特，还有史蒂芬妮148语法：S：：=[系统]根细胞Jn ：S[限制]一V：：=[value]（）[null value]Ju[name]Jd[目标]J（五;：：;五） [元组]Jx：P[抽象]D：：=[定义]>[空定义]JJ. 反应规则J成分[J：：=[join pattern]rx[消息模式]J同步化[姓名：n：：= [解析名称]R[ 资源名称]J一[单元格名称]r：：= [变量资源名称]R[ 资源名称]JX[变量]a：：= [变量单元格名称]一[单元格名称]JX[变量]d：：= [目标名称]一[靶膜]J一[目标内容]u：：=[name]a[细胞名称]r[变量资源名]Jd：r[资源定位]：：=[name pattern]u[name]J[任何名称]J d：[d处的资源]j：r [locatedrresource]Fig. 1. M-演算：符号和名称从一个细胞到另一个细胞。图1收集了M-演算中使用的不同形式的名称我们假设一个无限可数集的细胞名称，CELL（具有一个独特的元素），一个无限可数集的资源名称，REF（具有两个独特的元素，i和o），和一个无限可数集的变量，VAR。我们让x在VAR上变化，r在REF上变化，a在CELL上变化。M-演算中的值可以是空值（）、名称u（可以是单元名称、资源名称或寻址资源名称）、值V的元组或-抽象。请注意，不可能对定义中出现的资源名称进行抽象：x：hx.P i不是合法的M-演算术语。传递a构造与单元构造a（P）[Q]一起是M-演算所它允许细胞的膜过程P冻结整个细胞a的执行。pass运算符的参数是一个接受两个参数的函数：一个与钝化单元格P：：=[过程]0[null过程]JV[值]Ja（P）[P][细胞]J （PjP）[平行组合]J （PP）[应用]Jn：P[限制]J（[=V]P; P）[有条件]Ji[定义]J通过V[钝化]杰曼，拉科斯特，还有史蒂芬妮149Q一一一免费名称：fn（a）=fn（a）=fn（a）=fagfn（r）=frgf n（d：r）=f n（d）[frgf n（）=？fn（d：）=fn（d）fn（：frg）=frgfn（（））= fn（0）=？fn（x：P）= fn（P）n fxgfn（n：P）= fn（P）nfngfn（P Q）= fn（P）[fn（Q）fn（hDi）=fn（D）fn（D;D0）=fn（D）[fn（D0）f n（>）=？f n （ J.P ） = （ fn （ P ） nfn（J ））[d n（J ）fn（r1x1j： jrqxq）=fn（r1x1）[：[fn（rqx）f n（r（x1; ：： ;xp））=fr;x1; ： ：;xpgfn（a（P）[Q]）= fag[fn（P）[fn（Q）fn （ P j Q ） = fn （ P ） [fn（Q）fn（[=V]P;Q）=fn（）[fn（P）[fn（Q）[fn（V）fn（passV）=fag[fn（V）fn（n：S）= fn（S）nfngfn（[P]）= fn（P）fn（（V1; ： ;Vp））=fn（V1）[：fn（Vp）定义的本地名称：dln（n：P）= dln（P）n fngdln（P Q）=？dln（hDi）= dln（D）dln（D;D0）=dln（D）[dln（D0）dln（>）=？dl n（J. P）=dn（J）dln（a（P）[Q]）=？dln（P j Q）= dln（P）[dln（Q）dln（[= V] P; Q）=？通过V）=？dln（S）=？dln（V）=？dln（0）=？活性细胞：cells（n：P）= cells（P）n fngcells（P Q）=？细胞（h D i）=？cells（a（P）[Q]）= fag [cells（P）[cells（Q）cells（PjQ）= cells（P）[cells（Q）cells（[ =V] P; Q）=？细胞（通过V）=？cells（n：S）= cells（S）n fng细胞（[P]）=细胞（P）细胞（V）=？cells（0）=？cells（x（P）[Q]）=？图二. M演算：自由名、定义的局部名和活动单元以及对应于钝化电池的内容物的重命名。这个结构，连同高阶特征，负责M-演算的表达能力，如本节末尾的例子所示。一个M-上下文是一个根据与标准M-演算术语相同的语法构建的术语，加上一个常数，即洞。我们用Pfg表示M-上下文.用一个M-演算项Q填充Pf g中的洞，得到一个记为PfQ g的M-演算项.M-演算中的求值上下文是根据以下语法构建的M-上下文E：：= jEVjPE jn：E j（EjP）ja（P）[E]ja（E）[P]j[E]我们使用下面的符号约定：我们写fn（P）表示P的自由名称集，dn（J）表 示 连 接 模 式 J 的 定 义 名 称 集 。 更 精 确 地 ， dn （ r1x1j ： j rqxq ）=fr1; ：;rqg。 我们还将P的定义的局部名称的集合写成dl n（P），并且将在P中找到的活动单元的名称的多集合写成单元（P）。这些集合在图2中递归定义杰曼，拉科斯特，还有史蒂芬妮150一我们注意到=ft1=u1; ：;tq=uqg是一个有限的替换，其中项ti被替换为名称ui。 我们记P或Pft1=u1; ：;tq= uqg为代入项P的图像。 我们用t来表示项的有限元组（t1; ：;tq）。 当元组t和u具有相同的大小时，我们注意到ft=ug替换ft1=u1; ：;tp=upg。同样的符号约定也适用于元组的元组。我们还使用符号：P来表示形实转换程序x：P，其中x在P中不是自由的。两个过程P和Q直到-转化的等价性记为P = Q.我们记得在n：P中，x：P，r1x1 j： j rqxq。 P中，名称和变量n，x和xij在P中有界。2.2操作语义M -演算的运算语义是以CHAM风格[1]定义的，它使用一个结构方程和一个归约关系！. 结构等价关系是满足规则S的最小等价关系.努扎姆我是S。图3中给出的CONTEXT结构规则包括约束算子的作用域挤压规则和求值上下文的等价、欠转换和同余的标准规则。M -演算的归约关系，！定义为满足图3中给出的规则的最小关系。条件分支的计算规则使用match（）谓词，定义如下：match（; V）match（u;u）match（a：;a：r） match（：r;a：r）match（：;a：r）鲁尔河COMM类似于Join演算的JOIN规则：当一组本地消息匹配定义的模式时，定义中的受保护进程的一个新实例 鲁尔河PASSIV是新颖的，定义了语义关内 构建体指令传递V只能在一个叫A的细胞膜。 它的作用是冻结膜过程， 单元格的内容处理，并将结果thunk作为参数传递给函数V。路由规则处理消息到目标资源的传输。根据定义，局部信息的路由仅发生在同一细胞内的膜和内容物之间在寻址消息的路由规则中，我们将b或b写成b。这些规则处理当前在其目标细胞外、细胞膜内或细胞内容物内发现的消息的不同情况。已经到达它们的目标细胞膜或内容物的消息只是变成本地消息（规则R。的1. MM、CM、EM、CC、MC）。目标位于子单元内或目标单元的内容中的资源的given单元外部的消息被i端口上的细胞膜过滤（规则R. 的1. C和R。一台2. IN）。细胞膜内的信息可以在细胞内容物内或细胞外自由流动杰曼，拉科斯特，还有史蒂芬妮151一u（规则R。一台2. MC，ME）。最后，细胞内容内的消息针对膜中的子细胞或当前细胞外的细胞，由o端口上的细胞膜过滤（规则R）。 一台 2. （ 见 附件）。M演算中的路由规则对应于基本的路由步骤，它强制执行以下两个原则：所有消息每次路由一个边界（外部到膜，膜到内容，反之亦然）;没有消息可以进入或离开细胞的内容，除非首先被细胞的膜处理。2.3M-演算中的程序设计下面的例子说明了微积分的主要结构示例1.透明的通信a`laJoin演算可以通过使用细胞膜中的转发器在M演算中实现。一个样本转发器由以下过程给出：Fwd=hi（d;r;v）. d：rv;o（d;r;v）. d：rvi置于细胞膜中，Fwd只是在膜中释放传入和传出的信息。路由规则确保释放的消息继续其朝向其目标单元的旅程这样的转发器是完全无状态的，即使目标单元在消息被路由到它的同时移动，它也能示例2. 小区移动性可以使用高阶消息和钝化来实现（参见Join演算中的go构造和MobileAmbients中的进出能力）。下面的单元格Qm（a）可以被移动到不同的单元格：Qm（a） = a（Fwdjhgou . Go（a;u）i）[Q]Go（a; u）=通过p q：（u：enter：a（p（））[q（）]）一个（gou）请求导致单元格的钝化，并将其作为一个形实转换程序发送到名为u的单元格。如果请求来自细胞的外部，结果是一种客观形式的移动。如果请求来自单元格的内容，则结果是移动的主观形式单元格u的膜可以包含下面的过程Enter（u），以允许在其内容中插入新单元格：输入（u）= h输入f。 传递p q：u（p（））[q（）j f（）]i实施例3. 细胞膜可以实现各种形式的控制。下面的单元格Qo（a）Qo（a）=son：a（Fwdjhsus pendjon. S（a;s）;resumejs f. R（a;f;on）;打开. O（a）;更新f. U（a; f）i）[Q]S（a;s）=passa pq：a（p（）j（sq））[0]R（a;f;on）=passa pq：a（p（）jon）[f（）]O（a）=passapq：q（）U（a;f）=passapq：a（f（））[q（）]杰曼，拉科斯特，还有史蒂芬妮152XXi结构等同性规则：S. 努扎姆PARn62fn（Q）（n：P）j Qn：P j QS. 努扎姆顶部[ n：P ]n：[P]S. 努扎姆构件n62fn（Q）^n 6= aa（n：P）[Q]n：a（P）[Q]S.P =QPQS. 努扎姆CONTn62fn（P）^n 6= aa（P）[n：Q]n：a（P）[Q]S. 上下文PQEfPg EfQg约简规则：计算R.BETA（x：P）V！P fV = gR. 如果. 然后match（;V）（[= V]P;Q）！ PR. 如果. 其他：match（;V）（[= V ]P;Q）！QR. PASSIVa（passa V j P）[Q]！ V（：P）（：Q）R. COMMhDi=hD0;r1x1j ：jrnxn。PiVihDi jr1V 1j：j rnV n！hDij Pf = g0 0 0 0 0 0 0 0R. P. EQUIVPPP ！QQ QR. S. EQUIVS1S1S1！ S2 S2S2P！ QS1！S2精简规则：路由本地邮件R. L.MCr62dln（P）r 2 dln（Q）a（P jrV）[Q]！a（P）[Q jrV]R. L.CMr 2 dln（P） r62dln（Q）a（P）[Q jrV]！a（P jrV）[Q]简化规则：路由已寻址邮件R. 的1.MMr 2 dln（P）R. 的1.EMr 2 dln（P）R. 的1.CMr 2 dln（P）R. 的1.CCr 2 dln（Q）a（P）[Q j a：rV]！a（P）[Q jrV]R. 的1.MCr 2 dln（Q）a（P j a：rV）[Q]！a（P）[Q jrV]R. 的1.ECr 2 dln（Q）a：rVj a（P）[Q]！a（P ji（a; r;V））[Q]R. 一台2.在b2细胞（P）[细胞（Q）b 6= ab：r V j a（P）[Q]！a（P j i（b; r; V））[Q]R. 一台2.MCb2细胞（Q）n细胞（P）b 6=aa（P j b：rV）[Q]！a（P）[Q jb：rV]a（Pj a：r V）[Q]！a（P j rV）[Q]a：r V j a（P）[Q]！a（P j rV）[Q]a（P）[Q j a：rV]！a（PjrV）[Q]杰曼，拉科斯特，还有史蒂芬妮153R. 一台2.我b62个细胞（P）[细胞（Q）b6=aR. 一台2.出来b 62个细胞（Q）b aa（P j b：rV）[Q]！a（P）[Q]j b：rVa（P）[Q j b：rV]！a（P jo（b; r;V））[Q]图三.结构等价和归约规则杰曼，拉科斯特，还有史蒂芬妮1543M-演算抽象机我们现在描述一个用于M演算的分布式抽象机（AM），称为CLAM（细胞抽象机）。3.1设计原则验证基于M演算的“设计到实现”的正式方法来构建现实可靠的分布式基础设施意味着证明模型的有效可实现性。因此，M-演算应该在实现模型的实现的正式规范中进行细化-在本文中采用AM的形式。AM的抽象级别应该既紧密地反映分布式计算的现有基础设施，同时仍然足够接近微积分，以便于表达和证明与实现相关的属性。考虑到这一点，我们为AM做出了以下设计决策：AM是通过M -演算的直接细化获得的：AM内部受到演算的核心原语的强烈启发。此外，通过M-演算约化关系的近似一对一的平移，得到了AM态的约化AM在异步分布式环境中是有效可实现的。AM提供了逻辑和物理分布之间的清晰分离，如在Join演算中，其中位置树中的顶级位置代表托管该树的物理站点。真正的分布式交互通过物理站点之间的异步消息传递发生，即，在顶级位置之间。因此，相应的AM归约规则仅涉及单个位置，并且可能涉及用于消息发送或接收的全局以太（参见图4和诸如M. 的1. EC. R，M. 一台2. 我我R或M。图B.3和B.4中的FOR WAR D）。特别是，与路由有关的决策纯粹是本地的。AM组织是模块化的：AM清楚地将函数术语的评估（由一个明确的评估器处理）与专用于并发和分发管理的执行核心分离开来。名称管理和路由机制与计算机分离，AM的一部分。在创建单元格时，单元格名称保证是全局唯一的。 这个属性在演算中使用operator和scope extrusion规则来确保，并且在AM中使用限定名（包括对创建它们的位置的引用）来细化。为寻址消息获得确定性路由算法的一个关键特性是在执行过程中保持单元名称的唯一性。微积分使用[16]的类型系统（主语归约）来强制执行这一点。在实现级别，单元名称唯一性通过分布式查找服务来实现，该分布式查找服务包含定义的当前本地化（在位置中）和位置的当前本地化（在分布的物理单元上），并且该分布式查找服务用作在AM中细化M演算的路由规则的基础。杰曼，拉科斯特，还有史蒂芬妮1553.2概述我们对源语言做了三个微小的修改(1) 为了让一个明确的识别的CLAM组件专门在评估的funcional条款，我们介绍了语法类别的表达式，这对应于过程和值的M-演算语法，并在其上的功能评估器将执行计算返回值。(2) 我们增加了两个特殊的值，具体化膜和具体化内容，分别用于具体化细胞的膜和内容(3) 在M演算中，膜可以包括细胞的平行组合。在续集中，我们只考虑微积分的一个子集，其中膜过程在整个执行过程中保持平坦不包含任何子单元格。这种限制简化了AM的描述（完整演算的AM可以很容易地从我们下面描述的AM中导出），并且可以通过类型系统来实施，该类型系统是[16]中描述的类型系统的轻微变体。这种类型系统还强制执行一个属性的唯一性的细胞名称，这是至关重要的，以保证路由的确定性，在演算和抽象机，后者的描述是强烈的基础上，这一属性。CLAM采用位置集合的形式，可能分布在几台机器上。机器通过全局以太E连接，在任何时刻，它都包含在不同机器之间传输的消息集机器代表顶级执行单元，通常是UNIX系统进程的抽象为了支持路由，每台机器都包含一个查找服务来定位两个通信资源（在哪个位置定义了资源和位置（位置驻留在哪台机器我们将分别讨论本地路由和远程路由，这取决于消息是路由到同一台机器还是不同的机器。一个位置托管多个单位（即，非单元）进程共同生活在单元层次结构的同一级别，并保持指向多个子位置的指针因此，位置被组织在森林中，每台机器包含一个位置树。细胞膜在CLAM中由一种称为膜位置的特殊位置表示。由膜位置主持的平坦突起是构成细胞膜的过程。一个膜位置有两种子位置：一个单一的以太位置（或简称以太），它收集在细胞内容的顶层发现的扁平过程，以及实现在细胞内容中发现的子细胞的因此，位置树的每个元素要么是一个以太位置（叶），要么是一个膜位置（节点），后者只拥有一个以太子位置。我们将每个位置树的根称为顶部位置，通常写为l>。对于commodity，还引入了一个用于整个系统（机器和全局以太网）的虚拟根位置，名为>（参见图4）。CLAM中的每个位置都包括一个执行引擎和一个功能评估器，两个组件之间有一个定义良好的接口 执行杰曼，拉科斯特，还有史蒂芬妮156M1MnP1P n...年q1Qn不EM 1||......这是什么？见图4。CLAM分布模型引擎维护本地位置状态。函数求值器只是将给定的表达式作为输入返回值给执行引擎。更确切地说，函数求值器对应用程序和抽象进行操作，并返回值，这些值要么是M演算值，要么是对应于M演算的非函数原语的扩展值，即特殊值具体化膜和具体化内容、条件分支、单元、并行组合、限制、定义和钝化构造.为简洁起见，省略了评估器的正式特征。3.3机器和位置状态附录A中收集了对CLAM为了实现的目的，我们用一种特殊的名称来丰富值的集合：内部名称是用于指定内部位置的丰富名称，或者来自演算的实体，如资源或单元。它们保存创建它们的机器的名称，通常出现在进程环境中，其中演算级别的名称映射到内部名称。位置l由元组h; D; H; R; E; Li描述。位置名称l在整个系统的级别上是唯一的。演算中相应单元格的名称仅针对膜位置定义D表示在l中找到的可激活定义集，而H表示消息堆，其中保存着等待本地定义名称上的通信的消息R表示位置运行队列，其中存储要执行的进程最后，E和L被用来跟踪l的子位置，分别是醚类和膜类。注意，对于膜位置，E总是单例，或者对于醚位置，E总是空的-在这种情况下，机器由元组hm：N：O：L i表示，并且在分布式系统中由其机器名称m唯一标识。 N是一个名称工厂，用于创建新的内部名称。 O是机器本地查找服务。 L通过将位置名称映射到h; D; H; R; E; Li元组来跟踪驻留在m上的位置。杰曼，拉科斯特，还有史蒂芬妮157ee！H3.4减小规则位置的演变是由归约规则描述的，这些归约规则要么涉及单个机器内的活动，要么涉及向/从全局以太发送/接收消息的机器例如，我们写m： N： O：Lf lD： H！ h; Ri;：g k E fm！ Mle：LD0： H0七！镁！m： N0：O0：L0fl！ h;R0i; ：gkEfm！ m07！M：：Msggl：L0对于机器m，其中：（i）位置l的状态h;D;H;R;le;Li变为h;D0;H0;R0; l;L0i;（ii）在网络上发送消息msg（全局以太网E）从机器M到机器M0。在规则上下文中，我们编写任何非重要的位置状态的组成部分，例如，在一个实施例中，L; Ri.执行引擎的核心主要处理顺序计算（见图B.1）。为了保证执行财产的公平，为了确保位于运行队列中的进程最终将在有限数量的计算步骤之后运行，新创建的进程通常被放置在运行队列的末端：例如，通过立即运行P并调度Q以供稍后执行（M）来解释并行组合PjQ。PRL规则）。表达式通过委托给函数计算器来处理。然后将评估结果（扩展值）放置在运行队列的末尾分枝EVAL规则实际上描述了执行引擎和函数求值器之间的接口。两个抽象编码[[ ]]负载[[ ]]卸载捕获表达式加载和unlod-与函数求值器进行交互。我们不进一步描述函数求值器，但是可以为此插入任何用于值传递的求值器-calculus，假设求值器处理的值的范围覆盖了calculus中定义的值。新资源或单元名称的创建简单地通过新内部名称i的创建来表示，该内部名称i被添加到N（M）。新规则）。 在规则M中，如果. 然后，M。如果. 否则，我们使用环境来命名模式和价值观。本地通信由类似于Join演算AM [14]的规则（见图B.2）指定，因为所涉及的原语是直接Join演算构造。InM.DEF，一个新遇到的定义与适当的环 境 一 起 存 储 在 D The internal names corresponding to defined namesbecome new heap entries.在查找服务中还添加了将每个定义的名称与当前位置进行映射的在连接模式J中接收到的名字rn（J）只是出现在消息模式中的参数变量。对于新消息，如果接收者的名称已经作为堆条目存在，即，如果目标定义已经被处理，则消息被消费，并且其参数在匹配的堆条目中排队否则，将消息放回运行队列的末尾以供进一步处理（M。MSG规则）。定义的有效激活，即，当对于连接模式的每个定义名称，0杰曼，拉科斯特，还有史蒂芬妮158RV一个消息在堆中挂起（M. COMM规则）。改变位置森林的结构的操作是单元创建和单元钝化/激活。后者的讨论被推迟到细胞迁移机制的描述。细胞生成（M. CELL规则）在进程b（P）[Q]运行时发生。为新的细胞膜创建兄弟位置l0，以及为内容创建l0的子位置l00。然后分别用P和Q初始化运行队列10和100在启动时，给定的机器仅包含顶部位置，其中单元进程在其运行队列中以通过产生新的顶部位置后代来触发位置树的创建：为新的单元内容创建新的位置，并且顶部位置然后表示未来约简步骤中的新的单元膜（M。CELL>rule）。我们现在描述其他AM减少规则，其涉及远程通信和迁移。3.5远程通信和迁移路由依赖于分布式查找服务。对于这里被视为分布式数据库的查找服务，各种更新策略都是可能的，例如，通过使用原子广播来维护一致的视图，或者允许某些视图暂时不一致，但使用转发器将消息反弹到正确的目的地。数据库应满足以下属性：定义3.1分布式查找服务是可靠的，如果在分布式数据库的视图暂时不一致的情况下，消息路由的唯一后果是延迟消息发送或接收，前提是机器间通信可靠（全局以太网不会丢弃消息）。在我们的AM中，我们选择了分布式数据库的特定形式化，其中每个数据库片段都是定义和位置的本地查找服务。我们还选择了一个特定的路由算法R*，它使用转发器和捎带路由信息更新的通信消息。时间戳用于表示单元或定义的迁移的各个时刻，以避免由于查找服务中包含的陈旧路由信息而导致的通信不一致在R* 中，路由由两种类型的规则捕获，分别用于本地消息和寻址消息（见图B.3和B.4）。图5总结了位置之间的消息移动，表示为菱形，对于本地消息和寻址消息的情况。在图中还显示了细胞膜和内容边界，它们根据消息是从/到细胞的外部（E）、其膜（M）还是其内容（C）来命名归约规则，如规则M中所示。L. CM，其描述了局部信息从细胞内容物到膜的迁移。本地消息的规则严格遵循计算中的相应规则。例如，AM规则M。L. MC实现了微积分规则R。L. MC，并允许消息在位置树中向下移动：消息e可以直接输入杰曼，拉科斯特，还有史蒂芬妮159膜位置或虚拟位置TM.A1.EM /ECM.A2.INM.A2.ME膜M.A1.MM以太位置或全局以太M.A1.MCM.A2.MCM.A1.CMM.A2.OUTM.A1.CC内容膜M.L.MCM.L.CM内容当前位置的以太子位置，如果资源r被定义在该子位置内。本地消息的路由寻址消息图五. CLAM中的路由寻址消息的路由包括物理定位的路由规则，例如， M. 的1. EM. L，M。的1. EC. L或M。一台2. 我我L和物理上的远程路由规则，例如， M. 的1. EC. R和M。一台2. 我我R. 在这两种情况下，消息都是“按原样”路由的，实现目标小区的位置。以下是一些示例规则：物理定位规则：以位置l中定义的资源为目标的消息，并且当前位于其周围的以太中，可以直接进入其目的地（M。的1. EM. L规则）。一个膜位置和它的周围以太之间的消息路由也由规则M指定。一台2.IN. L和M。一台2. 我我L. target单元必须简单地为查找服务所知。物理远程规则：当一个消息在一个物理上遥远的位置时，它被打包在初始机器的顶部位置，连同路由信息（当前环境和本地查找服务的状态），并通过线路发送到目标机器;此外，转发器被留在本地查找服务中，用于消息参数中出现的名称（M。一台2. 我我R规则）。 当在目标机器的顶部位置1>处接收时，消息被解包并添加在1>（M）的运行队列的末尾。的1.EC. R规则）。通过将刚接收到的路由信息与其自身的路由信息合并，更新查找服务。这两个规则类似于AM的Join演算的远程通信规则[14]。最后，M。FORWARD规则处理发送到不再包含目标位置的机器的消息（由于先前的迁移）。电池钝化由规则M描述。PASSIV，而细胞激活由规则M描述。膜和M. 内容（见图B.2）。外-杰曼，拉科斯特，还有史蒂芬妮160e传递一 个V的操作会导致当前位置 l及其后代的双重具体化，使用值reifymembrane和reifycontent，然后将其作为参数传递给V。结果进程被移动到在l的兄弟节点中找到的以太位置。使用提取函数从当前机器当前托管的位置集合L中移除钝化的位置子树，这两者都根据子树的状态计算reify膜和reify内容值，并更新L2。钝化仅限于发生在非顶部位置的位置内。 分枝一台2. 我我R规则包括指定在远程消息发送操作之前更新本地查找服务的条件转发器留在本地查找服务中。与Join演算AM中不同，本地查找服务不能用所有迁移资源的目标位置来更新：一般而言，钝化资源将在钝化时未知的新位置中被激活（仅目标机器是已知的）。实际上，这个目标位置是在远程机器上完成消息接收操作之后动态确定的然后，我们的想法是修改每个钝化位置的本地每个钝化资源），使得：（i）每个钝化位置被映射到目标机器;(ii)被钝化的资源被映射到被写为j的特殊位置（未知位置），该位置本身被映射到目标机器。可以进行直接优化，因为来自钝化位置的严格子位置的所有钝化资源在激活之后保持它们自己的位置。分枝MEMBRANE规则导致在当前位置内解包具体化的组成部分膜使用插入物的方法平坦 功能3. 具体化可激活定义和未决消息分别在本地可激活定义集和消息堆中移动具体化的运行队列被插入到本地运行队列的末尾。然后，使用解包元素的新位置更新查找服务。分枝CONTENT规则导致使用insertsublocs函数在reify内容进程的组件的当前位置内解包。具体化的以太子位置直接与当前位置合并至于M.MEMBRANE规则，查找服务也会更新。AM满足一些性质，这些性质在约简下是不变不变量3.2在每台机器m上，位置被组织成一棵树。3.3如果机器m托管位置l，则该位置的名称包含在m的查找服务中：8（m; l）2（MN AME L OC N M）l2domm：L=）9 t2 T IME S TAMP f l7！hm; t igm：O不变式3.4（i）当在机器m上接收到以名称a：r为目标的消息时，在m上存在名为a的位置或用于2 给定位置l：h;D;H;R;l;Li，我们使用值具体化膜（D;H;R）具体化可激活的定义D、消息堆H和位置的运行队列R，并且值具体化内容（le;L）以具体化l的所有子位置，即，以太le，L的位置，以及它们所有的后代。3例如，这个函数可以定义为插入hD[D m; H[Hm; R：：R m i。flat （固化膜）（Dm）;Hm ;Rm ）;D;H;R）=杰曼，拉科斯特，还有史蒂芬妮161字节码字节码装载机剂调度器LOOK-UP运行时间数据服务结构剂3代理0（根）执行发动机移动远程通信。军事指挥部。顺序核心剂2评估器计算规则剂1见图6。VM的结构向另一台机器发送消息。(ii) 当一个作为消息参数被钝化的信元从机器m发送到m 0时，则在本地创建一个从m到m 0的转发器。第三个不变量保证机器之间的路由确定性（消息在给定时间只能被路由到单个机器），以及同一机器的位置之间的路由确定性（在给定机器中，消息在给定时间只能被路由到单个位置）。猜想3.5（合理性）使用R* 作为路由算法的查找服务族（Om）m2MNAME是合理的.最后，我们认为以下性质在归约下保持不变，这可能是证明CLAM关于M-演算的正确性的起点猜想3.6（正确性）8m2 MN AME8（l; r）2（L OC N MREF），使得l2dom m：L^ l：R=：（; P）：^ r2dom：lbm：O（（r））=）r2dln（P）4C-VM实现在本节中，我们简要描述了一个集中式的M-演算实现，称为C-VM（蜂窝虚拟机），基于上一节中定义的CLAMC-VM平台的设计目标是获得合理复杂度的CLAM的可移植且易于扩展的实现，将性能和其他优化留给进一步研究。我们选择实现一个抽象的机器代码解释器，这既是因为需要能够在机器之间移动代码，需要一个通用的可执行格式，也是因为它允许对M-演算表达式进行交互式求值。因此，C-VM平台以编译器的形式出现，该编译器将M-演算术语翻译成字节码，字节码又由虚拟机（VM）运行编译器是用OCaml编写VM本身是用Java编写鉴于杰曼，拉科斯特，还有史蒂芬妮162这个决定使得与许多用Java编写的现有分布式中间件（如Java RMI）进行互操作成为可能。与ZINC[7]，JO CAML或TyCO [10，12]等使用寄存器或代码闭包的实现相反，字节码非常接近汇编语言，我们选择使字节码更接近微积分语法而不是底层硬件-这也是Java虚拟机中的一个这个设计决策与第3节中介绍的CLAM是一致的，CLAM通过屏蔽许多实现特性来保持分布式系统的相当高的层次。这种选择带来了几个好处：在语言级别，它可以使实现的正确性证明更容易;它也是迈向面向效率的运行时的第一步：正如[12]所指出的，在字节码结构中反映过程项的嵌套允许直接优化：涉及处理项的内部数据结构的每个VM操作可以扩展为字节码指令序列的直接转换，这是一种在