π-演算与Polyadic同步：电子笔记68第二次，关于分布式系统的理论计算机科学

理论计算机科学电子笔记68第二次（2002年）网址：http://www.elsevier.nl/locate/entcs/volume68.html18页关于π-演算马尔科·卡博内金砖国家1，奥胡斯大学，丹麦奥胡斯。carbonem@brics.dk塞尔吉奥·马塞雷斯英国伦敦帝国理工学院maffeis@doc.ic.ac.uk摘要我们扩展的π演算与polyadic同步，一个概括的通信机制，允许通道名称是复合的。我们表明，这个操作很好地嵌入π演算的理论，并使之有可能获得无发散编码的分布式演算。我们给出了分离的π演算与polyadic同步（eπ）和原来的演算之间的结果，在风格的类似结果Palamidessi混合选择。我们对Local Areaπ进行编码，展示如何控制eπ中资源的本地使用。1介绍进程演算提供了一个有用的框架来推理分布式系统的理论：它们因非常简单和表达能力而受到称赞在设计π-演算[21]时，奥卡姆剃刀原理似乎发挥了重要作用：语言简洁而有力，在提出一个新的结构之前，应该展示令人信服的例子来证明这种扩展。因此，为了提倡多元同步的建议，我们开始从开放分布式系统的世界中引入两个表达性问题。第一个问题是对电子服务进行建模，其中保证客户不会无限期地参与与不提供服务的合作伙伴的交易。符合其要求的服务。绘制EDπ，在[6]中，我们显示1BRICS，计算机科学基础研究，由丹麦国家研究基金会资助。2002年2月出版，电子科学和B。 V. 操作访问根据C CB Y-NC-N D许可证进行。卡本和马菲2·· ⟨ ⟩编程解决方案的实用方法：提供抽象机制来表示事务。第二个问题是建立一个分布式对象系统的模型，当且仅当某个对象提供了请求中调用的方法，并且准备好执行时，消息才被发送到该对象。一个成熟的解决方案是Vasconcelos和Tokoro的对象演算的语义第一个问题要求只有当客户和服务提供商就一组服务参数达成一致时才能进行交互。第二个要求消息和接收者就对象标识和方法达成一致。这两个问题都可以概括为在不同过程中匹配值向量的问题的实例我们将匹配问题定义如下：有没有可能设计模块化的分布式系统，其中客户端和服务器只有在共享一定数量的值时才进行交互，而不会引入分歧？解决方案包括将每个流程的接口中要匹配的值直接带到系统中，并提供语义规则，当且仅当这些接口兼容时才允许交互。这是上述两种方法所采用我们表明，匹配问题不能解决π演算与混合选择，并克服这一限制，我们引入polyadic synchro- nisation：一个基本的和增量2的微积分扩展。这个想法是输入或输出动作的主题不再局限于一个名字，而是一个名字向量。例如，我们允许前缀诸如b（x）和a b v，其中信道由向量（a，b）标识。事实证明，有了这个扩展，匹配可以用通信机制，并且因此不再需要作为原始的。多元同步可以被认为是描述在具有结构化地址的通道上的通信，而不是原子地址。典型的π演算实现将测试给定名称在在发送消息之前，将通道名称池化。多元同步的实现将需要对每个部分重复该过程给定通道的地址。从不同的角度来看，考虑到作为单个地址的整个同步向量将允许π演算的现有实现的平滑适配。1.1建模地点许多分布式演算引用了一个明确的位置概念，旨在作为计算发生的分布单元。它们中的一些是作为π演算的扩展而提出的，并且基于这样的思想：在某个位置并行运行的进程可以独立地迁移或与本地或远程的其他进程这类语言的例子2正如Berger和Honda在[3]中所预期的那样。卡本和马菲3·⟨⟩[2019 - 12 - 15][2019 - 12 - 15][2019 - 12 - 15][2019 - 12 - 19]从实用的观点来看，这些模型在某种程度上比π演算更适合描述物理分布。从理论的角度来看，这些变体的必要性尚未在一般情况下，据我们所知。以分布式π演算[15]（其中类似π的过程被显式地封闭在位置中）作为一个范例。它的主要归约规则指出，两个进程之间的通信只有在它们处于同一位置时才能发生：（RCOMM） l[av.P]|l[a（x）. Q]›→l[P]|l[Q{v/x}]我们的观点是，一个位置可以被看作是一个名称，描述了一个进程参与的所有交互：因此，它可以被建模为一个附加的同步参数，在所有的通信过程中。迁移只是每个前缀的位置组件的动态（重新）绑定。例如，Dπ网络编码的结果l[am.P|a（x）。去x.bv.Q] |m [b（y）.R]是π-演算（eπ）的扩展过程，其中迁移构造gox消失，三个执行线程并行运行l·am.P |l·a（x）.x·bv.Q |m·b（y）·R.请注意，上面报告的规则（R）指出，当且仅当两个进程同时共享两个值（位置和通道）时，才允许它们做出反应，这是匹配问题的另一个实例因此，我们的表现力结果的一个可能的解释是，明确的位置是分布式演算中的一个基本类似地，我们建议嵌套位置在具有位置的可伸缩空间的模型中是不可编码的，例如，证明了缺乏Ambients到其他演算中的组合，无发散编码。1.2密码学建模作为另一个例子，我们声称eπ能够表达一类有趣的安全协议。 事实上，可以使用多元同步来编码安全信道：在密钥k下加密的数据m沿着公共信道a的发送被表示为a k m .P，这意味着除了公共名称a之外，m只能由知道秘密密码k的代理接收。相对于Abadi和Gordon [1]的Spi演算，该解决方案缺乏表达通过散列数据获得的密钥的能力。我们现在考虑一种不同的方式来表示eπ中的加密，仍然依赖于同步多个名称的能力，但更具表现力。我们提出了加密和解密数据的结构，这样加密的消息就表示为名称（因此仍然可以加密，发送或用作密钥），加密是不确定的（在同一密钥下加密同一消息两次会产生不同的结果）。这些结构是：卡本和马菲4K·K[[encrypt mR x in P]]=（νx）（！x·km |P）[[decryptxRminP]]=x k（m）.PK第一个构造在密钥k下加密数据m，并将加密的消息作为名称x返回，新的将在P所包含的所有范围内使用。通过密钥k对消息x的解密将延续部分P中的名称m绑定到原始消息，前提是密钥与用于加密它的密钥相同。注意，加密的结果x是一个受限制的名称，其作用域是进程P。这不是一个限制，因为x的范围可以使用挤出以标准方式扩展，允许定义中的模块化的过程。例如，很容易看到下面的系统演化为R{m/w} |S|A和A单独不能妥协的秘密m。接收者：（v k）securepublic（y）. 在R中解密yRw ： （ νm ） secure （ z ） 。 encryptmRzxinicx.SSystem：（ν secure）（|接收器）|一1.3相关工作引入事务代数，Ferrari [12]用复合前缀扩展了CCS，允许多方同步和多方之间同步的混合形式。Castellani和Boudol [5]研究了将有限计算视为并发语言语义上的原子事件的影响，但似乎在他们的框架中无法表达多元同步。Nestmann [23]在π演算框架中研究了联合输入的表达能力，这是[14]中连接模式的自由化：它可以被视为输入过程的双向同步的一种形式。由于缺乏相应的二元输出，它没有提供匹配问题的解决方案。Abadi和Gordon（[1]的附录A）提到了元组的同步，指出π演算可以更好地抵抗安全攻击，但没有进一步发展这个主题。米尔纳[22]在一次关于多项式π-演算的演讲中主张沿着元组同步的想法，但关于这个主题没有更多的参考文献1.4文件计划在第2节中，我们扩展了π演算与polyadic同步，我们表明，它的方程理论是强大的关于这个扩展。在第3节中，我们证明了多元同步增强了表达能力的演算显示分离的结果。我们在π-演算中给出了eπ的一个完全抽象的发散编码，并将我们的表达性结果与以前的结果联系起来。在第4节中，我们展示了eπ的表达性的一个例子，给出了局域π-演算的无发散一致编码[9]。3联合输入的主要归约规则是一个|bd| {a（x）}|b（y）}.P\P{c/x}{d/y}，其中{a（x）}|b（y）}，P可以看作na·b（x，y），P，y与nπ有区别.卡本和马菲5| |αfn（α）u（x），u<$vx<${a|a ∈u}bn（α）{x}ub{a|a∈u} <${b}<$2π-演算中的多元同步π演算[21]是一种形式主义，用于描述基于CCS继承的命名通道同步思想的通信进程的并发执行。我们的建议是将同步机制扩展到通道由名称向量表示的情况，仅当这些向量匹配元素时才允许交互发生。同步仍然是原子性的：我们强制执行全有或全无的行为。2.1语法过程的语法和结构同余关系与π演算文献中的相同，有时具有直接扩展：P、Q、R = 0 | P |Q|（νn）P|(νn) P| ! P不同之处在于输入和输出前缀的概括α：：=a1·. ·a k（x）|a1. ·a km一个通道现在是一个名称向量，同步向量：π演算是只允许长度为1的向量的实例。同步向量将用字母u和v表示，在必要的地方，我们将以CCS风格编写纯同步的前缀。输入或输出前缀的主语是用于通信的通道，宾语是参数。给定一个前缀α，我们回想起自由名（fn（α））、约束名（bn（α））和名（n（α）=fn（α）<$bn（α））的概念：函数fn和bn以通常的方式推广到过程。 一个名字对于集合S，如果s∈/S;对于过程P，如果s∈/n（P）。符号是101.. nP i是多元并行复合P 1的简写. P n.关于通信对象的多元性是与多元同步正交的概念：当需要时，我们将参考多元版本的演算。πN家族 我们用π k表示同步向量的长度至多为k的子语言。一个简并的例子是π0，其中通道是无名的，过程通过全局以太4：πvπ相互作用。 P|（x）.Q −→P|Q{v/x}。 特别地，π-演算=π1\π0，并且eπ=πN将表示演算族{π0，π1，π2，. }。nπn，而4它本质上是Ambient Calculus的局部通信机制[7]。卡本和马菲6⟨ ⟩ ⟨⟩αi−→···|·我−→我 我αu（x）2.2语义我们将多元同步的操作语义定义为π演算标记的转换系统的扩展，特别是将[21]的后期lts适应于同步向量。转换标签α是τ，表示无声动作，u（x）表示输入，u b表示自由输出，u νb表示约束输出。 我们省略了（CLOSE）和（CLOSE）的对称规则。Pub PJ，Qu（x）QJα.P−→P（PREFIX）−→ −→P|Q − τ → P J|QJ{b/x}（）P|！P−α→PJPu<$v x<$PJ，Qu（x）QJ（BANG）−→ −→（关闭）！P−α→PJP−α→PJP|Q −τ→（νx）（PJ|QJ）PuxPJ（νx）P−α→（νx）PJx/∈α（RES）−→（v x）Pu<$vx<$PJx/∈u（OPEN）匹配. 在eπ中，可以将匹配定义为导出算子。如果x在P中不是自由的，则 过 程 （ νx ） （ xmxn.P ） 等 价 于 π 演 算 过 程 [n=m]τ.P ： 根 据 规 则（Τ），两个过程xn.P和xm只有在n等于m时才能相互作用。注意，对名称x的限制防止了来自任何可能的上下文的干扰。如果匹配成功，将导致一个τ（隐藏）操作。2.3等式理论在本节中，我们证明了我们的扩展对于π-演算的方程理论是鲁棒的[20]。我们开始扩展的概念（强）早期互模拟同步向量的情况下。定义2.1[互模拟]过程上的二元对称α关系S是早期互模拟当且仅当：PSQ和P−→PJ意味着(i) 如果α = u（x），则αb。QJ：QQJ(ii) 如果α不是输入，则<$QJ：Q−→QJ<$PJS QJ。对于某些早期的双模拟S，P与Q（P_S_Q）在fP_S_Q中是早期双相似的。和π-演算一样，π是一个等价关系，但不是一个同余，因为它不是在inputprefix下关闭的。 F或实例a|你好。b+b。本我卡本和马菲7发明公开了一种复合材料，其中a是c（a）。（一个|（b）国家统计局c（a）。（a. b+b。a）。下的二进制运算的闭合任何上下文都是一个同余关系，我们将用表示;对于一个形式上的卡本和马菲8这是我们所讨论的问题[28]。eπ中的强早期互模拟比匹配的π-演算更精细。在[28]中，表明两个过程P1=a（x）. P和P2=P1+a（x）. [x=n]P是早期双相似的。 在eπ中，它们不是：在P2中的匹配变为（νb）（b·x|b·n.P），如果x=n，则P2可以在还原为P之前执行τ作用，而P1不能提供一个对应物现在考虑后期互模拟，它与早期互模拟在给定的b和QJ上的量化顺序上不同。后期互模拟仍然更精细，就像π演算中一样：替换上面的过程P1（也在P2）与过程P1J=a（x）.τ+a（x）.τ.P（它提供了缺失的τ作用量），得到了早而非晚的双相似过程前面的关系称为强互模拟。在某些情况下，抽象τ上的动作并考虑仅关于输入和输出动作的互模拟是有趣的。设=是− τ →的自反传递闭包，且=αbe=−α→=。通过将定义2.1中Q−α→QJ的所有实例替换为Q=α<$QJ，可以得到W E AK EARLY BISIMULATION（W E AK EARLY BISIMULATION）。异步的情况下。 在[4，16]之后，我们将异步eπ（a eπ）定义为具有非阻塞输出且没有求和的受限语言。文[27]证明了在无匹配的异步π-演算中，弱基互模拟5成为一个同余. 当i≥2时，由于编码匹配的能力，该结果不适用于πi例如b（x）。[x=a]xastecGb（x）. 0，但选择输出，使ch在c通道b上发送a我们有Ba|b（x）。[x = a] xa/Gba|b（x）。0.3多元同步在下文中，我们将参考De Boer和Palamidessi在[11]中给出的“合理”编码的概念，并在文献中广泛采用，特别是在[25]中。其思想是，语言的编码应该是组合的，在关于平行组合和非确定性选择的同态意义上，并且应该是终止不变的，这意味着过程的成功或失败应该通过翻译来保留3.1一类π-演算我们继续展示我们的主要表现力结果：过程演算的πN族严格地按照包含的表现力排序。特别地，我们证明了匹配问题是一个分离问题：在πk中不可能写出两个非发散过程来检测两个k+1个标识符的向量是否相等，而在πk+1中是可能的。匹配问题。 为了规范匹配概率的定义，5当只考虑定义2.1中的第二点时，互模拟是基础，其中α意味着任何行动。卡本和马菲9CC/→→↓a1，.，an（x，x）甲乙丙甲乙丙甲乙丙Kii→/→∀ ∃ ⇒ ∃ ∈ ↓∧甲乙丙lem，我们专注于微积分的一般概念：基于通信的计算（CBC）。一个进程代数是一个CBC，如果并行进程只能通过一个点对点的通信机制进行交互，基于这样一个概念，即用互补的刺激来呈现环境，共享的免费名称。此外，必须提供一个结构来表达无限行为（例如，复制操作符“！”），名称必须从一个简单的集合中得出：没有代数可以在它们上面定义。 在下文中，假设P和Q是某些CBC中的过程：我们将写P <$Q，这意味着P执行有限次约简（最终没有）并成为Q，并且P <$如果P陷入了僵局两个互补刺激的名称在α中，将被表示为byα1−·。→.. ·αn，α1−·。→.. ·αn。WedefineeobjectbarbsP↓伊希斯作为P的能力，具有对象为s的输出刺激的环境。PS将表示所有对象倒钩的集合，其中S中的值由过程P展示，即P↓S{s∈ S|P<$s<$}。最后，P是n次的过程模板，当且仅当其自由名（参数）是{y，x1，.，x n}，我们把它写成（y）（x1，.，xn）或者根据上下文简单地称为P。 的实例化P中的参数，名称为b，a1，...， a n，用P b表示. 我们将将b称为进程索引，将a称为1，...，进程标识符。例3.1为了熟悉前面的定义，我们给出了eπ（它是一个CBC，和大多数其他进程代数一样）中的一些例子。取一个eπ过程P = x1·x2<$x2<$|x1·x2（w）。“你看，这是一个好主意，把它看作是一个好主意。2次P（y）1 2 . 实例化其参数，如Pi=a·bb |a·b（w）。我们可以观察到，我=Q，（Pi↓⟨b⟩ Q↓持有，Pi↓{i，j}=n，w其中P↓{a，b，i，j}={b}。 最终y，Q<$/→。为了表达匹配系统背后的直觉，在下面的定义中，把每个过程L看作一把锁，把每个过程K看作一把钥匙。匹配系统的重要性指定了确定钥匙能够打开锁所需的参数数量。 在有限数量的步骤中，每个钥匙必须与一个互补锁相关联，如果存在的话。另一方面，不相关的钥匙和锁不得关联。定义3.2（匹配系统）设K和L为任意两个n阶过程模板。 K和L构成元数为n的匹配系统MSn（K，L）当且仅当，对于所有新指标的有限集合I和J，对于任何可能的选择标识符向量k i= k i，.，k i和l j= l j，...，l j，对于所有P1n1n形式为：我k，...，K| Πj∈JJlj，.，LJ ，则以下成立：1n1n(i) 对于每个过程Q，使得P

下载后可阅读完整内容，剩余1页未读，立即下载