理论计算机科学电子札记97（2004）97-124www.elsevier.com/locate/entcs分布式系统协调模型的语义研究：LogOp案例研究罗纳尔多·梅内塞斯a，1安德烈·奥米奇尼b，2米尔科·维罗利b，3佛罗里达理工学院地址：150 West University Blvd.Melbourne，FL 32901，USAbDEIS，Universit`adegliStudidiBolognaviaVenezia 52，47023切塞纳，意大利摘要L OG O P是一个扩展Linda的协调模型，它允许一个协调操作动态地处理多个可能分布的元组空间。Log O P的设计提出了协调和分布式系统工程领域普遍感兴趣的相关问题。特别是，设计的基础设施，支持制定协调法律，涉及多个物理分布的元组空间需要仔细处理的同步性，原子性，局部性的相互作用，和全球的协调规则的解释有关的方面。在本文中，我们阐述了这些一般性的问题，从研究的语义LO-GOP。首先，介绍了LOGOP协调模型作为Linda模型的然后，两个不同的语义，都符合LOG OP的非正式规格，正式描述和比较。最后，传统方法的协调（协调作为一种语言）的正式表征的局限性被指出，并通过不同的方法（协调作为一种服务），其好处是通过适当地重新制定LOGOP语义说明解决一方面，这提供了关于如何将LOGOP协调模型部署为分布式系统的协调基础设施所提供的交互式服务的另一方面，上述结果允许在开放和分布式系统中的协调的一些一般方面被清楚地指出，并充分讨论。关键词：协调模型，琳达，分布式系统，形式模型，软件基础设施1电子邮件：rmenezes@cs.fit.edu2 电子邮件地址：aomicini@deis.unibo.it3电子邮件：mviroli@deis.unibo.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.03398R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-1介绍协调模型和语言在当今和未来分布式系统的基础设施设计中扮演着关键角色，其目标是为复杂系统中的管理和统治交互提供手段。LINDA[15]可能是这种模型最著名的例子之一：元组空间扮演黑板的角色，被用作调解不同实体之间交互的手段，促进时间和空间解耦。虽然它起源于封闭的并行系统领域，但LINDA的主要特性和特征如今已在基础设施中得到利用-例如JavaSpaces [14]，TuCSoN[23，20]，Mars [8]和LIME[21]。- 旨在解决开放、分布式和高度动态系统中交互的复杂性。显然，在协调模式领域寻求新的解决方案仍然是一项主要挑战，其对成功技术发展的影响将越来越重要。在这篇文章中，我们研究了LOG OP[22]，这是一个扩展基本LINDA的协调模型，它增加了一次调用涉及多个元组空间的协调原语的能力。通过这个特性，协调规则不再局限于单个元组空间的上下文，而是可以通过瞬时形成扩展的可见性范围来定义，通过将不同的范围和可能分布的元组空间连接起来来获得。然而，这种新模式的重要性不仅在于增强的表现力和灵活性。与分布式系统中的管理交互有关的相关问题由LOGOP的设计明确提出，这在协调和分布式系统工程领域中具有普遍意义。特别是，表达一个协调法涉及物理分布的元组空间的想法需要一个仔细的处理有关的同步性，原子性，局部的相互作用，和全局解释的协调规则。事实上，这些问题在更一般的背景下是至关重要的，在这种背景下，基础设施是由分布式协调空间组成的，由相互作用的协调抽象构成。选择。在本文中，我们详细阐述了这些一般性的问题，通过LOG OP作为一个案例研究，并讨论其可能的语义。受构建封闭和并行系统的传统应用的启发，在第2节中，我们首先定义一个LINDA的形式模型，该模型具有多个元组空间，每个元组空间都可以通过调用协调原语单独访问。第3节指出了琳达模型的一些局限性，并说明了如何在LOGOP— 在其语法和非正式语义（如[22]中出现的）中定义— 是为了解决这些问题。R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-99第四节正式讨论了LOG OP通过扩展LINDA的形式化，并提供了一个关于分布式系统协调模型语义的典型问题的例子。事实上，两种不同的解释被证明与第3节中介绍的非正式语义学是相容的。特别是，最直接的延伸林达朝LOG OP，指的是作为强同步语义，其特征在于协调原语的原子执行然而，我们观察到，在分布式系统的上下文中，保持涉及物理分布式元组空间的操作的原子性可能需要相当具有挑战性的基础设施支持，包括例如事务管理的典型锁定和恢复机制通过放松这个强假设，我们开发了一个语义更合理的实现分布式系统，称为弱同步语义。在这种情况下，一个操作只被执行它的实体看作是原子的，而它在全局上被看作是一系列标准的LINDA操作。这两种语义进行了比较，并得出一些一般性的考虑。到目前为止，我们采用的语义方法是协调领域传统上使用的方法[3]：它是由协调模型作为构建应用程序交互部分的语言的传统应用所促进的，因此基于用于指定并发语言语义的相同框架另一方面，协调模型在当今计算机系统中最有趣的应用在那里，协调不容易被视为并发语言-例如。由编译器支持[26] -而是作为由多个协调媒体[10]提供的服务，例如LINDA-类元组空间。这种观点要求一个不同的语义模型，侧重于协调媒介的抽象及其交互行为。在[25，24]中，这两种观点之间的差异是有动机的，与许多相关的著作进行了比较，并在技术上进行了详细的分析特别是，前者被定义为作为语言的协调框架，而后者被称为作为服务的协调框架。这里最显着的区别是，将协调视为一种服务，促进了一些运行时方面的显式表示，这对协调模型的部署非常关键的影响，作为分布式系统的基础设施提供的交互式服务因此，从弱同步语义模型的LOG OP，第5节推导出一个公式的LOG OP作为一个协调服务提供的基础设施。这种新的表述展示了使用两种不同语义框架的含义，但也提供了一个重要的100R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-开发LOGOP规范。事实上，从LOG OP原语的语义-提供了LOG OP的抽象规范-导出了一个新的模型，该模型专注于LOG OP的交互行为。反过来，这个模型可以很容易地被解释为一个LOGOP基础设施的设计规范，因为它清楚地识别了所涉及的不同协调抽象，它们在整个协调过程中的角色，以及它们相互交互的管理。因此，指出并强调了一些对实现LOGOP服务至关重要的问题，而传统框架很容易忽视这些问题。更重要的是，本文的贡献不仅限于协调领域。相反，这篇论文也是为了提供一些重要的线索，今天的计算机系统的健全发展一般。在这里，事实上，我们超越了仅仅认识到，需要正式的模型来明确地指定和正确地理解复杂系统的行为我们在这项工作中建议的是，形式化模型也应该用于协调基础设施的设计，并且适当的形式主义实际上可以使抽象规范驱动基础设施开发走向合理和有效的实现。2琳达的语义LINDA是一个协调模型，它提供了使进程能够从元组空间中存储和检索元组的原语。在非常基本的LINDA模型[15]中，进程使用原语out来存储元组，使用原语in和rd来检索元组。特别地，in和rd原语接受一个模板，并使用关联匹配来选择一个要返回的元组-in删除匹配的元组，而rd则接受它的副本。in和rd都是阻塞原语。也就是说，如果在元组空间中没有找到匹配元组，则执行原语的过程阻塞，直到匹配元组实际上被放置在元组空间中并且可以被检索。为了保持文章简短而独立，我们考虑LINDA的子集，它通常用于形式语义的上下文中：特别是，我们只考虑原语out，rd和in，我们抽象出元组匹配机制，假设原语in和rd接受要查找的确切元组。然而，为了为分布式系统中复杂的协调问题铺平道路，我们用多个元组空间对LINDA进行建模，每个元组空间都有一个唯一的标识符i∈I，每个LINDA原语都可以通过其标识符单独访问。在这种形式化的传统方法中，例如[5]，LINDAR. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-101Σ被解释为一种用于构建封闭的并行应用程序的语言（这曾经是LINDA模型的第一个应用程序）。因此，LINDA的行为是通过向该语言提供操作语义来给出的，该操作语义描述了协调系统的可能演变，其中交互是根据LINDA协调语言来表达的协调实体可以建模为有限的，非确定性的过程，顺序执行一些林达协调原语。形式上，这些进程P的语法可以使用类似CCS的符号[18]表示如下：π：：=输出| 在|rd，β：：= π（i，x），P：：= 0 |β|P; P | P +P0表示空（或终止）进程，β表示在元组空间（具有标识符）i上执行原语操作π（i，x）-执行原语π的进程，涉及元组x-P;PJ，P+PJ是P和PJ之间的非确定性选择。其余部分中在本文中，运算符;被赋予比+更高的优先级，因此我们实际上用P;PJ+PJJ表示（P;PJ）+PJJ-其他歧义将像往常一样通过括号来解决例如，进程out（i1，x1）; rd（i2，x2）; 0 + in（i3，x3）; 0是在（i）顺序地执行运算out（i1，x1）和rd（i2，x2）或（ii）仅执行运算in（i3，x3）之间进行非确定性选择的进程。其中hI={a，b，c， . . . }作为Pa+Pb+Pc+的简写.. . ，并假设i∈{}Pi表示过程0。 然后，我们假设以下全等规则成立：0+P<$P P+PJ<$PJ+P（P+PJ）+PJJ<$P+（PJ+PJJ）0;PPP;0P（P+PJ）;Pjj（P;PJJ）+（PJ;PJJ）也就是说，我们认为两个不同的过程P和PJ是相同的，如果从a bove规则可以推断出PPJ。由于存在非自愿性规则，一个过程总是可以写为求和j∈J（βj;Pj），或者写为形式（β;P）+PJ. 一个LINDA配置L∈ L，表示一个在给定的时间，系统的语法由语法表示L：：= 0| 尼加拉瓜|P | （L）其中，符号“”通常用于并行合成。还假设以下一致性规则成立：0LLLJLJL（LLJ）LjjL（LJLJJ）102R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-因此，每个元素L都是一个由进程和项构成的有限组合，其类型为i，x，表示元组x出现在元组空间i中。一个操作语义可以通过一个转换系统<$L，−→ <$L赋予这种语言，其中转换关系−→是−→ <$L×L的类型。通常，语法L0−→L1用作<$L0，L1<$∈ −→的简写，并且意味着从配置L0时，系统可以移动到配置L1。 关系−→是定义为满足规则的最小关系：out（i，x）;P+PJ<$L−→P <$L <$<$i，x<$[L-OUT]rd（i，x）;P+PJ<$L<$i，x<$−→P<$L<$i，x<$[L-RD]in（i，x）;P+PJ<$L<$i，x<$−→P<$L[L-IN]这些可以被认为是LINDA：out发出元组的安全条件在元组空间上，rd等待出现在元组空间中的元组，而in等待元组，然后将其移除。此外，这些规则还为选择和顺序组合提供了语义：它们声明，每当执行原语操作时，任何其他选择（PJ）都被排除，而顺序组合到执行的原语（P）的过程被允许继续吧3LogOp毫无疑问，琳达不仅是第一个，也是最成功的协调模型：它的主要资产是在简单性和表达性之间实现的平衡。由于原语的有限集合，保证了简单性，同时获得了表现力，因为这几个原语可以用于对通信和同步模式的大量集合进行建模。尽管它的表现力，LINDA传统上被用作许多扩展的核心模型，以解决现代应用程序提出的问题，例如可编程行为（ReSpecT[19]），transactions和过期元组（JavaSpaces [14]），Prolog类功能（Shared Prolog [1]），可扩展性（SwarmLinda [17]）和移动性（LIME[21]），仅举几例。一个特别相关的扩展类已经开发出来，以处理新的应用领域的协调模型，从封闭的，集中的环境-主要的早期应用的LINDA-开放的，分布式的环境-最常见的框架，今天在那里，考虑由许多不同的元组空间提供的协调是明智的。具有多个参数的LINDA模型的推广R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-103除了上面提到的JavaSpaces，SwarmLinda和Lime之外，元组空间还包括其他空间，如TuCSoN[20]，Peer SPACES[6]和Bauhaus Linda [9]。特别是，在这个新的设置中，在和rd的阻塞特性和事实，这些原语只能处理一个元组空间的时间可能会阻碍LINDA表达复杂的协调模式的能力。更确切地说，LINDA中的原语迫使进程将元组空间视为不相交的：需要同时访问多个元组空间的进程必须通过串行化操作来实现这一点-即通过访问一个接一个的元组空间。因此，元组空间确实是不相交的，并且确实存在以形成元组的不同范围，在设计时识别。但是，可能需要不同的作用域，可能涉及多个空间，并且需要动态地（即时地）形成这样的作用域，然后丢弃。在任何时候组合元组空间的能力，形成一个单一操作的新范围，是Snyder和Menezes提议背后的主要动机[22 ]第22话合作 更具体地说，LOG OP旨在提高了LINDA原语的表现力，但由于表现力的原因，试图在实现级别上实现良好的性能。虽然观察到原始的LINDA模型缺乏表达涉及同时访问两个或更多个元组空间的协调的能力，但也注意到通常需要的元组空间之间的关联与基本逻辑运算符（如AND，OR和XOR）有关。我们在本文中考虑的LOG OP原语的语法如下：
：：= PRIM_NAME>（OP>（ts_id，..，ts_id），元组）：：= in|路|出来：：= AND|或|XOR其中ts id是元组空间标识符（或一般来说，元组空间的处理程序）。 逻辑运算符在L OG O P原语中用于指定目标元组空间：例如，原语out（AND（iA，iB），x）指定必须在iA和iB中插入元组x，rd（OR（iA，iB），x）指定必须从iA或iB（或两者）中读取匹配x的元组，以及in（XOR（iA，iB），x）指定必须从iA或iB中删除一个匹配x的元组，但不能从两者中删除。非正式地说，或运算符具有组合元组空间的效果，以便进程可以从任何指定的元组空间中存储和检索元组，而不必对元组空间的访问方式施加顺序。或运算符为模型增加了另一个层次的非确定性：元组将存储在列表中定义的某些元组空间中，也就是说，非确定性地存储在列表中的一个、多个或所有元组空间中104R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-XOR操作符类似于OR，但在这种情况下，元组可以从指定列表中的一个且仅一个元组空间中插入，读取或撤回。当客户端必须保证从列表中指定的元组空间中实际检索或删除的元组不超过一个时，此运算符非常有用。这里还添加了另一个非确定性级别，因为从中检索元组的元组空间先前是未知的。最后，AND运算符允许进程考虑一份名单 和与out一起使用允许进程将元组存储在列表中 一步就能完成元组空间的构建。 这与林达的情况相比，如果n个元组空间，则必须执行out原语n次。在和rd中的阻塞原语的情况下，和的语义是这样的，如果列表中的一个或多个元组空间未能包含与原语中给定的模板匹配的元组，则过程将阻塞4LogOp的语义在文献中，像上面这样的协调模型的语义的非正式描述通常被认为是可以接受的，甚至足以提供适合实现的规范。然而，在一般的并发系统领域，特别是协调模型领域，一个传统的问题是非正式描述固有的无法精确描述感兴趣的系统的属性。例如，在[4]中，对LINDA的out原语— 即，瞬时的，有序的，无序的-所有这些都实现了模型的现有非正式规范。更重要的是，在[7]中，Busi等人超越并展示了非正式规范如何甚至会导致不正确的系统，就像JavaSpaces协调模型[14]当前设计中事务的可串行性一样。LOG OP代表了这个问题的一个完美的案例研究-这确实是大多数非平凡的协调模型的普遍兴趣。因此，在下文中，我们提供了用于LOG OP的形式语义，其精确地说明了在元组空间上执行原语操作的效果以及由于并发访问而导致的可能的动态。事实上，我们表明，不同的语义实际上可以提供匹配的非正式描述的LO-GOP，如[22]和总结以上，不同的语义将导致实现不同的关键属性。特别是，我们表明，通过自然扩展LINDA（4.1小节）获得的模型并不适合为分布式系统设计LOG OP因此（4.2小节），我们通过提供一个更一般的语义模型来处理这个问题，比较R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-105两种不同的方法（第4.3小节），并最终设计出一些一般性的考虑。4.1强同步语义我们将第2节中提供的LINDA的语义扩展到LOG OP的情况，其中多个元组空间可以通过逻辑运算符关联在一起。在这个模型中，类似于LINDA的情况，原始操作的执行仍然被认为是系统中的一个单一事件，其结果是原子地改变协调空间的（分布式）状态。因此，域中的所有协调实体原子地感知协调原语的执行。因此，我们将LOG OP的这种语义称为强同步语义。我们在这种形式化中用来表示原始操作α（它是LINDA操作β的推广）的抽象语法现在是这样的：α：：= π（λ，x），λ：：= i. 吉吉|我... 吉吉|我... 吉吉在这里，λ是一个逻辑表达式，其中n元逻辑运算符AND（）、XOR（）和OR（）被应用于集合T中的元组空间标识符。给定元组空间标识符的有限集合I ={i0，i1，. 然而，该操作-操作π（i0i1. . 也可以写成π（i∈Ii，x），这意味着必须在集合I中的所有元组空间上执行本原π（逻辑连接AND）。类似地，π（i0<$i1<$. n，x）-等价地写为π（i∈Ii，x）— 这意味着原始π必须在以下元组空间中的一个上执行I（异或）。最后，π（i0<$i1<$... n，x）-或等同物-1999年，李嘉诚（i∈Ii，x）-意味着原始π必须在至少I中的元组空间之一（包含逻辑析取或）。A配置对于LOG OP系统S∈ S等价于LINDA模型的情形：S：：= 0| 尼加拉瓜 | P | (S ǁ S)给定元组空间标识符的有限集合I ={i0，.，in}，我们写i∈I<$i，x<$作为i0，x的简写ǁ ⟨in, x⟩,with0.i∈{}<$i，x<$自然地意味着为了将LOG OP的语义定义为LINDA情况的简单扩展，我们首先引入操作和元组之间的关系σ，使得σ（α，S）将可能涉及其执行的元组集合（连同其元组空间的标识符）关联到操作α，即，由out插入、由rd读取或由in移除的元组。这种关系是106R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-定义为满足规则的较小的一个：（2）A（i∈Ii，x），i∈I[S-AND]（2）A（i，x），<$i0，x<$）对任意i0∈I[S-XOR]i∈I（2）A（i，x），对于任何IJ，{}<$IJ <$I[S-OR]，i∈IiJ∈IJ正如非正式规范所报告的那样，操作符和涉及指定列表中所有元组空间中的元组，操作符XOR仅在一个元组空间中，而操作符或在元组空间集合的任何非空子集中。然后，LOG OP的语义由转换系统S，−→ S给出，其中转换关系−→ S×S由规则定义：out（λ，x）;P+PJ<$S−→P <$S <$SJifσ（out（λ，x），SJ）[LG-OUT]rd（λ，x）;P+PJ<$S <$SJ−→P<$S<$SJifσ（rd（λ，x），SJ）[LG-RD]in（λ，x）;P+PJ<$S<$SJ −→P<$Sifσ（in（λ，x），SJ）[LG-IN]这些规则直接将第2节中的规则[L-OUT]、[L-RD]和[L-IN]推广到LOG OP的情况，分别插入、读取和用-绘制通过关系σ得到的元组集。例如，LOG OP配置的有效转换包括以下内容：out （ id1id2id3 ， x ） −→id1 ， xid3 ， xrd（ id1id2id3 ， x ） id1 ， x− →id1 ， xin（id1id2，x）id1，xid2，x−→0注意，逻辑公式λ的语义仅由关系y给出σ。 因此，由于π（i∈{i0}i，x），π（i∈{i0}i，x）和π（i∈{i0}i，x）是-由σ关联到相同的项目i0，x，那么我们自然地表示它们的三个λ的简写为i0。 涉及这种λ的运算称为单空间操作，这可以很容易地显示为具有与第2节中描述的LINDA协调模型相同的语义。其他操作在这里称为多空间。R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-107S4.2弱同步语义显然，强同步在分布式系统中是一个不切实际的假设，它需要由事务机制支持的实现— 这很难满足当今分布式系统所要求的开放性、动态性和解耦 的替代语义模型LOG OP可以被定义为满足非正式规范，但在该约束被释放。具体地，原语的执行可以被建模为系统中的事件序列，每个事件对应于单空间LINDA操作。因此，虽然调用多空间操作的实体仍然将其执行视为原子，但系统的其他实体实际上可能会感知到整个多空间分布式系统的不一致的部分配置。这相当于我们所说的LOG OP的弱同步语义。由于这个新模型仍然满足LOG OP的非正式规范-实际上只考虑执行原语的单个进程的观点-LOG OP所期望的优点可以通过符合这种语义的实现来保持，这实际上更容易实现。为了定义这个新的形式模型，使其易于与强同步相比较，我们将其定义为从LOG OP配置到LOG OP配置的翻译形式，即从S到S的函数。非正式地，该函数将执行多空间操作的进程这些序列中的每一个的最终效果与相应的多空间操作所期望的相同，然而，一个这样的序列的任何实例都不是原子的，并且可以被一些其他协调实体交互W. I. 相同的元组。 在最高一级，这种编码被定义为函数。. . ：S ›→ S定义为：. .... 0的情况。0，..尼加拉瓜.... ... S.. i，x.S.. .. .... SSJ.. S..J..J.. .. ..J....S. - 是的S.、S S. α; P +P。S.α。O;。P.S+。P.S此函数保持配置的结构不变，但将其转换为108R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-.π.SS..ΣS. .通过编码将操作α转化为进程P。. .归纳定义为：... π（π，x）。0 [W-空].. π（ i∈I.i，x）。-是的i∈I.π（i，x）;.（iJ∈I\{ i}. ΣiJ，x）。O[W-和].. π（.i，x）。Σπ（i，x）[W-XOR]i∈I.Oi∈I.....ΣJ.. π（ i∈Ii，x）。. π（i∈Ii，x）。+i∈Iπ（i，x）;. π（ iJ∈IJ\{i}i，x）。O[W-OR]第一个规则处理逻辑表达式涉及零元组空间的情况-用符号表示-，在这种情况下我们得到空过程。运算符E1被定义为在集合I中的任何元组空间上的执行之间进行非确定性选择，然后递归地继续执行相应的剩余元组空间。运算符I被定义为非确定性地选择集合I中的一个元组空间用于原语执行。最后，定义运算符R1，以便在集合I中的任何元组空间上的执行之间进行非确定性选择;之后，该过程可以终止（左选择）或继续递归地在剩余的元组空间上执行操作（右选择）。例如，我们有以下映射：... （i1，i2，x）.=out（i1，x）;out（i2，x）+out（i2，x）;out（i1，x）... 在（i1<$i2，x）中。=in（i1，x）+in（i2，x）... rd（i1<$i2，x）.=rd（i1，x）+rd（i1，x）;rd（i2，x）+rd（i2，x）+rd（i2，x）;rd（i1，x）现在，弱同步语义可以用手段来描述。的. 一辆卡车。西蒂。对关系−→w<$S×S，定义为使得S−→wSJ保持i <$。S.−→。J. .也就是说，一个配置首先被翻译成具有单空间的版本OOOOOOOOR. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-109操作，然后由关系−→因此简单地应用。 它是。S. 自然要考虑等价关系编码引起的S翻转。. . ，这就是说，一个定义，使SSj. .. .S. S.S.SJ。S. 我们得到了下列由α诱导的联想的例子，=110R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-这为弱同步语义学提供了一个新的视角。out（i1i2i3，x）out（i1，x）;out（i2i3，x）+out（i2，x）;out（i1i3，x）+（i，x）;（i，x）in（i1<$i2<$i3，x）in（i1，x）+in（i2，x）+in（i3，x）rd（i1<$i2<$i3，x）<$rd（i1，x）+rd（i1，x）;rd（i2<$i3，x）+rd（i2，x）+rd（i2，x）;rd（i1<$i3，x）+rd（i3，x）+rd（i3，x）;rd（i1<$i2，x）粗略地说，示例的左侧对应于一些多空间原语调用（被执行实体视为原子的），而右侧表示可能被另一系统实体感知的4.3比较备注LOG OP的两种形式化模型之间的基本语义差异在于，弱同步语义比强同步语义允许更多的系统配置演化弱同步所允许的演化和强同步所阻止的演化包括由协调原语的执行所引起的元组空间的部分演化。考虑系统SE的情况，其中两个等价的协调实体希望首先通过（AND（i1，i2），x）中的原语从元组空间i 1和i 2消费元组x，然后在元组空间i3中产生元组x。这由以下配置表示：SE=in（i1<$i2，x）;out（i3，x）<$in（i1<$i2，x）;out（i3，x）<$<$i1，x<$$><$i2，x<$在强同步模型中，两个进程中的一个可以从i1和i2消耗x，在i3中产生x，然后终止，另一个进程保持阻塞。唯一允许的进化是：SE−→out（i3，x）in（i1i2，x）;out（i3，x）−→in（i1i2，x）;out（i3，x）i3，x相反，在弱同步的情况下，系统SE还可以包括不同的演化：两个进程可以并发地执行它们的原语，其中空间i1中的元组x被一个进程消耗，并且空间i 1中的元组x被一个进程消耗。R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-111Si2被另一个消耗SE−→win（i2，x）;out（i3，x）.Σin（i1，x）;in（i2，x）+in（i2，x）;in（i1，x）;out（i3，x）i2，x−→win（i2，x）;out（i3，x）−in（i1，x）;out（i3，x）结果，两个进程都保持阻塞状态，没有在i3中插入x-一个等待x在空间i2中再次出现，另一个在空间i1中-直到另一个进程进来并在空间i1或i2中插入元组x。通知这个例子在概念上类似于用餐哲学家[13]的典型情况，其中客户端需要对不同的分布式资源的互斥访问。当然，从代数的角度进一步深化这两种语义之间的技术差异是很有趣的，但这里不研究这一点，因为它超出了本文的范围然而，在[24]中发展了这个方向的一个步骤，其中研究了协调模型和协调介质的顺应性问题。根据这一概念，协调模型Y=<$Y0，Y1→ Y2被称为符合模型X=<$X0，X1→ X2，如果X能够让M。联合Y的一个ny转变。 M或Especifcally，there. sh.乌尔德河Xis.不一个编码.. ∈ Y <$→。X. 这样：（i）从y1→ y2，我们有。y1. →。y2.（ii）y ∈ Y0蕴涵. y. ∈ X0-其中X0和Y0用于表示成功状态集（通常为空配置）。值得注意的是，根据这个定义，强同步模型可以被证明符合weak-syncronyone，后者。B. 一个晚上都能睡前者的过渡，利用映射。. . 介绍了在以前科.另一个相关的工作是在[2]中开发的，其中评估了应用于并发语言的trans-mapping机制的表达性在它们的设置中，事务被建模为原子执行的原语序列，建模语言的特征，如Polis [11]和Shared Pro- log [1]。他们通过利用模块化嵌入的框架[12]获得的主要结果是，具有事务的语言比没有事务的语言更具表达力这基本上符合我们对强同步和弱同步之间的差异的观察：强同步语义允许强制特定的交互序列发生，而弱同步不能阻止其他协调实体的干扰然而，为了进一步深化与[2]中方法的比较，在选择算子存在的情况下研究模块嵌入也是至关重要的，这实际上显著增强了协调语言的表达能力。112R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-因此，一般来说，强同步保证了系统级多空间操作的原子性。 这种方法保证了更多的属性 协调系统，但几乎不适合开放和分布式系统的要求，在这些系统中，它需要与细粒度通信操作相关的昂贵的事务机制。另一方面，弱同步对协调基础设施提出了较低的要求，但可能会失去一些有趣的属性。例如，在上面的示例中，系统以死锁的情况结束，其中两个进程都被阻塞，等待元组的插入。然而，我们注意到，这些问题似乎是开放的，分布式系统的上下文中，例如，opti-可扩展的方法通常被用来从死锁情况下恢复的限制尽管如此，弱同步语义的LOG OP地址的表达限制的LINDA协调语言，通过允许多空间操作被视为原子在协调实体5LogOp服务的语义到目前为止，所描述的形式语义支持了LOGOP协调模型的观点，该协调模型由协调原语的语法和操作语义定义，用于表达并发系统的交互部分。如[25]所述，这种观点-称为协调作为一种语言-特别适合于以概念清晰和方便的方式分析协调模型的抽象属性，正如我们在这个LOGOP案例研究中所展示的那样。然而，就将协调模型部署到实际场景而言--最明显的是，在设计支持该模型的基础设施时--这种观点可能不是最合适的，因为它抽象了许多相关的运行时问题。这些包括协调过程中涉及的抽象的实际形状，最值得注意的是协调媒体，以及这些抽象之间发生的单个交互行为的动态。中引入了另一种称为协调即服务的观点，[25]为解决这一问题。在该框架中，协调系统被解释为被建模为被划分为协调空间、交互空间和协调空间，在协调空间中，服从协调的实体（即过程）存在，在交互空间中，通信事件发生以反映协调的动态，在协调空间中，协调介质（例如元组空间）存在并交互以提供协调服务。特别是，而不是考虑一个协调模型作为一种语言与协调原语，这个新的框架视图协调作为一个交互式服务提供的一些协调媒体。 通过关注协调媒体的互动行为，R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-113LogOpTSTSFig. 1. LOG OP基础设施模式框架考虑模型的关键运行时问题，从而评估其作为基础设施的可实现性，并勾勒出其实际实现的设计。如[24]中提出的方法学方法所示，这种规范旨在为实施者提供参考，提供必要的信息来检查实际实施是否符合原始模型。在本节中，我们将展示如何将Log O p协调模型的弱同步语义转化为LOGOP协调服务的规范，由充当协调实体前端并实现LOGOP服务核心部分的介质提供。5.1LOG OP服务我们在这里的总体目标是提供一个设计的LOG OP服务的基础设施之上，标准的LINDA元组空间（TS）的存在，符合第2节中描述的语义。因此，我们引入了一个协调介质实现所需的LOG OP语义的进一步管理。具体来说，这个抽象负责（i）接受执行L OG O P操作的请求，（ii）处理和管理与系统中元组空间的交互，以及最终（iii）向请求实体提供正确的回复。图1中报告了所得到的基础设施的图形表示。一般来说，不对基础设施实际上实现了多少个LOG O P协调介质并用于提供协调服务做出假设：可能的和合理的场景包括每个节点一个LOG O P协调介质，或者每个协作一个Log O p协调介质。CTS114R. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-协调实体，或者甚至是为每个LOGOP协调原语调用而在服务器上创建的实体。为了简单起见，在下文中，我们的形式主义是指单个LOG OP配位介质的情况：扩展到多个LOG OP配位介质是直接的，并且只需要稍微复杂的符号。在下文中，我们让：• 元变量f↑在由LOG OP介质发送到元组空间的请求集合F↑上的范围，这些请求属于n²β-类型，其中n是名称LOGOP介质本地进程的函数，称为handler，负责处理应答，β是要执行的单空原语操作• 元变量f↓，范围覆盖从元组空间发送到LOG OP介质的回复集合F↓，其属于类型nfok-其中n是处理程序• - 元变量e↑，其范围在LOG OP请求的集合E↑上，其属于id↑α类型，其中id是请求协调实体的标识符(C)α是多空间本原运算;• 元变量e↓在LOG OP回复的集合E↓上的范围，这些回复属于id↓ok类型。我们假设协调实体的标识符集合与处理程序的名称集合是不相交的，所以上面的四个集合都是不相交的。5.2表示元组空间我们首先定义一个林达元组空间协调介质符合第2节所示的规范。在[24]中的工作之后，LINDA元组空间很容易由转换系统TS，−→TS，ActTS，其中元素tsTS∈TS定义如下：TS：：= 0 |f↑|f↓|X|（TS TS）因此，LINDA元组空间的配置被视为元组、待处理的请求（f↑）和待发送的应答（f↓）的组合。动作集被定义为ActTS={τ}<$F↑ <$F ↓，表示内部静默动作、接收请求和生成回复。过渡关系是由规则定义：4这里只考虑肯定的回答，因为我们不研究可能失败的原语inp和rdpR. Menezes et al. / Electronic Notes in Theoretical Computer Science 97（2004）97-115TSTSTSf↑TS−→TS TSf↑[TS-]TSff↓−→TSTS[TS-REP]n²out（x）<$TS−→τ TS<$x[TS-<$T]n²rd（x）<$TS<$x−→τ TS<$x<$nfok[TS-RD]n²in（x）<$TS<$x−→τ TS<$nfok[TS-IN]这些规则直观地对应于第2节中所示的语义。事实上，前两个规则简单地处理
