全球计算中的META KLAIM：空间、时间和安全的建模与应用

网址：http://www.elsevier.nl/locate/entcs/volume62.html17页面向全局计算的G. 法拉利意大利比萨大学信息学系E. 莫吉信息与信息科学学院热那亚，意大利R. Pugliese信息系统学院意大利佛罗伦萨摘要META KLAIM是在空间、时间和安全方面建模的案例研究这是全球计算所必需的。 META KLAIM集成了META ML（扩展的SML用于多阶段编程）和KLAIM（用于代理交互和移动性的核心语言），以便允许元编程活动（如代码片段的汇编和链接）、安全检查（如在管理边界的类型检查）和正常计算活动的交错。的Meta ML的stagingannotations提供了对时间方面的细粒度控制，KLAIM的原语支持位置感知，而类型系统通过使用全局类型（与动态类型检查相结合）和通过使用多态性（a`lasystemF）的泛型代码来支持安全性。本文描述了META KCLAIM的语法、类型系统和操作语义，陈述了两个类型安全性结果，并举例说明了它在描述移动代码应用中的应用。1介绍支撑大多数广域网（WAN）应用的分布式软件架构（模型）通常由执行应用的组件的大量异构计算实体（有时称为网络的节点各种节点由具有不同管理策略和安全要求的不同机构处理。WAN应用程序的组件具有高度动态行为的特征。他们必须处理2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。2网络环境随时间的不可预测的变化（由于网络连接的可用性、缺乏服务、节点故障、网络重新配置等引起的变化）。此外，游牧或移动组件可以从节点分离并且稍后在不同的节点上重新附接。因此，组件必须设计为支持异构性和互操作性。与传统的分布式编程中间件不同，底层网络的结构对广域网应用程序的程序员是显而易见的我们参考[17]和[3]对这个问题进行了全面的分析与WAN应用开发相关的问题促使人们研究具有高级功能的编程语言的基础，这些高级功能包括用于代理移动性、用于管理安全性以及用于协调和监视资源使用的已经提出了几种基础演算来解决与WAN编程相关的大多数现象我们提到了分布式Join-calculus [16]，Klaim [8]，分布式π-calculus[21]，Ambient calculus [4]，Seal calculus [34]和Nomadic Pict [31]。所有这些基础模型都包含一个位置概念，以反映管理域的概念：在某个位置的计算是在特定权威的控制换句话说，它们关注WAN编程的空间维度（通常称为网络感知WAN编程的另一个关键方面涉及时间维度：运行时系统可以将计算活动与Meta编程活动（例如，组件的动态组装WAN应用程序的组件通常由不同的提供商开发和维护，并可按需下载动态链接和安全检查的动态执行（例如，认证和访问控制）增加了WAN应用程序的可扩展性，因为它们允许重新配置应用程序而无需重新启动它。几篇论文已经解决了正式理解动态链接（和单独编译）的问题[2，27，24，10，23，30];其他方法已经解决了移动代理系统中的安全问题[20，12，13，9，22]）。因此，广域网规划的空间和时间维度已经被研究得相当深入，但孤立，它们的相互作用还没有得到适当的形式化和理解。本文提出了一个基础模型，它集成了广域网规划的空间和时间方面。我们已经抽象了问题的基本特征，在一个calculus中，有可能在站点之间迁移的编程代理的原语，以及支持动态链接和安全检查的细粒度控制的原语我们的演算建立在KLAIM[8]和MetaML [26，1]上。KLAIM（内核局域网-Agents Interaction and Mobility）是一种实验性语言，受到Linda协调模型[18，5]的启发，该模型专门设计用于通过利用移动性对WAN应用进行建模和 M ETA ML支持SML和元编程结构的大多数特性。元编程3∆提供了一个理想的工具，用于描述定制和组合的软件组件，因为元编程结构具有相同的状态，其他编程结构。本文是[14，15]的后续在[14]中，我们解决了保护主机免受移动进程攻击或不当行为的问题 我们引入了H OT K LAIM（高阶类型的K LAIM），这是Klaim的一个变体，只允许流程抽象的移动性，即参数化过程具有本地意义的操作类型系统利用全局值和类型来确保具有局部含义的操作仅在局部使用在[15]中，我们描述了META KLAIM的一个初步版本，它只有简单的类型。在本文中，我们推进的集成e-orort，并提出了一个集成的HOTKLAIM和META ML，也考虑到多态和全局类型的HOT KLAIM。本文的其余部分组织如下：第2节介绍了META KLAIM的syn- tax，第3节给出了类型系统，第4节定义了操作语义，第5节给出了类型安全结果（省略了证明），第6节给出了一些移动代码应用程序的例子，第7节得出了一些结论。2MetaKlaim本节介绍META KLAIM，这是一种专门设计用于对全球计算的空间和时间方面进行META KLAIM在M eta ML中集成了KLAIM图1总结了演算的语法。定义2.1一个网N∈Net=μ（L×（E0+{err，dead}））是一个多重集由局部l和封闭项e组成的对，或者指示l处的进程已经崩溃的标记err，或者指示死计算的标记dead，或者已经被移除的元组的占位符□备注2.2[术语中的类型]在全球计算场景中，网络上可用的大多数软件函数抽象不足以表达所需的参数化形式。同样，像SML所支持的有限形式的多态性似乎是不够的（见第6节）。因此，在META KCLAIM中，包括多形态的ty pesa'lasystemF[19]。然而，他的设计选择以及在运行时对可判定类型检查的需要（因为输入原语执行动态类型检查）意味着MEETACLAIM程序必须包括大量类型信息（在运行时）。的描述请我们参考备注3.1的型号进一步研究的一个重要课题是找到类型系统，它不需要大量的类型注释，同时保证4| ∈• 类型t∈T：：=X|L|t1→t2|（t i|i∈m）|⟨t⟩|阿勒特|X .t全局类型g∈G：：= L|（g i）|i ∈m）|阿勒特• 上下文Γ ∈Ctx：：=|Γ，X n|其中k = l，g• 项e∈E：：=x|L|无|（我|i∈n）|e1e2|固定x：t：k.e|（e i）|i∈ m）| 奥普埃|⟨ e ⟩|埃莱|%e |ΛX.e |e {t}其中l的范围是局部的，nil是死锁计算，op的范围是局部运算的集合Op={spawn，output，input，new，run}。模式p∈P：：=x！t：k|X=e|（p i|i∈m）匹配规则mr：：= pe图1.一、类型和术语列表可判定的类型检查（在线性时间内）和足够的表达能力。□从KLAIM 我们借用计算范式，它识别亲，cesses作为计算的基本单位，而nets，即节点的集合，作为过程活动的协调员。每个节点都有一个地址，称为局部性，并由一个进程组件和一个元组空间（TS）组成，即元组的多集合。进程通过TS异步通信。M ETA K LAIM的类型包括地点类型L和（t i im）的元组。KLAIM原语采用多态局部操作的形式：• spawn（e）激活并行线程中的进程• 输出（l，e）将e的值加到l处的TS（输出是非阻塞的）。• 输入（l，（p i）i|i ∈ m））访问位于l处的TS。输入检查每个模式pi，并在TS中在l处查找匹配值v。如果这样的v存在，则将其从TS中移除，并且在匹配模式pj中声明的变量（即，由X表示的那些！t：k）在ej内被v中的相应值替换。如果没有找到匹配的元组，操作将被挂起，直到有一个可用的元组（因此输入是一个阻塞操作）。注意，输入利用了动态类型检查（即匹配的v必须与模式中声明的变量的类型一致）。• new（e）创建一个新的局部性l，在l处激活一个进程，并返回l。备注2.3[M]与KCLAIM]InKLAIM 有一个原始的eval（l，e）用于激活远程位置l处的进程。此原语用于对于流程流动性，但由于以下原因未纳入：梅塔·克莱姆为• eval依赖于动态作用域（一种潜在的危险机制），这在META KLAIM中是不可用的，因为在函数设置中，可以使用5⟨⟩⟨⟩⟨ ⟩ ⟨⟩⟨ ⟩⟨ ⟩ ⟨ ⟩ ⟨⟩⟨ ⟨ ⟩ ⟩ ⟨ ⟩⟨ ⟨ ⟩ ⟩ ⟨ ⟩(the更安全的机制）参数化。• 使用eval，节点可以激活另一个节点上的进程，但是目标节点不能控制传入的进程。这可能是安全问题的根源。特别是，局部类型安全（见定理5.2）失败，如果eval被添加。在本发明中，进程移动性仅通过“相互协议”发生，即（发送）节点可以在任何TS中输出进程抽象，但是只有在另一（接收）节点（处的进程）输入它时，抽象才节点之间的远程通信（如KLAIM提供的）对于实现这种形式的进程移动性至关重要。□从META ML中，我们借用了类型t来表示具有潜在未解析链接的代码（由动态变量表示），将评估分层为级别（级别0表示正常评估，级别n>0表示符号评估），以及以下阶段注释：• 方括号e构造表示通过e的符号求值获得的程序片段的代码，例如2+x是表示片段2 +x的nat类型的值，其中x是动态变量。• Escape_e返回由e表示的程序片段。在符号求值过程中，Escape用于将程序片段拼接成更大的程序，例如，λx。1+2+x的计算结果为λx。1+2+ xx= 0。• 跨阶段持久性%e允许在更高级别使用e的值，例如。%（1 + 1）+x计算为%2 +x。注意，%（1 + 1）和%1+ 1具有相同的类型，但它们的符号求值不同：第一个求值为%2，而第二个求值为1 + 1。• run（e）执行由e表示的程序，例如run1+ 1计算为2. 为了增强安全性，run被视为本地操作。注释2.4[META KLAIMvsMETA ML]在META ML中（更常见的是在多级语言中），可以在（动态）lambda下求值。这个特性对于允许代码生成和正常的计算，但它可能会导致新形式的不正确的运行时行为，这在传统的编程语言中不会出现• 执行带有未解析链接的程序片段，例如λx的计算。（run x;.. . ）将尝试在动态变量x绑定到一个值之前计算run x• 从绑定lambda的范围中挤出具有自由动态变量的值，例如λx的求值。return（i，x）;.. . ）将在位于l处的TS中输出x，从而失去与绑定lambda的连接有两种方法可以解决这些问题。解决方案1是设计一个类型系统，保证类型良好的程序不会表现出不正确的行为。”[1]这是一种“以人为本”的方法。6⟨ ⟩引入了一个封闭类型的类型系统（它还引入了一个死代码注释的绑定器，这有助于证明类型安全，并且在评估良好类型的程序时可以忽略）。解决方案2是动态地处理问题，例如：通过在不正确的行为发生之前停止（线程的）这可以通过在运行或输出之前（动态地）将x中的所有自由变量替换为nil来实现。在支持异常处理的语言中，更好的选择是用raiseunresolved_link代替nil。在静态类型语言中，第一种解决方案更可取，因为它避免了运行时开销。然而，META KLAIM具有动态类型检查（由于输入原语），因此上述参数不成立。事实上，一个更简单的动态类型检查算法可以补偿运行时开销。因此，在METAK权利要求中，人们具有以下权衡：• 解决方案1需要更复杂的类型系统（例如，使用封闭类型和穷举模式匹配），但它能够检测（在类型检查时）不适当的运行时行为• 解决方案2采用更简单的类型系统，但是它涉及实现某些操作（即，除了输入之外的所有局部操作）的开销，其与操作数的大小成线性关系，并且它可能引入死锁计算（作为用nil替换动态变量的结果）。我们选择了第二种解决方案。□3类型系统图2给出了用于派生以下形式的判断的类型系统• 即，Γ是一个格式良好的上下文• 即，t是n级的良构类型•ne：t，即e是n级t型良构项上下文Γ是一个声明序列，类型变量的形式为Xn，术语变量的形式为x：tn：k一个类型变量Xn的范围是在n级的类型t上，而一个项变量x：tn：k的范围是在n级的类型t和种类k的值。我们还考虑T的子集G，其元素称为全局类型。在语义上，类型t是全局的it= it（即一个项的类型为ti it的类型为it）。在某些类型规则中，我们使用以下派生判断：• Γn，ge：t意味着Γn和Γgne：t和e不包含局部运算op，其中Γg是通过仅保留形式Xm和x：tm：g的声明从Γ获得的上下文。注释3.1[Levels，Kinds and Type]Levels是典型的多级语言（如[6]中的λ在动态类型的多阶段语言中，如META KLAIM（参见[32]），类型变量在不同的阶段被绑定。7≤Γ<$XfreshΓ<$ntx freshΓ<$Xm∈ Γ且m≤nΓ，Xnr，x：tn：kΓ ►nXnt1t1→t2Γ►伊本湖Γnti i∈mn（t i|i ∈ m）Γn+1tΓ ►n⟨t⟩t伊宁r，XnntnΓ►nx：tx：tn：k∈ΓΓ ►I：Lt无：t{Γne（pi）：LΓ，Γn（pi）Γ nei：t2|i ∈ m}Γn（p ie i|i∈m）：t1→t2i∈m.t（pi）<$t1Γne1：t1→t2Γne2：t1Γne1e2：t2{ne i：t i|i ∈ m}Γn（e i|i ∈ m）：（t i|i∈ m）r，x：tn：gn，ge：tΓnfixx：t：g.e：tne：（）→tΓ►nspawn e:()r，x：tn：lne：tΓnfixx：t：l.e：tne：L→t新的e：Lrne：（L，t1→t2）rn输入e：t2rne：（L，t）rn输出e：（）我不知道运行时间：tΓn+1e：tΓ►n⟨e⟩:⟨t⟩你好，我是说，Γn+1e：tΓ►ne:trn+1%e：tr，Xnnne：tΓnΛX.e：<$X.tΓne：X.t2Γnt1T{t1}：t2[X：=t1]n，ge：tne：gne：图二、类型系统计算，因此良构性不仅对术语而且对类型都是依赖于级别的在META KCLAIM中，我们考虑了两种项：局部项，按类型l分类;全局项，按类型g分类，是那些没有局部运算op出现的项。 Type t是一个模态（参见[7]的λ Q），与项的分类有关，即Typet对类型t的全局值进行分类。因此，下面的子集关系保持tt（即类型为t的项也具有类型t）。□我们对一些类型规则进行注释：• 类型变量的规则支持一种形式的跨阶段持久化（如[32]），即在级别m声明的X可以在更高级别使用。类型的其他规则与预期的一样8⇒ |∈• 模式匹配规则（pi ei i m）强制所有模式都具有相同的类型，但它不要求所有情况都至少被9||>Ee>E一个模式。该规则使用辅助符号（类型t（p），上下文Γn（p）和项序列e（p）），通过对p的结构的归纳来定义：pt（ p）Γn（p）e（ p）x的！t：Gx的！t：l阿勒特不x： tn：gx： tn：l∅∅X=eLx： L：ge（p i|i∈m）（t（p i）|i∈m）Γ n（p0），.， Γ n（p m−1）e（ p0），.，e（ pm−1）• fixx：t：g.e的类型规则和fixt的引入规则是唯一使用派生判断的规则。• 与[15]不同，run（和其他局部操作）的类型不使用[1]的封闭类型构造函数，因为我们选择了一个更简单的类型系统（参见备注2.4），代价是在实现局部操作时增加额外的开销• 最后三条规则是从[14]中借用的。他们说，这是一个这两种类型在t是全局类型时是一致的类型系统具有以下属性。提议3.2（替代）下列规则是可以接受的r1<$mtr1，Xm，r2<$ntJΓ1， Γ2 [X：=t]<$ntJ[X：=t]r1<$mtr1，Xm，r2<$neJ：tJr1， r2 [X：=t]neJ[X：=t]：tJ[X：=t]Γ1m，ge：tΓ1，x：tm：g，Γ2neJ：tJr1， r2<$neJ [x：=e]：tJr1me：tr1，x：tm：l，r2neJ：tJr1， r2<$neJ [x：=e]：tJ4操作语义一个网的动力学由一个关系N=<$NJ给出，这个关系是用项的转移关系ea>eJ（和e >dead err 转换关系是根据评估上下文定义的（参见[35]），约化Γ，r0a> eJ（和r，r0>deaderr）对于操作和r11> eJ(andr1>err）进行符号求值。图3总结了操作语义的类别。净转换关系=由以下规则定义（根据>）：e>deade>errN（l：e）=N（l：dead）N（l：e）=N（l：err）τJi（v0）@l2 J⇒e10N（l：e）=N（l：eJ）N（l1：e）（l2：v0）=N（l1：eJ）（l2：dead）11我我e2 2翅片我我我12我我我我我我我我我我我我我我>E>e1• 水平n∈N上的值vn∈V n<$Ev0：：=l|（vmr0|i∈n）|（v0|i∈m）|100万美元|ΛX.ev n+1：：=x|L|无|（vmr n+1|i∈n）|v n+1v n+1|修复x：t：k.v n+1|（v n+1|i∈ m）|vn +2|%vn| ΛX.v n +1|v n+1 { t } v n +2 += v n +1|v n+1{t} vn+2+= ˜vn+1计算模式vp n∈ VP：：= x！t：k |x = v n|（vp n|i ∈ m）评估的匹配规则vmr0：：=vp0匹配vmrn+1：：=vpn +1vn+1• 在i∈ {0， 1}层上赎回ri∈rir0：：=x|无|v0v0|固定x：t：k.e|操作v0|埃莱|%e|v0{t}1 2r1：：= 0• 评价上下文En∈ECn在水平n∈N，洞在水平i∈ {0，1}E n：：=（vmr n，Ep ne，mr）|E n e|v n E n|（v n，E n，e）|操作En|En+1|E n{t}E n+1+=（vmr n+1，vp n+1<$E n+1，mr）|固定x：t：k.E n+1|˜E n|%E n|ΛX.En+1我我Ei+=[]我我我模式Ep n：：=x=E n的求值上下文|（vp n，Ep n，p）• 作用a∈A：：=τ|l：e|s（e）|i（v0）@l|o（v0）@l，其中FV（e）= FV（v0）=1。值、兑换和评估上下文o（v0）@l2 Js（e2）N（l1：e）=N（l1：eJ）（l2：v0）l：e> e1N（l：e）=<$N（l：e1）（l：e2）l2<$∈L（N）<${l1}N（l1：e）=<$N（l1：e1）（l2：e2）其中L（N）=l{l|你好（l：e）∈N}{L}是N中任意一个的集合。转换关系>由以下规则（根据>）定义：ee120Γ0（E0），r0 a>eJE0[r0] a> E0[eJ]r11>eJE0[r1]τ>E0[eJ]0 0 1 113001我我我00→0vn+1vn+1↓n，ΓXnilif x： tm： k∈ΓX否则vn+2vn+2↓n+1，ΓΛX.vn+1ΛX.vn+1↓n，Γvn+1{ t}vn+1↓n，Γ{ t↓n，Γ}vnvn↓n−1，Γ （n>0）修复x：t：k.vn+1固定x：t↓n，Γ：k.vn+1↓n，Γ%vn%vn↓n−1，Γ ifn> 0◦vn否则不t↓n，Γ∈TX<$X.X如果Xm∈Γ且m>nX否则⟨t ⟩t↓n+1，ΓX.tX.t↓n，Γvpn+1vpn+1↓n，Γ∈Px的！t： kx的！t↓n，r： kx= vn+1x= vn+1↓n，Γvmrn+1vmrn+1↓n，Γvpn+1 vpn+1 vpn+1↓n，r vn+1↓n，rΓ0（E0），r0>死|errE0[r0]> dead |errr1>错误E0[r1]>err其中，Γn（En）是求值上下文中孔的类型上下文En∈ECn，这个类型化上下文只在运行的约简中需要。图4定义了约简>，并使用了以下操作：• 降级vn+1↓n，Γ∈E通过在vn+1∈Vn+1上的归纳来定义：◦vn是vn的替换实例，其中所有自由项变量都被nil替换。在所有其他情况下↓n，Γ与顶级类型和术语结构互换• 函数match（vp0，v0）和matcht（vp0，v0）要么失败，要么返回ρ：X鳍V0。它们由vp0∈VP0上的归纳法定义，基本情况是：vp0match（ vp0，v0）0matcht（ vp0，v0）0x的！t：lx的！t：lx：= v00x：= v00x：= v00失败如果不匹配0v0：t，0否则x的！t：Gx的！t：Gx：= v00x：= v00x：= v00失败ifn=0，gv0：t0否则x= v0x= v0x：= v00失败x：= v00失败如果v0∈L0否则matcht执行动态类型检查（用于输入减少），而match忽略类型（用于14∀·• ∈函数应用）。• 闭包eE0是e的替换实例，其中所有自由项变量x被nil替换，所有自由类型变量X被X.X替换。 e用于防止内窥镜挤出（见备注2.4）。15我我τo（·v）@ls（·v（））·0，Γ我∆（vp0e|i∈ n）v0τ>e [ρ]，若j ∈ n且match（vp0，v0）= ρiijJmatch（vp0，v0）=fail（vp0e i|i∈ n）v0>deadifi∈n.match（vp0，v0）= fail我我0i（v0）@l0 0输入（l，（vpi）i|i∈n））>ej[ρ]ifj∈nanddmatc ht（vpj， v） =ρmatcht（vp0，v0）=failnil>dead fixx：t：k.e> e[x：=fixx：t：k.e]return（l，v0）0>（）spawn（v0）0>（）new（v0）l：v0l>Lr，运行v1τ>v1↓（ΛX.e）{t}τ>e[X：=t]r0>在所有其他情况下都是错误的，除了当r0是输入（l，（vp0是输入i）时|i ∈n））在所有其他情况下，错误v11>v1r1>err见图4。行动和象征性评价5式安全为了说明类型安全性质，我们引入了良构网的两个概念：一个是全局性质，另一个是相对于节点子集L定义5.1[良型网]一个网N是良型的<$<$<$<$（l：err）<$<$∈N当l∈L（N）时，对每个（l：e）∈N，存在ts.t.你好。一个网N是w.r.t.当l∈L时，L<$L（N）<$$>（l：err）<$$> ∈N，且对任意（l：e）∈N，其中l∈L，e<$∈V0存在ts.t.你好。□在良构网w.r.t. L中的赋值元组v0没有任何说明。事实上，L外部的进程可能会在L的节点中插入一个病态类型的元组。定理5.2（类型安全）如果N=<$NJ，则• （全局）N良构意味着NJ良构• （局部）N格式良好的w.r.t.L蕴涵NJ合式w.r.t.L注释5.3局部安全属性由META KLAIM的两个特性强制执行：由输入操作执行的动态类型检查，这防止了病态类型的项污染良好类型的进程（因为匹配t在病态类型的元组上失败）;KLAIM的eval原语的缺失16允许L外部的进程激活位于L中的病态进程。□176示例人们普遍认为，移动性将为设计和实施WAN应用提供正确的抽象特别是，移动性的有用性出现时，开发应用程序的设备与间歇访问网络，网络服务具有不同的访问策略。我们参考[29，17]，详细讨论了移动性范式。WAN应用程序的另一个关键问题是组件编程。网络上可用的组件预期是高度参数化的，以便适应多种应用并适应各种平台和环境。协调泛型和高效性的一种方法是使用生成组件，它体现了一种构造高效目标代码的方法，一旦组件的大多数参数被固定。Kamin、Callahan和Clausen [25]给出了几个用于生成目标代码的组件的例子这些组件被描述为函数元语言中的高阶宏具有类似于META ML的那些的Escape和Escape结构。在这第节中，我们介绍了如何使用META KLAIM编程WAN应用程序。特别是，我们讨论两个具体的例子。第一个例子（游牧数据收集器）解决了移动性问题第二个例子（动态链接器和加载器）讨论生成式组件编程。在本节的其余部分，我们将自由地使用函数式语言的典型特性（如局部声明，数据库等）。此外，由于类型设置的原因，我们写[]而不是[]，并且VX。而不是X。6.1游牧式数据采集器请考虑下面的场景。某个用户需要在一段数据上组装信息（例如，某些设备的价格用户应用程序的部分然而，有一些活动是独立于它的。用户的应用程序可以被构造为利用移动性范例：移动组件可以动态地在这里，为了简单起见，我们假设分布式数据库的每个节点包含形式为（i，d）的元组，其中i是搜索关键字，d是关联数据，或者形式为（i，l）的元组，其中l是可以搜索与i我们使用以下类型：L（* 地点 *）Key=.（* 授权密钥*）数据=.（* 多态类型的本地操作输入，输出，产卵*）I=VX。 VY.（L，[]X->Y）->YO=VX. （L，[]X）->（）S=VX。（（）->X）->（）（* 输入、输出、生成的元操作的多态类型 *）18MI=VX.VY. （L>，[]X->Y>）->MO=VX. （L>，[]X>）-><（）>MS=VX. （（）->X>）-><（）>（*带有 静态安全检查的代码抽象 *）MEnvK=（L>，Key->MI，Key->MO，MS）CAK = MEnvK->（）>多态类型的Meta操作利用代码类型，因此元操作能够将本地提供的操作的代码片段代码抽象的类型（例如，移动代码的类型）相对于位置（代码将被执行的位置）和元操作被参数化换句话说，代码抽象的类型可以直观地解释为代码的网络环境。必须向该环境提供有关当前位置及其本地操作的信息我们要强调的事实是，用于通信的元操作需要授权密钥作为参数。以这种方式，取决于键k的值，“k”中我们现在讨论移动应用程序的主要模块：游牧式数据收集器。代码抽象pca（k，i，u）是在分布式数据库上检索所需信息的移动代码参数k是授权密钥，i是搜索密钥，u是应该收集与i相关联的所有（远程）数据的位置（端系统的地址）移动代码pca（k，i，u）的行为是相当直观的。 在被激活之后，pca（k，i，u）产生一个执行本地查询的进程（这里查询删除本地数据库中与搜索关键字i相关联的数据）。 然后，移动代码将查询的结果转发到位于u处的元组空间，并将其自身的副本（即， 的PCA（k，i，u））发送到可能包含与i相关联的数据的地点。请注意，在代码抽象pca（k，i，u）中，跨阶段持久性允许在更高级别上使用参数i和u。pca（k：Key：g，i：Data：g，u：L：g）：CAK：g =修复ca：CAK：g。fn（<~（ fix p：（）：l.~（in(self’, 数据：g）=>~（out固定p：（）：l.~（in(self'<，（_=%i，l！L：g）=>~（out代码抽象pca（k，i，u）由进程实例化和激活执行. 这个过程从本地的19元组空间，通过提供节点的局部性和元操作来实例化它们，最后激活专用代码。execute（self：L：g，env：MEnvK：l）：（）：l=fix exec：（）：l.input（self，X！CAK：g => spawn（（）=> run（X env））;exec）6.2动态链接和加载在全局计算编程中，一个重要的问题是控制组件加载策略的能力例如，Java虚拟机支持类的动态链接和加载[28，11]。在某些情况下（具有良好连接性的地方或可信的地方），人们希望在需要时加载组件，在其他情况下，人们可能更喜欢提前获取简单的解决方案是将应用程序参数化。链接器，并在需要组件（或服务）时调用链接器这并不能确保足够的可扩展性，更好的间Meta连接体。元链接器可以决定是在代码生成时加载所请求的组件，还是在运行时推迟加载，即通过为对链接器的调用生成代码在下面的例子中，我们假设应用程序是参数化的w.r.t.给出服务名称的链接器或者通过返回授权密钥成功地在服务和应用程序之间建立连接，或者引发异常。我们对链接器的细节不感兴趣，但抽象行为可以是：检查服务（或其代理）是否存在于本地，如果不存在，则远程搜索并在本地复制（或创建代理）。我们使用以下类型：L（* 地点 *）Key=.（* 授权密钥 *）名称=.（* service names *）Linker=Name-> Key（* linker*）MLinker=名称->键>（* 元链接器 *）（*参数化应用程序代码 *）CApp=MLinker->（）>进程execute从本地元组位置获取应用程序代码，通过传递元链接器生成代码，然后生成一个执行生成的代码的进程Mexecute（self：L：g，mlinker：MLinker：l）：（）：l = fix exec：（）：l.input（self，x！CApp：g => spawn（（）=> run（x mlinker））;exec）元链接器的调用将采用以下形式<.~（mlinker n）.> .使用Meta编程工具，元链接器可以决定是否立即调用链接器，即mlinker n = %（linker n）>，或者是否生成用于调用链接器的代码，即mlinker n = %linker %n>。在20第一种情况，当链接器无法建立连接时，代码根本不会被执行7结论M ETA K LAIM是一种演算，它结合了来自移动性，协调性和阶段性语言的各种功能。 在全球计算中，移动性似乎是一个基本方面，协调对于控制和安全性很重要，分段对于组装组件和在执行之前生成专门的代码很重要。据我们所知，META KLAIM是第一种将多阶段编程功能与移动过程的形式化相集成的致谢。 我们感谢裁判的有益的意见。引用[1] 卡尔卡尼奥角，E. Moggi和T.用于安全命令式MetaML的剪切、（2001年），出版。[2] 卡尔代利湖， 程序片段，链接和模块化，在：Proc. ACM Symposium onPrinciples of Programming Languages（1997）.[3] 卡尔代利湖，移动计算的抽象，在：J. Vitek和C。Jensen，editors，SecureInternet Programming ： Security Issues for Mobile and Distributed Objects ，number 1603 in LNCS，Springer-Verlag，1999 pp.51比94[4] 卡尔代利湖和A.戈登，移动环境，理论计算机科学240（2000）。[5] Carriero，N.和D.Gelernter，Linda in Context，Comm.ACM32（1989），pp.444-458[6] 戴维斯河，结合时间分析的时间逻辑方法，在：计算机科学逻辑研讨会（LICS184-195。[7] 戴 维 斯 河 和 F. Pfenning ， A modular analysis of staged computation ， in ：Symposium on Principles of Programming Languages（POPL258-270。[8] 德尼古拉河， G. Ferrari和R. Pugliese，KLAIM：一种用于Agent Interaction and Mobility，IEEE Transactions on Software Engineering24（1998），pp.315-330[9] 德尼古拉河，G. 费拉里河，巴西-地Pugliese和B.Venneri，Types for AccessControl，Theoretical Computer Science240（2000），pp.215-254[10] Drossopoulou，S.，面向Java动态链接和验证的抽象模型，在：Proc. of Typesin Compilation，2000。