提交连接编程：理论、实现和应用

理论计算机科学电子笔记104（2004）39-59www.elsevier.com/locate/entcsFlat Committed Join Join1布鲁尼，她的生日和你的生日I-5612 7 Pisa，I tally，I- 56127Pisa，I-{bruni，melgratt，ugo}@ di.unipi.it摘要CommittedJoin（cJoin）是Join的一个扩展，它具有高级原语，用于编程带补偿的动态嵌套协商。在本文中，我们表明，在cJoin进程（即没有子谈判的进程）可以编码在普通的加入演算利用分布式两阶段提交协议。特别地，我们首先定义了一个类型系统，该类型系统挑选出了cJoin进程并证明了它的主题归约。然后，我们证明了所有cJoin进程都可以用一个等价的规范形式来写，其中使用了一些基本的定义模式。最后，我们表明，规范的可扩展进程可以在Join中实现。值得注意的是，协商原语被编码为所有参与者之间的完全分布式协议，从而避免了集中式协调器。关键词：提交连接，连接演算，分布式协商，零安全网，演示。1介绍最近，在形式语言领域，学术界和工业界的研究都对设计用于编程大部分分布式和长期运行的决策过程的管弦乐队原语重新产生了兴趣[3，8，2，13]。在电子商务、Web服务编排和编排模式领域，越来越多的应用程序需要对这些语言进行严格的数学表示，以支持形式化的分析和验证。1 由 MSR Cambridge ProjectNAPI 、 FET-GC Project IST-2001-32747AGILE 、 MIURProjectCOFIN2001013518COMETA 和 MURST-CNR1999Project ， SoftwareArchitectures on Cooperative WAN支持的研究。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.09.02140R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-CommittedJoin（cJoin）[5]是Join演算的扩展，用于处理分布式协商（也称为契约）。粗略地说，协商是在受控环境中执行的过程，直到完成，当它们提交并使其结果对系统的其余部分可观察时。此外，它们可以被显式地中止，在这种情况下，可以激活合适的补偿程序以恢复局部一致的状态。cJoin的一个显著特点是，在执行过程中，可以将多个协商合并为一个更大的协商。当两个或多个谈判参与者通过称为合并名称的特殊端口进行通信时，就会发生这种情况。交互式协商是绑定在一起的，因此它们将共同达成相同的决定，即如果其中一个最终提交（相应地）。中止）所有最终将提交（相应地，中止）。这对于设计多方协商尤其重要，其中独立参与者可以提供事务服务，从而明确各方可以交互的方式，并且在运行时发现协商的实际结构。cJoin的方法与[3]等方法形成对比，在[ 3]中，业务流程被描述为跨组织边界生成的图，要求所有参与者都是静态已知的。此外，合作伙伴不能隐藏与第三方的互动，这可能会影响最终决定。关于cJoin实现的关键点是：（1）作为全局决策的交互式协商的提交，以及（2）参与者的数量及其身份不是静态已知的。我们表明，对于cJoin的一个重要片段，全局决策可以在一个完整的通过使用[4]中提出的用于实现零安全网[6]（Petri网的事务扩展）的分布式两阶段提交协议（D2PC请注意，在零安全网的情况下，为D2PC编写的Join代码可以导入并在cJoin编码中进行微小修改后重用，从而证明其通用性。cJoin比零安全网更具表现力，因为它保留了普通Join的全部表现力。补偿和合并名称的存在增加了编码的复杂程度，使其远非微不足道。实际上，我们只考虑可以被类型化为cJoin at的cJoin进程，这意味着它们永远不会生成嵌套协商。我们证明了cjoin的subject reduction property，从而证明了cJoin的subject reduction process形成了cJoin的一个子演算。此外，cJoin保证了可串行化的适当形式。我们证明了任何零安全网络的cJoin编码都是一个可重复的过程。为了便于翻译，我们定义了以合适的规范形式编写的可伸缩过程的编码，其中只有一些基本定义R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-41§§模式是允许的。这可以做到不失一般性，因为我们表明，任何一个可转换的过程可以在一个等价的过程中的规范形式。我们考虑的基本定义模式受到零安全网中转换的基本形状的启发：它们是通过对单个约简中可以消费/产生的消息数量施加严格限制而获得的。虽然我们表明，加入是表达足够的编码cjoin，即新的原语的cjoin谈判不增加语言的表达能力，我们认为，cJoin的语法产生的关注点分离，这是困难的，以实现在加入的水平，因此cJoin有利于编程和推理分布式合同。我们推测，通过进一步详细说明的编码的martinat进程应该能够实现完整的cJoin的加入。论文的结构。在第二章中，我们介绍了cJoin的语法和语义。在第3章中，我们定义了一个随机过程的类型系统，证明了主题归约，并证明了在[5]中提出的零安全网的编码产生了随机过程。此外，我们还证明了Rupat过程具有等价的正则表示-只使用基本定义模式的句子。 在§4中，我们提出了一个在cJoin进程中对规范的正则表达式进行正确和完整的分布式编码，加盟.2背景cJoin语法。 Join演算[10]是一种具有异步名称传递通信的进程描述语言（PDL），它具有与异步π演算相同的表达能力。CommittedJoin（cJoin）[5]是Join的一个保守扩展，它具有额外的高级原语，用于编程动态嵌套协商和补偿。像Join一样，cJoin依赖于名称x，y，.的无限集合，u，v，. 以模拟通信信道和传输值。 Nametuplesarewritte n →u. 图1中给出了cJoin的syn税。cJoin与Join的区别在于额外的运算符abort、[P：Q]和JP。消息M可以是惰性进程0、异步发射x→y→ p或x上的y，或M的并行组合M|N.进程P可以是普通消息，特殊常量abort导致其封闭协商的中止，协商[P：Q]，其中P是活动的正常执行，Q是在中止情况下的补偿，进程P的并行组合|Q，或者P中的进程定义D，其配备有由D定义的本地端口。定义D是普通反应规则和合并反应规则Jd P的合取42R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-M，N：：=0|xy→|M|ND，E：：=JdP|JP|D=P，Q=M|b或t|【P：Q】|P|Q|defDinPJ，K：：=xy→x|J|K图1. cJoin微积分dn（x∈y→n）={x} dn（J|K）=dn（J）<$dn（K）rn（x<$y→n）={y→}rn（J|K）=rn（J）<$rn（K）dno（DE）= dno（D）dno（E）dno（J d P）= dn（J）dno（JP）= dnm（DE）= dnm（D）dn m（E）dnm（J d P）=dn m（J P）= dn（J）fn（DE）fn（J P）= fn（J d P）= dn（J）（fn（P）\rn（J））fn（0）=fn（abort）=fn（xy→）={x}{y→}fn（P|Q）=fn（P）<$fn（Q）fn（defDinP）=（fn（P）<$fn（D））\dn（D）fn（[P：Q]）=fn（P）<$fn（Q）图2.被定义的，被接受的，自由的名字。m：：= P| D| CUP|{[S]}S：：= m| m，S图3. cJoin分子和溶液的制备和JP，它们将连接模式J与受保护进程相P. 由定义D在P中的定义D引入的名称被约束在整个进程P以及包含在D中的受保护进程。 定义名称dn、接收名称rn和自由名称fn的集合在图2中定义。特别地，我们区分了定义的普通名称dno（D）和定义的合并名称dnm（D），它们总是被假设为不相交的名称集合。cham.cJoin的操作语义以rexexiveCHAM风格[10]给出，其中状态（称为解）是项的有限多集（称为分子），计算是多集重写。多集被写为m1，.，m n.我们通常把m1，...，m n，其中mim i。解决方案可以通过使用操作员成员以层次化的方式构造。]}，将溶液分组为分子。变换由一组化学规则描述，可以分为两种：溶液中分子的结构重排的加热/冷却（或结构）规则，以及基本计算步骤的反应规则规则只处理解决方案中实际移动的部分，并且可以应用于层次结构中的任何级别。用于cJoin的分子m和溶液S在图3中。注意，过程和定义都是分子。此外，具有形式SQIQ的分子表示冻结在溶液中的补偿，除非它们的协商中止，否则不会执行。为了推理到结构等价，我们将重载→以也表示序列→。R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-431||≡ ⟨ ⟩ncJoin的操作语义。cJoin的化学规则如图4所示。第一个化学规则是连接的普通规则。规则STR-NULL规定可以在任何解决方案中添加或删除0 规则STR-JOIN和STR-AND代表结合性和交换性|和。 STR-DEF表示激活本地定义，它通过适当地用全局新名称重命名已定义的端口我们写的替代名称%s %x% 1. . . xnbyy1. . . yn为σ={y1. . yn/x.. . x}，其中m（σ）={x1， . . ，xn}并且range（σ）={y1， . . ，yn}。我们用σN表示一个内射子σ使得dom（σ）=N。我们要求新定义的名称必须是全局新鲜的，这意味着在应用规则的隐式上下文中是新鲜的。反应RED描述了将主动定义JdP应用于匹配模式J的消息Jσ（对于合适的替换σ，dom（σ）=rn（J））。J的实例被消耗并被新的实例Pσ替换，守护进程P.规则STR-1指出，表示合约的项对应于由两个分子组成的子解：过程P和它的补偿Q，它被冻结（因为操作者不确定）。禁止封闭的进程进行计算）。在提交时，在协商中产生的本地资源M通过规则提交释放，只有当所有内部计算完成时才能执行规则提交。在提交时，私有定义可以丢弃合约的名称，因为正在释放的消息既不包含这些名称，也不可能在之前挤出这些名称。在提交之后，其补偿过程是无用的，可以丢弃也 谈判的中止由规则ABORT处理，只要解中存在abort，就释放Q协商之间的交互通过merge来处理，merge消耗来自不同合约的消息，并通过将原始合约的定义和消息与保护过程Pσ的新实例相结合来创建更大的协商，其中dom（σ）= rn（J1. J n）。避免了名称冲突，因为我们假设STR-DEF生成全局新名称。联合谈判的补偿是所有原始补偿的平行合成。示例2.1邮件列表。考虑一个数据结构，它允许以原子方式将消息发送到一个订阅者列表（在这个意义上，它要么发送给所有订阅者，要么不发送给任何订阅者）。这种结构可以定义为MLMailingList k dMLDef，其中：MLDef def在k中列出add，tell，close|lnil44R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-NN⟨⟩STRING-NULL0字符串连接P|QP、QSTR-和DED，ESTR-DEfdefDinPDσdn（D），P σdn（D）（range（σdn（D））globallyfresh）红色J d P，Jσ→J d P，σ弦线【P：Q】{[P，Q]}提交{[M |def D in 0，Q]} → M中止|P，{Q} → QME RGEJ1|.... . . 你 好 。 . |Jn<$P，i{[Jiσ，Si，<$Qi]}→J1|.. . . . . 你 好 。 . |JnP，{[iSi，P σ，Q1|.... . . 你 好 。 . |Qn]}图4. cJoin的操作语义。Listnilv，ww∧ 洛伊奇|add x d defz v，w x v|y v，win l z阿利什基|tellvd [defzd 0 inyv，z|ly：ly]∧ 洛伊奇|关闭登录0通过向端口MailingList发送消息来创建新的邮件列表。由于cJoin遵循“continuation passing”的新列表的创建定义了五个新端口nil、l、add、tell和close：其中三个（即add、tell和close）将用于从“外部”与列表交互其余两个端口永远不会被挤出。它们表示空列表（nil）和列表的实际状态（l）。一旦创建了列表，就可以通过发送一个消息add来添加新的订阅者，该消息带有它将监听新消息的端口的名称x在这种情况下，通过安装z（在它的顶部）来修改列表，z是消息到x的转发器。端口tell用于向列表发送消息v。当接收到tell时，生成一个新的协商，由一个新的名称z标识，结构的状态被放入协商中，因此所有其他活动，如添加或关闭，都被阻止，直到协商结束。在协商中，消息v被发送到列表y顶部的转发器，并带有协商z的标识符。请注意，每个转发器都将消息发送到相应的订阅者和列表中的下一个转发器 这是重复的，直到达到零，当一个消息到标识符，的交易被发送。触发规则z d0消耗最后一个本地名称，合约通过释放所有发送给订阅者的消息和列表的状态来提交。然后，列表就可以为新的请求提供服务了。R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-45||Q►⟨ ⟩3平面cJoin扁平事务作为保证组合活动原子执行的基本机制被引入数据库界。术语“事务处理”指明了构成事务的活动是基本动作，例如读和写，但它们本身不能是事务。类似地，我们定义了cJoin的一个子演算，称为cJoin的子演算，其中协商不能嵌套。在本节中，我们将cJoin进程描述为良好类型的术语，并证明任何cJoin进程都可以用等价的规范形式编写。3.1一个用于cJoin的类型系统我们使用图5中的类型系统挑选出cJoin的可扩展进程。它取类型的集合T={Q0，Q1，Q2}，并使用以下类型判断：► P：Q0谈判的建构者[ ： [1]在P中没有出现。►Q1P不包含主动谈判，但可以激活谈判合同.► Q2P可以有或生成可重复协商，但不能有嵌套协商.► D：Q0D不包含用于协商的构造函数.► Q1D可以包含或启动可扩展协商，但不能包含嵌套协商.规则（SUB-P）和（SUB-D）代表子类型顺序Q0Q1Q2。<<我们说，一个过程P（resp。定义D）是良好类型的，如果P：Q2（分别为► D：Q1）。显然，内部过程为0，messgex→y的发射和consttabort不包含用于协商的构造函数，并且类型为Q0。根据规则（PAR），如果P和Q都是Qi型的，则并行组合PQ可以是Qi型的。因此，P-Q类型对应于最大的较低类型可以分配给P和Q。事实上，考虑到P和Q是良好类型的，如果P包含活动协商（即，P：Q2），与Q的结构无关，过程P|Q包含活动合约（即，CUP|Q：Q2）.规则（NEG）通过声明[P：Q]可以被键入来防止嵌套2只有当P不具有协商（即，P：Q0）。 相反，补偿Q可以用谈判来定义。这不会损害补偿条件，因为补偿是在顶层执行的，而不是在它们起源的 规则（DEF）结合了定义的类型和流程. 请注意，只有当D和P都不是时，使用构造函数进行协商，即如果两者都有类型Q0。相反，当协商仅以定义（D或包含的定义）出现时，它可以被键入Q146R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-►→⟨⟩⟨⟩中文（简体）公司简介（S ub-P）（S ub-D）Q：Qi（ZERO）► 0：Q0（男）► xx xx：Q0（ABORT）► 中止：Q0（PAR）► P：QjI j中国：Q0► D：Q1P：Qi（NEG）粤ICP备0900000号-1（DEF）D：Qi（CONJ）► P|Q：Qi（ORD-0）► [P：Q]：Q2（ORD）► defDinP：Qmax（i，j）（M）QiQiQi► D：QiQ1：Q0► J d P：Q0P：Qi► J d P：Q1► Q：Q0图5. FlatcJoin Typing.在P中）。最后，如果P中的defD键入Q2，则其活动协商出现在P中，因此P键入Q2。根据规则（CONJ），定义的共轭只有在以下两种情况下才被类型化为Qi：子项类型Qi. 根据规则（ORD）和（ORD-0），一个普通的定义当J d P的被保护进程P是良类型的时，J d P是良类型的。而且如果P不包含用于协商的构造函数（即，P：Q0）。不同的是，一个合并规则只有当P的类型为Q0时才是良类型的（rule（M））。这是为了避免嵌套，因为P的实例将在协商中执行。示例3.1类型良好的术语。考虑例2.1中介绍的邮件列表过程。下面是几个子术语及其类型P1defzd 0 inyv，z|lyP2[P1：ly]D1ly|告诉你的朋友P2D2|关闭登录0P1：Q0此外，它还支持XMLDef：Q1（它没有活动的协商，但可以发起协商）和XMLML：Q1.例3.2反例[defDinx：0]中的术语defx[P：0]不是良好类型的，因为它有一个合并定义，其保护过程是一个协商（规则（M）不能应用，因为x[P：0]：Q0）。事实上，它在[defDin[P：0]：0]中简化为defx[P：0]，当x dn（D）时，它具有嵌套的契约。命题3.3（Join进程是Q0）设P是一个Join进程，则P：Q0.引理3.4（Q 0的主语归约）设P：Q0. 如果P≠P J，则PJ：Q0.下面的结果确保了嵌套进程不会引入嵌套。►R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-47→Ⓧ→定理3.5（Q ~ 2的主语归约）设P：Q ~2. 如果PpJ然后PJ：Q2.受试者减少并不适用于第一季度。 考虑Pdefxd[Q：QJ]在x中，其中Q：Q0和QJ：Q1。 虽然P=P：Q1，但P在[Q：QJ]中简化为Pjdefxd[Q：QJ]，它可以被类型化为Q2，但不能被类型化为Q1。定义3.6[FlatcJoin]设P是一个cJoin进程。P在i=P：Q2时为零。 FlatcJoin是所有可扩展进程的子演算。在[5]中，我们定义了浅进程类，并证明了它们的可串行化结果，这意味着不相交的协商不能相互干扰（除非它们被合并）。虽然这里没有报告浅过程的定义，但检查浅过程是否也是浅的是微不足道的推论3.7（可串行化）任何可串行化的进程P都是浅的，因此是可串行化的。3.2零安全网和cJoin。零安全网（Zero-safe nets，ZSnets）[6]已经被引入到并发系统中的可串行化事务的建模中。它们支持多路交易，即具有多个入口和出口点以及静态未知数量的参与者。最近，它们已经在[4]中被用于对Microsoft BiztalkR（一个商业工作流程管理系统）的短期运行事务进行编码[13]。然而，ZS网不适合建模有趣的方面，如名称移动性，可编程补偿和嵌套，这是cJoin的主要特点。类似于Petri网，ZS网依赖于位置（即资源，消息的存储库），令牌（即，地点的实例）、标记U（即，位置的多集合）和转换U[j]（即，获取和产生标记的多集合的基本活动）。然而，ZS网的位置被划分为普通的和事务的（分别称为稳定和零Corres-令人困惑的是，标记U可以被看作具有U=S+Z的对（S，Z），其中S和Z分别是稳定资源和零资源的多集。零位置中的令牌是属于某些正在进行的协商的瞬态数据，而稳定位置中的令牌对通过协商实现的承诺决策进行建模，这些决策从稳定标记开始并导致稳定标记（即稳定位置的多集）。关键点是，在协商中产生的稳定令牌仅在提交时可用，此时没有零令牌。ZS网的操作语义由图6中的两个关系T和T（由转换集T索引）定义。规则的触发和步进是Petri网中常见的规则规则串联组成零48R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-（Ⅲ）（Ⅲ）⟩（）（）（Ⅲ）（射击）S+Z[<$SJ+ZJ∈T（步骤）（S1，Z1）→T（S1J，Z1J）（S2，Z2）→T（S2J，Z2J）（S+SJJ，Z+ZJJ）→T（SJ+SJJ，ZJ+ZJJ）（CONCATENATION）（S1，Z）→T（S1J，ZJJ）（S2，ZJJ）→T（S2J，ZJ）（S1+S2，Z）→T（S1J+S2J，ZJ）（S1+S2，Z1+Z2）→T（S1J+S2J，Z1J+Z2J）（关闭）（S，n）→T（SJ，n）（S，n）T（SJ，n）图6. ZS网的操作语义（+表示多集并）。令牌是串行的，但稳定令牌是并行的，因此第一步产生的稳定令牌不能被第二步消耗协商（S，j）T（SJ，j）是从稳定标记到稳定标记（规则关闭）的步骤的串联。在文献中，ZS网已经在Join[4]（通过用于建立协商结束的分布式两阶段提交协议）和cJoin[5]（几乎直接地，利用额外的协商原语）中编码。我们简单地回忆一下后者的编码cJ，因为：• 在不失一般性的情况下，这两种编码都是针对由图7（a）中的基本形状构成的ZS网（与一般网一样具有表现力）定义的，其中E是任何稳定位置，e，e1，e2是任何零位置。我们使用诸如Eopene之类的助记符名称来表示可以产生新的本地协商的转换E[e]，以及eforke1，e2来表示可以在正在运行的协商中创建并行线程的转换e[e1+e2基本形状类似我们在对数据进行编码时将考虑的基本定义模式C加入• ZS网络不具有可编程补偿。编码cJ表明，适当的默认补偿可以恢复协商的初始状态。作为一个原始结果，在下面的命题3.8中，我们证明了ZS网被编码为可重构过程。在cJoin中编码zs网。图7（b）中的转换cJ将cJoin定义（分别为消息）与每个基本形状的转换（分别稳定标记）。地点被视为端口，令牌被视为消息。在稳定位置的代币没有价值，而在零位置的代币带有它们所属的交易的标识符。 对于T为转换集，S为ZS网的初始标记，我们让 TcJ=t∈T tcJ，然后将cJoin进程defTcJinScJ，其包括初始标记S在环境中的平移包含了所有与T中的跃迁相关的定义。其预设包含零位置的转换被转换为合并定义，否则被转换为普通的Join定义。R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-49开放，，，，（Ⅲ）（Ⅲ），，，，，，<$Eopene）cJ：：=Ed[defzd0inez：E]叉1e叉e1，e 2下降电子降2c：：=ez0，，e1cce2得双曲余切值.e1， e2加入e、Ee关闭E、、<$E）cJ：：=E(b)基本形状和标记的翻译。r，，~，~z，E，，e1calceE打开ee、e2e1计算e2e、e叉e1，e2cJ：：= eze1z|e2ze1，e2joinecJ：：= e1z1|e2z2ez1<$e1calce2）cJ：：=e1ze2z、、，，，<$ecloseE）cJ：：=ezE，r rcjo，i，，n、clr，，~osz，e<$S1+ S2）cJ：：=<$S1）cJ|（2）cJ(a)ZS的基本形状网。图7. cJoin中的ZSNets编码。我们将简要讨论编码的一些特性（详细信息见[5]）。形式E open e的转换的翻译是一个cJoin定义，它可以打开一个新的协商，包含新名称z（事务的标识符）的定义以及消息ez，其默认补偿是唯一稳定的资源E。 虚拟定义z_d 0是为协商定义局部标识符的一种方便方法，并且没有计算意义。事实上，端口上不会产生任何消息z.端口e对应于homebooks零位置，它是一个通过merge定义外部定义的名称（起源于T中从位置e获取的那些转换），它可以用于计算内部协商，甚至通过cJoin的反应MERGE合并它们。 例如，两个不相交的与e1和e2中的本地令牌的协商可以通过触发转换来合并e1，e2加入e，即通过执行e1z1的合并反应|e2z2ez1。请注意，标识符z1和z2则成为相同较大协商的等效标识符。关键点在于，当稳定消息E_bet在协商内被释放时，例如，而他们，也不可能，因为他们，在协商提交之前获取，因为所有可以使用它们的规则都是普通规则，并且在协商边界之外。虽然编码的正确性和完整性可以在[5]中找到，但这里我们基于图5中的类型系统陈述以下原始结果。e50R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-（2）≡ ⟨⟩ |⟨ ⟩⟨⟩⟨⟩|⟨ ⟩⟨⟩count（0）=1count（x→u）=1count（P|Q）=count（P） +count（Q）count（abort）= 1count（[P：Q]）=count（P）count（defDinP）=count（P）图8. 计数（P）的定义。OPENx→vd P& 第二季度& cont（P）=1ORD-MOVx→ud P& 第一季度& cunt（P）≤2MERGE-MOVx→uP&Q1 ：Q0&cunt（P）≤2ORD-JOINx→v |yw→d P&第一季度&count（P）=1MERGE-JOINx1v→1|.... . . 你 好 。 . |xnv→np&Q1：Q0&cont（P）=1图9. 规范形式命题3.8（zs网的cJoin编码是可扩展的）► defTcJinScJ：Q2.3.3Reynat过程的一个标准型与ZS网一样，我们将把注意力限制在用一些基本形状构建的过程上，以简化将cJoin编码为Join的定义。特别是，我们禁止定义消费和生产消息自由.图8中的辅助函数count对进程中存在的原子代理进行计数。定义3.9[标准形式]设P是一个随机过程，如果P中的任何定义满足图9中的条件之一，则P是标准形式。值得注意的是，这些条件与ZS网的基本形状相匹配通过（O PEN），创建新协商的反应消耗恰好一条消息，并且在新协商中仅产生一个代理。Rule（O RD-J OIN）确保同步消耗两条消息并恰好产生一个新的代理。不同的是，规则（M-J OIN）允许同时加入多个协商。此外，一个join不能直接产生一个新的协商（一个留给（O PEN）的任务）。最后，规则（ORD-MOV）和（M-MOV）是ZS网的转换calc、fork和close（drop是一种特殊情况）命题3.10设P是一个随机过程。P可以写成一个等价的正则的双曲型过程。例3.11例2.1中的进程MLDef不是规范形式。 事实上，L y告诉v d [defzd 0 iny v，zl y：l y] 是一个连接，它使用两个内部消息创建协商。它可以重写为R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-51►⟨⟩（2）（Ⅲ）⟨ ⟩∈告诉j l y|告诉你，adefbdyv，z|lyinb：ly]其中a和b是新名字。请注意，告诉J：Q1。它的第一条规则是O rd-J oin，而第二条规则是O pen。实际上，包含在协商中的进程具有类型Q0，并且发出的消息的计数为1（即，（b）。合同中出现的定义是规范形式的，实际上它们对应于O RD-M OV：zd 0是一个drop，bd yv，z|ly是叉子。命题3.12（zs的编码是标准型的）设N=（T，S）是ZS网，则S cJ中的defTcJ已经是标准型的。4在Join中的cJoin处编码索引。在本节中，我们将描述在cJoin过程中的规范连接由于我们对从一致状态开始并导致一致状态的计算感兴趣，因此我们将注意力限制在不进行主动协商的过程上，即另外类型为Q1的规范的cJoin过程。为简单起见，编码依赖于使用数据扩展的连接类型SET，用于有限集合和空集合的标准运算，并集运算，和差异。进程通过考虑两组名称来编码：S表示一组普通名称，B包含合并名称，用于决定P中的自由名称是普通名称还是合并名称。因此，只有当fn（P）SB且SB =时，编码才是定义良好的。定义4.1[编码]。 与规范连接器关联的连接具有类型Q1的cJoin进程P是（P）fn（P），fn（参见图10）。顶级流程。函数PS，B定义了顶层进程的编码。请注意，在稳定名称x中的消息的发射被转换为xs或xb上的消息，考虑到第r个参数s→u是普通名称还是rge名称。端口xs或xb通过下面给出的定义的编码来引入。对于隐含的所有名称sin→u都是常规的或规则的，但是可以通过使用不同的端口来扩展呈现以用于任何可能的组合。一个顶级的消息在一个消息名（x）上的年龄x→uB）生活在谈判中，不能被消费。此外，它是不可观测的，因为x是一个52R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-BS<$x∈BS，B= 0ifx∈B（Ⅲ）（Ⅲ）（）（）（）（Ⅲ）（）（）（）p，a，np，a，n（Ⅲ）p，a，n（Ⅲ）（）（）（））其中，S，B（1）S，B= 0S、BS'，B'S、BOput，abt，{lock}<$0）S，B=pl，，p，a，nB<$x→u）S，B=pl，，{x→u}ifx∈S→u∈Sp，a，nSp，a，nB<$x∈ B→u∈S）S，B=x∈ B→u，p，a，l∈ifx/∈S<$B→u∈Sp，a，nz<$x∈ B→u∈ B）S，B=x∈ B→u，p，a，l∈ifx/∈S∈B→u∈Bp，a，nSp，a，nB<$x∈ B→u∈S）S，B=xs∈B→u，p，a，l∈ifx∈B→u∈Sp，a，nz<$x∈ B→u∈ B）S，B=xs∈B→u，p，a，l∈ifx∈B→u∈Bp，a，n（p1，p2），（a1，a2），1（p1，p2），（a1，a2），<$defDinP）S，B=def <$D）S，Bin<$P）S，B如果count（P）= 1（p1，p2），（a1，a2），p1，a1，a 2p2，a2，p<$defDinP）S，B=def <$D）S，Bin<$P）S，B如果count（P）= 2p，a，nS（1）A，B = A，B=A，B1p，a，nT级过程0S，B= 0x∈ B→u∈S，B=x∈B→u∈ifx/∈B→u∈S<$x∈ B→u∈ B）S，B=x∈B→u∈ifx/∈B→u∈BP|Q S，B= PS，B|Q S，B0J J<$defDinP）=defDin<$P）''S=S±dn（D）B=B±dn（D）[P：Q] S，B= defDcmpd QS，B处于状态{cmp}| PS，B谈判中的程序x∈ S→u∈S，B=p∈l，n，{x∈→u∈}nfx∈S→u∈B<$x∈S→u/∈（S<$B），B= 0ifx∈S→u/∈（S<$B）<$x→u）S，B=x→u，p，a，lifx/∈SB→u/∈SBx∈ B→u∈S，B=xz∈B→u，p，a，l∈ifx∈B→u/∈S∈BP|Q S，B= P S，B|Q S，Bif count（P）= count（Q）= 1图10.规范的随机过程的编码。定义名称因此，它是无用的，并编码为惰性进程0。类似于abort，它在合同之外没有意义。请注意，当使用局部定义，即在定义时到SJ和BJP中的D）S，B. 在这种情况下，通过考虑dn（D）对D和P进行编码。我们用来表示不相交集合的并集。(Note定义的名称总是可以用新的名称重新命名。当一个协商被转换为Join时，它与一个新的协调器D相关联（图12），后者将监视合同的执行。作为P将作为协商的一部分运行，它被编码为∈put，abt，{lock}阿布特锁dno（D）.我们可以有把握地假设P以唯一线程因为我们正在转换具有类型Q1的规范过程，因此，在count（P）= 1的定义中，出现[P：Q]。补偿Q被编码为顶级进程，它通过本地端口cmp上的消息激活。由于cmp仅用于初始化协调器的状态（状态{cmp}），因此仅当协调器（并且MR. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-53（Ⅲ）zS联系我们⟨∅ ∅⟩因此，合同终止。谈判过程辅助编码p，a，l描述了线程S、 B由管理器D监控，该管理器D定义用于接收的信道p和a提交或中止确认。集合l收集对同一协商中的已知方的引用（称为同步集合）。协商中的惰性进程0意味着线程完成，它被转换为p l，，以通知它已准备好提交。消息包含l以通知D关于已知方。一个messagex en→un n的nc d需要对其中涉及的不同类型的名称进行分析。当消息被发送到自由名称或发送到在顶层（x ∈ S）定义的普通名称时，存在两种不同的情况。 如果您不是本地人，例如： →u∈S，则therea试图通过使用x→u来结束协商。 Henceitisencodingg a commitnoti fic tionpl，n，{xs→u}.如果协商最终提交，则不会释放该文件。相反，当参数是合约中定义的名称时，谈判可以进入停顿状态，除非其他参与者中止整个合约。 事实上，这样的消息在提交之前不能被消费， 启用合约的提交（提交要求所有本地名称不出现在消息中）。停止情况用0编码，这样线程结束时不通知协调器，也mit nor abort，协调器将被阻塞（除非其中一方中止）。另一方面，在协商中定义的名称x通过使用三个不同的端口进行编码：xz，xb和xs以处理不同类型的参数，即，本地、合并和顶级。类似地，合并名称的编码考虑到了它们的参数类型，但它们也应该考虑到当接收到的名称不是本地的时，协商可以结束。端口xk（带有k z，b，s）用于对合并名称的行为进行编码，该合并名称接收类型k的名称并继续执行协商。相反，端口xk也允许提交合约的可能性，即使消息没有被消费。请注意，x上的发射被转换为携带值p、a和l的消息，用于与管理器交互。（下面是关于编码合并定义的深思熟虑的讨论）。常量进程中止被转换为一条消息，关于About abort abort过程定义D在P中的转换涉及到D和P的转换。当count（P）= 1时，通过使用分配给整个进程的相同协调器来编码P。54R. Bruni et al. / Electronic Notes in Theoretical Computer Science 104（2004）39-（）（）（2）（Ⅲ）S、B（Ⅲ）（五）z1z||nz⟨⟩SS、BQ SS10（Ⅲ）<$DE）S，B=<$D）S，B<$E）S，Bfor i= 1，21zp，a，nBp，a，nSp，a，n<$x→ud<$ P）S，B=x→ud<$P）S±{→u}，Bx→ud<$P）S，B±{→u}（remainingpathomitted）S、Bk=s，bSSSzp，xzzS、Bk=s，bSSzxz→u，p1，a1，ldefD1D2in<$P）（put1，put2），（abt1，abt2），{lock1，lock2}S、BIszdefDinstateS{a}|（P）put，abt，ii{lock}|xu→1，p1，a1，l1.... . . 你 好 。 . xu→n，pn，an，l