（计算机科学与技术专业论文）基于异步π演算的两阶段提交协议的形式化描述和验证.pdfVIP

国防科学技术大学研究生院工学硕士学位论文 摘要 兀演算是r m i l n e r 等人在c c s 的基础上提出的传名演算，可描述通信拓扑 结构动态变化的并发通信系统，因此也被称为移动进程演算。胥演算与c c s 的不 同之处在于允许进程之间传送和接收通道名，并且可以引入和输出局部名，因而 具有简洁和表达能力强的突出特点弘演算已作为研究并发通信系统的基本工具， 被广泛用于并发分布式系统和通信协议的形式化描述和验证中。而异步开演算是一 种消息发送不受阻塞的哥演算。 原子提交协议是分布式事务处理中一个用于确保一致性的算法，即协调者和 所有的参与者要么都提交事务，要么都撤销而两阶段提交协议是最简单且最常 用的原子提交协议，该协议使分布式事务的提交具有原子性和持久性，并且允许 每个事务管理器有权单方面决定中止还没有准备提交的事务。 本文的目的就是要用异步冗演算来描述和验证两阶段提交协议。为了使这种刻 画、分析和验证工作更详细、更准确、更完整，本文首先对异步小演算进行了如下 几个方面的扩展： 1 增加了站点的定义； 2 增加了站点失效和恢复等相关规则； 3 增加了计时器的定义； 4 增加了站点问的消息丢失、消息复制等相关规则。 然后，本文依次对两阶段提交协议的各种情况( 不考虑失效，考虑站点失效和 消息失效等) 进行了深入讨论和分析，并分别用上述扩展的异步静演算对两阶段提 交协议进行了形式化描述和验证。 本文的工作表明两阶段提交协议能确保分布式事务处理中的一致性。在只有 局部站点失效或局部通信失效的情况下两阶段提交协议有可能发生阻塞，但这并 不影响其正确性。 主题词：分布式系统形式化方法异步矿演算互模拟两阶段提交协议 第i 页 国防科学技术大学研究生院工学硕士学位论文 a b s t r a c t 兀- c a l c u l u s ，p r o p o s e db yr m i l n e ra n dh i sf e l l o w s ，i san a m e - p a s s i n gc a l c u l u s w h i c hi si n h e r i t e df r o mt h ed e v e l o p m e n to fc c s i tc a nn a t u r a l l ym o d e ic o n c u r r e n t s y s t e m sw h i c hh a v ed y n a m i cc o m m u n i c a t i o ns t r u c t u r e ，w h i c hi sw h yi t i sc a l l e da c a l c u l u so fm o b i l ep r o c e s s e s t h ed i s t i n c t i o no f 兀一c a l c u l u sc o m e sf r o mt h a ti tp e r m i t s t r a n s m i s s i o no fc h a n l l e ln a m e sb e t w e e np r o c e s s e sa n dc a ni n t r o d u c ea n de x p o r tl o c a l n a m e s i ti sc o n c i s ea n dh a sr i c he x p r e s s i o np o w e r 7 【- c a l e u l u sh a sb e e nu s e da sa n e s s e n t i a lt o o li ns t u d y i n gc o n c u r r e n tc o m m u n i c a t i o ns y s t e m s i ti sw i d e l ya p p l i e dt o f o r m a l d e s c r i p t i o na n dv e f i f l c m i o no fc o n c u r r e n ta n d d i s t r i b u t e ds y s t e m sa n d c o m m u n i c a t i o np r o t o c o l s t h ea s y n c h r o n o u s 兀c a l c u l u si sav a r i a n to ft h e7 c c a l c u l u s w h e r em e s s a g ee m i s s i o ni sn o n - b l o c k i n g a na t o m i cc o m m i t m e n tp r o t o c o li sa na l g o r i t h mt h a te n s u r e sc o n s i s t e n c y i ti sa n a l g o r i t h mf o rt h ec o o r d i n a t o ra n dp a r t i c i p a n t ss u c ht h a te i t h e r , t h ec o o r d i n a t o ra n da l l p a r t i c i p a n t sc o m m i tt h et r a n s a c t i o n , o rt h e ya l la b o r ti t n et w o p h a s ec o m m i t p r o t o c o li st h es i m p l e s ta n dm o s tp o p u l a ra t o m i cc o m m i t m e n tp r o t o c 0 1 i tg u a r a n t e e s t h ea t o m i c i t ya n dd u r a b i l i t yi nt h ec o m m i t m e n to fd i s t r i b u t e dt r a n s a c t i o n s i tp e r m i t s a n yt r a n s a c t i o nm a n a g e rt ou n i l a t e r a l l yd e c i d et oa b o r tt r a n s a c t i o n sw h i c hh a v en o tb e e n c o m m i t t e d n ep u r p o s eo ft h i sp a p e ri st od e s c r i b ea n dv e r i f yt h et w o - p h a s ec o m m i t p r o t o c o lb a s e do na s y n c h r o n o u s 耳- c a l c u l u s i no r d e rt oc r e a t em o r ed e t a i l e d ，p r e c i s ea n d i n t e g r a lw o r k , w ee x t e n dt h ea s y n c h r o n o u sn - c a l c u l u sw i t i l 1 s i t ec o n c e p t i o n , 2 t h ep o s s i b i h t yo fs i t ef a i l u r ea n dap e r s i s t e n c em e c h a n i s mt od e a lw i t hs i t e f a i l u r e s ， 3 t i m e rc o n c e p t i o n , 4 t h e p o s s i b i l i t y o fm e s s a g el o s sa n dm e s s a g ed u p l i c a t i o ni ni n t e r - s i t e c o m m u n i c a t i o n w ed i s c u s sa n da n a l y z et h et w o - p h a s ec o m m i tp r o t o c o li ns e v e r a lc o n d i t i o n s ( i n c l u d i n g ，n oa n yf a i l u r e ，s i t ef a i l u r e ，m e s s a g ef a i l u r e ，e t c ) ，a n dc l e a r l ya n d i n c r e m e n t a l l yr e p r e s e n tt h et w op h a s ec o m m i tp r o t o c o li nt h ea s y n c h r o n o u sn - e a l c u l n s t h ew o r ko ft h i sp a d e ri n d i c a t e st h a tt h et w o p h a s ec o m m i tp r o t o c 0 1c a ne n s u r e t h ec o n s i s t e n c yi nt h ed i s t r i b u t e dt r a n s a c t i o np r o c e s s i n g b l o c k i n gm a yo c c u ro n l yi na p a r t i a ls i t ef a i l u r eo rm e s s a g ef a i l u r e ，b u tt h ec o r r e c t n e s si ss t i l la s s u r e d k e yw o r d s = d i s t r i b u t e ds y s t e m ，f o r m a lm e t h o d ，a s y n c h r o n o u s 尢一c a l c u l u s ， b i s i m u l a t i o n ，2 p c p 第i i 页 国防科学技术大学研究生院工学硕士学位论文 表目录 表2 1 自由名和约束名( 异步兀演算) 表2 2 结构同余( 异步兀演算) 表2 3 变迁规则( 异步兀演算) 二7 表4 1 自由名和约束名( 异步7 c 演算扩展1 ) 。2 1 表4 2 结构同余( 异步尢演算扩展1 ) 。2 1 表4 - 3 变迁规则( 异步兀演算扩展1 ) 。2 3 表5 1 自由名和约束名( 异步小演算扩展2 ) 。3 3 表5 2 结构同余( 异步冗演算扩展2 ) 表5 3 变迁规则( 异步兀演算扩展2 ) 一3 5 第1 i i 页 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得 的研究成果尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含 其他人已经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它 教育机构的学位或证书而使用过的材料与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示谢意 学位论文题日：基王是生巫二渲簋盟煎睑壁量塞盐遮鲍星盎垡拦鎏狸坠适 学位论文作者签名： i 塾生垒 日期：2 0 0 6 年5 月1 0 日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定本人授权 国防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子 文档，允许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据 库进行检索，可以采用影印缩印或扫描等复制手段保存、汇编学位论文 ( 保密学位论文在解密后适用本授权书) 学位论文题目：蕉土是生速簋盟煎睑基握塞垃遮鲍理耋丝整鲨塑坠适 学位论文作者签名： ；迳丛 日期：2 0 0 6 牟- 5 月1 0 日 作者指导教师签名： 日期：2 0 0 6 年5 月1 2 日 国防科学技术大学研究生院工学硕士学位论文 第一章引言 1 1 并发分布式系统 随着计算机技术和网络通信技术的高速发展，以并发性、分布性、实时性、 异构性和互操作性等为主要特征的并发分布式系统己成为当前计算机技术的主流 方向，并已得到广泛应用。由于并发分布式系统本身非常复杂，因此其开发过程 不仅难度大，效率低，周期长，而且很难避免和发现其中隐含的错误和缺陷。对 于安全攸关系统( s a f e t yc r i t i c a ls y s t e m s ) ，其正确性就更为重要。 并发，顾名思义，指的是多个活动同时发生的现象简单的说，具有并发行 为的系统都可称为并发系统。本文主要关心由多个计算主体组成，以通讯实现协 作以共同完成计算任务的系统。 早期的计算机主要用于数学计算，例如计算一个复杂的函数，求解一个方程 或方程组等等。因此，人们关心的是给定输入数据，程序运行完以后的结果是什 么，答案是否正确这时的程序只被看作一个从输入值到输出值的转换器，并且 一旦给定输入值，程序的运行过程和结果就是确定的，这就是我们通常所说的串 行( 顺序程序的概念。对于两个串行程序来说，如果它们对所有相同输入值的 计算结果都相同，则可以认为这两个程序在函数的意义下是相互等价的。也就是 说，对这类程序的区分，需要考查的只是程序的输入和输出，而程序执行的细节 过程则并不重要。另外，串行程序的正确性除了要求程序对给定输入必须得到符 合要求的输出结果外，还要求程序一定在有穷时间内终止。 但是随着技术的发展，计算机被用于更广泛的领域，在我们身边，从家电、 电话到互联网等各种控制系统和通信系统，其中许多程序己不再像串行程序那样 只需关心输入和输出：它们总在和其它对象及系统进行着通信和交互，它们的执 行结果往往依赖于更多的环境因素；或者即使把这些环境的影响都看成是输入， 那么这些输入也会因为顺序和时间上的差别而导致程序的执行结果变得不确定。 这些都是由于程序并发执行所造成的结果不管是紧密耦合的并行系统还是松散 耦合的分布式系统，都可以看作是并发系统。 ， 在并发系统中，需要解决的问题有很多，例如通讯实体之间传送数据带来的 问题，以及进程发生移动所带来的问题，这些都是当前国际并发领域研究的热点 和难点所在。对并发程序的基础研究主要是寻找能够准确并有效的解决上述问题 的数学工列”。 在并发系统中，除了可以在进程之问传送数据外，还存在进程或计算发生移 动的情形，从计算本质上来看，这也可看作是通信拓扑结构随着计算而动态改变 第1 页 国防科学技术大学研究生院工学硕士学位论文 的并发系统。例如，在i n t e m e t 上，如果甲本来不知道乙的联络方式( 甲和乙本来 无连接) ，但经过访问丙的网页后，通过丙网页上的超链接与乙建立了连接，从 而可以把本来在丙处进行的计算移动到乙处继续，等等这些都可归为移动计算的 范畴目前已有的能刻画移动计算的形式模型有m 演算 2 3 a i 、j o i n 演算嘲以及m o b i l e a m b i e n t s l 6 1 等等，它们从不同的角度对移动计算进行了刻画。m i l n e r 等人提出的移 动进程演算氕演算中，通过传递名字可以改变系统的通信拓扑结构，从而能描 述一般的移动计算行为。 分布式 1 , 8 1 是并发的一种，特指并发实体间不通过共享存储器而以消息传递的 方式实现交互。但是分布式系统中一些常用操作并不能用传名的形式表示，如站 点失效恢复，消息失效以及计时器等等。因此本文对异步开演算进行了扩展，并 对一个典型的分布式协议两阶段提交协议进行了形式化描述和验证。 1 2 形式化验证 随着计算机系统规模的不断增大，功能日趋复杂，系统开发中出现错误和问 题的可能性也越来越大，因而给系统的开发和维护带来了许多困难。为了提高系 统的可靠性，对系统进行严格的验证正越来越受到广泛的重视。目前在实际中， 人们普遍采用的方法是对系统进行大量的测试，通过输入多个测试用例并检查执 行结果是否正确来发现系统中可能存在的问题，但是这种方法在验证系统时通常 无法穷举系统所有可能的行为。因此人们提出了形式化验证的方法，希望借助数 学工具来完成系统的验证工作，即通过定义了各种系统的模型和语义( 行为) 后， 采用基于数学方法的技术和工具对系统进行严格的分析和验证。使用这种方法， 可以增进对系统的了解，帮助发现系统中存在的问题，有助于系统的开发和维护， 这种方法通常被称作形式化方法( f o r m a lm e t h o d ) 9 1 。 形式化验证主要包括演绎验证( d e d u c t i v ev e r i f i c a t i o n ) 和模型检测( m o d e l c h e c k i n g ) 两类方法，它们分别基于定理证明( t h e o r e m p r o v i n g ) 和状态搜索( s t a t e e x p l o r a t i o n ) 两种思想。 演绎验证使用逻辑公式来描述系统及其性质，采用由公理出发推导出最终性 质的过程，来实现对系统的验证，在该过程中还往往需要用户提供或引入某些定 义或引理。演绎验证的优点是可以使用归纳的方法来处理无限状态的问题，并且 证明的中间步骤使用户对系统和被证明的性质有更多的了解；其缺点则是一般不 能够做到完全自动化，还需要与用户交互，导致证明过程相当耗时且容易出错。 模型检测的基本思想是状态空间的穷尽搜索，搜索的可穷尽性有赖于为系统 建立有穷状态的模型或可归结为有穷状态的模型；这为建模造成了一定难度，但 能保证搜索过程的终止。模型检测的优点是完全自动化。即使是只给出了部分描 第2 页 国防科学技术大学研究生院工学硕士学位论文 述的系统，通过搜索也可以提供关于已知部分正确性的有用信息。尤其重要的是， 在性质未能被满足时，搜索终止时可以给出反例这种信息常常反映了系统设计 中的细微失误，因而对于用户排错有极大的帮助。这类方法的缺点是状态爆炸问 题一所谓状态爆炸问题，在这里主要指的是系统状态数随并发分量的增加呈指 数增长的问题，所以需要采用各种手段消减算法搜索的状态数。 演绎验证和模型验证有各自的特点和优势。模型检测由于其自动化程度高等 优点而为用户所青睐，而演绎验证则在一些情况下可处理无限状态的问题，因而 也具有独特的优势。本文在形式化验证中将详细讨论互模拟技术常用于并发 理论中判定形式规约和系统实现之间的行为等价的一种标准技术，这种技术也可 被视为一种广义的模型检测翻。 1 3 课题研究的主要内容 本文的目的就是要用异步兀演算来描述和验证两阶段提交协议。 本文的主要的工作有： 1 使用异步兀演算对不考虑失效的两阶段提交协议进行了形式化描述， 并证明了其实现和规约是弱互模拟的。 2 考虑到分布式系统中的站点失效，对异步m 演算进行了扩展，增加了 站点和挽救点的定义，并增加了站点失效和恢复等相关规则，并用扩 展的异步7 【演算对考虑站点失效的两阶段提交协议进行了形式化描述 和验证。 3 考虑到分布式系统中为控制消息失效等而设置的计时器，对异步兀演 算再次进行了扩展，增加了计时器的定义，并增加了消失丢失和消息 复制等相关规则，并用扩展的异步1 1 ：演算对考虑各种失效情况的两阶 段提交协议进行了形式化描述和验证 1 4 论文结构 本文共分六章。 第l 章引言。介绍了课题的研究背景和意义，提出了课题的研究目标，说明 了研究的内容。 第二章异步7 c 演算。介绍了异步7 c 演算的基本理论，包括异步7 c 一演算特点和 思想简介、异步兀演算语法、异步n 一演算语义和异步兀一演算的行为等价理论。 第三章使用异步冗一演算验证2 p c p ：不考虑失效。使用异步兀一演算对不考虑失 效情况的2 p c p 进行了形式化描述，并对其正确性进行了验证 第3 页 国防科学技术大学研究生院工学硕士学位论文 第四章使用异步矿演算验证2 p c p ：考虑站点失效。对异步矿演算进行了扩展， 在语法上增加了站点、失效和挽救点的定义，在语义上增加了失效、恢复等迁移 规则，并使用扩展的异步矿演算对考虑站点失效的2 p c p 进行了形式化描述和验证。 第五章使用异步7 r 演算验证2 p c p ：考虑消息失效。对异步7 r 演算在第四章的 基础上再次进行了扩展，在语法上增加了超时装置的定义，在语义上增加了消息 丢失与复制等迁移规则，并使用扩展的异步兀一演算对完整的2 p c p 进行了形式化描 述和验证。 结束语总结了课题的主要工作，并对课题后续的发展提出了自己的看法。 第4 页 国防科学技术大学研究生院工学硕士学位论文 第二章异步7 c 演算 本章介绍移动进程代数异步兀一演算的基本理论，奠定后续研究工作的理论基 础。具体内容包括异步兀一演算特点和思想简介、异步7 r 演算语法、异步矿演算语 义和异步矿演算的行为等价理论。 2 1 引言 计算模型一直是计算机科学研究的重要问题。卜演算是顺序计算的经典模型。 而矿演算瞻”1 是九十年代计算机并行理论领域最重要的并发计算模型，它是r o b i n m i l n e r 等人在c c s “”的基础上提出的传名演算，可描述通信拓扑结构动态变化的 分布式通信系统( 例如移动电话系统) 。它允许进程之间传送和接收通道名，并 且可以引入和输出局部名。因此，矿演算不仅非常简洁，而且具有很强的表达能 力。 伴随通信系统和网络分布计算的发展，许多计算都涉及交互，并因此涉及具 有多个并发活动构件的软件系统。而传统的计算模型，如图灵机和卜演算，它们 在交互系统的建模方面存在不足，它们的基本活动是读取存储器或函数应用，却 无力描述交互和并发执行的软件系统。因此，7 r 演算应运而生，它旨在成为交互 并发系统的理论基础，并因此采用交互作为它的基元( p r i m i t i v e ) ，如同九一演算 采用函数应用作为它的基元。 7 r 演算的另外一个特点是描述移动和结构变化的计算系统。移动能够分为两 类，一类是进程之间的移动，另一类是进程自身移动。矿演算能够直接表达连接 移动，若通过编码，就能够表达进程移动。 名字是矿演算中最基本的概念。与传值c c s 不同，丌- 演算将数据值、数据变 元、输入参变元以及传递数据的通道不加区别，一律作为名字来处理。直观上名 字即对象的引用，一个进程所具有的自由名代表了该进程当前所拥有的关于其它 进程的知识或与其它进程的联系。在7 r 演算中，所有复杂数据类型以及基本函数， 都可以通过编码定义，而不需要作为基本对象。 因此，7 c 一演算是移动、交互、并发系统的理论模型，它提供相关的概念框架 和数学工具，用于表达移动、交互系统和推论它们的行为，增强对移动系统的理 解。 异步7 【演算 1 2 , 1 3 , 1 4 , 1 5 1 是7 【演算的一个变体，其消息传递( 通信) 的实现方式是 异步的，即发送与接受动作不一定同时发生。它没有非确定性选择和输出前缀， 但是其进程间的交互模型与兀演算是基本一致的。正是由于没有输出前缀，异步舻 第5 页 国防科学技术大学研究生院工学硕士学位论文 演算的输出动作与其他动作只能并发执行，因此不能控制其具体执彳亍时间。 2 2 异步兀演算基本语法 进程演算是一种以代数方式刻画抽象程序的形式语言。它包含一系列满足一 定代数性质的组合算子和元素，并将相应代数系统中的表达式( 项) 称为进程。 我们约定为名字工，弘z ，v ， 的可数无穷集。x 是单个名字，i 与工互为对 偶名字，进程通过对偶名字进行交互。歹是多个名字组成的元组。下面我们用b n f 语法给出异步矿演算进程表达式的定义： p ：= o l 双歹) l 工( 歹) e l ! x ( y ) p , = y e l pip l ( o , ) p 进程构造算子的直观意义如下： 0 代表一个没有任何动作的进程； 孑 表示一个输出动作，在通道x 输出i i 元向量歹( 歹是y 。n 以的简 写) ，异步7 r 演算中输出动作是没有后继的； “萝) ，表示进程有一个输入前缀，在通道x 等待一个疗元向量歹的输入； p ip 表示两个进程的并发合成； ! 工 ) p 表示可数无穷多个x ) ，的并发合成； i x = ) ，l p 表示先对x 和y 进行比较，若相等则演化为p ，否则为o ； “w ) p 把名字x 的作用域限制在p 中。 该语言有两个约束构造：限名( v x ) e 和输入x ) j 分别将x 和歹约束在p 中。 进程p 的约束名字集和自由名字集分别用b n ( p ) 和f n ( p ) 表示，定义见表2 1 仅在 约束名字上不同的进程称为伽等价的，用黾表示。我们将不区分a 等价的进程。替 换是从到的部分映射，用a 表示。替换是后缀算子，其优先级高于语言中其它 的任何算子。 表2 1 自由名和约束名( 异步m 演算) 力( o ) = a 乃g ) = k 刃 力g ( 乃p ) = 缸) u o 螽( p ) 、舻) ) 力o z ) p ) = 扛) u ( p ) 、侈 ) 加 = y 】p ) = 扛，y ) u 办p ) 办p i 翻= 乃u 加( q ) 力( ( ) p ) = 乃( p ) 、 砌( o ) = g 砌( i ) ) = a 6 弗g ( 哥) p ) = 6 一p ) up 6 o 石( 乃，) = 6 丹( p ) u p 砌 = j ，h = 砌( p ) 砌c p lq ) = b n ( p ) u b n ( q ) b n ( ( t r x ) p ) = b n ( p ) l o ( x 定义2 2 1 ( 结构同余) 结构同余；是由表2 2 中的规则生成的进程上的最小 第5 页 国防科学技术大学研究生院工学硕士学位论文 同余关系。 表2 2 结构同余( 异步m 演算) a l p h ap ；qi f p ；。q p 0p 0 ；p p 1p i q s q i pp 2p l ( q i r ) - ( p l q ) r r o ( o x ) o - = 0 r ib x p i q ) ；尸l b ) qi f x 盛乃( p ) i 匕b ) ) p ；( 吵) b 妒r 3 ( v x ) ( a e ) - a ( ) x ) p 西x 正办( 口) u 6 n ( 口) r 4b ，) 0i f x i s t h e s u b j e c t o f a d ob c p i 工卅h p m ob = y 】p ；oi f x a n d y a r e d i s t i n c tm lb = 巾i p p l r - q i ri fe q( u x ) p = ( l 珥) qi fp o 引理2 2 2 若x 仨力( p ) 则 ) 尸z p 证明：b ) p ；( o x x p l o ) ；p l 缸) o z p l 0 ；p 2 3 异步兀演算迁移关系 进程演算的语义通常以加标迁移的方式给出，即通过一系列类似p l p r 的 表2 3 变迁规则( 异步m 演算) i 仃) 马o m a t c h 嵩 矾丽万j 西硼工( 哥) p 三i 1 2 p 拓哥 p a r p - - - - ! - - + p b n ( i ) n f n ( q ) = o p i o 山p j o c 。m 号卷乎r e p 丽丽乒丽 p lq 二呻p ，iq 双歹) i ! x ( 刃q 二斗q 涉j l ! x ) q r e s ! 二兰垒兰：鱼盟! 型2o p e n ( 慨) p l ( 眦) q a l p h a ! ：呈! 羔! ： p 与q p 马qv e x ，v 信 i 面j 巫五万一 。”p 巫虹立! l p q ：f i l q ， 吼0 8 e 砸二方蟊硒o 产p i q _ 妒l ) 第7 页 国防科学技术大学研究生院工学硕士学位论文 迁移给出，该式表示进程p 可通过完成一个标记为增q 动作后变成p 。迁移关系通 过定义进程能够执行的动作，既能描述系统内部活动，也能描述系统与环境的交 互活动。迁移关系运用系列推导规则定义，并由动作进行标记。迁移关系定义进 程能够执行的动作，表明进程的行为能力异步7 【演算中，定义迁移关系时，它的 标记动作，分为三类：引办x 仨鼻f 。 定义2 3 ( 迁移关系) 给定进程集合，它的迁移关系 l l ，a c t 由表 ， 2 3 中的规则定义，即能够根据该规则推出的所有迁移的集合。该表中省略了三个 与p a r 、c o m 、c l o s e 对称的规则，只需把其中p 、q 的位置相互交换即可得到 2 4 异步舡演算行为等价理论 矿演算理论重心是行为等价理论，即如何判定两个并发执行、并与环境交互 的系统是否有相等行为。如果两个系统行为相等，那么从任何环境中取出其中一 个而放入另外一个，环境不会感知替换发生。研究行为等价理论是具有重要的实 践和理论意义互模拟是并发领域中一种标准的进程同等价关系。矿演算基本的 互模拟理论在 3 ，i s 中给出，而异步矿演算的互模拟理论在【1 7 中给出。 定义2 4 1 一个对称二元关系孵称为异步强互模拟关系，如果q ) 吼蕴涵： 如果p 二l p ，则 或者存在q 使得q ! 垃哼q 并且( p ，q ，) 贸； 或者存在q 使得q 二_ 专g 并且( p ，q ，l 万( x ) ) 瑕； 对满足6 n ) n 力( p ，o ) - - 的其它动作口，如果p 兰呻p ，则存在q 使 得q 苎哼q ，并且p ，q ) e9 t 。 我们用。表示最大的异步强互模拟关系。 强互模拟是同余关系，具有很好的数学性质它将所有动作平等看待，即使是 只有内部可见的t 动作也不例外。有时候我们并不希望把f 动作与其它动作平等看 待，因为t 动作对外部观察者而言是不可见的。于是，需要在互模拟的定义中忽略 t 动作，这样就得到了弱互模拟关系 定义2 4 2 双箭头关系可以如下定义： f p = p 。 口 p 与q 蕴涵p j q 。 口口 尸山j q 蕴涵p j q 。 第8 页 国防科学技术大学研究生院工学硕士学位论文 如果口不是口g ) 的形式，那么p 当b q 蕴涵p 当q 我们将当写为当；当口，时，当写为当；将当写为j 定义2 4 3 一个对称关系孵称为异步弱互模拟关系，如果( p ，q ) 孵蕴涵： 如果p 垃专户7 ，则 o 或者存在纱使得q q ，并且( ，q ，) 孵； 或者存在矿使得q j 并且( 尸：i 万o ) ) 孵； 对满足锄 ) n 办q ) = 西的其它动作口j 如果p 曼_ p ，则存在q ，使 左 得q j 并且( p ，q ) 吼 我们用表示最大的异步弱互模拟关系。 下述的属性是异步 r 演算所特有的： 引理2 4 4 1 若尸啦p ，则p pj 万( 石) 。 2 若p 三色生p 7 ，则p 一。( o x ) ( p i 万( x ) ) 。 3 若p 驾山p ，则p 与三屿，。 4 若p i 竺：l 生p 且z 诺力( 口) u 6 以( a ) ，则尸已主p 5 若p 啦坞p 7 且y 是新鲜的，则p 山p ，p y 】。 6 若p 垫立哼亟丑斗p ，且y 是新鲜的，则p 三一( w ) ( p 卜，】) 。 2 5 小结 随着计算机技术和网络通信技术的高速发展，以并发性、分布性、实时性、 异构性和互操作性等为主要特征的并发分布式系统已成为当前计算机技术的主流 方向，并已得到广泛应用。由于并发分布式系统本身非常复杂，因此其开发过程 不仅难度大，效率低，周期长，而且很难避免和发现其中隐含的错误和缺陷。对 于安全攸关系统( s a f e t yc r i t i c a ls y s t e m s ) ，其正确性就更为重要。 形式化方法被公认为是一种行之有效的减少设计错误、提高系统可信度的重 要途径。传统的形式化方法以严格的数学理论为支撑，对顺序计算的本质作了深 刻的诠释。并发已成为新一代计算范型的本质特征，对并发计算的研究引起了许 多学者的兴趣并取得了巨大的成果。 以通信系统演算( c c s ) 为代表的进程代数方法，因概念简洁，可用的数学工 具丰富，在并发系统的规约、分析、设计和验证等方面获得了广泛应用7 【演算是 第9 页 国防科学技术大学研究生院工学硕士学位论文 在c c s 基础上发展起来的，它具有更强大的表达能力。其将通道，常元、变元统 一看作名字作为消息值域，从而能对通信拓扑结构可变的并发系统做出自然的描 述，因此也被称为“移动进程演算”。 矿演算是对应用的广度，即理论的一般性，和理论的完美同时追求的结果， 通过较高抽象级来获得二者的统一。就概念简洁性和一般性而言，矿演算类似于 作为函数计算基础的卜演算，因而可作为研究并发通信系统的基本工具。异步伽 演算是兀演算的一个变体，其消息传递( 通信) 的实现方式是异步的，即发送与接 受动作不一定同时发生。它没有非确定性选择和输出前缀，但是其进程间的交互 模型与冗演算是基本一致的。关于异步7 r 演算的语法和语义理论参见文献 1 2 ，1 3 ，1 4 ，1 5 。 第l o 页 国防科学技术大学研究生院工学硕士学位论文 第三章使用异步7 r 演算验证2 p c p 不考虑失效 3 1 引言 原子提交协议【1 5 , 1 9 1 ( a t o m i cc o m m i t m e n tp r o t o c 0 1 ) 是分布式事务处理中一个 用于确保一致性的算法，即协调者和所有的参与者要么都提交事务，要么都撤销 两阶段提交协议( 2 p c p ) 是最简单且最常用的原子提交协议，该协议使分布式事务 的提交具有原子性和持久性，并且允许每个事务管理器有权单方面决定中止还没 有准备提交的事务。两阶段提交主要是用于协调在一个事物内各个独立的资源管 理器的工作，这对处理被延迟到事务完成时( 阶段1 ) 的完整性检查，以及延迟到 事务最终被提交时( 阶段2 ) 的有关工作特别有用。 在本章中，我们使用异步兀一演算对基本的两阶段提交协议进行描述，并证明了 其实现与规约之间是弱互模拟的。 3 22 p c p ：不考虑失效的情况 对于每一个分布式事务l 在执行r 的每一个站点都有一个进程。这些进程关 于r 执行原子提交协议。在r 的主站点( 即r 的发起站点) 的进程称为r 的协调 者，其余进程则称为r 的参与者。创建某一分布式事务的协调者成为该分布事务 的协调者，它在分布式事务结束时负责提交或放弃事务。分布式事务访问的每个 服务器都是该事务的参与方，每个服务器提供一个我们称为参与者的对象。每个 事务参与者负责跟踪所有参与分布式事务的可恢复对象。这些参与者配合协调者 共同执行提交协议。在事务的执行过程中，协调者在列表中记录所有对参与者的 引用，因此它可以给所有的参与者发送消息，而每一个参与者都记录一个对协调 者的引用。 原子提交协议( a c p ) 是参与分布式事务的服务器使用的一个协作过程，它 使多个服务器能够共同决策是提交事务还是放弃事务；也是一个确保一致性的算 法，即协调者和所有的参与者要么都提交事务，要么都撤销。每个进程只有一张 投票：y e s 或者n o ，并且最后的决定也只有一个：c o m m i t 或者a b o r t 。 一个a c p 算法必须满足： a c i ：收到决定的所有进程，其决定必须是一致的。 a c 2 ：进程收到决定之后是不能对其进行更改的。 a c 3 ：若决定是提交，则所有进程的投票一定是y e s 。 a c 4 ：若没有任何失效发生，且所有的进程都投y e s 票，则决定将会是提交。 第1 l 页 国防科学技术大学研究生院工学硕士学位论文 a c 5 ：考虑执行中发生的失效仅是算法可以允许的失效，则在执行过程中，当 所有的失效都修复之后，且在一定时间内没有新的失效发生时，所有的进程最终 一定会有一个决定。 a c l 是对事务终止时一致性的要求。但需要注意的是它并不要求所有的进程 都收到决定，因为有的进程可能会发生失效并且永远不能恢复。而且它也不要求 所有运行的进程都收到决定，因为当有通讯失效和全局失效发生时，进程可能会 阻塞。然而，a c 5 要求一旦恢复完成，所有的进程都能够收到一个决定。 a c 2 要求事务在某个站点的结束是一个不可取消的操作。即，事务不能在提 交之后又撤销，也不能在撤销之后又提交。 a c 3 要求事务只有在执行其的所有站点都同意提交之后才能提交。a c 4 比 a c 3 的逆命题较弱一点。因为任何a c p 都不能保证发生失效的进程能够独立恢复， 所以有可能所有的进程都投了y e s 票，而最后的决定是撤销。从a c 3 可以看到， 只要进程没有投y e s 票，就可以随时单方面的决定撤销。但一旦进程投了y e s 票， 就不能有单方面的动作了。在进程投y e s 票直至收到决定期间，称为进程的非确 定阶段。处在非确定阶段的进程称为不确定的。不确定的进程是不知道其最后是 要撤销还是要提交，因此是不可以单方面决定撤销的。 两阶段提交协议是由g r a y 提出的最简单且最常用的原子提交协议。 在不考虑失效发生的情况下，2 p c p 的描述如下： 1 协调者向每个参与者发送v o t e - r e q 消息。 2 当参与者收到v o t e - r e q 消息，就给协调者发送其投票：y e s 或者n o 。若参 与者的投票是n 0 ，则其立即自行决定撤销并终止；若参与者的投票是y e s ， 则等待协调者的消息。 3 协调者收集所有参与者的投票。若都是y e s 且协调者自己的投票也是y e s ， 则协调者决定提交并向每个参与者发送c o m m i t 消息。只要有一张投票是 n o ，则协调者决定撤销并向每个投y e s 票的参与者发送a b o r t 消息。两种 情况下，协调者在发送消息后都将终止。 4 投y e s 票的参与者收到协调者的c o m m i t 或a b o r t 消息后，则做出相应决定 并终止。 前两步是2 p e p 的投票阶段，后两步则是2 p c p 的决定阶段。一个参与者的非 确定阶段是从给协调者发送y e s 票直至收到协调者的c o 删i t 或a b o r t 消息。协调 者是没有不确定阶段的，因为协调者在其投票之后立即有了最终的决定。 3 3 形式化描述 在我们的描述中，2 p c p 由时1 个进程并发组成：一个协调者c 和甩个参与者 第1 2 页 国防科学技术大学研究生院工学硕士学位论文 p l ，b 。协调者和各个参与者之间通过单独的通道c t 和d ：进行通讯。 2 p c p ；嘲i c i 墨1 1 只) 协调者本身又由多个子进程并发组成： c ；b 云i c wl c i c “i c ”) c ”s m 。印甲；巧( 咫q ) c ；n 二l 。q ”q “；z g ) ( p = d 】- j 扛= 嘲) x e y e s n o c “i b l 如。以c ” c c “”o c ”“ c ”；口c “ c “；兀二c ，c p ；巧( 4 口d ) c | ；n p c p 。t ；蚕| i c o 蚋 c w 进程表示协议初始时协调者向每个参与者发送v o t e r e q 消息；c 进 程表示协调者等待参与者的投票；c 耐进程收齐所有参与者的y e s 投票之后，协 调者最终做一个决定是提交还是撤销，若提交则向每个参与者发送c o m m i t 消息， 若撤销则发送a b o r t 消息；如果有一个参与者投了n o 票，则c ”进