理论计算机科学电子笔记241（2009）85-100www.elsevier.com/locate/entcsπ演算中的封装与动态模块性DanielHirschko n，Aur'elienPardonENSLyon，LIP，Universit'edeLyon，CNRS，INRIA汤姆·赫斯科维茨LAMA，Universit'edeSavoie，CNRS塞缪尔·海姆LIFL、Universit'edeLille1、INRIA、CNRS达米安·普斯SARDES、LIG、格勒诺布尔、CNRS、INRIA摘要我们描述了一个过程演算具有高层次的结构，面向组件的编程在分布式环境中。我们提出了一个高阶π演算的扩展，旨在捕获与基于组件的编程相关的几个重要机制，如动态更新，重新配置和代码迁移。在本文中，我们主要关注的是建立一个分布式实现我们的演算的可能性。因此，我们定义了一个低级演算，它描述了如何实现高级构造，以及在运行时操作的数据结构的细节。我们还讨论了当前和未来的研究方向，我们的分析基于组件的编程。关键词：分布式计算，基于组件的编程，进程代数，高阶演算，抽象机。1动态模块化的核心演算1.1这项工作本文介绍了面向组件编程和π演算的工作。我们的长期目标是设计和实现满足以下要求的原型编程语言。这一工作得到了法国项目ANRArassia“M o dulari t'e Dynamique Fiable”的支持。1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.06.00586D. Hirschkoff等人/理论计算机科学电子笔记241（2009）85• 它应该适合并发的分布式编程。例如，通常的分布式并行算法应该容易实现，以及网络的低层通信基础设施。此外，它应该享有一个很好理解和易于处理的行为理论。• 它应该提供模块化的构造，在标准的非正式意义上，程序应该被构建为在显式接口上交互的相对独立的计算单元（或模块）的组装。此外，模块化应该具有封装特性，例如，应该可以交换实现相同接口的两个模块，而不需要删除代码的其余部分• 程序的模块化结构应该在执行时可用，以便简化标准的动态操作，如迁移，动态更新或模块的钝化。我们称这种需求为动态模块化。动态模块化的概念集合了我们对建模和分析感兴趣的• 最后，我们正在寻求一种合理的可实现的语言，至少允许分布式应用程序的快速原型在本文中，我们描述了我们的核心进程代数来表示和分析动态模块化的建议（本节）。在设计这个正式的模型，我们把重点放在可能性部署和执行过程中的分布式方式。在第2节中，我们通过定义用于分布式执行进程的实验机来描述我们的原型实现。这种描述是通过定义一个新的过程演算来给出的，其中底层方面与实现（特别是通信协议）以及数据结构有关。 在机器中工作，是明确的。1.2kπ的性质和语义为了提供一个正式的处理上述问题，我们研究 高阶π演算的一个扩展，称为kπ。我们选择π-演算 有两个主要原因：首先，基于消息的并发似乎是在合理的抽象级别上定义并发编程模型的合适选择。第二，在像π-演算这样的过程代数的背景下工作，可以定义一个核心形式主义，我们可以在其中分析主要问题，理论和实用的，涉及到实现动态模块化的原语。第三，我们可能希望这能从基于π演算的形式主义的大量研究我们的演算继承了许多以前的研究，其中[8，7，3]，特别是凯尔演算[2，14]的思想。 进程的语法在图1除了通常的π-演算结构，我们还有模n[P]，它可以被看作是定位过程（注意，模可以嵌套）。 M.P是一个愿意发出（第一或更高阶）消息M，然后继续进行的过程， P. Rd P代表愿意获取资源的进程：这可能意味着接收到一阶或高阶消息（分别为a（x）和a（X）），或者D. Hirschkoff等人/理论计算机科学电子笔记241（2009）8587.............→⟨ ⟩→≡关于我们P，Q：：= P|P（νn）P 0n [P]n [X]M.PRd P（过程）M：：=a n a P a X（输出前缀）R：：=a（x）a（X）n[X]（输入前缀）E：：=[] E |P（νn）En [E]（evaluationcontext）Fig. 1. kπ：过程、评价环境的a，b∈/capt（E1）capt（E2）E[E1 [a] b] p|E2 [a（x）d Q]] → E [E1 [P]|E2 [Q {b/x}]]K-COMMHOfn（PJ）（capt（E1）capt（E2））=E[E1 [aPJ.P]|E2 [a（X）d Q]] → E [E1 [P]|E2 [Q {PJ/X}]]E [n [P]|n [X] d Q] → E [Q {P/X}]K-CONGRPJ <$P→Q Q <$QJPJ→QJ图二. kπ的运算语义钝化模块。输入前缀和限制是绑定构造，我们将进程P的自由名写成fn（P）。b /x（分别 P/X）表示 捕获避免了名称x的替换（分别，过程变量X），带有名称b（分别方法P）。请注意，过程变量（X）本身并不构成过程：它必须可以包含在模块（n[X]）或消息（a X .P）中。这个限制主要保证了几个模块的内容不能合并到一个模块中;这有助于简化微积分的实现图2给出了定义归约关系的规则。它利用了评估上下文，这是一个没有在前缀下出现的洞的过程（图1）。给定一个求值上下文E，我们定义E中捕获的名字的集合，写作capt（E），作为E中出现洞时绑定的名字的集合。的定义利用了结构同余，满足以下公理的最小同余：P|0 PP|Q Q|PP|（Q|R）（P |Q）|R（νc）（νd）P（νd）（νc）P（νc）（P|Q）可持续发展|（νc）Q如果c∈/fn（P）（νc）0<$0K-COMMK-P屁股88D. Hirschkoff等人/理论计算机科学电子笔记241（2009）85|⟨ ⟩⟨ ⟩≡N2一N3K1K2K3BN1M一个kπ过程的例子。图三. 一种配置。kπ项表示由模块层次结构组成的配置，其中执行进程。为了说明在kπ中工作的机制，我们简要讨论一个示例配置。 给定一些kπ过程P、PiJ、Qi，图3描绘了以下形式的过程：（va）（m[P]|n1[P1]|n2[P2]|n3[P3J]|k1[（νb）（Q1|k2[Q2]|k3[Q3]）]）(note对A和B的限制的局部化没有出现在图片上）。kπ中的相互作用基本上有两种形式：通信和钝化。通信涉及一个名称或一个过程的传输;它是遥远的，在这个意义上，一个过程a b .P可以与位于不同位置的接收者a（x）dQ同步，只要他们共享名称a。在图中，运行在k3中的进程可以与运行在n3中的另一个进程交换消息（使用通道a），也可以与运行在k2中的第三个进程交换消息（使用通道b）。相反，钝化是局部的：只有在n1处运行的进程才能钝化模块n2。这是由图2的第三个公理描述的：直到结构一致，被钝化的模块和控制它的过程必须是并行的。钝化是我们的形式主义中的一个核心结构，可以用来实现与动态模块化相关的非常不同的操作。例如，在上面的约简中取Q=nJ[X]会导致一个简单的模块重命名操作;当Q=c X时，模块n将被“冻结”并编组到一个消息中，在通道c上发送;最后当考虑kπ过程行为的实际实现时，似乎最后两个例子显然比第一个例子涉及更昂贵的操作1.3关于kπ定义的设计选择1.3.1作为本地化资源的我们在kπ的设计中做出的一个重要承诺是，与现有的几个建议相反，我们不允许通道名称跨模块边界挤出：我们既不包括结构同余中的形式n[（νb）P]（νb）n[PD. Hirschkoff等人/理论计算机科学电子笔记241（2009）8589模块沿着减少步骤，将需要它。这种设计选择与我们在kπ中提出的模的概念有关：如果我们允许名称挤出，一些过程将允许两个合法但非常不同的缩减路径。的确，Pd=efm [（νa）b <$a <$.P]|b（x）.Q|m [X] d（m1 [X]|m2 [X]）。我们将有以下的减少序列P →（νa）（m [P]|Q {a/x}|m [X] d（m1 [X]|m2 [X]））→（νa）（Q {a/x}|m1 [P]|m2 [P]）和P → b（x）.Q|m1 [（νa）b <$a <$.P]|m2 [（νa）b <$a <$.P]→（νa）（Q {a/x}|m1 [P]）|m2 [（νa）b <$a <$.P]我们声称，这些路径都不是完全令人满意的，这种情况应该避免-这两种行为之间的选择被留给用户，通过显式编程。因此，我们将模块内部声明的名称解释为私有资源，这些资源应该保持在该模块的本地。因此，钝化模块n意味着获得本地计算以及在n中分配的资源。通常，在模块n中分配的名称可以被视为为在n处发生的计算分配的临时资源，或者为n的子模块提供的方法，其中n充当库。因此，用户意识到资源的本地化;这种选择也极大地帮助了kπ的实现，本质上是因为我们总是知道如何将消息路由到通道（见下文;类似的想法存在于π演算相关进程代数的现有实现中，例如[4]）。同时，这也阻碍了消息传递的表现力：一个愿意将名称n发送到对n进行限制的模块之外的进程被卡住了。因此，如果两个远程代理共享一个共同的名称，则该名称应被分配在对两者可见的位置，即， 在模块的层次结构中位于它们之上。 换句话说，挤出对用户来说是不透明的，并且必须必要时可编程。当然，在某些情况下，人们希望在当前模块之外分配一个新名称。事实证明，远程分配的相应原语νn@m可以以很小的成本添加到我们的实现中（第11节）。2）。用kπ写的例子的实验表明，我们希望能够编程的习惯用法与我们在形式主义中执行的纪律是兼容的。需要进一步的调查，特别是与较大的例子，以了解的可能性o通过编程在kπ。1.3.2模块化与物理部署应该注意的是，由kπ过程描述的模块层次结构不一定对应于从模块到物理站点的给定映射我们90D. Hirschkoff等人/理论计算机科学电子笔记241（2009）85HH'L LXY Z不HH'L LX Z不 YHXX'LHXX'L'见图4。 一些kπ构型图4显示了一些示例，说明我们打算如何使用kπ进程来表达分布式编程中的典型情况。在左上图中，主机模块H包含库模块L以及两个其它子模块X和XJ。X和XJ通过一些驻留在H上的名字与模L相连。物理上，这可以很好地对应于H和L在同一站点（提供库的站点）上运行的情况，而X和XJ在（可能不同的）远程机器上，并且依赖于远程通信与L交互。在右上图中，H中的一个进程已经钝化了L（H和L在物理上位于同一位置），以便用库的更新版本（LJ）替换它左下图描绘了一个不同的场景，基于相同的在这种配置中，给定模块的所有子模块都在同一台机器上执行。出于负载平衡的目的，可能会出现这样的情况：一台主机钝化本地客户端，以便通过网络将其发送到另一个位置：在右下角的图表中有说明2分布式实现在本节中，我们描述一个实现kπ的分布式抽象机。 这台机器从数据表示等问题中抽象出来，专注于在存在钝化的情况下实现分布式通信。这台机器的设计已经在一个原型分布式实现上进行了测试，以确保我们的实现选择是合理的（参见[9]）。2.1实现选择在介绍我们的抽象机器的形式定义之前，我们给出了它如何工作的高级视图。这应该有助于遵循我们在第二节中给出的更技术性的解释2.2.D. Hirschkoff等人/理论计算机科学电子笔记241（2009）8591计算单位。我们的机器的第一个（标准的）特征是它扩展了计算单元的层次结构：例如，组成图3程序的七个模块中的每一个都由机器在其自己的异步位置执行。为了保持树结构，每个位置存储并维护其子位置的列表。 正如预期的那样，当一个模块创建一个子模块时，后者将在一个新的位置生成。为了确保位置可以以异步方式实现，我们让它们仅通过（异步）消息进行交互通讯远程通信的协议是相当标准的：一个愿意发送消息的进程将消息发送到包含实现通道的队列的位置;因此，愿意接收消息的进程将其位置发送到队列位置并挂起执行，以便当消息服务器租用-美国服务租用使用我们对模块的解释，运行通道队列的自然位置是创建名称的模块的位置;这是可能的通过我们的选择，以防止通道名称被挤出此模块： 如果模块被钝化了，它的所有子模块也会被钝化，这样任何试图在信道上进行通信也将被钝化钝化。钝化不可能是原子的，因为模块的层次结构已经被简化了，如上所述（这与[1]中的机器有很大的不同）。因此，我们以增量方式实现它，从钝化模块到其子模块，传递。在钝化会话的传播过程中，我们必须处理两个主要的干扰源• 首先，在某些子模块已经开始钝化的情况下，我们的机器优先考虑内部钝化会话• 更重要的是，我们需要清理钝化子模块中正在运行的通信会话。如上所述，对于属于钝化模块的名称的通信，这不是问题。对于位于钝化模块上方的名称的通信，我们使用与拥有所涉及通道的模块的简单交互：状态消息用于查询是否已发生通信的提交，以便计算可以完成或中止。分布式实现。我们已经编写了这个抽象机器的OCaml实现[9]。该实现利用了两个库：一个用于高级通信，其中消息传递作为内存写入或套接字通信执行，这取决于它是本地还是远程;另一个用于OCaml线程的通信，thunki化和产卵，以及它们的定义集。92D. Hirschkoff等人/理论计算机科学电子笔记241（2009）85..S.S.hI：：=PI|Iω（aBdP，M）α（V）κ（I）（Local态）H....................我a，n，x，u，h，g，s∈Names（Names）X∈PV ars（过程变量）B：：=（x）（X）[X] a P X（Binder/Argument）P：：= 0 P |P（νa）Pn [X]aB d P（过程）V：：=ug K·<$（值）G：：= 0。 G |G. s（h，u，V）。 s（？）（请求）ρ：：=<$ρ，a<$→ugρ，X<$→K（表）K：：=I;ρ;g（Thunk）M：：=0 hI g G（Messages）S：：= M S |S（νa）Sh [K]g [G]（状态）Hρ：：= h [[]|I; ρ; g]（上下文）Gg：：=g [[]|G]图五. 抽象机器的概念。名称（为了优化钝化过程，实现模块的数据结构带有一个收集模块已知的所有名称的表）。 最后，语言的每个语法结构都被编译成一个简单的函数，该函数使用前面的库，并遵循我们下面描述的机器的形式规范。特别是，我们不需要在运行时操作显式的抽象语法树。2.2抽象机用于kπ进程分布式执行的抽象机器被定义为进程演算，其中关于我们在实现中使用的数据结构和工作中的协议的细节是显而易见的。抽象机器的构造。图5给出了抽象机器的语法。如前所述，我们依靠在两个无限集合的名称（Names）和过程变量（PV ar）上;名称将用于kπ过程以及机器所需的各种内部标识符：分配的名称标识符（u），逻辑位置（g，h）和会话标识符（s）。此外，我们让i在相对数（Z）上取值。虽然它们以稍微不同的方式表示，但机器的进程（P）本质上与以前相同：唯一的区别是我们允许模块只包含进程变量（条目n[P]消失，D. Hirschkoff等人/理论计算机科学电子笔记241（2009）8593只剩下n[X]服从这个约束，我们递归地定义一个预编译步骤 . 的映射过程微积分（如图所示1）到那些机器（F3ig.（5）唯一不平凡的94D. Hirschkoff等人/理论计算机科学电子笔记241（2009）85|当B=（x）且V=ug时，则B =（x），x→ug;3案例是：n[P] 3 =（νa）（a <$P 3 <$d 0 |a（X）d n [X]）（其中a是新名称）。从闭源进程到状态的最终转换如下，其中h和g是两个任意不同的名称：=（νh，g）（h [P;; g]|g [0]）。（P）在运行时，此状态将演变为这样一种状态，其中，P的树结构由形式h[K]g[G]的构型表示，其中 K=I;ρ;g是形实转换子，并且：• h是低级逻辑位置;可以在同一物理位置上执行多个这样的位置;• I是正在执行的本地进程，以及一些状态信息;• g是另一个相关的低级逻辑位置的地址，模块分配的名称将在这里处理（在G的帮助下）-• ρ是一个表（或环境），将进程变量绑定到thunks，并将名称绑定到形式为ugJ的对：u是唯一标识符，gJ是处理名称的通道。在OCaml实现中，h和g对应于两个通道（根据端点的物理位置，使用共享内存或套接字实现）。反过来，K和G对应于两个线程，监听这些通道。在这些信道上传输的消息分别是I和G形式。我们解释各种语法条目以及操作语义，如下所示。表被看作是从名称和过程变量到值的部分函数;这些函数递归地扩展到绑定器和参数（语法中的条目B），如下所示：ρ（a）=ρ（a）ρ（<$P<$）=（P;ρ;g）（对于某些g∈/fn（ρ））ρ（<$X<$）=ρ（X）ρ（（x））=ρ（（X））=·ρ（[X]） 未完成下面的操作对于扩展表很有用ρ+B<$→V=ρ，X<$→K ，若B=（X）或B=[X]，且V=K;不然的话。⎪D. Hirschkoff等人/理论计算机科学电子笔记241（2009）8595H·¬·¬我们还需要对thunks执行以下替换操作K {g}=I {g/gJ} ; ρ {g/gJ}; g其中K= I; ρ; gJ。操作语义学。我们有足够的材料来解释抽象机器的操作语义，如图6所示。前三个规则是标准的;结构同余在这里没有定义，它包含了没有惊喜：源kπ过程的结构同余是继承的;平行合成和0元素形成结合交换幺半群;并且允许α转换和作用域挤出。我们在下面解释其他归约规则;它们利用上下文（Hρ，Gg• 通信在规则I-RE q中，通过在处理发生在a上的通信的信道上发送请求s（h，u，V）（根据B的形状，用于接收或用于发射）来执行预定过程。一个新的会话标识符s允许我们唯一地标识通信协议的这一部分。等待恢复计算的进程被本地存储在形状为ωs（aB d P，M）的元素中;如果在通信实际发生之前发生钝化，则将发送消息M注意，如果B是[X]形式，则该规则不适用：在这种情况下，ρ（B）是unfined。这种情况对应于钝化前缀，由规则I-STARTPASS处理。规则I-C OMPL描述了成功的完成消息如何释放前缀动作的继续：消息αs（V）满足元素ωs（... ）使用相同的会话标识符：释放延续进程（P），并且，如果我们在接收方，则生成并添加新的绑定局部过程（ρ）的表在规则I-ABORT中，一个形状为αs（）的消息告诉冻结的进程撤销它的提交：重新安装原始的prefixed进程正如我们将在下面看到的，这可能发生在钝化的情况• 路由。规则I-ROUTE和I-ROUTE规则I-COMM描述了两个发射和接收请求如何分别发生在同一个名称标识符u上，并且来自位置h1和h2，满足：生成具有标识会话名称的向下确认消息;将消息的内容发送到接收方进程。规则I-STAT显示了取消承诺的消息（αs（））是如何生成的：当请求通信的消息被状态消息s（？）（见下文第一• 分布····96D. Hirschkoff等人/理论计算机科学电子笔记241（2009）85H∈gg hh11 22 12HHHH0我一期+1我i−10S→SJS0|S → S0|SJ语境封闭S→SJ（νa）S→（νa）SJ通信SS0S0→S0JS→SJS0JSJρ（a）=ugρ（B）=V s/fn（Hρ[aB d P]）I-R E q Hρ[aB d P] →（νs）`g <$s（h，u，V）<$|Hρ[ωs（aB d P，g <$s（？）（）]"I-COMPLV=/<$ρJ=ρ+B<$→VI-A博尔特Hρ[ωs（aB d P，）的方式|αs（V）]→ Hρ'[P]路由H[ωs（aB d P，）的方式|αs（<$）] → H[aB d P]I-ROUTEG[0]|g G→G[G]I-ROUTE' H [ 0]|hI→H[I]I-C OMMG[s（h，u，V）|s（h，u，·）] → G[0] |h αs1（·）|h αs2（V）I-S TATG[s（h，u，V）|s（？）] →G[0]|hαs（<$）分布I-FRESHa，u∈/fn（h[I|（νa）P;ρ;g]）h[I|（νa）P;ρ;g] →（νu）h[I|P;ρ，a <$→ ug; g]ρ（X）=Kh，g∈/fn（Hρ'[n[X]]）I-S卒HHρ'[n[X]] →（νhg）`h[K{g}]|g[0]|Hρ'[ωh（n[X]d n[X]，h <$κh'（0）<$）]′钝化I-STARTPASSM=/0H[n[X]dP| ωh（n[X]d n[X]，M）] → H[ωh（n[X]d P，0）]|MI-P质量标准M/=0H[κh（I）]| ωs（aB d P，M）]→ H[κh（一）|ωs（aB d P，0））]|MI-DECRH[κh（I）]| α（V）]→H[κh（一）|α（V）]I-PACKhJ[P|κh（I）;ρ;g]→ h<$αh'（P|I;ρ; g）图第六章抽象机器的操作语义规则I-FRESH显示了如何分配kπ个名字：生成一个新的标识符u，我们在本地表中存储关于名字a的通信由顶级通信通道g与标识符u处理的信息， 与当前位置（h）相关联规则I-SPAWN是最复杂的规则：它生成一个新的位置，以便执行当前模块的子模块。如上所述，这涉及生成两个信道，一个（h）用于执行子模块的代码，另一个（g）用于处理由该子模块分配的信道上的通信模块（g是顶层通信通道）。等待执行的子模块具有形式n[X]。 局部表（ρ）告诉哪个thunki化的计算与它（K）相关联。此形实转换程序先前已链接到顶级通信通道，该通道用于··D. Hirschkoff等人/理论计算机科学电子笔记241（2009）859700/- -⟨⟩⟨⟩⟨⟩⟨ ¬ ⟩处理通信通道（K可能是一个在被钝化之前已经运行和分配名称一段时间由于这个通道不能再使用了（因为形实转换程序可能已经物理移动，或者被复制了），所以必须创建一个新的通道（g）和一个新的线程（g[0]），我们需要在所有可以在K中找到的表中用g替换旧的地址，从而更新K g。请注意，在实际实现中，由于使用了表，应用这种替换确实涉及在运行时检查代码：我们只对表执行操作，表是运行时数据结构，用于监督代码的执行规则的棘手部分是元素ωh（n[X]Dn[X]，h κhJ（0）），在子模块生成后，保留在父位置。这个元素让我们回想起在原始树层次结构中h是hJ的子元素;在父位置想要钝化该子位置或被钝化的情况下，它将以两种方式使用。这两种情况分别对应于下面给出的规则（I-STARTPASS，I-PASSSESS）。• 钝化。规则I-S TARTPASS发起一个钝化协议：当前模块想要钝化一个名为n的子模块，并且由于形式为ω（n [X] Dn[X]，M）的元素，我们知道存在这样一个子模块。 它会释放消息M：根据规则I-S PAWN，M的形式为h κhJ（0），其中h是子模块的位置，我们将在其余的规则中看到，在接收到该消息时，子模块将使自己钝化，并将其thunki化的版本发送回HJ，即父模块的位置。此外，我们更新ω-元素，使得它将通过规则I-COMPL在接收到钝化的孩子时产生预期的结果。请注意，检查M=0是很重要的：否则，如果P的形式为n[X]，我们可能会错误地应用该规则两次。钝化通过规则I-P_ASS_ESS传播到整个子树：κ元素充当记录钝化的当前状态的缓冲器，并通过发送消息M接受形式为ω（，M）的任何元素。这可能对应于两种情况：- ω-元素表示子模块，在这种情况下，消息告诉子模块递归地钝化自身- ω元素对应于待处理的通信请求在这种情况下，由于规则I-Req，M的形式为gs（？）：通过发送这个状态消息，我们强制g应答请求（如果完成消息刚刚发送，什么都没有发生，状态消息丢失;否则，规则I-STAT适用，产生中止消息h s（））。在这两种情况下，我们递增存储在κ元素中的计数器：我们需要记录我们必须等待答案（α消息）。规则I-DECR允许k元素通过缓冲它们并递减其计数器来消耗这些答案。最后，规则I-Pack可以在整个状态被清除之后使用：只有源进程P保留在位置中;所有ω和α元素都已被清除。····98D. Hirschkoff等人/理论计算机科学电子笔记241（2009）85⟨ ⟩⟨ ⟩积分到κ-缓冲器，并且κ-计数器为空。缓冲器、剩余的源进程、当前表和当前名称处理程序的地址， g被发送回父位置（h），并且在h处运行的线程被杀死（我们也可以向关联的通道（g）发送消息以杀死对应的线程2.3相关作品：分布式计算在分布式编程中实现进程演算的几项工作都集中在类似环境的模型上（Mobile [5]，Safe [6，10]，Boxed [13]）。 我们已经提到[1]，它为Kell演算引入了一个抽象机器。 这项工作与以前的工作最重要的区别是在微积分中存在钝化算子，这是实际实现时微妙问题的根源。kπ与Kell演算有关。我们介绍的机器提供了分布式交互的更细粒度的表示;特别是，钝化涉及复杂的分布式协议，而它在[1]中是原子的我们在下一节讨论我们的机器的形式验证3总结发言kπ的定义过程及其实现的研究提出了几个问题，我们目前正在研究，或者我们希望在未来解决。3.1正在进行的工作防止非法名称挤出的类型系统为了让机器正常工作，我们需要确保不会被挤出到其定义模块之外。 一个解决方案是在运行时检查每条消息的内容，并阻止非法通信。为了避免由这种方法引起的不合理性，我们希望依赖于类型系统 静态地强制执行这种确认策略：一个类型良好的术语永远不会试图将一个名称挤出其范围。我们正在研究的类型系统利用模块层次结构的分析来检测病态通信。一个输出an是合法的，仅当约束n在模结构中约束a的约束之上（或者n是自由的过程中）。 如果，而不是a或n，我们有名字绑定到接收（如， 例如，在一个实施例中，c（x）d a x），则与传输信道相关联的类型信息给出了分配了正在传送的名称的模块的近似值（直观地，该信息归结为D. Hirschkoff等人/理论计算机科学电子笔记241（2009）8599⟨ ⟩⟨⟩ |⟨ ⟩|或作为通信对象）。过程值的通信遵循相同的思想：在P中，我们强制P的所有自由名称都应分配到上面a.因此，在模块名称和进程传输通道的类型中，我们提供了正在执行的进程的自由名称的这种空间界限（分别为：沟通）。除了主题归约的标准属性之外，我们的类型系统的正确性还通过显示每个可类型化进程都有良好的作用域来表达，这直观地意味着这样的进程不会试图发出其作用域之外的名称。由于这个属性是通过归约保留的，所以我们可以避免在运行时检查作用域拉伸。 虽然我们需要进一步实验我们的类型系统的表达能力，但初步的尝试表明，我们的系统所执行的策略是合理的，在某种意义上，我们所考虑的示例可以以一种相当自然的方式进行类型化。我们将类型系统的演示以及相应的正确性证明推迟到我们工作的未来演示。抽象机的正确性证明第2节的抽象机器提供了一个相当低层次的描述，kπ进程应该在分布式环境中执行。 为了证明其正确性， 也就是说，编译的结果表现出与原始源进程相同的行为是一项具有挑战性的任务。像[5，10]这样的例子说明了这一点-相反，像[2，13]中的机器，通过提供更高层次的实现，可以构建更简单的正确性证明。主要的困难是，这类证明往往是一个真正的大部分数学;适当的技术是必要的，使他们更容易处理，以 能够完成它们。在我们的设置中就是这种情况，特别是因为钝化机制带来了一些技术上的微妙之处。kπ过程的归约和机器状态的执行由两个转移系统描述。 我们可以希望建立一个互模拟结果，提供证据表明编译版本本质上表现出与源进程相同的行为。然而，因为钝化在我们的设置中不是原子的（与[1]相反），所以这是不可能的。实际上，考虑以下过程：m[a u n[b v]] m[X]d Q. m的钝化的实际执行可以经历其中b上的发射被阻挡而m上的发射被阻挡的状态。a仍然是活动的;这样的状态在原始演算中没有对应物。相反，我们的机器的正确性应该被表述为耦合互模拟结果[12]：尽管这种行为等价比普通互模拟弱，但它需要操作等价（任何kπ约简步骤都可以被机器模拟，并且机器的任何约简步骤都可以完成为微积分的一个步骤）。 可以注意到，[13]的机器的正确性证明分为两部分（可靠性和完整性），在概念上接近于2-模拟结果，这反过来又是通过从耦合模拟的定义中删除一个子句来获得的。100D. Hirschkoff等人/理论计算机科学电子笔记241（2009）853.2未来扩展机器的优化抽象机的定义和实现在kπ的设计中起着至关重要的作用，因为它提供了对形式模型背后的主要设计决策的实际见解。除此之外，该实现还提出了一些改进或扩展，我们希望进一步研究。我们已经提到了远程名称分配的原语νn@m，这个操作原则上可以被编码，但是在当前的机器设计中，作为原语的成本非常低。 另一个值得研究的方向是如何通过考虑诸如以下信息来专门化机器的一般行为，例如，整个模块层次结构在一台机器上运行。模块接口。实际上，我们上面描述的类型系统将基本信息与模块名相关联，而模块名只与在该模块内运行的进程访问的区域相关（属性如定义更多信息的模块接口会很有趣，特别是描述与模块托管的名称的使用相关的行为的某些方面（以及递归地与子模块关联的接口）。例如，可以考虑让通道c的类型描述期望在c上发送的参数。除此之外，如果能够在资源获取和消费方面表达期望，将是有益的。此外，找到有意义的类型规程来控制钝化的使用也是一个有趣的问题（一个简单的例子是，为了实现的目的，能够保证钝化的进程将以一种简单的方式使用-也就是说，没有重复-由钝化代理）。 基于π演算的形式主义的现有类型系统，以及 至于面向对象语言，应该是研究这些问题的有趣想法的来源。处理（重新）绑定。在目前的形式中，kπ只能实现有限形式的动态模块化。当模块被钝化时，它可以四处移动，复制，并且可以恢复计算，只要遵守与限制的本地化相关联的约束。在用kπ编写示例时，在钝化模块时，能够以某种方式将其与它正在使用的某些本地资源断开连接似乎是有帮助的。这将使得将钝化模块发送到它正在使用的名称的范围之外成为可能，可能发送到另一个站点，在该站点中，在再次连接到另一组资源之后可以恢复计算。用动态（重新）绑定的机制扩展kπ，同时保持断言模块关于其资源使用的静态属性的可能性，这是一种D. Hirschkoff等人/理论计算机科学电子笔记241（2009）85101困难的任务。Acute [15]的工作可能为此提供有趣的灵感。从更低层次的角度来看，我们相信在我们的机器中运行时操作的表是经过精心设计的，可以支持这样的扩展。行为等价。我们不仅想执行kπ程序，而且还想陈述和证明它们的性质。在基础层面上，我们有兴趣分析kπ中提供的行为等价概念，并理解钝化在这方面的作用。[11]的工作是朝着这个方向发展的（[8]也是在荷马演算的背景引用[1] Bidinger，P.，A. Schmitt和J. Stefani，An Abstract Machine for the Kell Calculus，in：In Proc.FMOODS31比46[2] Bidinger，P. and J. Stefani，The Kell Calculus：Operational Semantics and Type System，in：InProc. FMOODS109-123[3] Fournet，C.，“Join-Calculus：分布式移动编程的微积分”，博士。毕业论文，Ecole Polytechnique（1998）。[4] Fournet，C.，F. L.费桑特湖Maranget和A. Schmitt，JoCaml：A Language for Concurrent Distributedand Mobile Programming ， in ： Proc. Advanced Functional Programming 2002 ， LNCS2638（2002），pp. 129比158[5] Fournet，C.，J. - J.L'evy和A. 一种移动环境的分布式实现。，in：In Proc.IFIP TCS '00 ， LNCS1872， 2000，pp . 348-364.[6] Giannini，P.，D. Sangiorgi和A.安全环境：抽象机器和分布式实现，科学。Comput. 程序. 59（2006），pp.209-249[7] Hennessy，M.，“A Distributed[8] Hildebrandt，T.，Godskesen和M. Bundgaard，Homer的互模拟同余-高阶移动嵌入资源的演算，技术报告TR-2004-52，哥本哈根大学（2004）。[9] Hirschko ， D. ， T. Hirschowitz， S. Hym ， A.Pardon 和 D. Pous ， Abstract Machine forkπ ：Prototype Implementation，可从http://perso.ens-lyon.fr/damien.pous/kp/kpam.tgz（2008）获得。[10] Hirschko，D.，D. Pous和D. Sangiorgi，A Correct Abstract Machine for Safe Ambients，in：In Proc.COordination十七比三十二[11] Lenglet， S.， A.施 密 特 和 J. - B. Stefani ， 钝 化 过 程 结 石 的 正 态 互 模 拟 ， 研 究 报 告 RR-6664 ， INRIA（2008）。[12] P. 和P. Sjöodin，Multiwaysynch r onizaton verifieddwithwoupleddsimulation，in：InP roc. CONCUR，1992，pp. 518-533.[13] Phillips，A.T.，N. Yoshida和S.Eisenbach，一个分布 式的抽象机器 ，用于盒装环 境演算 ，在：Proc.ESOP '04，计算机 科学讲义2986 （2004年）， 第100页。155-170[14] Schmitt ， A. 和 J. Stefani ， The Kell Calculus ： A Family of Higher-Order Distributed ProcessCalculi，in：In Proc. Global Computing，LNCS 3267（2005），pp. 146-178。[15] Sewell ， P. ， J. J. Leifer ， K.Wansbrough ， F.Z. Nardelli ， M.Allen-Williams ， P.Habouzit 和V.Vafeiadis，Acute：分布式计算的高级编程语言设计，在：在Proc。 ICFP（2005），pp. 15-26
