分布式和并发事务协调的真正并发方法

理论计算机科学电子笔记238（2010）63-79www.elsevier.com/locate/entcs交易第二章：将隐含的情景明确化*Sotiris Moschoyiannis1 阿米尔·拉扎维 保罗·克劳斯3英国萨里大学计算机系，吉尔福德，萨里，GU2 7XH，英国摘要我们描述了一个真正的并发方法来管理长期运行的事务的分布式和并发协调器组件之间的依赖关系。在之前的工作中，我们已经描述了如何将场景中指定的交互转换为基于元组的行为描述，即向量语言。在本文中，我们将展示如何推理对这些语言的顺序理论属性可以揭示失踪的行为，没有明确描述的情况下，但仍然是可能的。我们的方法支持将交互场景逐步细化为一套完整的行为，包括所有理想的执行顺序，并禁止交易的紧急行为关键词：事务，交互，依赖，并发，UML 2.0序列图，向量语义1介绍互联网的采用和交互式计算的新兴范例已经培育了一种环境，在这种环境中，许多分布式服务可以通过不同的组件获得。这增加了对联网组织之间的业务活动和工作流程自动化的需求，并且越来越多地关注与涉及多个合作伙伴的业务活动相对应的长期运行的事务在这种情况下，事务的具体化通常包括许多活动，这些活动依赖于来自不同提供者的不同组件的多个底层服务的执行，其中一些可能需要几分钟或几小时甚至几天才能完成-因此长期运行事务。这需要这项工作得到了欧盟项目OPAALS的支持，合同FP 6 -034824。1电邮地址：s.moschoyiannis@ surrey.ac.uk2电子邮件：a. surrey.ac.uk3电子邮件：p. surrey.ac.uk1571-0661皇冠版权所有© 2010由Elsevier B. V.出版，CC BY-NC-ND许可证下开放访问。doi：10.1016/j.entcs.2010.06.00564S. Moschoyiannis等人理论计算机科学电子笔记238（2010）63参与组件和底层服务执行的编排以及补偿机制的提供，在故障（网络/平台断开或延迟，服务不可用）的情况下，在本文中，我们将不关注恢复管理-初步想法可以在[13]中找到。在本文中，我们将关注管理事务中并发组件和分布式组件的服务之间出现的依赖关系，旨在全面了解服务调用序列应表现出的行为模式，以增加成功结果的信心。由于在服务调用时需要进行排序（例如，只有在预订机票后才能预订酒店）或由于数据共享（一个服务使用另一个服务的结果），可能会存在重复性。当前针对Web服务的事务模型，如业务事务协议（BTP）[4]和Web服务事务（WS-Tx）[2]，没有考虑用于协调事务执行中涉及的服务的正式模型。这使得根除紧急行为变得困难，也就是说，非故意的干扰，而是由相互作用本身的复杂相互作用引起的，例如竞争条件。 由于这个原因，BTP和WS-Tx似乎都面向集中控制（使用WS-Coordination [2]，需要底层服务的紧耦合，这违背了面向服务计算（SOC）的基本前提[11]，以及参与组件的内部构建的一些知识，这违反了参与者平台的本地自治性在以前的工作[8，9]中，我们描述了一个真正的并发模型，基于向量语言[16]，用于捕获组件的交互行为，并展示了如何从描述交互场景的UML 2.0序列图中直接获得这种行为描述。在本文中，我们使用序列图来描述在一个事务中涉及的各种协调器组件之间的服务交互，并将它们转换成基于向量的行为描述的形式语言我们描述了如何推理对向量语言的顺序理论属性这些在最初的设计规范中根本没有考虑到，或者表明了紧急行为，例如，由于交互中并发性和非确定性之间的微妙相互作用。我们的方法被有效地用于将初始的交互场景细化为更全面的场景，这些场景被逐渐细化以排除紧急行为，并包括所有理想的执行顺序本文件的结构如下。在第2节中，我们将描述如何对事务进行建模，重点是它们的结构和交互。在第3节中，我们提出了一个正式的语言，用于描述协调器组件之间的交互事务。在第4节中，我们展示了如何使用形式语言来推理不同协调器组件的服务之间的依赖关系，并揭示初始序列图中隐含的执行场景。本文S. Moschoyiannis等人理论计算机科学电子笔记238（2010）6365在第5节中提出了一些结论性意见和对未来工作的想法。2对长时间运行的事务在本节中，我们简要描述了事务的结构，然后展示了如何使用UML2.0 [10]对参与者的协调器组件之间的服务交互进行我们已经看到，长时间运行的事务涉及多个服务提供者之间的交互，需要对这些交互进行编排，以便在部署之前提高所需的编排需要以尊重底层服务的松耦合的方式执行- SOA的基本前提[11]。为此，每个联网组织（服务提供者/消费者）通过协调器组件提供其服务，并且还请求其他组织的服务，该协调器组件管理不同平台之间的通信和相应服务的部署。在不深入太多细节的情况下，它可以在其本地服务存储库中部署（在接收到调用时）服务，并且可以在给定事务内调用它需要的来自其他组件的服务，这些组件的服务描述（例如，在WSDL中）在其全局服务存储库中列出。协调器组件的结构如图所示。1.一、Fig. 1.事务中的协调器组件在早期的工作[14]中，我们描述了一个多服务事务分布式协调的事务模型。这是基于日志结构，以有向图的形式给出，它允许每个平台的协调器组件只需要知道自己的服务及其对其他组件服务的依赖关系-事实上，它只需要知道在由于篇幅限制，我们省略了更多细节。在我们的方法中，事务由一个树结构表示，该树结构捕获嵌套的子事务，并举例说明所涉及的服务需要一致执行借鉴最新的工作，66S. Moschoyiannis等人理论计算机科学电子笔记238（2010）63作为业务环境的扩展的面向服务的体系结构[11]，我们考虑了五种不同的组合类型或组合器，它们允许我们模型中的各种服务交互模式。顺序：服务的执行依赖于前一个服务;此合成器处理顺序提交依赖（SCD）和顺序数据依赖（SDD）面向流程的服务合成。并行：服务是并发执行的; composer处理面向流程的服务组合，包括有提交依赖的并行（PCD）、有数据依赖的并行（PDD）和无依赖的并行（PND）。顺序选择：服务将被连续尝试，直到产生所需的结果，如某些标准所指定的（例如，成本）。并行替代：替代服务并行执行，一旦服务产生所需的结果，其余的服务将被中止。面向数据：这个合成器处理面向数据的服务合成，并处理事务内外的发布数据项委托：此组合器允许将（部分）事务委托给另一个平台，例如以克服瓶颈或低带宽连接。关于我们模型中考虑的组成类型的更多细节可以在[14]中找到。使用Netbeans 6生成事务上下文的XML描述的模式，由相应事务树中使用的合成器指定，如图所示。二、图二、用于描述事务上下文的XML模式在本文中，我们将关注的顺序，并行和顺序交替组成类型。图3示出了具有四个基本服务的事务树-具有协调器组件CC1的本地平台的a1和a2、CC2的b1和CC3的c1-其执行顺序由相应的S. Moschoyiannis等人理论计算机科学电子笔记238（2010）6367组合类型。例如，树指定服务调用a2和c1是顺序编写器的子级，因此c1只能发生在a2之后。这个composer上的连接线表示相应服务部署之间的数据依赖关系。示例事务树的相应XML描述来自图2的模式，可以在下面的[1]中找到。图3中描述的场景出现在[14]中，在这里被简化了一些，但仍然足够复杂来说明关键思想。事务树所隐含的服务交互可以使用UML序列图进行建模。图4显示了事务的三个协调器组件以及在我们的示例中事务图3.第三章。树结构中的简单事务cc1cc2cc3的1altB1一个2C1B1图四、简单事务的行为场景可以看出，由相应的UML序列图给出的行为场景决定了参与组件的服务的执行顺序在本文的其余部分，我们将关注一种形式化的推理方法，旨在识别交易上下文的初始基于规范的规范中的缺失行为（如果有的话）我们将看到，缺失的行为可能表明紧急行为（例如，由于竞争条件）或在初始设计规范中根本没有想到的执行场景。首先，我们需要更正式地描述事务，以便彻底理解底层服务调用应该展示的行为模式68S. Moschoyiannis等人理论计算机科学电子笔记238（2010）633用于交易的在本节中，我们将介绍一种用于长时间运行事务的形式化语言，该语言捕获所涉及的各种协调器组件的服务执行之间的依赖关系，并启用关于交互的形式化推理以揭示隐藏的场景。在事务环境中，存在高度的并发性，因为实际问题需要并行地进行许多活动。因此，我们将在[16]中找到并行行为的非交织表示的一般理论，这在下文中非常有用语义的目的是在部署级别上根据事务的服务来描述事务的行为，而不是由服务本身执行的低级计算。事实上，在某些情况下，例如商业服务的数字生态系统由不同的服务提供商提供，重要的是我们要推迟干扰服务执行的本地状态。这意味着认为交易模型中的任何行为都没有显著的持续时间是合适的，从这个意义上说，（i）它要么作为一个整体发生，要么根本不发生(ii)它要么完全在其他行动之前发生，要么完全在其他行动之后发生，要么完全与其他行动同时发生。如第2节所述，交易涉及代表不同方（服务提供商、消费者或两者）的多个本地代理，这些代理合作执行业务活动。为了保持每个平台的本地自主性，它们通过协调器组件进行通信，协调器组件管理所需的服务交互（请回忆图1）。第3和第4段）。事务T与一组协调器组件C和一组动作M相关联。我们感兴趣的是协调器组件上的可观察事件，因此可以将操作理解为参与组件之间的服务调用，如图1的场景所示四、因此，每个组件在C中，它与一组操作相关联，这些操作对应于部署（它自己的）或请求（我们用μ（i）表示这个集合，对于每个i∈C，其中μ是由μ：C→M给出。进一步，我们要求i∈Cμ（i）<$M。如图3所示，事务具有多个激活或访问点，即参与交互的协调器组件的接口因此，而不是建模的行为，一个事务的顺序过程，这将产生一个单一的接入点的痕迹，我们认为，伯这样的序列，一个组件，在同一时间。这借鉴了Shields向量。事务向量。假设T是一个交易。 我们定义VT为所有函数v：C→M的集合，使得v（i）∈μ（i）<$。我们用μ（i）表示mu（i）上的有限序列集。在数学上，集合VT是集合μ（i）的笛卡尔积，对于每个i。实际上，是n元组其中每个坐标对应于事务中的坐标组件（因此，n是组件的数量），并且包含在该组件上发生的动作的有限序列。S. Moschoyiannis等人理论计算机科学电子笔记238（2010）6369当事务中发生操作时，也就是说，当在协调器组件上调用服务时，它将出现在新的事务向量上的适当坐标处。例如，向量（a1， Λ， Λ）描述了事务的行为的一部分，其中动作a1（例如，服务调用）已经在分配给第一坐标的对应组件上发生。向量（a1，b 1， Λ）描述了a1和b1都发生在相应分量上的行为部分，而向量（a1a 2，b 1， Λ）描述了在对应于第一坐标的分量上发生a1和a 2，以及在第二坐标上发生b1-在对应于第三坐标的分量上没有发生任何事情从上面给出的示例可以看出，在特定接入点或组件上的动作之间已经存在排序，例如，1后跟 2。这种基于向量的事务行为描述还可以捕获不同组件上的服务调用之间的顺序，这相当于出现在不同向量坐标上的动作。然而，这需要更仔细地考虑这些向量的数学性质，这将在下文中描述。在这个阶段，需要理解每个事务向量提供行为快照，捕获已经发生的操作，交易的哪一部分（组成部分）。然而，在描述事务的行为时，我们只对那些描述我们期望协调器组件在事务执行过程中参与的动作（的顺序）的向量感兴趣。换句话说，对于给定的事务T，我们感兴趣的是在T上形成的所有可能向量的特定子集。我们将使用术语事务语言来指代适当的子集在给定的事务T上形成的所有可能向量VT中的V。 其思想是，对于特定的事务，事务向量的特定子集表示相应服务编排中所需的排序约束。为了识别只捕获预期行为的向量的适当子集，我们将注意力转向描述服务交互所需序列的相应UML模型。我们在第4节中概述了UML 2.0序列图[10]如何被转换为事务向量，并展示了如何使用针对事务语言的序理论属性的形式化推理（下面给出）来确定事务的完整行为集，并通知初始UML模型的细化。3.1transaction vectors现在我们来考察一下到目前为止我们的形式构造的基本数学性质。讨论仅限于本文其余部分中使用的那些操作。详细的数学处理可以在[7，16]中找到我们首先引入一种特定的事务向量，它在我们的模型中用于描述动作（例如，服务调用）。列向量。设T是一个事务，VT是它的事务向量集70S. Moschoyiannis等人理论计算机科学电子笔记238（2010）63我们定义AT={α∈VT\ {ΛT}：i∈C = ε|α（i）|≤1}其中|X|表示序列的长度|X|.因此，列向量本身就是事务向量，但有一个额外的约束，即它们的每个坐标要么是空序列，要么是单个操作。例如，向量（a1， Λ， Λ）表示与第一个坐标相关联的分量上的动作a1我们已经看到，事务向量本质上是序列的元组。这可以在定义向量上的运算时利用众所周知的序列运算。向量运算。 对于u，v∈VT，我们定义，• 联合v是唯一向量w，使得w（i）= u（i）。v（i），对于每个i∈C（concate-nation）• u≤vi <$u（i）≤v（i），对于每个i∈C（前缀序）• uHv是满足w（i）=min（u（i），v（i））的向量w，对于每个i• uHv（如果存在）是满足w（i）=max（u（i），v（i））的向量w• 如果u≤v，则我们定义v/u为唯一元素z∈ VT，使得u。z= v（右-取消）因此，向量上的连接操作是根据出现在它们各自坐标上的序列的连接来定义的。例如，（a 1，b 1，Λ）。（a2， Λ， Λ）=（a1 a2， b1， Λ）.向量之间的排序是根据对出现在其各自坐标上的序列的通常前缀排序操作来定义的。例如，（a1，b 1， Λ）≤（a1a 2，b 1， Λ），因为a1≤a 1a 2且b1≤b 1且Λ≤Λ。换句话说，第二个向量在第一个坐标上“获胜”（因为它在这个坐标上有一个更长的序列），而两个向量在所有其他坐标上“绘制”。不难看出，有些向量是无法比拟的。 事实证明 这些向量描述所讨论的事务的并行或替代行为，这将在以下部分中进一步讨论运算正如我们将看到的，这些操作是我们方法中处理并发性的核心。右消去算子“/”表示，如果u是一个交易向量，描述了 这个手术是治疗的关键我们的方法中的补偿。我们将在本文的结论部分回到这一讨论。重要的是要强调，所有对向量的操作都是以坐标方式执行的，这简化了证明，但也使形式模型易于实现。现在我们将展示如何使用事务向量来捕获事务中协调器组件的服务交互之间的依赖关系。S. Moschoyiannis等人理论计算机科学电子笔记238（2010）63713.2管理依赖关系事务向量上的前缀排序关系可以被看作是部分执行的排序，其中每个向量对应于事务已经参与其坐标上出现的动作的行为部分。这可以更简洁地表达为u≤v意味着u是导致v的行为的早期部分。对数学结构的更仔细的考察表明，我们可以说的不止这些。事实上，我们发现确定事务向量的直接前导（或后继）是有用的封面设u，v∈V <$VT.我们说v在V中覆盖u，我们把u写成vi(i)（ii）若z∈V使得u≤z≤v，则z=u<$z=v.因此，当u≤v时，我们也有uav，那么最后一个动作形成每一个向量都是连续发生的一个接一个。这允许对事务内部的顺序依赖性进行建模。回顾图的例子。其中服务c1只能在a2之后被调用我们对并发动作（可以并行发生的动作）建模的方法借鉴了Shields向量语言[ 15 ]和Mazurkiewicz跟踪语言[ 6 ]中的概念因此，在我们的事务的正式模型中的并发处理采用了非交错的并发模型，它将额外的结构引入到正式语言中，以描述非顺序行为。额外的利用[16]中独立关系i到行为向量的扩展，Mazurkiewicz迹中动作之间的独立性概念可以很容易地解释为我们的方法中的事务向量。独立对于u，v∈V <$VT，我们定义uindv<$$>i∈C：u（i）>Λ<$ v（i）= Λ这个定义是说，如果两个事务向量描述的对象涉及事务的不同组件（对应于不同协调器组件上的服务调用），则这两个事务向量是独立的。这意味着由u和v描述的行为可以独立地发生。在列向量的情况下，独立性捕获这样的事实，即在一个向量中出现的动作可以独立于在另一个向量中出现的动作而发生。此外，如果表示这些操作的向量在一个表达式中相邻（形成相应事务向量的一系列串联的表达式），则这些操作是并发的。因此，只要两个动作是独立的并且都被启用（都可以在某个点发生，在某个行为之后），那么它们对应的列向量就会交换，即α1。α2 = α2。α1，并且在结果行为中，两个动作是并发的。基于集合V中事务向量之间的前缀排序，我们可以72S. Moschoyiannis等人理论计算机科学电子笔记238（2010）63也可以在行动之间做出选择。也就是说，一个动作的发生排除了另一个动作的发生在讨论长时间运行的事务中的并发操作时，我们看到两个不可比的事务向量表示并行行为。它们覆盖的向量实际上是它们的最大下界，并且是通过应用前面给出的运算“H”获得的这两个不可比向量表示并发操作的事实只是因为它们在集合中有界（由事务向量限定，事务向量是它们的最小上界，由' H '给出只要后一个要求不成立，我们就可以谈论冲突中的事件用图像和相关的哈塞图来区分可能是有益的 在图5的图中，a1和d1是顺序的（d1仅可以在图5（i）中的1）之后调用，它们在图5（ii）中是并发的，而在图5（ii）中它们之间存在选择（替代）。5（三）。(a1，d1）（a1，d1）（a1，a2）（a1，a2）（第1天）（a1，a2）（第1天）（，）（一）（，）（二）（，）（三）其他事项图五、事务处理语言的顺序结构注意，（i）中的向量集合不包括（Λ，dl），这意味着dl从不在a1之前出现;在（iii）中，它不包括（a1，dl），这意味着不存在交易处理系统的有效行为，其中a1和a2都在a1之前出现。d1已经发生;在（ii）中，它包括所有四个向量，这意味着单独的a1，单独的d1，以及a1，d1一起，都是对其中a1和d1同时发生的事务的行为的有效观察。这是由熟悉的菱形形状表示的，它显示了相应的有序结构，表现出有限晶格的特征结构在进一步的解释中，位于菱形底部的向量是位于菱形中间的两个不可比向量（a1，A）和（A，d 1）中的最大下限菱形作为一个整体描述了交易行为的那一部分其中a1和d1同时发生关于如何订购的更多细节动作之间的关系表现在向量的结果集的顺序结构中，可以在[7]中找到3.3行为描述在描述事务的行为时，我们感兴趣的是其各个组件上的动作（activations）。这些在我们的模型中使用列向量捕获。因此，我们不考虑所有可能的事务向量，而是只考虑通过与列向量的连接获得的事务向量。这给出了事务在其协调器组件的操作方面的行为，并可用于强制基础服务的协调S. Moschoyiannis等人理论计算机科学电子笔记238（2010）6373我们已经看到，事务向量是通过坐标关联获得的。因此，可以看到它们是从空向量开始，通过一系列与表示动作的列向量的连接建立起来的。[16，9]中对向量语言的研究表明，为了确保所考虑的向量仅是与列向量连接的结果，事务向量集必须满足某些性质。我们接下来介绍这些属性第一个属性捕获了这样一个事实，即系统的计算总是具有 一个起点，并确保只有有限数量的行动可能发生在有限的时间。如果两个向量描述的行为比第三个向量更早，也在集合中，那么它们的最小上界和最大下界也在集合中这在下面的定义中被正式提出离散性。 设VT V，无论何时u，v，w∈V使得u，v≤w则（i）uHv∈V和（ii）uHv∈V.注意，uHv被理解为断言离散性强加了一个有限性约束，在这个意义上，它排除了关于时间顺序的无限上升或下降的行动链。事实上，它确保了像那些导致泽诺类型悖论的情况永远不会出现。我们进一步要求，每一个动作的发生（例如，服务调用）被记录在与事务相关联的向量集中。这保证了行为的任何早期部分本身就是一种行为，并激发了以下定义。局部左闭合设V<$VT，i∈C，x∈μ（i）<$.则V是局部左闭的i ∈ V，当v∈V且Λ

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