全局计算语言：pik演算的容错抽象

116网址：http://www.elsevier.nl/locate/entcs/volume66.html29页容错全局计算的抽象（扩展抽象）多米尼克·达根1史蒂文斯理工学院计算机科学系Hoboken，NJ 07030.摘要全局计算（WAN编程，Internet编程）与本地计算（LAN计算）的区别在于，它将网络暴露给应用程序，而不是像LAN编程那样试图用网络透明性来隐藏它全局计算语言寻求为在这样的环境中构建应用程序提供有用的抽象。本文介绍了pik演算，异步分布式编程的演算，它包含了构建容错全局应用程序的抽象该演算结合了原子故障和故障依赖性的概念，从中可以构建各种形式的分布式事务和乐观计算。pik-calculus扩展了异步pi-calculus，引入了日志和用于修改这些日志的“安全”操作的概念1引言全局计算，有时被称为广域计算，广域网编程或互联网编程[10]，为应用程序开发人员带来了有趣的挑战。这是因为用于分布式应用开发的传统编程环境基于跨越局域网和企业内部网络的应用。本地计算环境的特点不同于全球计算环境的特点，因此需要采用不同的方法。本地计算语言是围绕位置透明原则组织的相反，全局计算语言将网络暴露给应用程序，认识到网络管理和导航是全局应用程序的重要方面，1 电子邮件地址：dduggan@cs.stevens-tech.educ 2002年由Elsevier Science B出版。诉在CC BY-NC-ND许可下开放访问。117并寻求为应用程序开发人员提供有用的高级抽象Java Jini系统[4]给出了一个商业示例，而环境演算[11]给出了一个正式的方法。关于全局计算语言语义的工作集中在各种类型的移动性[21，11，12，42，29]。除了基于故障-停止故障模型的工作之外，很少有人注意Argus语言是一种支持容错的本地计算语言容错基于监护人和嵌套事务[37，35]。对事务的模拟支持由Avalan/C++和Venari/ML等语言提供[17，28]，并且是各种知名分布式计算平台的组成部分，包括CORBA OTS、COM MTS和JavaJini和JavaBeans [47，13，4]。作为构建容错全局应用程序的工具，我们希望解决事务的两个方面(i) 第一个方面是事务本身的某种单一概念。事务包括失败原子性、并发控制、持久性和撤销效果的概念这种特殊的组合对于事务最初设计的数据库应用程序类型很有用。尚不清楚这种特定组合或任何特定组合是否适用于所有全球应用。例如，对于各种其他类型的应用程序，特别是对于长期应用程序，已经提出了许多事务的变体[19]。在本文中，我们提出了一套很大程度上正交的抽象，可以结合起来，建立不同类别的容错应用程序。事务是可以通过这种组合构建的机制之一图1提供了我们的抽象集。(ii) 在用于构建容错应用的机制的核心是一些协议集合，这些协议集合又依赖于用于传递协议消息的通信系统。在全局计算中，建立通信信道本身可能是全局应用的重要部分。例如，如今的互联网通信必须通过防火墙、代理、网络地址转换器和负载平衡器。目前，这是以一种特殊的方式完成的，这种方式违反了数据抽象和协议的假定分层。环境演算基于应用程序明确导航由防火墙界定的管理域的概念。如果容错协议是构建全局应用程序的底层支持的一部分，那么如何以语义正确（和安全）的方式传递协议消息？在本文中，我们取得了一些进展，提供了一个答案，这个问题，通过隔离的通信需求的协议，在语义的底层抽象的构建容错的全球应用程序。存在稳定存储和日志的概念;流程可以查询118并扩展自己的本地日志，但只能查询远程站点的日志。如何查询一个远程站点的日志，而不依赖于底层的通信基础设施的问题，是留给续集论文。Jini系统[4]对容错的支持为两阶段提交协议[5]提供了我们的立场是，这种方法的级别太高，并且过于特定于协议。在异步分布式系统中，原子提交通常是不可能实现的，从这个意义上说，它是太高的级别另一方面，构建一个特定的（潜在的阻塞）协议，用于将原子提交到语言语义中，会将语言设计过度提交给特定的实现。相反，我们的重点是隔离应该由稳定存储维护的不变量，并提供应用程序可以用来改变稳定存储的机制，诸如两阶段提交之类的协议可以作为这些原语之上的库来提供。因此，我们的方法类似于全局编程环境的类型系统，尽管在运行时检查稳定存储上的不变保持操作这在我们的演算中由追加到日志的操作表示，在允许这样的追加之前需要满足先决条件。在图中的抽象的核心1是原子故障的概念。原子故障是通过将进程分组到进程组中来实现的;我们将这样的进程组称为conclave。一个秘密会议在最简单的层面上是一组进程cfP1 j：j Pk g其中秘密会议标识符C用作组的名称其意图是，如果秘密会议中的任何进程我们确定因果关系作为衡量不同的秘密会议的失败之间的依赖关系的基本尺度，我们提出因果一致性作为正确执行涉及原子故障的正确性标准。如果一个秘密会议c1消耗了另一个秘密会议c2的一些输出，这就建立了从c2到c1的因果依赖关系。如果c2随后中止，则c1也必须中止。因果一致性的直觉是，与传统事务一样，一系列失败的秘密会议在某种意义上应该等同于没有失败发生的秘密会议，或者至少失败的秘密会议除了失败之外没有任何影响（后一种选择对于嵌套事务是可能的）。所谓而不是限制树结构的因果关系，我们允许任意有向图结构，包括循环图。我们把这里介绍的微积分称为pik-微积分。在第2节中，我们回顾了pik演算的基本机制，包括pi演算的消息传递原语，以及pik演算添加的原子故障和日志的概念。在第3节中，我们描述了因果关系和因果闭合的表示，而在第4节中，我们描述了原子承诺的机制。在119传奇ATF微积分拆分-连接事务交易乐观计算完成有序组播反完备化因果关系延长用于定义原子故障，持久性Fig. 1.抽象的应用第5节我们描述了原子反承诺的机制，消除了乐观承诺的秘密会议的影响。第6节考虑微积分的正确性概念。最后，第7节提供了与相关工作和结论的比较。2原子故障和故障我们的迷你语言pik演算的语法如图2所示。通常在这样的演算中，进程是简单的在这种情况下，该语言是异步π演算[36，31，43]的扩展，这是一种用于描述分布式程序的流行演算，其中通道名称是全局唯一的，并且可以在消息中传输例如，客户端-服务器应用程序可以通过让客户端向服务器发送私有回复通道来描述除了用于发送和接收消息的结构之外，还有一个操作用于生成新的通道名称，用于复制进程（这可以用于定义递归进程描述）和用于形成进程的并行组合。对于形式推理的目的，消息被限制为名称的元组。出于实现原因，我们进一步阻止在未本地定义的通道上接收消息。在我们对这种演算的扩展中，进程被分组到集合中，称为秘密会议。作为秘密会议c的一部分执行的进程P由网络项cfPg表示.网络C是在秘密会议中执行的进程的集合。120p 2参数：：=JP 2过程：：=jjjjJxn;c停止sendhp1;：;pkionp从P中的romn中接收（x1;：;xk）新的n在重复P（P1j P2）(a)核心pi演算变量名已停止进程消息接收作用域名称复制并联组成(b)pik演算的推广P 2流程：：=Jlogif cfLg then P1else P2lo gawait（x1;：;xn）cfLginP检查日志条目等待日志条目C2网络J：：=logappend hpk i with rule-name in P空附加到日志空网络JcfPg秘密会议进程JcfLg日志JC中的新n作用域名称二级日志条目J：：=（C1j C2）真j L1^L2平行组成，导线空对数，合取JJc1; c2预关闭 J 关闭（S） J 关闭c1紧接在c2没有更多的因果前身J预先承诺 j承诺（c）承诺协议J致力 j中止已提交，已中止J抗感染性（c;S）反承诺协议JUndoAdministrator（ S）反承诺管理员S2名称集J：：=撤销的 （c1）fp1;：;pkg准备撤销承诺图二. pik演算的推广除了将进程组织成秘密会议，这种演算的另一个创新是增加了稳定存储。在我们的演算中，稳定或持久的存储由多个定位命题表示，抽象地表示“日121志”中的条目每个秘密会议都有一个日志，由逻辑命题L的集合表示。一个日志是为一个名为c的秘密会议准备的，这一事实用一个“located”来表示122;空j CC C1jC2C2j C1（C1j C2）j C3 C1j（C2j C3）（ne wninC1）jC2ne wnin（C1 jC2）;n2=fn（C2）new n1in new n2in C new n2in new n1inCnewninCC;n2=fn（C）真^ LLL1L2L2 L1（L1^L2）^L3L1^（L2^L3）cfstopg空cfP1j P2g（cfP1g j cfP2g）cfn ne wninPg new nincfPg;n6=cstop j P PP1j P2 P2j P1（P1j P2）j P3P1j（P2j P3）（ne wninP1）jP2ne wnin（P1 jP2）;n2=fn（P2）新n1在新n2在P新n2在新n1在P重复P P j重复P图三. pik演算的等价规则格式cfLg的日志。日志命题的谓词名称被预先确定为演算的一部分，但是演算可以用其他形式的日志条目来扩展。pik演算的语义使用各种判断形式来指定P1P2L1L2C1 C2工艺等同性对数等同性网络等值图3图3图3C1！ C2计算图4C j= cfLg日志查询图4Cj=c c0故障依赖性c y图5C;（xk规则名）j=！cfLg日志附加规则图5、6、9123E[ ]：：=[ ] j（E[ ] j C）j newn inE[]C =E[1C0 ]C00C =E[ C]01 1222C1！(Red聪）（c1fsendhnkionng j c2freceive（xk）from romninPg）！c2ffnk=xkgP g(Red收）cfL0gj=cffnk=xk gL g（cfL0g j c0fl o gawait（xk）cfL g inP g）！（cfL0g jc0ffnk=xk gPg）(Red等待）(cfLgj c flogif cfLg then P 1else P 2 g）！0 00 0(RedIfLogTrue）（cfL0g j c0fl o gifcfL g thenP1elseP2 g）！（cfL0g jc0fP2 g）（红色IfLogFalse）C=（C0jcflo gappendhnki，规则名称在Pg jcfL1 g中）C;（xk）j=规则名称 cfL2！C！（C0jcfPg jcfL1^fnk=xkgL2 g）(Red追加）Cij=cfLg，对于某些i2f1;2g（C1j C2）j= cfLgn2=fn（L）[fcgCj=cfLg（C中的新n） j= cfLgLL0^L00cfLgj=cfL0 g(b)日志查询(PredPar）(Pred（新）(Pred日见图4。pik演算的基本语义进程和秘密会议的结构等价规则见图10。3.第三章。进程P的规则是pi演算的通常等价规则秘密会议的规则复制了进程的规则，还包括以下内容：cfstopg空cfP1j P2g124cfnn e ninPg nenincfPg; n6=c这些规则将进程与秘密会议联系起来;位于秘密会议中的进程集合等价于“原子”进程的集合，每个进程执行位于秘密会议中每个这样的原子进程具有cfPg的形式，其中P具有上述形式之一，并且其中c表示进程的在这个演算中，我们将进程带到作用域名称的重命名转换（重命名），因此假定进程和秘密会议上的所有替换都是避免捕获的。秘密会议与氛围有很多不同之处，我们只提到最相关的两个。首先，环境没有平行构图的分布规则。这反映了演算的不同目标：环境希望所有通信都是本地的，而我们不希望原子故障的边界干扰通信。因此，我们不会用“导航”秘密会议的操作来复杂化我们的演算，而这种导航是环境演算的核心。其次，秘密会议不能相互嵌套;我们不追求微积分的这种复杂性，因为不清楚这种扩展的动机是什么对这种嵌套的需求可能是出于对类似于嵌套事务的需求[37，35]。然而，嵌套的事务在全球计算环境中是足够复杂的，我们更喜欢从简单的概念建立它们，正如第二节中所提到的。7.第一次会议。一些操作需要检查秘密会议的所有日志条目，例如，以确保不存在特定的日志条目。因此，每个秘密会议c需要有一个单独的日志，形式为cfLg，其中L是日志条目的合取。与稳定存储交互有三种结构：P：：= logif cfLg then P1else P2jlo gawait（x1;：;xk）cfL ginPjlo gappendhp1;：;pki，规则名称在P这些构造的语义以及消息传递的语义在图1中提供4（a）. logif构造允许进程检查特定日志条目的存在除非小心使用，否则此构造存在明显的竞争条件这反映在（RedIfLogFalse）规则中，该规则允许条件式悲观地假设（可能是远程的）日志条目不存在。使用这种构造的应用程序必须考虑到这种假设有时是错误的。尽管有其局限性，这种构造在某些应用中是有用的，例如在第4节中提供的atf演算的翻译中，它用于轮询来自已提交进程的消息的通信信道。logawait构造会阻塞，直到与模式匹配的日志条目处于稳定存储中例如，可以指定撤消操作的形式为logawait（）cfAbortedg in P125如果秘密会议c被中止，那么进程P将执行，可能会取消被中止的秘密会议的一些影响。在操作语义中，await构造的转换规则具有以下形式：cfL0gj=cffnk=xk gL g（cfL0g j c0fl o gawait（xk）cfL g inP g）！（cfL0g jc0ffnk=xk gPg）(Red等待）这使用判断形式C0j=cfLg来查询命题L是否存在于秘密会议c的日志中。用于查询日志的规则在图4（b）中提供。这些规则相当直接地分解了所需形式的日志条目的周围上下文。日志查询规则的一般形式对于检查日志附加规则的前提条件非常有用，这些规则将在后续部分中提供。logappend构造用于添加到稳定存储的内容，在日志中添加条目。添加到稳定存储的操作由命名规则指定。每个规则都需要一些先决条件，并向稳定存储器添加一些新的命题集合。这些规则被预定义为演算的一部分，以确保操作语义的某些一致性属性。这些日志附加规则在图5、图6和图9中指定，使用判断形式C;（xk规则名）j=！cfLg其中rule-name是规则的名称，C是周围的上下文（用于检查先决条件），c是执行规则的秘密会议的名称，L是重写规则添加到存储器中的命题，x1;：;xk是L给出的模式中的自由变量。然后，改变存储的转换规则由下式给出：C=（C0jcflo gappendhnki，规则名称在Pg jcfL1g中）C;（xk规则名）j=！cfL2gC！ （C0j cfPg j cfL1^fnk=xkg L2g）（红色附录）秘密会议c只能添加到自己的日志条目中。可以在周围的上下文C中检查先决条件。此上下文包括c的log，cfL1g。对于某些规则来说，一个秘密会议可能有必要检查其他秘密会议的日志，尽管只有在积极的情况下（存在，而不是缺席，其他地点的日志条目）。在某些情况下，这可能需要与保存这些日志的远程站点进行 这些远程站点由网络xtC0的一部分捕获。应该对与远程日志的通信进行语义抽象。一种明显的方法是在“底层”发送和接收系统消息，可能是在应用程序消息的基础上这假定进程之间的点对点通信通道可用，但可能并不总是可用。我们在结论中对另一种方法进行了评论。关键在于，在这个模型中所做的唯一远程通信假设是进程能够查询远程进程的日志状态。126CommitEx1AbortEx1CommitEx2稳定存储在我们的演算是用来安全地保存状态的秘密会议，其中状态是记录了几个命题类型，因果关系，commitment协议状态等，作为一个初步的例子，我们已经指定了它意味着什么秘密会议提交或中止。在数据库应用程序中，中止意味着必须撤消更新并释放锁，而提交意味着必须将计划的更新写入数据库。我们把中止或提交的确切语义留给应用程序，只要求在秘密会议的中止或提交状态的存储中保留一个记录。对于一个与其他conclave没有因果依赖关系的conclave，我们可以提供两个重写规则，分别用于提交和中止：C j= cf中止gC;（）j=！委员会dgC j= cfCommittedg（红色提交Ex1）C;（）j=！中止dg（红色中止Ex1）这些规则是在检查重写规则的前提条件时能够查看本地秘密会议的所有日志条目的设施的示例，并且因此能够检查某些日志命题的缺失。这种查看所有日志条目的能力依赖于每个秘密会议具有单个日志的不变量对于一个有因果前导的秘密会议，如果秘密会议的所有因果前导都被提交，那么下面的重写规则允许秘密会议自己提交。以下规则的前件检查conclav ecave已提交的任何因果前件c0Cj=cfAbortedg（Cj=cfc0;cgorCj=c0fCommittedg）forallc02fn（C）C;（）j=！委员会dg(Red提交Ex2）本节中提供的日志附加规则仅是说明性示例。实际的规则在以下各节中提供。3因果关系在分布式系统社区中，因果关系已经被认为是分布式计算的重要推理，在描述全局状态，计算分布式快照，设计容错复制系统等方面[15，46]。传统上，因果关系的特征是由并发执行的顺序进程之间交换的消息引起的依赖性（例如，Lamport然而，在沟通层面跟踪因果依赖关系的方法前者可能127C j= cfPreClosedgC;（x）j=！cfx;cgC j= xfc; xgC;（x）j=！cfc;xgC;（）j=！cfPre关闭dg卡萨普雷(Red因果预测）卡萨尔·苏(Red因果成功）预关闭(Red已关闭）S=f 2019 -02 -22 00：00：0C） j C j= c; cgC=（ CkfLk g）00KCj=c0fPr e Closedg或Cj=c0fClosedgforc0 2SC;（）j=！关闭d关闭(Red已关闭）(a)计算规则C j= cfc1; c2 gC j= c; c(Pred因果日志）1 2C j= c;c(Pred因果关系C j= c; c C j= c; c1 223C j= c; c(Pred因果转换）1 3C j= cf闭合（S）gC j= cfClosedg(Pred已关闭）(b)日志查询规则图五. Pik演算中因果关系的语义由于通信系统外部的隐藏信道（例如，管道中的物理压力）而发生，而后者可能由于在发送的消息和就在消息发送之前接收的消息之间不存在因果依赖性（在应用层）而发生。Cheriton和Skeen [14]认为，所需要的是一种在应用程序级别而不是通信级别跟踪因果依赖关系的机制，因为应用程序可以知道隐藏的通道，并可以避免错误的依赖关系。考虑到原子故障和因果关系之间的联系，我们使用秘密会议作为在应用程序级别跟踪因果关系的机制因果关系不是消息发送和接收事件之间的关系，而是秘密会议之间的失败依赖关系：如果秘密会议失败，那么依赖于它的秘密会议也必须失败。此外，基于通信之间的通信来跟踪因果依赖性将是错误的。128;棍棒例如，不同机器上的两个秘密会议可以通过防火墙守护进程进行通信，但我们不希望防火墙守护进程因为它传递的消息失败而失败相反，我们允许应用程序本身断言秘密会议之间的因果依赖关系因此，没有可扩展的方法来防止因果依赖图中的循环。这对完成分布式秘密会议有影响为了保持因果一致性，秘密会议不能承诺，直到所有的因果前辈已经承诺或也愿意承诺。由于因果循环，可能需要几个秘密会议（因果图中强连接组件的所有成员我们要求每个秘会在一个特定的网络站点执行，但是秘会可以和其他站点的其他秘会交流因此，可能有必要在不可靠的网络上运行一个涉及多个秘密会议的原子提交协议由于这通常是一个无法解决的问题，我们采用了一种方法，可以作为广泛使用的协议，如两阶段提交和早期准备提交的基础当事务中止时，必须撤消其影响。如果对数据库进行了更改，则必须恢复更改的变量的先前值。我们并不提供自动的支持来撤销那些流产的秘密会议的影响除了数据库的特殊情况外，还不清楚撤销应该采取什么形式。例如，撤销资金转移可能涉及通过普通邮件发送律师函。在任何情况下，如果原始消息的接收者已经接受了对消息发送者的因果依赖性，则接收者将被阻止完成。因果关系被记录在存储器中，使用形式为cfc0;cg的定位命题，记录（在c的日志中）c 0是c的因果前趋。 这些命题由使用logappend构造的过程添加，使用图中的（Red Causal Pred）转换规则。五、 因果前导也可以有形式为c0fc0;cg的日志条目，记录它们的后继。 为了确保相互一致，我们要求记录因果后继者的日志条目通过记录因果前导者的日志条目的存在来证明。 这是通过（红色因果成功）规则的前件来强制执行的，该规则用于添加记录因果后继者的日志条目。 因果后继者日志条目是反承诺所必需的，如第2.2节所述。五、因果日志条目产生自反传递关系c1c2，有规则示于图五、有些决定必须基于秘密会议的所有因果关系都是已知的假设在做出这样的决定之后，不能添加因果前导。因此，我们添加了另一个日志条目类型cfClosed（S）g，它表示不能为秘密会议c添加更多的因果前驱，并且S（秘密会议名称的集合）是c的所有因果前驱的集合。我们还添加了另一个命题Closed，它是从前一个命题类型派生出来的，并且简单地表示因果前导集是封闭的。一个秘密会议不能自动关闭它的因果前身的集合，因为它的一个前身可能对因果扩展开放。秘密会议可以129等待直到它的每一个前任都被关闭，然后再关闭自己以进行进一步的扩展。然而，如果存在因果循环，这可能导致死锁因此我们增加了一个缓冲状态，PreClosed，一个秘密会议可以无条件地转换到当秘密会议的所有因果前身，包括秘密会议本身，都处于PreClosed状态时，转换到Closed这是由图中的（红色闭合）过渡给出的五、在后一个转移中，集合S是秘密体c的所有因果前趋者的集合，逆传递封闭。转换规则要求所有这些前置任务的日志都在日志追加操作的上下文中。 这是为了检查所有的precedent都是因果关闭的或准备关闭的。如果这个条件得到满足，秘密会议c就成为因果性的关闭。其他因果闭包的协议可以建立在这个框架之上，使用因果关系的传递性来修剪日志。例如，一个秘密会议必须有证据表明，它的所有因果前身，而不仅仅是它的直接因果前身，要么处于封闭状态，要么处于封闭如果一个秘密会议是因果封闭的，那么它的所有因果前身都是封闭的，利用这个属性，协议可以将其注意力限制在因果图的强连接组件中的所有秘密会议上。强连接组件的协调器可以使用两阶段提交协议来检查组件中的所有秘密会议都是预先关闭的，并且组件外部的所有直接因果前导都是关闭的，以授权组件中的秘密会议转换到关闭状态：关闭关闭关闭关闭预封闭预封闭预封闭预封闭预封闭在这幅图中，节点表示处于各种状态的秘密会议（因果关闭，预先关闭），边缘表示因果依赖关系，而大椭圆表示相互依赖的秘密会议的集合，这些秘密会议可以使用某种原子提交协议进行合作以实现因果关闭，使用这个集合之外的前任秘密会议已经关闭的事实130C j= cfPreClosedg(Red在StUndo）CAtStUndo;（）j =！cfUndoablegCj=cfLgforL2fPr e Committed;Committed;UndoPr e epad（c）UndoAdministr ator（S）g0;CAtStAbort;（）j =！cf中止g(Red在StAbort）Cj=cfLgforL2fAbortedd;UndoPr epar ed（c）UndoAdministr ator（S）g0;CAtStPreCommit;（）j =！cfPreCommittedg(Red在StPreCmt）Cj=c0cCj=c0f流产dg;(Red在PcAbort）CAtPc中止;（）j =！cf中止gC j= cfPreCommittedg C j= cfClosed（ S） gCj=cfLg，对于L2fUndoPr epar ed（c0）UndoAdministr ator（S0）g;（Cj=c0fClosedgandCj=c0fPr Committedg）或Cj=c0fCommittedgforc0 2S（Cj=cfc0cg或Cj=c0fCommitable（c）g），对于c0 2S;CAtPcCommit;（）j =！cfCommittedg(Red在PcCommit）(a) 计算规则Cj=c0fPr e Closedg和（Cj=c0fUndoableg或Cj=c0fc0cg）;Cj= c0f可承诺e（c）g(Pred在PcCommit）(b) 日志查询规则见图6。Pik演算中承诺的语义4承诺秘密会议封装了一组进程，这些进程执行一些最终成功或失败的操作。我们把这些选择称为承诺和堕胎。承诺建立在因果关系之上，因为秘密会议不能承诺，除非它的所有因果前任都承诺。如果秘密会议的所有因果前身都处于Committed状态，那么定义一个允许转换到Committed状态的转换规则是很有诱惑力的然而（与因果闭合一样）如果存在因果循环，这是不够的与因果闭包一样，我们引入了一个缓冲状态PreCommitted，处于启动状态的秘密会议可以无条件地过渡到该状态-131ally（图中的Rule（RedAtStPreCmt）6）。当所有因果前置任务都已提交或已预提交且因果关闭时，将启用到已提交状态的转换（Rule（RedAtPcCommit））。（RedAtPcCommit）规则的前件的最后一行引用了反提交，在下一节中将进行更详细的描述 如果一个秘密会议是可撤销的（它可以随后被取消提交），那么提交规则要求在日志中记录它的直接因果前导（所有其他秘密会议只需要记录直接因果后继，因果关系从其推导出来）。前面提到的最后一行要求，如果c0 是c的直接因果前驱，则c必须相对于c 0是可提交的（由c0处的派生日志条目Commitabl e（c）表示）。 使用（PredAtPcCommit）规则定义的后一个日志条目声明concl av ec0是因果关闭的，并且如果c 0是可撤消的，则具有记录c作为直接后继者的日志条目。在检查可撤消性条件的同时检查c 0上的闭合条件可确保c0随后无法被撤消。与因果关闭相反，也有可能过渡到Aborted状态。一个尚未预提交的秘密会议可以无条件中止（规则（红色在StAbort））。 处于预提交状态的秘密会议只有在其因果前身之一已经中止时才能中止（规则红色AtPcAbort）。一个秘密会议可能的状态转换总结开始预先承诺致力中止从提交状态到中止状态的过渡是由anticommission- mitment提供五、示例：分布式事务。暂时忽略锁定的各个方面，我们将分布式事务[5]定义为一个秘密会议的集合。在最初的地点有一个家长秘密会议，用于开始该事务调用远程站点上的操作;远程站点上的事务的每个实例由该远程站点上的一个秘密会议表示，该秘密会议由父秘密会议产生。每个子秘密会议都接受父秘密会议的因果依赖关系，反之亦然。在trans-action结束时，父秘密会议执行两阶段提交协议：(i) 父秘会充当协议的管理者。它联系每一个孩子秘密会议，诱导后者进入预提交状态，并确定是否有孩子失败。(ii) 如果所有的孩子都进入了预先承诺的状态，132由管理员管理并传递给孩子们。后者使用此证据进入已提交状态。否则，管理员中止并诱导其余子节点中止（进入中止状态）。示例：拆分-联接事务。这样的事务支持将事务分成两个事务的拆分操作，以及执行相反操作的联接操作[40]。我们可以定义一个分割操作，如果我们扩展演算，使用下面的操作来P 2过程：：= cfPgJ loginit in P与操作规则c 1 fc 2 fPgg！c 2 fPg（Red Exec）C=ckfPkgc2=fck gnewcin（cfloginit in Pgj C）！newc in（cftruegj cfPgj C）（Red LogInit）派生构造cfPg仍然不意味着任何conclave的嵌套，相反，它只是一种conclave挤出 在另一个 conclave中执行的代码的方式 loginit构造允许为conclave创建初始空日志。对上下文C的语法限制和pi演算的静态作用域规则然后定义（将c拆分为P2，然后拆分为P1） (new c in（cfloginit in P2gj P1））然后c1f在p2中拆分c2然后p1gc1f在c2中新建c2在p2中floginit在p2g jp1g新的c2in c1fc2floginit in P2gj P1gnew c2in（c1fc2floginit in P2gg j c1fP1g）！new c2in（c2floginit in P2gj c1fP1g）！ne wc2in（c2ftrueg jc2fP2g jc1fP1g）：连接操作是通过使两个事务的秘密会议变得相互依赖来提供的。例如：ATF演算。atf演算[18]是一种进程演算，其核心组织原则是原子故障，保证可以从任何执行跟踪导出无故障的执行跟踪这个例子演示了如何在pik演算的原语之上构造具有原子故障的特定编程模式atf演算的语法由下式给出：133A2进程：：=停止j重复A j（A1jA2）j新的x在A j发送hpk i在p j接收（xk）从n在A j接收提交（xk）从n在AJ prepare j abort j commitT 2事务：：= T中新的空j tfAg j tfLg j（T1j T2）jL 2 Log：：= true j L1^L2j tflogreg j tfabortg j tfcommitgj（t1fsend h nk i on ngj t2freceive（xk）from n inAg）atf演算的语义如图所示。7.第一次会议。除了用于停止进程、复制、并行合成、新名称生成和消息传递的通常操作之外，还有用于中止和提交事务的操作提交类似于早期准备提交协议[48]，其中参与者准备提交，然后管理员决定参与者是否应该提交。 它也类似于pik演算中的完成，除了后者有更多的自由度让应用程序决定何时进入承诺协议的阶段。准备操作将参与者置于准备好的状态，由形式L（tfreg）的日志条目记录。一个参与者可以提交，如果它的所有因果前导者要么已提交要么已准备好。如果参与者的任何因果前导者已中止，则参与者可以中止。参与者可以在进入准备状态之前的任何时间自主中止。与pik演算一样，也有tfLg形式的对数，每个trans-action最多一个。有四种日志条目类型，格式为tfAg。其中三种日志条目类型记录事务是处于准备、提交还是中止状态。第四个日志条目类型记录事务t2中的进程接收到事务t1中的进程发送的消息。此日志条目类型隐式地记录了从t1到t2的因果依赖关系;它还可用于撤消已中止事务的影响，重新传输事务在中止之前收到的任何消息。这是由图中的（红色ATF撤销）规则完成的。7.第一次会议。接收消息有两种操作。第一个操作对应于接收消息并接受对发送事务的因果依赖。如果事务已经进入准备状态，则它通常不能接收新消息，因为这可能会对事务引入新的因果依赖关系，然后可能会中止，使任何早期的提交决策无效。这是由（红色ATF接收）规则中的先行项强制执行的。然而，第二个消息接收操作将接收到的消息限制为那些由已提交事务发送的消息（因此进程可以将其自身与未提交事务的影响隔离开）。一旦事务进入准备状态，它就只能接收来自其他已提交事务的消息。这防止在提交事务时引入进一步的因果依赖性，并且防止已提交事务获得对中止事务的因果依赖性这是由（红色ATF RecvComm）规则强制执行的，用于仅接收来自已提交事务的消息。对于消息接收操作的第一种形式，在接收事务中保存日志，既记录因果依赖关系，134以允许在接收器随后中止的情况下撤销消息接收。我们不记录消息接收操作的第二种形式，因为这样的事件不会影响可提交性，并且永远不会撤消（发送者永远不会中止）。剩下的规则相当简单。（Red ATF Abort）和（Red ATF Prepare）规则分别允许事务中止或进入准备状态，前提是它尚未进入任何其他状态。（红色ATF PrepAbort）规则允许事务在处于准备状态时中止，如果其因果前导之一已中止。（Red ATFCommit）规则允许事务提交，前提是它的所有因果前导都处于预提交状态或已经提交。最后，（红色ATF撤销）规则允许在接收过程中止后使用日志撤销消息接收atf演算到pik演算的转换在图中提供四、这种转换是使用各种元函数指定的T[[T]]将交易翻译成秘密会议T[[L]]将日志条目转换为撤消代码L[[L]]S将atf演算日志转换为pik演算日志P[[A]]t将atf演算过程转换为pik演算过程事务T[[T] 的转换通过从每个当前可见事务t到其直接因果关系的集合的映射来参数化当转换生成Closed（S）形式的日志条目时，这用于计算因果前导S的集合。对于日志L，转换T[[L]构造了一个进程的集合，该进程等待相应的事务中止，然后重新发送该事务接收转换L[[L]]S从atf演算日志条目转换当应用于atf演算中的日志时，顶级转换T[[T ]]c调用上述两种转换;否则，唯一其他有趣的情况是对于进程，其中它调用从atf演算进程转换到pik演算进程的转换P[[A]]c在后一种转换中，在第一个消息接收操作的转换中，消息被增加了发送消息的事务的秘密会议标识符，并且这在接收者处被用来记录发送者和接收者之间的因果依赖关系。对于第二个消息接收操作，即只从已提交事务接收消息的接收-提交这就是我们使用logif结构的地方，并证明了它的有用性，即使在存在日志条目的情况下，该结构也可能不确定地选择假分支：在这种情况下，该过程只是循环再次检查条件，以获得通道上的另一条消息。执行此轮询的进程由递归元函数RECVCOMM定义;这可以以通常的方式转换为非递归进程描述[36]。135T1=t1fsendhn1;：;nkionngT2=t2freceive（x1;：;xk）fromr omninPgt2fLg 6j=t2 fLag regT1jT2jt2fLg！t2fL^（T1jT2）g jt2ffnk=xkgPg(Red ATF接收）T1= t1 fsend hn1;：; nk i on ng T2= t2 freceive committed（ x1;：; xk） from n inPg t1 fLg j= t1 fcommittgT1jT2jt1fLg！t1fLg jt2ffnk=xkgPg(Red ATF RecvComm）tfLg6j=t fpreg;t fcommitgtfabortgjtfLg！tfL^tfabortggtfLg 6j= tfabortgtfugregjtfLg！tfL^tfbn reggtfLg 6j= tfcommitg(Red ATF中止）(Red ATF准备）TjtfLgj=tfpreg;tfabortg;t;t00tfabortgjtfLgj T！tfL^tfabortgg(Red ATF准备中止）S=ft g=f t2 fn（ T） j T j= t; tg T= tk fLk g000KT= T0 j tfLgTj=tfp r epa regTj=t0fcommi tg或Tj=t0fp r eparegfort02Stfcommitgj tfLgj T0！tfL^tfcommittgg j T0(Red ATF提交）T1= t1 fsend hn1;：; nk i on ng T2= t2 freceive（ x1;：; xk） from n inPgt 2 fL^（T 1j T 2）^t 2 fabortgg！T 1j t 2 fL^t 2fabortgg(Red ATF撤消）(a)计算规则2016年02T j T） g j= t;21 21 2(Pred ATF因果假说）(b)日志查