理论计算机科学电子笔记105（2004）119-132www.elsevier.com/locate/entcs原子提交劳拉·博奇1卢西恩·维斯奇克2博洛尼亚大学计算机科学系意大利摘要本文指出了进程演算和原子提交之间的紧密联系。亲-Cess演算集合是用于原子提交的抽象语义。进程演算会合的实现是原子提交协议。因此，原子提交的传统正确性属性是由微积分实现的互模拟证明所包含的。实际上，在pi演算中发现的传统会合只对应于原子提交的一种特殊情况，称为二进制内聚。如果我们考虑原子提交的一般情况，这会导致类似于连接演算的更丰富形式的演算集合[10]。作为演算和原子提交之间的类比的扩展示例，我们使用诱导演算来重新表述Berger和Honda [1]的早期2PCP正确性结果。保留字：同步交会，pi演算互模拟，原子提交协议，2PCP1介绍本文概述了进程演算和原子提交之间的紧密联系。进程演算是并发和分布式交互系统的模型或语言。它们也支持新兴的Web服务标准[7，8，11]。进程演算通过同步会合（synchronous rendezvous）工作，其中一方（如Web服务）通过通信信道等待数据;另一方（客户端）通过信道发送数据;一旦数据交换完毕，双方继续。规范过程演算是pi演算[12]。1电子邮件：bocchi@cs.unibo.it2电子邮件：lu@wischik.com1571-0661 © 2004由Elsevier B. V.出版在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.05.003120L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119近年来，交易和微积分已经相遇。首先，进程演算已经被用于形式化事务中使用的协议，例如两阶段提交[1]，补偿触发[5，6]，嵌套[4]和共识[13]。其次，事务的特性被添加到进程演算中：[3]添加了原子性，隔离性和持久性的原语，[5]添加了补偿事务的原语。本文描述了进程计算和事务之间的一个更基本的联系：基本的同步会合机制本身已经是原子提交的一个特例。这意味着原子提交协议构成进程演算的实现，并且进程演算的实现构成原子提交协议的特殊情况-我们注意到传统的此外，进程演算及其实现之间的互模拟的优雅概念需要通常为原子提交提供的正确性属性的ad-hoc集合。所有这一切都带来了一种吸引人的可能性。(1)同步会合是原子提交的高级语义，具有简洁的符号。 (2)Web服务语言已经从进程演算中借用了异步会合（异步会合是发送者不等待其消息被消费的时候）。（3）Web服务语言也讨论了事务的原子性。把这些放在一起，也许我们可以创建（4）一个新的Web服务语言，它使用同步和异步会合。这样一种语言不需要提到原子性（因为原子性将隐含在它的会合中）。它也将享受与过程演算的强有力的正式联系。如前所述，传统的基于pi演算的同步会合是原子提交的一种特殊情况我们将看到，一般的原子提交引入了更丰富的会合机制，类似于连接演算的此外，内聚提交一般认为，同步交会相当于解决分布式一致性问题.这是不正确的：会合严格来说更容易。特别地，如果任何参与方已经崩溃，分布式共识块;只要两方保持活跃，二元内聚就不需要块本文的研究计划如下。第1节和第2节介绍了传统的重定向，然后介绍了传统的原子提交。后者以非标准的方式呈现，揭示了对应关系。第三节给出了一个具有更丰富形式的会合的过程演算，它对应于任意的L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119121˜˜原子提交第4节回顾了[1]的两阶段提交协议，将其正确性声明重新转换为具有更丰富进程演算的互模拟。在这样做，我们提供了一个正式的协议和传统的正确性属性的原子提交之间的联系。本文的主要创新之处在于形式化地揭示了原子提交与会合之间的联系。2交会我们给出了一个简短的总结会合，在π演算中使用。它假定以下设置。有N个分布式方执行他们的代码。一方可能最终到达发送命令ux（指示希望在信道u上发送数据x），于是它阻塞。 或者，一方可以到达接收命令u（y）（希望通过信道u接收形式参数y），于是它也阻塞。如果在一个信道上有一个发送者和一个接收者被阻塞，他们最终可能会会合约会严格限于两方即使有几方愿意在频道上接收，也只有一方这样做。定义2.1（Pi演算）假设一个名称集合N，其范围为：x，y， . 。 。。 我们需要一个时间表.. 。 联合国PiccalculustermsPareP：：= 0 。 ux.P。 u（x）.P.Vx.P.P|P.算子νx.P和u（x）.P约束x。我们识别程序，直到绑定名称的alpha重命名和直到结构同余，如下所示，在上下文下关闭：P|0 - 0P|Q Q|PP|（Q|R）（P |Q）|R（结构）vx. vy.pv v y. vx.pv x. （P|Q）可持续发展|νx.Q如果x/∈ fn P（scope）反应关系式→，也称为“可逆”，是使u x满足的最小关系式。P|u（y）。Q→P|Q{xe/ye}和包含多个字符串和字符串扩展的数据集。观测值P↓u由下式给出：ux。P↓uu（x）。P↓uP|Q↓u，如果P↓u或Q↓uνx.P↓u如果P ↓u和uxπ演算会合可以用图解表示。在下面，写u x.P |u（y）.Q|R一般指的 是任何状态，122L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119互补输出u x.P和输入u（y）.Q，以及对于无状态的R j。ux.P |u（y）.Q|RRJczP|Q {x/y}|R（一）在进程演算中有一个标准的技术，互模拟，用于判断两个转换系统是否具有相同的交互行为：定义2.2（互模拟）设（P，→p，↓p）和（Q，→q，↓q）是两个转移系统，每个系统都配备有一个观测关系。让SP ×Q联系它们的状态。把写成→，把写成↓。则S是互模拟当且仅当每当PSQ，则• P≠pu当且仅当Q ≠qu;• P<$pPJ蕴涵Q<$q QJ，其中PJSQJ;• Q<$qQJ蕴含P <$pPJ，其中PJS QJ。两个项P∈ P和Q∈ Q称为双相似的，当存在一个双相似项时，·他们之间的恩怨。对于最大的互模拟，写。例如，从π演算中取P和Q，则A = ux |u（y）.PB = x|我是。（u（y）.u Jy|uJ（y）.P）通过S ={（A，B）}<$I是双相似的。3原子提交我们给出原子承诺的一个简要的总结。这一摘要是非常规的：它的结构是为了揭示与会合的相似性原子提交的典型设置是在分布式数据库系统中。当提出一个事务时，一些分布式部件可能能够或不能接受该事务。只有当每个人都能够提交时，才能提交事务。我们假设有N个独立的政党。他们每个• 要么能，要么不能。• 当被要求投票决定是否应该进行交易时，投票是（如果当事人能够接受交易）或否（如果不能接受）;• 做出提交或中止的决定，并终止。要求所有分布式参与方达成相同的决策（提交或中止）。我们称之为“集体决策”。为了实现这种一致性，各方之间进行一项协议，发送他们的投票和交换信息。该议定书必须考虑到L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119123一些消息丢失（通信故障）或一些方崩溃（站点故障）的可能性形式上，对于一个被称为“原子提交”协议的协议AC1。 所有达成决定的各方都达成了同一个决定。AC 2. 一方当事人在作出决定后不能改变其决定。AC3. 只有在所有各方都投赞成票的情况下才能达成承诺。 能够）。AC4。 如果所有各方都有能力，而且没有失败，集体决定将是承诺。AC5。在任何阶段，如果所有的故障都得到修复，那么各方最终都会达成一个决定。(This也称为弱终止或活性）。存在现有文献所暗示的并且现有协议所满足的其他性质：AC6。 一方不能从有能力变为无能力，反之亦然。AC7。 如果有足够的失败，集体决定将中止。把一个协议看作是一组状态，它们之间有转换→。转换可能是消息的发射，或同时广播和接收（在即时通信的情况下），或消息丢失事件或站点故障。我们将把所有可能的状态划分为以下不相交和穷举的划分。写（x，y）表示x方决定提交而y方决定中止的状态写（x，y）a，如果所有各方都能，写（x，y）u，如果有些人不能。让i，j的范围大于1. N−1。这些分区为：• （0， 0）a• （0， 0）u• （i，0）• （0，j）a• （0，j）u• （N，0）• （0，N）a• （0，N）u• （i，j），其中i+j N• （i，j），其中i+j=N。每个属性都对哪些状态间转换是不允许的或哪些必须存在施加了约束。例如，AC4意味着存在124L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119一个序列（0， 0）一个序列（N，0）。AC2意味着没有（0，N）→（N，0）的转换序列下表总结了所有转换，并在后面进行了解释。通过AC 1，两个状态（i，j）：i+j N和（i，j）：i+j=N从未达到;因此从表中省略。从\到（0， 0）a（0， 0）u（i，0）（0，j）a（0，j）u（N，0）（0，N）a（0，N）u（0，0）aIDAC6AC/16AC4AC7AC6（0，0）uAC6IDAC3AC6AC\/3aAC6aAC5a（i，0）AC2AC3IDAC2AC2AC5b阿、中、2bAC2b（0，j）aAC2AC6AC2IDAC6AC/2cAC5cAC/6c（0，j）uAC6AC2AC2AC6IDAC2dAC6dAC5d（N，0）AC2AC2AC2AC/12AC/12IDAC/12AC2（0，N）aAC2AC6AC2AC/12AC2AC2IDAC6（0，N）uAC6AC2AC2AC2AC/16AC2AC6ID为了解释，该表显示了从状态（行）到状态（列）的某种转换序列是否可能。例如，由于AC4，从（0，0）到（N，0）的序列是可能的。这并不意味着这个序列一定会被采用;它只是意味着它是可能的，假设幸运的非确定性选择和没有失败。该表以粗体标记这些可能性，并使用指示该可能性的规则的名称。根据定义，每个状态都允许空的转移序列回到它自己，它被表示为id。如果其中一个属性排除了过渡，则用叉表示。我们注意到AC5（弱终止）的使用。我们用（a）表示的一个例子是，从（0， 0）u有可能到达（N，0）或（0，N）a或（0，N）u。碰巧的是，（N，0）由于AC3而被排除，并且（0，N）a由于AC6而被排除。 唯一的可能性是（0，N）u。该表已用上标和…d显示AC5的四个单独应用。表中的一些空格是未指定的，例如对于（0， 0）a（i，0）。因此，允许协议包括转换，或允许省略它。定义3.1（协议）原子提交协议是任何转换系统（P，→，↓），其中P可以划分为上面列出的八个状态，并且其中转换序列P PJ根据上表被允许或不允许。在所有各方都能够的状态下写P↓a，在L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119125、有些是不能的，P ↓ cmt在一方或多方决定提交的状态下，P ↓ abt在一方或多方决定放弃的状态下。具体地，以下是一种可能的原子提交协议。（0，0）a、、、、（0， 0）ucz，，，，，，v（N，0）（0，N）a中文（简体）（0，N）u这是一个明显的图表，它对应于我们对原子提交协议是什么的直觉人们可能会认为它是原子提交的高级语义。下面的定理证明了这一点：定理3.2（正确性）一个变迁系统（P，→，↓）是一个原子提交协议当且仅当它与图2是双相似的.证据 简单的表格查找。在图2中还有一个进一步的改进。“中止”的本意是使一方返回到尝试提交之前的状态。因此，它能够接受进一步的承诺。这可以由跃迁（0，N）a→（0， 0）a和（0，N）u→（0， 0）u表示。通过这些转换，图退化，并且AC7是冗余的：（0，0）acz（N，0）（0，0）u（三）请注意，图1和图3基本相同。4一般Renminbi前一节已经从进程演算领域中获得了互模拟，并将其应用于原子提交。在本节中，我们采用一般承诺，并使用它来归纳一般会合机制。使用下面的类比。原子承诺就像一个会合。当各方能够提交时，就像微积分中有ux和u（y）一样。当一方决定提交时，它就像是由于已经执行了会合而解除了自身的阻塞。Atomic commit允许多方参与，而Pi ren-commit只允许两方参与。这意味着要考虑一种不同的形式，126L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119˜˜例如，允许多方参与的UA|VB|WC |u（x）<$v（y）<$w（z）.P→ P {abc/xyz}.将连接模式u1（x1）写成J。n（xn）.Pn.基于内聚事务中的提交，还有进一步的推广。BTP中提出了Cohesor（参见[9]的概述），WS-Transactions [8]中也有类似的概念通常，原子提交要求所有参与方都中止或全部提交。但是一个cohesor要求要么所有的都中止，要么一些预定义的子集提交，而其余的都一个cohesor有一个可接受子集的列表。举个例子，考虑一个假日预订，其中包括前往威尼斯和租用水上出租车或贡多拉。有两个可接受的子集：（平面）和（平面Gondola）。凝聚诱导微积分中的选择算子。例如，写p（）表示飞机，w（）表示水上出租车，g（）表示缆车，p .P| t.Q|p（）<$w（）.T + p（）<$g（）.G→ P|Q| T.p .P| g.Q|p（）w（）.T + p（）g（）.G→P|Q|G.定义4.1一般交会演算有项P，就像对于圆周演算（定义2）一样。1）utwithinputsu（xn）. 编写人：P：：=.。 J1 +...+ Jm.我们再一次确定了最多到1000的术语。反应关系→是满足以下条件的最小关系，并且在上下文下是封闭的：u1x1.P1|......这是什么？|J1+...|J1+ ... + Jm|R →P1|......这是什么？|Q1 { x 1 / y 1}|......这是什么？|... |R|R如果某个Jj= u1（y1）.Q1≠...un（yn）.观察结果与π演算相同，但J1 +. . 。 + Jm↓u，如果某个Jic满足u（x∈ u）. P.任何用于原子或内聚提交的协议都必须与该演算中的简单会合点双相似。联接模式和联接模式的求和是在Fournet和Gonthier的联接演算 [10]但实际上，连接演算和我们的工作之间有本质的区别在join演算中，n没有延续（所以只有p而不是p.P）。此外，给定名称的所有接收者必须位于同一物理位置。这两个约束L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119127·这意味着会合不再需要任何协议;这允许非常轻量级的会合实现。相比之下，我们的项目是使用会合作为承诺协议的高级模型。5快递2PCP我们通过回顾Berger和Honda [1]的一个较早的正确性结果来说明我们的一般会合演算。本节的目的是通过将我们的会合演算应用于一个现有问题来展示一个实际的例子。因此，本节要求对所引用的工作有所了解。然而，这一部分是不需要为其余的文件。Berger和Honda在他们的有损网络的正式模型上实现了一个两阶段提交协议（基于修改的异步pi演算）。·写2PCP为他们的协议，他们证明了2PCP的错误！中止任务！承诺在所有上下文中：对于外部观察者，协议要么提交要么中止。这里的符号P Q是非确定性选择;它是νc的简写。（c）|c（）.P|c（）.Q）。注意：本节并不独立;它假设读者熟悉[1]。我们现在重新表述它们的正确性结果。他们考虑了n个政党的设置，其中每个政党非确定性地选择能够或不能。写AC作为它的高级表示：AC=u1（）. un（）.KC|u1.K1！una|......这是什么？|un.Kn⊕! 乌娜。为Berger和Honda的AC实现编写[[[AC]]]，使，使，使那么所需的正确性结果基本·AC[[AC]]。即使所有参与方都能够做出反应（通过正确的非确定性选择），协议的一个实例仍然有可能导致失败（通过消息丢失）。将[1]中的引理5.3应用到上面的图3中，我们让每一方尝试通过重试从这种失败中恢复。有一个微妙之处。两阶段提交是一个非组合协议：它有一个固定的拓扑结构，在这个意义上，协议中涉及的所有各方都已经固定为在交互中使用彼此作为合作伙伴，而不是其他人。 在AC中，被定义为“用户名”。我们认为，根据K.和pro vi ng vu。AC [vu. AC]]。=0，这个证明很大程度上类似于Berger和Honda给出的证明。 为了不重复太多他们的工作，我们采用了一种更简单的设置。根据[1]的引理5.2，我们将所有超时替换为输入保护选择：128L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119Pi=u|P JI我NNN我JJ JJtimer（u.P，Q）= νt. （t |u.P + t.Q）。我们忽略网站故障（即。崩溃/恢复）。让协调员自己不要投票。考虑到这些简化，伯杰和本田的协议如下。这是写在[1]的低级网络计算中的;我们在这里不重复它的定义。在下文中，我们使用[[ui]。Ki]]=Pi且[[[u1（）]= Pi 。 。 un（）. KC]]=C，并且对于n∈NPn.[[AC]] 为你好。。[C]ueee|[P1！联合国1|.... . . 你 好 。 。 |[Pn！n我J=定时器（di [Ki，（diei）Pi]，ei|P J）C=维察的; 。CWAIT|CTRUE|Cfalse等我= 计时器（ui.ci，a）Ctrue= c1（）......... cn（）。（Strue）|KC）Cfalse为a（）. 我的意思是，（Sfalse|C{dJeJ/d e}真我的虚假=我离开了|是真的= dirightdJej|ei（）.Sfalse我我我·Theorem5.1vu. AC [vu. AC]]。证据从较小的引理开始，使用[1] 4.1节的同余式。（对于P的n个并行副本，写Pn。）第一个引理允许在成功不可避免时进行简化;它对应于[1]引理5.3。对于任意的n和m，我们有vde。。[d leftm|e.Strue]|[en|定时器（d [K，（de）P]，e|P J）] d.（4）证明：用（m，n）表示左手边。 构造S ={（（m，n），K）}对于所有m，n。左手边允许这些内部转换：或者超时产生（m，n +1）;或者e上的交互产生（m +1，n-1）;或者e上的消息丢失产生（m，n-1），或者d上的 消 息 丢 失 产 生 （ m-1 ， n ） ， 或 者 d 上 的 交 互 产 生 K| vde 。（dleftm−1|e.Strue|en）。除了K中的跃迁外，它不允许任何外部跃迁。因此，它是一个。对于下一个引理，回想一下这个过程是在循环中进行的。这个引理允许简化，当下一轮开始时，可以丢弃前一轮。我是说我是。。drightdJejm|即假|C{dJeJ/de}|定时器（d [ K，（de）P ]，e|P j ） de .|P J)Σ ≈ νde. （C）|P）。（五）证明：用（m，n）表示左边。这允许与4相同的跃迁，但这一次d上的最终相互作用产生νdJeJ。（C{d e/de}|P {d e/de}|PCS我L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119129我J JW1nnN1nndeeeca.[C W|C/de} |CC|a]ueee|[P1]d1|.. . . . . 你 好 。 。|[Pn]dnvde。（drightdJej|即假|en））。这是我的。（C{dJeJ/de}|P{dJeJ/de}C|P.下一个引理允许一个方便的简化：内部通道ci是否与C真反应，是无关紧要的。就像[1]引理5.6.v.武奇岛（c i）|ci.P）（六）证明：微不足道。我们现在证明的情况下，每一方都作出了非确定性的选择，能够：你好。。[C] ueee|[P1] d1|.... . . 你 好 。 。 |[Pn] dnKC|K1|.... . . 你 好 。 。|Kn.（七）这种情况对应于[1]定理5.1.ii.在做出所有非确定性选择之后，我们确定三个阶段：(i) 收集选票在这个阶段，我们用一个投票ui：i∈V尚未发送的参与方集合V<$N和一个函数E：N<$→int来描述状态，使得有E（i）个e i的副本。也是将N划分为W，C，A使得仍有Cwait：i∈W和ci：i∈C，并且A中的每个元素都有a。此阶段的状态为我会的。。[Cwait|CTRUE|Cfalse|CC|一|一|[英语泛读材料|[PJJ]d| ... | [P JJ] dΣ.其中P JJ= un|eE㈠|P J和n =如果i ∈ V则1 else 0。通过等式6，我我我其中ci已经与Ctrue反应的任何后续状态与该阶段中的状态双相似。(ii) 全体赞成。此阶段的状态为你好。。[Strue|KC|va.CFALSE]UEE|[PJJ]d| ... | [P JJ] dΣ.其中，V=N，PJJ如上所述 根据公式4，这是|K1|......这是什么？ |Kn.(iii) 一些人投反对票。 此阶段的状态为νdeeee等一下真假dJeJnJJJJ'其中W≠N，对于任何n。通过等式5，所有这些状态都被等式7所取代。·为了完成等式7的证明，构造S={（Q，KC|K1|......这是什么？|（Kn）}对于上述任何阶段中的所有Q。由任何Q产生的唯一外部跃迁是来自相位2的跃迁，由某个K匹配。至于内部过渡，·在内部转换下，这三个相被关闭（直到1000）11|S| C{。130L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119不能的情况（如上文第7条，但其中至少一方作出了 一个不确定的选择！[1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19]L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119131这个结果是把有能力和没有能力的情况结合起来得出的。6结论我们评论组合性。原子提交协议的传统分析（例如，[1，4]）不是组成性的：分析从一组固定的当事人开始，不考虑其他当事人我们在第4节中的演算是部分合成的，因为项u（）<$v（）.P可以放在任何上下文中（“合成”）。|单位质量|u.R|“行，行。因此，程序选择进行涉及一个u服务和一个v服务的事务，但它不指定哪些特定的服务提供者考虑一个完全组合的会合也是有趣的，其中协议中的全部参与者都不为发起者所知这对应于嵌套事务的Web服务情况：例如。我与机票代理商进行交易，作为交易的一部分，机票代理商与航空公司及其银行进行子交易。我们推测，这种完全的组合性可以通过允许输出的连接来实现，而不仅仅是我们在连接模式中发现的输入的连接agent（）gondola（）.P|贡多拉|代理商航空公司（）航空银行（）.R|航空公司|银行这一项应允许所有各方同时会合，给出P|Q|R|S|T.我们把这个留到以后的工作中。(We注意到输入和输出的总和在传统上被认为是不可实现的[14]，理由是某些会合不能在有限的时间内解决。找到这种不可实现性如何应用于嵌套事务似乎很重要。）进一步工作我们有兴趣将本文的技术应用于补偿。补偿用于长时间运行的事务，在这种情况下，当原子提交协议继续进行时，保持所有参与方锁定是这个想法是，一方可以乐观地假设事务成功，但如果这个假设被证明是错误的，则回滚（“补偿”）。带有补偿的程序通常会产生中间状态，在这些中间状态中，一些参与者对是否应该做出决策存在分歧;但是观察到这种分歧的任何观察者本身都会被回滚，因此这些分歧不应该被视为可观察的。132L. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119i∈N˜我们从[5]的补偿π演算开始这定义了一个补偿触发机制，以及一个排序运算符（;）。但是，它没有提供用于对事件回滚进行编程的原语。这样的程序员回滚是正在进行的研究的主题同时，我们给出了一个更简单的补偿pi演算中的原子提交的例子--一个同时利用补偿触发和排序的例子它使用上下文t（P，F，B，C）。该上下文的行为与进程P类似，但如果它简化为中止命令，则触发补偿F;F代表故障处理程序。术语B和C用于事务的嵌套，但这里不需要。 （我们再一次把形式主义的定义留给[5]。）低级原子提交实现是[[AC2]] = t.（（abort done））; x，！乌纳湾其中B=C=完成。在程序中，所有N方都做出一个不确定的选择，是放弃还是继续。这些决定是由结构性规则所巩固的。|abort中止并完成|P/P到一个单一的中止; x或完成; x。从一开始，t（abort; x，！una，done， done）→！乌娜。从第二个开始，·t（done;x，！una，B，C）→ Bax.因此，这是一个具有高级语义的匹配：令AC2= νu。（u1（）. un（）.x|你好！una|......这是什么？| un⊕! una）。话又说回来·AC2[[AC2]]。引用[1] Berger，M.和K.本田，两阶段承诺协议在一个扩展的π演算，在：EXPRESSURLftp://ftp.dcs.qmw.ac.uk/lfp/martinb/express00.ps.gz[2] 伯恩斯坦，宾夕法尼亚州，V. Hadzilacos和N. Goodman，网址http://research.microsoft.com/pubs/ccontrol/[3] 布莱克，A.，克雷梅河Guerraoui和M. Odersky，交易的等式理论，在：G。Goose，J.Hartmanis and J. van Leeuwen ， editors ， FSTTCS 2003 ， Lecture Notes in ComputerScience2914（2003），pp. 38比49URLhttp://www.cse.ogi.edu/~black/publications/fsttcs221.pdf[4] 博奇湖，一个计算长时间运行的事务，在：FASE 2004，2004年，出现。网址http://www.cs.unibo.it/~bocchi/pubs.htmlL. 博基湖Wischik/Electronic Notes in Theoretical Computer Science 105（2004）119133[5] 博奇湖，C. Laneve和G.Zavattaro，A calculus for long running transactions，in：E.Najm，联合Nestmann和P.Stevens，编辑，FMOODS 2003，计算机科学讲义第2884（2003）号来文，第288页。124-138网址http://www.cs.unibo.it/~laneve/papers/biztalk.pdf[6] 布鲁尼河，C. Laneve和U.Montanari，在连接演算中解释事务，在：L。布里姆，P. 我是一个很好的朋友，M。 Kretinsky'a和A. KuJingcera，editors，CONCUR200 2，L.NotesinComputerScience2421（2002），pp. 321-337URLhttp://www.cs.unibo.it/~laneve/papers/zsimpl.ps[7] 业务流程管理倡议，业务流程建模符号（BPML），网站。网址http://www.bpmi.org/[8] Cabrera，F.，G.科普兰湾考克斯，T. Freund，J. Klein，T. Storey和S. Thatte，Web服务事务，网站。网址http://www-106.ibm.com/developerworks/webservices/library/ws-transpec/[9] Dalal，S.，S. Temel，M. Little，M. Potts和J.Webber，Coordinating business transactionson the web，IEEEInternet Computing7（2003），pp. 30比39URLhttp://csdl.computer.org/comp/mags/ic/2003/01/w1030abs.htm[10] 富尔内角和G. Gonthier，反应性化学抽象机和联合演算，在：POPL '96会议记录，ACM（1996），pp. 372-385.URLhttp://research.microsoft.com/~fournet/papers/reflexive-cham-join-calculus.ps[11] 微软，Biztalk服务器，网站。网址http://www.microsoft.com/biztalk/[12] 米尔纳河，“Communicating and mobile systems: the Pi-calculus,” Cambridge UniversityPress,[13] Nestmann，U.，R. Fuzzati和M.Merro，Modeling consensus in process calculus，in：R.Amadio和D. Lugiez，editors，CONCUR 2003 ，Lecture Notes in Computer Science2761（2003），pp. 400-414.URLhttp://lamp.epfl.ch/~uwe/doc/nestmann.fuzzati.merro-concur03.pdf[14] Palamidessi，C.， 比较同步和异步π演算的表达能力，在：POPL'97，ACM SIGPLAN/SIGACT（1997），pp. 256-265。URLhttp://www.cse.psu.edu/~catuscia/papers/pi_calc/popl.ps
我的内容管理
展开
