图变换的同步代数：全球计算中的模拟和建模技术

理论计算机科学电子笔记138（2005）43-60www.elsevier.com/locate/entcs图变换的可迁移同步代数Ivan Lanese and Ugo Montanari伊万·兰尼斯和乌戈·蒙塔纳里1，2Dipartimento diInformaticaUniversit`adiPisa意大利比萨摘要我们提出了一个广义的同步代数，允许处理移动性和本地资源处理。我们展示了它如何可以用来模拟通信原语的分布式和移动计算，如在全球计算领域中使用的。 我们提出了一个图形变换形式主义的同步超边缘替换方法，这是参数w.r.t.同步代数，从而允许基于所选择的通信原语对复杂系统进行建模。因此，我们统一了文献中描述的不同模型，并允许轻松定义新模型。我们提出了各种各样的例子和案例研究融合演算，显示如何不同的语义，它可以使用不同的同步代数。关键词：图变换，同步超边替换，同步代数，迁移率，融合演算。1介绍全球计算（GC）处理部署在世界范围内的大型计算系统。为了开发、分析和管理这样一种复杂的系统，其中协调、安全和移动性等不同问题相互作用，需要合适的正式工具。*研究部分由EU-FET项目AGILEIST-2001-32747支持。1电子邮件：lanese@di.unipi.it2 电子邮件地址：ugo@di.unipi.it1571-0661 © 2005 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.00444I. 兰尼斯群岛Montanari/Electronic Notes in Theoretical Computer Science 138（2005）43我们认为，这些系统必须在不同的抽象层次上进行分析。特别是，在低层，必须开发协议和算法，以在通常是异步和不可靠的基本基础设施之外构建高效和可靠的中间件在更高的层次上，中间件中定义的原语必须用于协调不同子系统的演化。在GC场景中，我们也可能有复杂的同步原语，涉及多个计算实体，因此我们需要一种合适的方式来建模它们，然后我们需要一个框架来描述基于这些原语的大型系统为了使实现步骤更容易，计算必须是分布式的，协调部分必须是明确个性化的。特别是，必须禁止需要对整个系统的拓扑结构有很强知识的计算，因为这种知识通常不可用。我们选择图（或者更准确地说，超图）作为基本模型，因为它们具有暗示性的表示，并且它们自然地对分布式系统的拓扑结构进行建模。我们将以下计算解释与图相关联：边表示过程或子系统，而节点则表示通道或端口。通信通过共享节点执行。计算通过同步超边缘替换（SHR）方法中的图形变换进行建模[2]。在这个框架中，上下文无关的产生式描述了边缘的局部演化。这样的产品可以很容易地实现，因为它只涉及一个组件。为了指定复杂的重新配置，我们引入了一个同步机制，该机制基于对共享节点施加的约束来决定哪些产生式可以在一个步骤中应用我们还想直接对移动性建模，我们在Fusion Calculus [14]风格中使用名称移动性来做到这一点[7，4]。基于局部产生式的方法将SHR与其他图转换框架（如Double Pushout [3]和Bigraphs [5]）区分开来，其中使用具有任意复杂左侧的规则，并且它允许分布式实现[2]。我们提出了一个框架，其中同步和移动性模式由适当的代数指定，该代数扩展了同步代数[15]。相对于标准的同步代数，我们的方法也能够处理移动性和本地资源处理，这是GC系统的两个基本特征具有迁移率的同步代数允许恢复SHR文献[4，12，9]中提出的同步模型，并轻松定义更复杂的模型。这一点很重要，因为文献中的模型都是非常低级的，而复杂的高级原语对GC很有用。我们给出了许多例子来说明同步代数I. 兰尼斯群岛Montanari/Electronic Notes in Theoretical Computer Science 138（2005）4345与移动性可以用来指定同步原语，以及如何SHR可以用来模拟全球和无处不在的计算感兴趣的场景作为一个有趣的案例研究，我们提出了一个映射融合演算[14]（一个进程代数，扩展了π-演算[13]与融合的概念如在[11]中证明的，在Fusion Calculus和具有Milner同步的SHR我们表明，使用同步代数不同的语义可以提供融合Cal- culus，从而允许将其应用到基于不同的通信原语的系统本文结构图、同步超边替换和同步代数的背景在§2中给出。在§3中，我们提出了具有移动性的同步代数，而§4包含参数SHR的规则§5中给出了一些例子，第6节。最后§7提出了结论和未来工作的痕迹2背景2.1图作为句法判断我们希望使用超图来建模系统，超图概括了允许（超）边连接到任何数量的连接节点的图。特别地，我们使用具有标记边缘的（超）图，即边缘是具有标签的原子项（来自排名字母表LE ={LEn}n=0，1，. ），并具有与其标签L的rank rank（L）一样多的有序触角。 一组如果每条边通过其触角连接到其附着节点，则节点与一组这样的边一起形成图。图通过接口连接到其环境，该接口是其节点的子集。接口中的节点称为自由节点，而其他节点称为绑定节点。我们consider图同构，保持自由节点，标签的边缘，边缘和节点之间的连接。我们使用图的线性表示作为（句法）判断，这更适合于定义变换[8]。在这种表示中，节点对应于名称，自由节点对应于自由名称，边对应于基本术语，形式L（x1，.，xn），其中xi是任意名称，L∈LEn. 我们使用一个常数nil来表示空图，一个并行复合算子| to build large graphs from smaller ones and a ν operator to bind nodes.定义2.1（图作为判断）设N是一个固定的有限名称集，LE是一个排序的标签字母表。一个判断的形式为ΓG46I. 兰尼斯群岛Montanari/Electronic Notes in Theoretical Computer Science 138（2005）43(AG1)（G1）|G2）|G3-G1|（G2）|G3） (AG2) G1|G2-G2|G1（AG3）G|nil G（AG4）νxνyG<$νyνxG（AG5）νxG<$Gifx∈/fn（G）（AG6）νxG<$νyG{y/x}ify∈/fn（G）（AG7）νx（G1|G2）（νxG1）|G2ifx∈/fn（G2）表1图项的结构同余。其中：(i) [1][2][3][4][5][6][7][8][9][10][11][12][10][11][12][13][14][15][16][17][18][19][10][19(ii) G是由语法G：：= L（x）|G|G| νy G|无其中x是名称的向量，L是具有rank（L）= |X|和Y是一个名字。我们把限制算子ν定义为一个结合子。我们用fn表示函数，该函数在给定项G的情况下返回G中自由名的集合fn（G）。我们要求fn（G）<$ r。在定义界面时，我们用记法Γ，x来表示由x加到Γ而得到的集合，假设x∈/Γ和Γ1，Γ2表示Γ 1和Γ 2的并集，假设Γ 1 <$Γ 2= Γ。图项被认为是表1中的结构同余公理。就判断而言，我们定义了Γ<$G<$ ΓJ<$GJ i <$Γ = ΓJ和G<$GJ。公理（AG1）、（AG2）和（AG3）分别定义了零上运算的结合性、交换性和恒等式|. 公理（AG4）和（AG5）指出，图的节点只能以任何顺序隐藏一次公理（AG 6）定义了图的α-变换。绑定的名字。公理（AG7）定义了限制和平行合成之间的相互作用。注意，函数fn在等价类上定义良好定理2.2（表示的可靠性[6]）直到结构同余的判断同构于直到同构的图。2.2同步超边缘替换我们在这里介绍同步超边替换（SHR）[2，7，4]，这是一种图变换形式主义，其中通过同步上下文无关产生来指定转换，该上下文无关产生描述了如何重写单个边。生产将边重写为具有相同接口的图，并公开其接口节点上的操作。操作是约束，如果约束施加在I. 兰尼斯群岛Montanari/Electronic Notes in Theoretical Computer Science 138（2005）4347Λ，πΛ，π共享节点是兼容的。对节点的引用的元组被附加到动作，并表示在同步期间通信的名称此外，产生式可以通过适当的替换来强制接口中的节点之间的合并我们也使用基于判断的符号来表示过渡。定义2.3（SHR转换）设Act是一组动作，并给出a∈ Act设ar（a）为它的arity。SHR转变的形式为ΓG−−→ Φ φGJ其中，Γ<$G和 Φ<$GJ是图的判断， Λ：Γ→（Act×N<$）是一个全函数，π：Γ → Γ是一个幂等代换.函数Λ给每个节点x分配动作a∈Act和通过转换暴露在x上的节点引用的向量y（在更消息传递的观点中，我们说节点引用被发送到x）。 如果Λ（x）=（a，y），则我们定义行为Λ（x）= a且n Λ（x）= y。 我们要求ar（act Λ（x））= |n Λ（x）|.我们定义：• n（Λ）= {z| <$x.z∈ n Λ（x）}一组暴露的名称;• Γ Λ= n（Λ）\ Γ一组新名字被曝光置换π允许合并节点。由于π是幂等的，它将每个节点映射到其等价类的标准表示我们要求<$x∈ n（Λ）.π（x）= x，即只有对代表的引用可以被暴露。此外，我们要求Φ = π（Γ）<$Γ Λ，即自由节点永远不会被擦除（π），新节点除非暴露（π），否则被绑定。注意，结果图的自由名集合Φ完全由Λ和π决定（因为Γ = dom（Λ））。当把Λ写成对的集合时，我们把对（x，（a，y））写成三元组（x，a，y）。SHR转换是使用适当的推理规则集从基本产生式模式导出的（参见§4）。定义2.4（生产模式）生产模式是以下形式的SHR转换x1， .. . ，xnL（x1， . . ，xn）−−→ΦG其中所有xi，i = 1，. n是不同的。我们假设对于每一个元数n的边标签L，有一个特殊的空闲亲，Λc，idduc tionschemax1， .. . ，xnL（x1， . . ，xn）−→x1， . . ，xnL（x1， . . ，xn）其中，对于每个i，Λ（xi）=（，）（是特殊的“空闲”动作，ar（）=0）。当我们有一个生产模式，我们假设也有所有的生产48I. 兰尼斯群岛Montanari/Electronic Notes in Theoretical Computer Science 138（2005）43可通过{x1，.，xn} Φ。2.3同步代数我们在这里提出同步代数，在[15]中提出来处理进程之间的同步，因为它们在CCS中执行。为了与标准SHR符号保持一致，我们在这里使用了稍微不同的表示法。一般来说，我们考虑一个框架，其中流程可以执行操作，操作可能同步，也可能不同步。假设两个进程P和PJ可以分别执行动作a和aJ。如果动作a和J同步，则它们的同步执行对应于仅一个动作，否则它们不能一起执行由于一个动作也可以异步执行，我们还必须引入一个表示“无动作”的动作前缀因此，a和Pj的同步执行对应于a的异步执行，而PJ保持空闲。定义2.5（同步代数）一个同步代数由一个二元的、部分的、结合的和交换的算子·在一个动作集Act上构成，其中包含一个区别元n.我们要求：a，b∈Act.a· b = a，b = a，b = b，并且a不是Act中唯一的动作。二元运算符·表示动作如何组合形成同步动作：如果a·b未定义，则a和b不能同步，否则a·b是组合动作。附加条件要求动作永远不会消失，因此同步两个非同步动作的结果永远不会被同步。3具有迁移性的我们在这里提出了同步代数的推广[15]，它也可以处理移动性和本地资源处理。特别是，我们对Fusion Calculus [14]风格中的名称移动性感兴趣，其中通过将进程控制的通道与其他进程控制的通道合并来建模进程的移动性，从而建模它们的接近度。我们为每个动作附加一个通道引用元组，当动作同步时，必须指定通道之间的融合模式对结果通道的引用附加到同步操作。在我们的框架中，通道可以是公共的，也可以在一组进程中共享（从而对本地资源进行建模）。在本地通道上，我们只能进行完全同步，即不需要任何进一步操作的同步在其他通道上，我们也可能有部分同步-I. 兰尼斯群岛Montanari/Electronic Notes in Theoretical Computer Science 138（2005）4349将由环境提供的动作完成的动作我们现在给出带移动性的同步代数的形式定义，它考虑了所有这些方面。作为一种表示法，我们用表示不交集并。在这里，我们用[1，n]来表示。[2，n]）对应于n∈A的元素（分别为n∈B）。定义3.1（具有移动性的同步代数）具有移动性的同步代数）y（a，s>）z（a，t>）yXzSR不Xy（a，s>）（一）yWXN（a，r>）Nz（a，t>）wz（a，u>）sR不（b）第（1）款uFig. 1. 复制网络的生产（a）和过渡（b）。以及由秩（N）= 3的N标记的边。{（x，a，r），（y，a，s），（z，a，t）}，idx，y，z<$N（x，y，z）−→x，y，z，r，s，t <$N（x，y，z）|N（r，s，t）图1（a）是生产的图形表示，而在图1（b）中，我们有一个简单的过渡。为了导出这个转换，我们必须取两个适当重命名的生产模式实例，然后使用规则（par）获取：x，y，z，w，y1，z1<$N（x，y，z）|N（w，y1，z1）{（x，a，r），（y，a，s），（z，a，t）（w，a，u），（y1，a，s1），（z1，a，t1）}，id−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−→x，y，z，r，s，t，w，y1，z1，u，s1，t1<$N（x，y，z）|N（r，s，t）|N（w，y1，z1）|N（u，s1，t1）然后，我们可以应用两次规则（合并），其中σ={y/y1}和σ={z/z1}最后得到x，y，z，w <$N（x，y，z）|N（w，y，z）{（x，a，r），（y，a，s），（z，a，t）（w，a，u）}，id−−−−−−−−−−−−−−−−−−−−−−→x，y，z，r，s，t，w，u <$N（x，y，z）|N（r，s，t）|N（w，y，z）|N（u，s，t）如所期望的。 注意，当应用第一个（合并）规则时，我们有S1={s =因此，我们可以选择ρ ={s/s1}。可以通过这种转换建模的现实场景是例如在端口上接受通信的服务器进程，其可以被建模为仅具有一个空闲节点的图，并且当客户端需要时NNN NN N56I. 兰尼斯群岛Montanari/Electronic Notes in Theoretical Computer Science 138（2005）43例5.2（生命的游戏）3生命的游戏[1]是一个著名的元胞自动机，它是一个由进化中的细胞组成的网格。单元格可以是空的，活着（Alive）如果一个活细胞有一个或没有活的邻居（孤独），或者如果它有四个或更多的活邻居（过度繁殖），那么它就会死亡，否则就会存活下来。如果一个空的细胞正好有三个存活的邻居，那么它就变成存活的。为了模拟生命游戏，我们使用代表细胞的边，标签A代表活着，E代表空。 它们的边缘与八个相邻的-通过共享节点进行传输。在每一步中，边缘必须在每条链路上传达其状态，同时接收其邻居的状态。这可以使用四个动作（e，e）、（a，a）、（e，a）和（a，e）来完成。例如，最后一个动作的含义是“我活着，你是空的”。我们还引入了一个动作ok来表示成功的同步。由于网络是静态的，我们没有移动性，即，所有动作具有arity 0。我们使用以下同步代数（带移动性）：• Act={（e，e），（a，a），（e，a），（a，e），ok，};• ·a=a对于每个a∈Act，（e，e）·（e，e）=ok，（e，a）·（a，e）=ok，（a，a）·（a，a）=ok;• int= {int，int}，int={int};• Mob仅包含来自于 我也是。为了强制完成同步，必须绑定所有内部节点。 我们使用一个简化的符号来表示生成：我们只写边的标签和动作的序列。在这里，我们有一些产品：（a，e），（a，a），（a，e），（a，e），（a，e），（a，e），（a，e）孤独一−−→E（a，e），（a，a），（a，e），（a，a），（a，e），（a，a），（a，e），（a，e）生存一−→A（a，a），（a，a），（a，e），（a，a），（a，a），（a，a），（a，a），（a，e）在p算子A−→E上（e，a），（e，e），（e，e），（e，a），（e，e），（e，e），（e，a），（e，e）populateE−→A例5.3（阈值同步）我们在这里定义了一个阈值同步的代数，它允许一组进程从发送者那里获得一些信息，但前提是至少有m个进程同意。具有移动性的同步代数定义如下：• Act= {out，n}{（in，n）|n ∈}<${（in <$，n）|} ;• out和（in，n）的arity为1，（inn，n）的arity为2，否则为1• ·a=aI. 兰尼斯群岛Montanari/Electronic Notes in Theoretical Computer Science 138（2005）43573我们感谢罗宾·米尔纳，他在达格斯图尔研讨会04241上提出了这个例子。58I. 兰尼斯群岛Montanari/Electronic Notes in Theoretical Computer Science 138（2005）43out·（in，n）=（in，n），（in，n1）·（in，n2）=（in，n1+n2），（in，n1）·（in，n2）=（in，n1+n2）;• F in= {}{（in，n）|n∈}，Init= {n};• Mob总是将（in，n）的参数和（inn，n）的第一个参数映射到结果的第一个参数，并且将out的参数和（in n，n）的第二个参数（无论何时定义）映射到结果的第二个参数（inn，n），如果n

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