（计算机软件与理论专业论文）异步非对称chi演算的互模拟关系研究.pdf

异步非对称c h i 演算的互模拟关系研究 摘要 在现有的1 ：发分布式系统中，信息的发送往往是非阻塞的，必 须采用异步的通信方式。而实际的程序设计严格区分输入和输出动 作，即非对称通信。本文研究一个新进程演算，即异步非对称c h i 演算。异步非对称c h i 演算是目前最接近于现有的分布式程序设计 语言的形式化演算，值得深入研究。我们研究异步非对称c h i 演算 的互模拟关系，从而为进一步研究该演算的互模拟同余公理化铺平 道路。 本文定义了异步非对称c h i 演算的语法和操作语义，通过统一 框架定义了一组一互模拟关系。但是这些互模拟关系大部分是重叠 的，可把它们分成几个组，每个组内的互模拟关系完全相同。可以 从每个组中取出一个互模拟关系，作为该组的代表元，按这些代表 元之间的包含关系构造异步非对称c h i 演算的互模拟格。本文研究 了与互模拟格中最大元相关的b a r b e d 互模拟关系。 关键词：异步非对称c h i 演算；c h i 演算；互模拟格；进程代数 o nb i s i m i l a r i t i e so fa s y n c h r o n o u s a s y m m e t r i c c h i c a l c u l u s a b s t r a c t i ne x i s t i n gd i s t r i b u t e ds y s t e m s ，t h es e n d i n go fm e s s a g ei so f t e n u n b l o c k e dt h a tc o r r e s p o n d st oa s y n c h r o n o u sc o m m u n i c a t io nm o d e a n d i n p r a c t i c a lp r o g r a m m i n g ，w em u s ts t r i c t l yd i s t i n g u i s hb e t w e e ni n p u t a c t i o n sa n do u t p u ta c t i o n s ，t h a ti st os a y , c o m m u n i c a t i o ni sa s y m m e t r i c an e w p r o c e s sc a l c u l u s ，c a l l e d t h e a s y n c h r o n o u sa s y m m e t r i c c h i - c a l c u l u s ，i ss t u d i e di nt h et h e s i s t h ea s y n c h r o n o u sa s y m m e t r i c c h i - c a l c u l u si sac a l c u l u sw h i c hi sc l o s e s tt ot h ee x i s t i n gd i s t r i b u t e d p r o g r a m m i n gl a n g u a g ea n dw o r t h yo f r e s e a r c hf u r t h e r w es t u d y b i s i m u l a r i t i e so fa s y n c h r o n o u sa s y m m e t r i cc h i - c a l c u l u s ，a c c o r d i n g l yw e p a v e t h e w a y f o rf u r t h e rr e s e a r c ho n a x i o m a t i z i n g b i s i m u l a t i o n c o n g r u e n c e so ft h ec a l c u l u s t h et h e s i sd e f i n e st h es y n t a xa n ds e m a n t i c so ft h ea s y n c h r o n o u s a s y m m e t r i cc h i - c a l c u l u sa n dd e f i n e sag r o u po fl b i s i m i l a r i t yr e l a t i o n s b yp r o v i d i n ga u n i f o r mf r a m e w o r k b u tm o s to ft h e s eb i s i m i l a r i t i e sa r e o v e r l a p p e dt h a tc a nb ed i v i d e di n t os e v e r a lg r o u p s f o re a c hg r o u p ，a l l o fb i s i m i l a r i t i e sa r ei d e n t i c a l ，a n dt h e nw ec h o o s eab i s i m i l a r i t ya st h e r e p r e s e n t a t i v e w ec o n s t r u c tt h eb i s i m u l a t i o nl a t t i c eo ft h ea s y n c h r o n o u s l l a s y m m e t r i c c h i c a l c u l u s a c c o r d i n g t ot h e i n c l u s i v eo r d e ro ft h e s e r e p r e s e n t a t i v e s t h eb a r b e db i s i m i l a r i t y t h a ti sr e l e v a n tt ot h et o p e l e m e n to ft h eb is i m u l a t i o n1 a t t i c ei ss t u d i e di nt h et h e s i s k e yw o r d s ：a s y n c h r o n o u sa s y m m e t r i cc h ic a l c u l u s ；c h ic a l c u l u s ； b i s i m u l a t i o nl a t t ic e ；p r o c e s sa l g e b r a 符号说明 下面说明列出了本文在异步非对称c h i 演算中所用到的各种符号。 名 口，b ，c ， f i - ，b ，石， 口 x n n 办u 砌u n o 进程 0 a x p a x 尸ip 。 ( x ) p 陋= y p 【x y j p p 七p ( x ) a x p 【少x 】p ( y x 】p z p 兄 j p ，q ，r c 兄 ( x ) p 条件算子 【y 仨y 】 名 余名 名或余名 名序列，而，x 3 ，的缩写 所有名的集合 所有余名的集合 某实体的自由名集合 某实体的约束名集合 某实体的所有名集合 非活动进程 带输入前缀算子的进程 输出进程 并发算子 局部化算子 等名算子 不等名算子 选择算子 约束输入前缀 自由更新前缀 约束更新前缀 内部通信前缀 任意前缀算子 进程 进程集合 进程五0 的缩写 ( 玉) ( 艺) 尸的缩写 不等名序列【y y j 】眇虬】的缩写，其 中y = m ，以) 条件 不等名算子序列 等名算子序列 够逻辑蕴含缈 妒逻辑等价于 伊和少的连接 原子代换 代换 代换仃作用在进程p 上 代换仃的定义域 代换仃的值域 代换仃的所有的名集合 v 自由输入动作 约束输入动作 自由输出动作 约束输出动作 自由更新动作 约束更新动作 内部通信动作 任意动作 非( 约束) 更新动作 自由输入动作集 约束输入动作集 自由输出动作集 约束输出动作集 自由更新动作集 约束更新动作集 动作集 动作集幂集 上下文表示 杪 ， ，仃、旷， 0 刁 支 万恻峥缈懒州3胎圳嘶州摊州删酬酬叭f旯yn力加甜ml托印 口 c e 】 互模拟关系 6 o 占 迁移 厶 v i 上下文空位 上下文实例化 l 互模拟 b a r b e d 互模拟 开b a r b e d 互模拟 标号迁移 任意内部通信迁移 弱迁移 可带内部通信可观察迁移的缩写 语法相等 定义等式 可推导 有限下标集 f。f1。ff竞 暑何= h ， 浙江师范大学学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及 取得的研究成果。论文中除了特别加以标注和致谢的地方外，不包含其他 人或其他机构已经发表或撰写过的研究成果。其他同志对本研究的启发和 所做的贡献均已在论文中作了明确的声明并表示了谢意。本人完全意识到 本声明的法律结果由本人承担。 作：名搬l 坟日期：加 4 5 f 月苫日 、 学位论文使用授权声明 本人完全了解浙江师范大学有关保留、使用学位论文的规定，即：学校有 权保留并向国家有关机关或机构送交论文的复印件和电子文档，允许论文被查 阅和借阅，可以采j h 影印、缩印或扫描等手段保存、汇编学位论文。同意浙江 师范大学可以用刁i 同方式在不同媒体上发表、传播论文的全部或部分内容。 保密的学位论文在解密后遵守此协议。 名：伽生虢揶山。f 同 第一章绪论 并行分布式计算是计算机科学的重要研究内容，它的特征主要包括：并发 性、分布性、实时性、异构性、互操作性等。我们知道并发计算十分复杂，并 发分布式系统的开发和研究十分困难，为保证并发分布式系统的正确性和可靠 性，我们需要使用形式化方法。 c c s 模型i 1 7 ，1 8 i 是r m i l n e r 在研究多进程交互的复杂系统时提出的最早的并 发计算模型。该模型对于理解多进程系统的本质并发和通信，起到了重要的 作用。但c c s 只能描述静态结构的并发系统。 二十几年来，各种移动进程演算一直是并发理论研究的焦点。p i 演算是一 个并发计算模型1 2 0 儿2 2 j ，它是由r m i l n e r 、j p a r r o w 和d w a l k e r 提出的移动进程 演算。这个演算与传统的进程演算( 如c c s ) 有所区别，它忽略了c c s 中通道 和变量的差别，将两者统一为名，因而在保持c c s 代数性质的同时扩展了并发 计算能力。在该演算中，计算实体包括名和进程，进程之间的通信通过传名实 现，并允许名的动态生成和通信。研究者们以p i 演算为基础，从不同角度提出 许多p i 演算的变种。例如，r m i l n e r 研究了应用中常见的多维( p o l y a d i c ) p i 演算 【2 5 1 ，就是在一次通信中同时传递多个名的p i 演算。s a n g i o r g i 研究了高阶p i 演 算和进程的移动。2 6 , 2 7 】，就是在通信中把进程作为数据传递，讨论了高阶与一 阶p i 演算，表明了高阶p i 演算与一阶p i 演算具有相同的表达能力。k h o n d a 和m t o k o r o 引入了异步7 c 演算i l 】，g b o u d o l 也独立提出这个演算【2 1 ，异步p i 演算被认为是实验并发和分布式程序语言的基础，研究显示，异步p i 演算与同 步p i 演算具有相同的表达能力。傅育熙教授提出了c h i 演算【6 - 8 , 2 1j 。c h i 演算是 移动进程演算家族中新增加的一个演算。同时，j p a r r o w 和b v i c t o r 提出u p d a t e 演算 2 8 】，接下来义提出f u s i o n 演算【2 9 3 0 1 。用统一的术语说，u p d a t e 演算是非 对称c h i 演算，而f u s i o n 演算是多维的c 1 1 i 演算。 c 1 1 i 演算引入有两个目的：一是使用了统一的名形式，去除了p i 演算的输入、 输出前缀的差异，达到语言概念上的简化；二是实现了将通信看作“割消除” 的一个实例，反映图形象地描述了c h i 演算的内在通信机制【2 引。c h i 演算把通信 看作是信息的交换和更新。c h i 演算比p i 演算具有更大的并行自由度。因此， c h i 演算的提出使我们朝着提出更抽象的并发计算模型迈进了一步。 c h i 演算与p i 演算的主要区别是通信发生的方式不同，c h i 演算采用信息 交换或信息更新的通信机制，从而代替了p i 演算中采用的传名的通信机制。c h i 演算具有通信的对称性。c h i 演算通过局部化算子描述通信的代数语义，使得 互模拟的定义更力i i 简洁，证明更加方便，代数性质更好。两者的比较： p i 演算c h i 演算 输入和输出 非对称：口0 ) p 和a x p 统一为：似尸 闭名 两种： ) p 和口o ) p一种： ) 尸 并行性 预先设定计算：口o ) ( p i q ) 或 更自由的并行性： 尸i a ) q( x ) ( p lc r r 9 通信机制传名 信息交换 在p i 演算中，有像( x ) p 中的约束名x 和a ( x ) p 中的抽象名x ，对于一个并 发计算的基本模型，两种封闭名太多了，可以只使用一种局部名来代替。在c m 演算中，由局部化算子充当辖域分界符，使概念更简洁。 在移动进程代数理论的研究中，许多研究都集中在进程的互模拟等价关系 的研究，这是进希，j 匕数最有影响的特点之一。有关c h i 演算互模拟等价关系的 研究取得了一系列的成果，包括引入了l 。互模拟的概念，用互模拟格对所有l 互 模拟关系进行分类以及用丌形态的互模拟刻画l 互模拟的特性。 傅育熙教授引入了局部互模拟关系【7 l ，该互模拟关系基于如下的思想：两个 进程是观察等价的，当且仅当这两个进程处于相同的环境中，并演化得到两个新 的观察等价的进程。局部互模拟关系在局部化算子和并行复合算子下都是封闭 的。c l l i 演算的代数特性也根据局部互模拟关系来研究。 c h i 演算的一个新特征是对名作了一致性处理，名的一致性是指输入、输 出前缀没有区别。下面是c h i 演算通信的例子： ) ( a x 尸i a y q i r ) 二专尸陟詹】| 9 弘】j 尺陟詹】( 1 ) ) ( a x p la y q i r ) 与p 吣旭嗍l 尺吣】 ( 2 ) 0 ) a x p ia y q - 尸陟詹】l q( 3 ) g ) a x p a y q l 尸【y 詹】1 9( 4 ) 口z p 和a y q 是前缀形式的进程，x 和y 是全局名。0 ) 是局部化算子，它 在它作用的范围内限制名x 为局部名。上面的四个归约说明c h i 演算中通信的 对称性。具有同样的输入、输出前缀形式和通信的对称性是c h i 演算的一大特 点。在理论上，具有同样的输入、输出前缀形式和通信的对称性是c h i 演算的一 个完美的性质。 如果我们坚持认为输入前缀操作和输出前缀操作是不同的，我们就得到了 非对称的c h i 演算。在非对称c h i 演算中，上例中的规约( 1 ) 和( 3 ) 是允许的，规 约( 2 ) 和( 4 ) 是不允许的。在实际的程序设计中，往往需要非对称的通信方式，也就 是说必须严格区分输入、输出动作。因此，我们有必要研究非对称c h i 演算。 非对称c h i 演算是适合实际需要的具有非对称通信特点的c h i 演算的一个变种。 异步演算的输出进程为积，以盈i 尸代替了同步演算的舐p ，体现了异步 输出信息与后续进程在时间上没有先后性，异步通信在输出形式上a x 没有后 继，异步信息的发送往往是非阻塞的，它非常好地模拟了异步通信的这个特点。 大多数并发分布式系统及其协议没有全局时钟，其通信是非阻塞的，同时 异步通信易于实现，与现有的并发分布式系统的通信原语非常接近。因此多数 分布式系统很自然的采用异步通信机制。因此，从并发分布式程序设计语言的 角度看，异步通信是比较令我们感兴趣的。 我们从异步c h i 演算中去除通信的对称性得到了异步非对称c h i 演算，因 此，异步非对称c h i 演算是一种与其他演算比较起来较简洁的移动进程演算， 具有异步和非对称通信二个特点。 我们需要研究异步非对称c h i 演算的互模拟关系，从而为进一步研究该演 算的互模拟同余公理化铺平道路。 第二章异步非对称c hi 演算 2 1引言 自9 0 年代以来，移动进程演算已成为并行计算的焦点之一。有关c h i 演算 的研究丰富了类p i 移动进程演算的内容。从操作角度看，c h i 演算是通过消除 p i 演算的非对称性而得到的，这一改进对观察性质产生了重要的变化。 非对称c h i 演算是c h i 演算的一个变种，它体现了非对称通信的特点。这 一演算有两个变种：带不等名算子的非对称c h i 演算和不带不等名算子的非对 称c h i 演算。由于实际的并发分布式系统的特点，我们需要研究异步的非对称 c h i 演算，它体现了异步通信的特点，即通信是非阻塞的，该演算的输出进程 没有后继。文献表明，不等名算子对进程演算的代数语义具有重要影响，丰富 了进程演算的代数语义。因此，本文研究的异步非对称c h i 演算是带有不等名 算子的。异步非对称c h i 演算是一个全新的模型，它具有特有的优点，因此特 别值得我们进行硎究。 本文所要研究的是异步非对称c h i 演算的互模拟格，目的在于理解异步性、 非对称性和不等名算子对c h i 演算代数理论的影响。 本章将定义带不等名算子的异步非对称c h i 演算的语法，该演算的操作语 义由下面的标号迁移系统来定义。 2 2 异步非对称c h i 演算的语法 异步非对称c h i 演算有两类对象：名和进程，其中进程是具有拓扑结构的 计算对象，拓扑绵构规定进程在演化过程中的动态行为，名是定义进程拓扑结 构所必须的。 令是名集，它是由小写字母所组成，如a n 。n 是余名集，定义为 ；ix n 。希腊字母口表示为集合u 的一个元素，即口n u 。 本文研究有限c h i 进程的互模拟关系。有限异步非对称c h i 进程定义如下： p ：= 0 a x 尸i 薇l ( x ) pi 尸ipi 尸+ 尸i x = y pi 【x y p 。 异步非对称c h i 进程的集合用c 表示。 像通常一样，0 是不活动的进程，该进程不做任何动作。 a x p 是一个带输入前缀算子的输入进程。 积是一个输 进程，它没有后继，体现了异步性的特点。 ( x ) p 是一个名工局部于尸的进程，就是进程p 中的名x 受约束算子( x ) 的约 束，在进程( x ) p 中名z 作为进程尸的局部名，而不受其他进程的影响。 4 pp 是一个并行复合形式的进程，此处户和p 。能各自独立地演化，并且可 能在它们的演化过程中相互通信。 选择进程尸+ p 。为不确定选择进程，该进程表示或者选择子进程p ，或者 选择子进程p ，一旦某个子进程被选中，则另一个子进程被丢弃。 条件进程【x = y l p ：如果x = y ，它的行为与p 一样的；如果x y ，它的行 为与不活动进程0 是一样的。 条件进程【x y l p ：如果x y ，它的行为与p 一样的：如果x = y ，它的行 为与不活动进程0 是一样的。 在异步演算中，我们用薇lp 来代替同步演算中的赢尸。我们可以假定输出 进程薇的后继是进程o 。 在书写进程时，下列算子的优先级次序被呈现出来：代换算子 约束算子， 输入f j 缀算子，r 自，缀算子，匹配算子 并行复合算子 选择算子。 出现在尸中的局部名集被定义为l n ( p ) ，而在p 中的全局名集被定义为 办( p ) 。集合n ( p ) 是集合l n ( p ) 和集合办( 尸) 的并集。 我们将采用著名的口变换，口变换是指进程中的局部名可以用新名来替 换，并且不会对这个进程有任何影响。事实上，局部名只是一个占位符号。 接下来，我们引入以下四个辅助算子： 口( x ) p = ( x ) a x p ，其中工萑 口，历) ； 【y x 】尸= ( 口) ( 砂ia x 尸) ， ( y x 】p = ( y ) y x 】p ，其中x y ； c l e f r p = ( 6 ) 【6 外p 。 2 3 异步非对称c h i 演算的操作语义 我们开始定义进程能做的动作，如 y 口 x 】，万【x 】，口( x ) ，万( x ) ia ，石n ) u f ) ， 旯 口 x 】，万【x 】口( x ) ，万( x ) ，【y x 】，( y x 】l 口，x ，y n u r 。 这里y 、兄是动作标号。r 为内部动作：a x 】为自由输入动作，它表示通 过通道a 输入一个自由名x ；a - - i x 】为自由输出动作，它表示通过通道a 输出一个 自由名x ；a ( x ) 为约束输出动作，它表示通过通道口输出一个约束名x ；a ( x ) 为 约束输入动作，它表示通过通道a 输入一个约束名工；【y x 】为自由更新动作： ( j ，x 】为约束更新动作。由此，一个动作是输入还是输出动作依赖于对象名是 被接收还是发送。我们把兄作为进程五0 的缩写。 异步非对称c h i 演算的操作语义由标号迁移系统定义。这些规则定义了进 程在交互过程中其拓扑结构的变化方式，这里的迁移是尸山q ，口属于某个 动作集。在下面形式中，对称规则被系统省略了。 前缀a x p 屿尸s q n o ， 复合 尸与尸b n ( y ) n f n ( q ) = 西 p j q 与尸l q p 一! 业 尸 尸i9 上! 屿p iq y x 】 尸卫马p y 芒f n ( q ) p lg 上坞p lq y x 通信 p 屿尸 q 屿q 尸iq 二专p 。 y x 】iq 尸旦j 尸 q 型生哼q 约束 尸iq 二专( x ) ( 尸iq ) 尸巫专p q 型丛寸q 。 pq 屿尸 y x 】iq y x 】 p 坞尸q 至盟寸q 。 j p q 二专尸lq 尸u 一尸q 吗q 。y 仨办( 尸) 尸iq 上屿尸 y x iq 。 y x 】 p 与p x 仨n ( 2 ) ( x ) 尸与( x ) p 。 p 型一p 。 x 仨 口，云) ( x ) 尸屿p 。 尸卫生屿p 。 ( x ) 尸 p p 上山p ( y ) 尸屿尸 尸业型一p 。 ( 工) p 二专( y ) 尸 6 c m p o ， c m p l ， c m p 2 ； c m m o ， c m m l ， c m m 2 ， c m m 3 ， c m m 4 ； l o e o ， l o c l ， l o t 2 ， l o c 4 ； 条件 p 一尸。 【x = x p 与尸 尸二寸尸 【工y l 与尸 不确定选择 尸二_ 尸 p + q 2 一p m a t c h ， m i s m a t c h ； s u m 下面我们说明异步非对称c h i 演算的标号迁移系统的各条规则的意思。前 缀规则说明：进程a x p 必须在完成输入动作a x 】之后，才能做后续进程p 的所有 可能的动作；输出进程薇在完成输出动作a x 】之后，成为o 进程，充分体现了输出 进程没有后继的异步语义的特点 三条复合规则描述了复合进程中的每个进程可以相互独立地演进，由于自 由更新和约束更新动作对邻近进程会产生副作用，故对这两个动作分别进行处 理在通信规则中，c m m o 描述一个进程接收其它进程所发送的自由名，c m m l 描述一个进程接收其它进程所发送的约束名；c m m 2 和c m m 4 分别引入自由更 新和约束更新动作，这两条规则改进了语言通信的定义。为了简化异步非对称 c h i 演算的代数语义而增加的c m m 3 ，可以看作是规则c m m 2 的补充。 在约束规则中，自由更新动作和约束更新动作可以将它们理解为正在发生 但还没有完成的通信以及从内部看到的通信。由此看出约束算子具有约束、限 制的作用并且起到界定通信范围的作用。l o c o 说明了局部名的影响范围。l o c l 说明引入约束动作之后的规则。l o c 3 说明了我们有必要引入约束更新动作。 l o c 2 和l o c 4 定义出通信的范围。 在条件规则中，m a t c h 和m i s m a t c h 分别表示等名测试条件和不等名测试条 件，一旦等名算子或不等名算子为真，则进程【x = x l p 和进程【x y p 能做的动 作与进程p 是一样的，否则进程k = x e 和进程【x y p 为0 进程。 不确定选择规则表示：如果进程尸+ q 选择做p 所能做的某个动作，则整个 进程也做这个动作，并且丢弃进程q ：如果选择q 所能做的某个动作，则整个 进程也做这个动作，并且丢弃进程p 。 【y 萑r p 是指 y y 。】 y y 2 眇儿】尸。令表示等式算子序列，万表示 不等式算子序列。如果( 或万) 的长度为零，则尸( 或万尸) 表示尸。 符号【y x 】是把名x 替换为y 的原子替换。一般代换仃是多个原子代换的 复合，即：p y l 一儿y 2 x 2 】【儿】( p y l 五】【儿一i 一i 】) 儿x n 】。0 个原子 代换的复合是空代换，它对进程没有影响。 目前提出的所有进程代数都是基于通道概念的。通常，一个通道可用一个 通道名来表示，它具有唯一性的特征，即它是区别于其它任何通道的。由于这 个原因，人们经常把通道说为通道名或仅仅名。进程通过通道进行通信。 其实，代换仃是从到的函数，是有限集。这个集合 zi 工n ，c r ( x ) x j 是有限集。代换仃的定义域，记为d o m ( c r ) ，为集合 xx n ，c r ( x ) x 】。仃的值域是r n g ( o ) ，是d o m ( o ) 的像。代换仃为 m x i 】 儿矗】时，有d o r a ( o r ) = ，毛) 和r n g ( o ) = y l ，y o 。 引理2 1 似设a 仨f - ( p ) 并且口b ，下面性质成立： ( 1 ) 如果( x ) ( 尸f 口 x 】) 与尸。f a y 】，则p j 丛生专尸： ( 2 ) 如果( x ) ( 尸i 讲x 】) 业寸尸ia x 】，则p 皇屿p ； ( 3 ) 如果( x ) ( j di 口 x 】) 丛生一p 。ia x 】，贝0p 屿p 。 证明：( 1 ) 归约( 工) ( p i 讲z 】) 山p 。ia y 所使用的最后一条规则一定是 l o c 2 ，其前提为尸l 饥x 】屿p la y 】，它由尸屿尸通过使用c m p l 规则 得到。 ( 2 ) 归约( x ) ( p l 讲x 】) 灿p i a x 】所使用的最后一条规则一定是l o c i ， 其前提是pf 讲z 】坐b p la x 】，它由p ! 盟专尸通过使用规则c m p o 得到。 ( 3 ) 归约( x ) ( j pl 口【叫) 屿p 。ia x 】所使用的最后一条规则一定是l o c i ， 其前提是pl 讲x 】坐b 尸。la x 】，它由p 坐b 尸通过使用规则c m p o 得到。 证毕。 我们把与的自反传递闭包记为j 。我们把与j ( j 与j ) 记为( j ) 。并且j 表示为：如果r ，它为；如果= f ，它为j 。 我们用元来定义一个名x l ，oo $ 的序列。我们也将( 五) ( ) ( ) 尸缩写为 ( i ) p 。当这个序列元的长度是0 时，( i ) 尸也就是尸。 本章给出了异步非对称c h i 演算的语法和操作语义定义。在语法定义中， 前缀算子具有非对称的特性，而且该演算具有异步性的特点，即输出进程没有 后继，由舐表示。操作语义中的自由更新动作和约束更新动作是不完全通信动 作，定义这二个动作的目的在于表达出通信对相邻进程有副作用。约束算子不 仅限制约束名的作用范围，而且也界定了通信的影响范围。除此之外，我们定 义了一些符号表示，并给出了一些常用的技术性引理。 异步非对称演算具有三个基本的特征结构： ( a ) 非对称的通信方式。具有输入前缀a x 的进程只能通过通道a 接收一个 名，而输出进程薇只能通过通道a 发送一个名，从而将输入和输出动作严格地 区分开来了，显示了该演算具有非对称通信的特点。 ( b ) 异步的通信方式。它把输出进程写为薇，没有后继，显示了通信是非阻 塞的，从而跟现有的并发分布式系统的通信原语比较接近。 ( c ) 不等名算子。由于历来的研究都表明，不等名算子丰富了演算的代数语 义，是比较好的算子，所以我们引入该算子。 9 第三章互模拟格弟二早旦个吴亍以怕 3 1引言 进程演算中的一个关键性概念是进程间的行为等价，我们集中关注基于互 模拟关系的行为等价。 对于某个进和演算，不只有一个弱互模拟等价关系，而是有一组等价关系， 这些等价关系在进程允许执行的动作范围上是不同的。 我们引入l 互模拟，它是局部互模拟的精简，它为我们定义全部互模拟关 系提供了一个统一的框架。 l 互模拟的基本思想是：不同的互模拟关系所能看到的进程行为是不同的， 他们所能区别的进程也是不一样的，因此，我们提供一个统一的框架，来研究 所有的互模拟关系。 我们把外部动作集划分为了六个动作集，使用统一的框架，选择某个组合 的动作集，来构造我们需要的互模拟关系，但是这些互模拟关系大部分是重叠 的，我们可把它们分为好几个组，每个组内的互模拟关系完全相同，我们可以 从每个组中取出一个互模拟关系，作为该组的一个代表元。我们只需要研究这 些代表元就可以获得所有的互模拟关系的性质。这些代表元是互不相同的，某 些代表元之间具有包含关系。我们按这些代表元之间的包含序关系构造出异步 非对称c h i 演算的互模拟格，该互模拟格由这些互异的l 互模拟关系组成。由 此，我们将看到互模拟格具有许多好处，首先互模拟格的代表元数目较少，其 次代表元之间具有包含关系，这大大减少了我们浪费在重复研究上的大量精力， 并使我们对各种! j | 模拟之间的关系有了更深的体会。 本章将定义异步非对称c h i 演算的l 互模拟关系，并构造出该演算的互模 拟格。 3 2l 互模拟 我们将定义一类c h i 进程上的互模拟等式，它们由不同允许动作集所诱导。 l 互模拟和互模拟格是建立在动作分类的基础上的。为这个目的，我们引 入下列符号。定义加为自由输出集 a x l 口，x n ) ，定义， 为自由输入集 a x 】i 口，x n ) ，定义厂f 为约束输入集 a ( x ) i 口，x n ) ，定义r o 为约束输出集 a ( x ) l 口，x n ，定义u 为自由更新集 眇x 】ix ，y n ，定义l u 为约束更新集 ( y x ix ，y n ) 。这六个动作集是对整个动作集合的一个划分。 定义l 为 u ss 声，r i ，i 0 ，u ，r u s 矽) 。 1 0 上下文是有空位的进程。它被递归地定义如下： 定义3 1 ( a ) 】是一个上下文； ( b ) 如果c 玎是一个上下文，那么c 口lp ，pc 口，( x ) c 口，a x c 口， x = j ， c 】是上下文。 一个在c 上的二元关系r ，如果对任何上下文c 【】，pr q 蕴涵c p r c q 】， 则称r 是上下文封闭的。上下文的封闭性确保以后定义的l 互模拟对于上下文 是稳定的。但对于完全上下文是不包括在内的，我们本文不考虑完全上下文的 情况。完全上下文是：如果c 是一个上下文，那么c 】+ 尸，尸+ c 【】， x y 】c 】 是完全上下文。 一个在c 上的二元关系r ，如果对于任意代换盯，p r q 蕴涵有尸仃r q c r ， 那么r 是对代换封闭的。 定义3 2 令r 是c 上的一个二元对称关系并且是l 的一个元素。如果当 p r q ，并且对于任意旯l u r 有p 与p ，那么存在q 。使得q j q r 尸。 称关系r 是一个关系。 工互模拟是 ：下文封闭的关系。，是最大的工互模拟。 根掘定义，如果p 的一个允许动作五，也就是a l ，能被q 的同一动作所 模拟，并且反之办然，则p 和9 是互模拟的。 上下文封闭性保证了三互模拟对所有操作( 除了s u m 操作外) 是稳定的。 定理3 3 如果pj 只。q 并且qj q l p ，那么p 。q 。 证明：我们将证明r = ( p ，q ) ipj 日。饼n q q l 。p ) 是 并且互模拟 关系。对于动1 仨五r , u ( r ) ，如果p p ，那么由已知q l 。p ，根据定义， 存在q 使得q ljq 。p 。由此推出q jq 。p 。反之，也一样，对于动作 五气三u f ) ，如果q 与q 。，那么由已知鼻。q ，根据定义，存在p 使得 e j 尸。q ，由此推得尸j 尸。q 。根据l 互模拟定义，即定义3 2 ，即得到 p q 。 弓i 理3 4 如果p ，q ，r c ，贝0 ； ( 1 ) a x p la x q ： ( 2 ) 尸ir lql 尺，尺ij p rq ； ( 3 ) ( x ) p 气( x ) q ； ( 4 ) 瞳= y e 【x = y 】q ； ( 5 ) x y p 【x y 】q 证明：显然可以从定义3 2 直接推出。 定理3 5 如果p 。q ，那么对于任何代换盯，尸盯 。 证明： 假设p q 。我们必须证明x f n ( pq ) 并且y x ，有 p y x 】lo y x 】。 设b 是一个新名，假设五l 并且n ( 2 ) n 办( piq ) = 。由引理3 4 的( 2 ) 和( 3 ) ， 我们有：( x ) ( pi ( 砂ih 兄) ) 。( x ) ( qi ( 砂ib x 力) ) 。 显然，( x ) ( 尸i ( 砂1 版旯) ) 山与p l y x 】l ( 0 lo ) ， 由定义3 2 和定理3 3 知，存在9 7 使得 ( x ) ( ql ( b yl 撅兄) ) ( x ) ( ql ( b yi 如力) ) j l q 。 j ，x i ( ol 旯) jql ( 00 ) le y x 】l ( 00 ) 由定义3 2 ， 有q 。p y lx 】。对于某个q 。和q l 使得qjq 且 q y x g p y x 。因此我们得到：q y x 】jq y x 】jg lp y x 】。 同理，存在鼻使得? y x 】日lq y x 】。由定理3 3 ，我们有p y x 】q y x 】。 综上所述，我们可归纳得到：对于任意代换盯，有尸仃，q o - 。 由于l 关系乇备了引理3 4 的( 2 ) 、( 3 ) ，以及定理3 5 ，我们得到l 关系是 上下文封闭的，即l 关系就是l 互模拟关系。 3 3互模拟格 令l ( z ) 为 ，il l ) ，是所有l - 互模拟关系的集合。l ( z ) 是由c 来实现 的包含序关系。x j 。f 厶，岛l ( z ) 来说，u 如是它们的最大下确界，实际上 就是交集，即i i u l 2 互厶并且，1 u k k 。在异步非对称c h i 演算中，我们称 ( l ( z ) ，c ) 为异步非对称c h i 进程的互模拟格。由定义3 2 ，可导出6 3 个一 互模拟关系，但它们并非都是互异的。在下面的定理中，我们将提供必要的信 息，用来构造出异步非对称c h i 演算的互模拟格。 定理3 6l 是l 上的一个元素，对于异步非对称c h i 演算下列的特性成立： ( 1 ) ，。玲。= 力； ( 2 ) 如果f i nl , = 矽并且厶，则l 鐾厶： ( 3 ) 如果r u n & = 矽并且r u l 2 ，那么鐾岛； ( 4 ) 如果”n 厶= 并且“厶，那么厶岛： ( 5 ) 少，。，。c 。； ( 6 ) 。u ，i ，。， 。，。， ，。互不相同。 证明：( 1 ) ( a ) 假定尸lq 、尸玛p 。、r 为( y ) a y b y ，6 为新名。那么根据引 理3 4 的( 2 ) ，我们有尸lr lal 尺。 那么尸ir 山坐bp 。l0 ，根据定义3 2 ，存在q 使得qr j q 。10 并且 p 10 ，q 10 。在qr q 10 ，必须在o 与r 之f , j 的通信发生后才做动作6 0 ) 。 因此qjq 。即9 g 灿0 2j9 。 据定义3 2 ，我们仃p 。o 。 即，互 1 2 ( b ) 假定p q 并且尸旦盟一p 。又假定万l 并且挖( 万) n f n ( plq ) = 矽，并 有某个新名z ，掘引理3 4 的( 2 ) ，我们有pi ( 瑟+ ) qi ( 琵+ ) 。如果 尸l ( 瑟+ ) 山异io ，对于新名z 使得p 兰e z x z 】。那么必须存在某个g 使 得ql ( 瑟+ ) jq l0 p l0 。因此，q jg 只。因此，根据定理3 5 ， 我们有q l x ：】。x z 】。 我们根据引理2 4 ，我们有 q j q , x z 】正p , l x z 】- p 。i n n ，假定p 。q 并且q 屿q ，我们同样可 得到pj x z ，q , x z 】三q 。根据定义3 2 ，并且由于动作口( x ) r i ，因此 我们有p 。q 。凶此，。 ( c ) 假定p ，q 并且p 旦【屿p 。令r 为口【对 使得艿l 并且 n ( 8 ) f l f n ( pq ) = 矽 。根据 引 理3 4 的( 2 ) ，我们有 尸i ( 口【x 】+ ) ，qi ( 口【x 】+ ) 。勇b 么pi ( 口 x 】+ ) = _ 专尸。l0 。紧接着存 在q 。使得9f ( 口 x 】+ ) j9 10 并且p 。q 。由于该演算具有非对称性，一 定是这样的情况：q q 。同理，假定p 。q 并且q 蚂q ，我们同样可得 到：尸p 。根扔：定义3 2 ，我们有p 向q 。因此，我们得到了向。 由( a ) ，得加。，。，d ；由( b ) ，得。：由( c ) ，得。加，并综合 起来，得至0 ：。= ，= ，白。 ( 2 ) 假设少n 厶= 矽并且厶。那么 ( x ) a x ( 6 ) ( 6 【z 】i 缸) l 口【z 】+ ( x ) a x ( 6 ) ( 6 z 】ih ) 但是 ( x ) a x ( 6 ) ( 6 z 】l6 x ) 笋l 2a z 】+ ( x ) a x ( 6 ) ( 6 z 】i 缸) 。 可得厶名矿 ( 3 ) 很明显，我们有( 口) ( ( x ) 甜l 讲y 】) 笋，- u 0 ， 但是当，“n 厶= 矽时，( d ) ( ( x ) 甜l 口【y 】) 厶0 。 可得厶g 岛。 ( 4 ) 令r 为( 6 ) ( z ) ( 6 zlb x ( 口) ( 口吲i 矽+ a y 】i 死) ) 。 假定un 厶= 并且列厶。 另b 么r 厶( 口) ( 口【x 】i 石少) + 足，但是r 乒l 。( 口) ( 口【x 】i 石少) + 尺。 可得厶垡岛。 ( 5 ) 由( 1 ) ，得： ，i ，口，。，。，d 。 由( 2 ) ，可得：，口g ，； 由( 3 ) ，可得：。鐾。； 由( 4 ) ，可得：。鐾。 即得：，i ，c ，d 。 ( 6 ) 从。u _ j 、。w 、，i 啪、。、 和。中任取二个互模拟关系，通过使 用( 2 ) 、( 3 ) 、( 4 ) ，侈| j 如。和。，由( 2 ) 可得：。u 。g 。u 一，即得。u 。u ，7 。 由于选取互模拟关系的任意性，类似地，可得。u 一，。w ，一。，。， 。，。互不相同。 证毕。 综合起来，根据定理3 6 的( 1 ) 、( 5 ) 、( 6 ) ，我们可以构造出由严格包含序关 系c 实现的异步非对称c h i 演算的互模拟格，该演算的互模拟格能在下图中画 图l 中箭头为严格包含序关系c 。每个标号节点上的符号表示一组完全相 同的l 一互模拟关系中的一个代表元。例如，符号为“肌，加。”的节点是l - 互模 拟关系等价类 i r gl a f i uu l r uu