（计算机应用技术专业论文）基于进程代数的多路访问协议模型研究与实现.pdf

华东师范大学硕士学位论文基于进程代数的多路访问协议模型研究与实现摘要通信需要各种协议的参与，如何描述这些协议，如何确保这些协议的一致性，正确性和完备性成为一个难题。人们提出了很多理论来刻画这些协议，如p e t r i 网，形式化方法等。进程代数属于形式化方法的一种，它具有强大的机制，对于分析和描述复杂的网络协议拥有较大的优势。多路访问协议是为了解决媒体存取控制子层中数据帧发送问题而提出的一簇协议。分析协议内容可知，它所解决的是多个客户端同时向通信信道发送数据的问题，明了的说就是解决的多个进程并发的问题。多个进程在资源有限的情况下，如何利用有限的资源让系统推行下去，是该协议所要解决的问题。本文的目的在于以多路访问协议为基础，抽象出多进程并发的共同特征，提出一种简单的通用模型，使用进程代数分支之一通信系统演算( c c s )对模型进行形式化建模。使得该模型不仅适用多路访问协议也能适用于其它多进程并发问题，如多核c p u 调度模型中。最后，使用模型检验工具e c w 对模型的正确性进行证明，并把该模型应用到多路访问协议和多核c p u 调度模型中以检验模型的适用程度。关键词：并发；多路访问协议；通信系统演算英文摘要a b s t r a c tc o m m u n i c a t i o nn e e d sm a n yc o m m u n i c a t i o np r o t o c o l sc o o p e r a t et o g e t h e r h o wt od e s c r i b et h e s ep r o t o c o l sa n dh o wt om a k es u r et h ea c c o r d ，c o r r e c t n e s sa n di n t e g r i t yi sah a r dw o r k m a n yp r o t o c o l sh a db e e nr a i s e dt od e s c r i b et h e s ep r o t o c o l s ，s u c ha sp e t r in e ta n df o r m a lm e t h o d se t c p r o c e s sa l g e b r ai sb r a n c ho ff o r m a lm e t h o d sa n do w n sp o w e r f u lm e c h a n i s m b e c a u s eo ft h i sa d v a n t a g e ，i tc a l la n a l y s ea n dd e s c r i b ec o m p l e xn e t w o r kp r o t o c 0 1 m u l t i p l ea c c e s sp r o t o c o l sa r eac l u s t e ro fp r o t o c o li no r d e rt ot a c k l ew i t hs e n d i n gd a t a - f r a m ep r o b l e mi nt h em e d i u ma c c e s sc o n t r o ls u b l a y e r 。t h ea i mo ft h e s ep r o t o c o l si st ot a c k l ew i t hp r o b l e mt h a tm a n yc e e n t ss e n d i n gd a t at oac h a n n e l ，a l s og i v e sas o l u t i o nt od e a lw i t hm u l t i - p r o c e s sp a r a l l e lp r o b l e m t h ep r o t o c o lf o c u so nh o wt om a k e st h es y s t e mr u nv e r yw e l lw i t hl i m i t e dr e s o u r c e t h ea i mo ft h i sp a p e ri st oa b s t r a c tc o m m o nc h a r a c t e ro ft h ep r o t o c o l sa n dt ob u i l dac o m m o nm o d e lb a s eo nt h em u l t i p l ea c c e s sp r o t o c o l s w ew i l lc o n s t r u c taf o r m a lm o d e lu s i n gc a l c u l u so fc o m m u n i c a t i o ns y s t e m sw h i c hi sb r a n c ho ft h ep r o c e s sa l g e b r aa n dv e r i f yt h ec o r r e c t n e s so ft h em o d e l 1w i l lm a k es u r et h em o d e ln o to n l yc a nb eu s e di nt h em u l t i p l ea c c e s sp r o t o c o lb u ta l s oc a nb eu s e di nt h eo t h e rs i t u a t i o na b o u tm u l t i p l ep r o c e s sp a r a l l e l ，s u c ha st h em o d e la b o u ts c h e d u l i n gm u l t i c o r eo nc p u a tl a s t ，1w i l lu s em o d e lc h e c kt o o l e c wt oc h e c kt h ec o r r e c t n e s so ft h em o d e la n du s et h ep r o t o t y p et od e s c r i b em u l t i p l ea c c e s sp r o c e s sa n dt h em o d e ls c h e d u l i n gm u l t i c o r eo nc p ut ov e r i f ya p p l i c a b i l i t yo ft h em o d e l k e yw o r d s ：c o n c u r r e n t ；m u l t i p l ea c c e s sp r o t o c o l s ；c a l c u l u so fc o m m u n i c a t i o ns y s t e m s一1 1 学位论文独创性声明本文所呈交的学位论文是我在导师的指导下进行的研究工作及取得的研究成果。据我所知，除文中已经注明引用的内容外，本论文不包含其他个人已经发表或者撰写过的研究成果。对本文的研究做出重要贡献的个人和集体，均己在文中做了明确说明并表示谢意。作者签名：俏凌驾日期：如。7 ，2 、|学位论文授权使用声明本人完全了解华东师范大学有关保留、使用学位论文的规定，学校有权保留学位论文并向国家主管部门或其指定机构送交论文的电子版和纸质版。有权将学位论文用于非赢利目的的少量复制并允许论文进入学校图书馆被查阅。有权将学位论文的内容编入有关数据库进行检索。有权将学位论文的标题和摘要汇编出版。保密的学位论文在解密后适用本规定。学位论文作者签名：付凌驾导师签名：豸庭硝日期：b 9 胁日期：沁7 ，1 飞fo r i g i n a l i t yn o t i c ei np r e s e n t i n gt h i st h e s i si np a r t i a lf u l f i l l m e n to ft h er e q u i r e m e n t sf o rt h em a s t e r sd e g r e ea te a s tc h i n an o r m a lu n i v e r s i t y , 1w a r -r a n tt h a tt h i st h e s i si so r i g i n a la n da n yo ft h et e c h n i q u e sp r e s e n t e di nt h et h e s i sh a v eb e e nf i g u r e do u tb ym e a n yo ft h er e f e r e n c e st ot h ec o p y r i g h t ，t r a d e m a r k ，p a t e n t ，s t a t u t o r yr i g h t ，o rp r o p r i e t yr i g h to fo t h e r sh a v eb e e ne x p l i c i t l ya c k n o w l e d g e da n di n c l u d e di nt h er e f e r e n c e ss e c t i o na tt h ee n do ft h i st h e s i s s i g n a t u r e ：j 瓜c o p y r i g h tn o t i c eih e r e i na g r e et h a tt h el i b r a r yo fe c n us h a l lm a k ei t sc o p i e sf r e e l ya v a i l a b l ef o ri n s p e c t i o n if u r t h e ra g r e et h a te x t e n s i v ec o p y i n go ft h et h e s i si sa l l o w a b l eo n l yf o rs c h o l a r l yp u r p o s e s ，i np a r t i c u l a r ，s t o r i n gt h ec o n t e n to ft h i st h e s i si n t or e l e v a n td a t a b a s e s ，a sw e l la sc o m p i l i n ga n dp u b l i s h i n gt h et i t l ea n da b s t r a c to ft h i st h e s i s ，c o n s i s t e n tw i t h ”f a i ru s e a sp r e s c r i b e di nt h ec o p y r i g h tl a wo ft h ep e o p l e sr e p u b l i co fc h i n a a u t h o rs i g n a t u r e ：d a t e ：汕5 ，、l付姿莺h 、弋m e n t o rs i g n a t u r e ：l 哆办)华东师范大学硕士学位论文基于进程代数的多路访问协议模型研究与实现第一章绪论1 1 本文研究的背景计算机科学从诞生开始就是一门发展迅猛的学科，而且应用范围广泛，渗透到社会生活中的各个领域，如天气预报、图像处理和各种信息管理支持系统都会用到计算机来处理数据。而计算机科学在发展的过程中也遇到了很多问题，如当今大家所关注的进程的并发问题。简单介绍一下并发问题：在计算机发展的初期，还没有操作系统，计算机至始至终执行地一个程序，这个程序直接访问机器的所有资源。这样的一个程序运行在没有保护的硬件上，写起来相当困难。由于每次只能运行一个程序，不能很好的利用计算机的硬件资源，比如程序访问内存的时候，处理器空闲出来，浪费了宝贵的处理器时间。如何充分利用资源，即让多个程序同时在一计算机上执行不浪费资源，就产生了并发。程序的并发带来了很多问题，如公平性：程序a 和程序b 同时在计算机上执行，可能程序a 执行了很长的一段时间，而程序b 却一点也没有执行；还有临界资源的访问问题：程序c 和程序d 都需要访问打印机，如果程序c 访问打印机打印了一行就退出，程序d 接着执行程序打印了一行也退出了执行，程序c 和程序d 如是反复，结果打印出来的东西很乱导致无法阅读，也得不出想要的结果。如何描述和控制程序的并发是当今计算机科学界所关注度的热点问题之一。我们知道，计算机非常重要的一个用途是用来通信，而通信需要多个协议参与，在计算机的各种的协议中，描述的并发的不在少数。如何描述这些协议，如何确保这些协议的正确性。出现了很多方法来刻划网路协议，虫u p e t r i 网，形式化方法等。其中在形式化方法中一个十分重要的分支一进程代数，进程代数中主要有三种，c c s ( t h ec a l c u l u so fc o m m u n i c a t i n gs y s t e m s 通信系统演算) 、丌演算( 7 rc a l c u l u s ) 署 i c s p ( c o m m u n i c a t i n gs e q u e n t i mp r o c e s s e s通信顺序进程) 。c s p 是c a r h o a r e 提出的，是面向分布式系统的程序设计语言；c c s 是和丌演算r o b i nm i l n e r 发明的，分别是用于描述通信并发系统和一】一1 2 相关领域的研究状况移动通信并发系统的代数理论。1 2 相关领域的研究状况在进程代数的各个分支中，c s p 和c c s 是最为著名的两种。在c s p 语言中，一个并发系统由若干并行运行的顺序进程组成，进程之间通过通道传递消息来进行通信，每个进程不能对其他进程的变量赋值。进程之间只能通过一对通信原语实现协作：q 一 x 表示从进程q 输入一个值到变量x 中；p x ，同时q 进程执行p v m cii n l pj ( 1 a r g ejv m cl os t o p ) ) )c s p 部分语法定义如下：1 c a rh o s ec o m m u n i c a t i n gs e q u e n t i a lp r o c e s s e sp 8a c mu s a1 9 7 8 82 一华东师范大学硕士学位论文基于进程代数的多路访问协议模型研究与实现尸：= s = f 。u 尸is k i piq _ plp 口pip 几尸lp clp ；pipi lpipi l i pp ；p 表示顺序复合，pi i i p 表示交错。对于每一个进程p ，还应该说明其字母符号集，即该进程动作的集合。后来出现的实用编程语言0 c c a m 即以c s p 为基础发展而成2 。下面简要介绍一下c s p 的基本运算规则：并行合成规则有p i i q s n pl l i q 两种形式。同步并行合成p i i q ，对于p ，q 共同事件集合( q pn 口q ) ，要求p ，q 的行为要严格同步发生，如果只出现p 或q 中的事件则可以独立发生。除了一些基本运算规律外，还有一些严格地依赖于符号表的运算性质。另一种是不确定并行合成p q ，口p 兰q q ，p 和q 各自完全独立作用，而不管其符号表是否相同。系统的每一个作用都是从p 或q 之一的一个作用。若p ，q 的作用同时发生，则从这二个作用中随机地选择一个作为系统的作用3 。选择规则c s p 中有两种选择算子，当环境不能控制进程的选择时，它是“非确定o r ，记为( p n q ) 。产生这类选择的原因可能是有些动作不能被当前环境影响，也不能被观察，这些动作都是内部动作的组合。如自动售货机找零钱的组合从观察者的角度来看就没有办法控制售货机的行为，因为找零钱的组合是内部动作，对外部观察者来说不可观察。如果环境可以控制进程之间的选择，则记为( p i s iq ) ，即只要能控制第一个事件的选择，就可以决定选择是一个进程。若初始时候不能选择p 的第一个作用，则选2 林惠( h t t p ：i k n o w s e f o r g e o r g s e w i k i x e 9 8 0 9 a e 4b fa l e 9 一a l _ b a e 5 一b a 一8 f e 8 一b f 一9 b e 7 一a 8 8 b c o m m u n i c a t i n g s e q u e n t i a l p r o c e s s e s e f b c 一8 c c s p )3 肖育东并发进程模型c s p 与c c sp 2 7 一忍8 计算机科学1 9 9 1n o 63 一1 3 论文的研究内容及创新之处择q ；若p ，q 的第一个作用都不能选择，则他们之间的选择是不确定的。这两种选择算子的区别的表达式如下：c _ p 3 d _ q = copld qt ，c d而c p w l d _ q = cjp 几d - - - + q删除规则一般地讲，一个进程的动作符号表恰好包含它所涉及的事件。但在描述一个系统的内部行为时通常要考虑表示其内部作用的事件。在一个系统构造完成以后，其组分结构及内部作用是不再希望被看到的，因为内部动作在需要的时候会自动出现，而且又不能被外部观察者所观察和控制。例如：( p c ) 是一进程，c 中的每一个事件都被删除，其行为像p ，a ( p c ) = ( q p ) c 。如( o 寸c _ pi ic _ b - - - 4 q ) e ) 可化为a _ p x ，( aob - xib ajx ) 。c s p 还有很多其它定义，在此不做介绍。将在第二章对c c s 进行详细介绍。1 3 论文的研究内容及创新之处在计算机通信协议中，很多协议都是都和多进程的并发相关，多路访问协议就是其中之一。多路访问协议是一种用在网络上规范数据传输方法的协议，主要用来规定客户端处于何种状态可以占有物理资源一时间和频率。多路访问技术包括a l o h a ，c s m a c d ，t o k e nr i n g 和t o k e nb u s 。这几种技术都能解决发送数据时候产生的冲突，而且各有各的特点。对于多进程并发执行的时候入一演算不再适用。在并发系统中，进程和函数不再等价，计算的主体不再是函数，而是进程，进程是交互计算的主体，它的行为就是与环境进行交互。基于以上观点，r m i l n e r 于7 0 年代末提出通信系统演算c c s 作为开发系统的语意范型，后来为了描述通信拓扑结构的动态变化的系统，他又与d w a l k e r 和j p a r r o w 合作于8 0 年代末提出了开演算。对于多进程并发问题国内外对这方面的研究有很多，我们所能接触到大都集中在应用领域。如在操作系统多进程并发执行中，可能由于资源( 一般指物理资源如硬盘等) 不足而导致进程相互等待无法推进产生死锁，d i j k s t r a 提出4 一华东师范大学硕士学位论文基于进程代数的多路访问协议模型研究与文现了银行家算法来避免死锁，还有其他的解决死锁的方法如死锁检测和死锁解除方法等。但是它们都是从工程技术的角度来解决问题，本文拟从理论角度来看待这个问题，提出一种解决此问题的通用模型。本文要做的主要工作就是扩展多路访问协议，用c c s 理论对该协议进行抽象提出一种通用的模型，并且对该模型进行相应的扩展。使资源不再局限于某种具体的形式。譬如，多路访问协议中的资源指的是时间和频率，理论模型中的资源不仅仅是指时间或频率，可以是其它的任何物理资源，打印机、磁盘阵列、多核处理器等。模型不作改动或作很少的改动都可以适用到此类类型。最后手工演算或者用自动化验证工具e c w ( t h ee d i n b u r g hc o n c u r r e n c yw o r k b e n c h ) 对模型的正确性进行验证。1 4 论文的内容安排本文组织如下：第一章：绪论。介绍研究课题的背景，提出待研究问题，介绍国内外研究状况，及本文的研究内容和创新之处。第二章：c c s 的发展历程，回顾形式化技术的发展历程，介绍进程代数的分类，重点介绍c c s 相关技术及其分类，以及c c s 模型的验证方式。第三章：对多路访问协议的研究。从本质上揭示多路访问协议存在的实质性问题，介绍多进程并发操作的研究现状和用进程代数的方法研究多进程并发操作的近况。第四章：利用形式化语义的方法构建通用模型。并对模型进行验证，对模型的可能的应用的情况加以说明。第五章：多进程模型的应用。把通用模型应用在多路访问协议和多核的计算机系统中，并对模型进行验证。第六章：总结与进一步的工作。总结本文所做的主要工作和模型中存在的不足，结合形式化语义在实际问题中的发展情况，提出今后进一步的工作。一5 一第二章c c s 的发展历程2 1 形式化技术发展回顾形式化方法在逻辑学中是指分析和研究思维形式结构的方法1 。它把各种不同内容的思维形式( 主要是命题和推理) 进行分析比较，找出它们之间相互关联的方式，例如推理中各个命题之间的联结，命题中包含概念之间的联结，抽取出它们结构上的共同形式；再用表达形式结构的符号语言，用符号之间的联系表达命题或推理的形式结构。例如，把联言命题、假言命题分别形式化为：“p 八口、“pjq 。又例如：一个具体的假言联言推理“如果今天下雨，则我们今天就不去野餐，若我们今天不野餐，则我们明天将去野餐 。因此，如今天下雨，则我们明天将野餐。设p 是命题今天下雨，q 是命题今天去野餐，r 是命题明天去野餐。这个推理的形式结构是：如果p ，则非q ；如果非q ，贝j j r ；若p ，则r 。可以用形式化公式表示如下：( _ 一口) 八( 一口- - - r ) 三p - - 47 。形式化方法在很早以前就已经开始运用了，在现代逻辑中有了进一步的发展和完善。形式化方法特别在数学、计算机科学、高级机器学习等领域得到广泛运用，它能精确地揭示各种逻辑规律。使用形式化方法能方便的制定出相应的逻辑规则，使得各种理论体系更加严密。2 1 1 形式化方法起源及发展软件形式化方法最早始于二十世纪五十年代后期，这个时期开始了对程序设计语言编译技术的研究，出现了各种词法、语法分析程序的自动生成器以及语法制导的编译方法。使得编译系统的开发从手工作坊式发展成为具有成熟理论基础的系统方法。大概过了十年，这个时期是软件历史上的软件危机时期，这次软件危机促使对形式化方法的研究达到了高潮。针对软件危机，人们提出了各种解决办法，总结起来有两类：一是采用工程方法组织和管理软件的开发；二是深入探讨程序设计和程序开发的规律，建立一套严密的理论，用来指1 f e o s u mh t t p ：l l b a i k e b a i d u c o m l v i e w l l 7 3 1 6 7 9 h t m l t t p = 8 0 16 一第二章c c s 的发展历程导软件的开发实践。前者致使“软件工程”的出现和发展，后者则推动了形式化方法的深入研究。形式化方法发展到现在取得了丰硕成果，从早期最简单的一阶谓词演算方法到现在应用于不同领域、不同阶段的基于逻辑、网络、状态机、代数、进程代数等众多形式方法。形式化方法的渐渐融入了软件开发的各个阶段，从最初的需求分析、功能描述，到中间的体系结构的设计直至最后的编码实现、测试和维护。2 1 2 形式化方法定义形式化方法中用来描述计算机系统开发的方法都是描述一些系统性质的数据技术，这些方法提供了一个框架，人们可以在框架中以系统的方式刻划、开发和验证系统。如果一个方法有良好的数学基础，那么我们就可以说它就是形式化的，典型地以形式化规约语言给出。这个基础要提供一系列精准定义的概念，如：一致性和完整性，以及定义规范的实现和正确性。形式化方法的本质是基于数学的方法来描述目标软件系统属性的一种技术。不同的形式化方法的有着不同的数学基础，有的以集合论和一阶谓词演算为基础( 如z 和v d m ) ，有的则以时态逻辑为基础。形式化方法还需要形式化规约说明语言的支持。2 1 3 形式化方法研究内容形式化方法研究的一个重要内容是形式化规约，它是对程序“做什么”的数学描述，用具有精确语义的形式语言书写的程序功能描述，它是设计和编制程序的出发点，同时也是验证程序是否正确的依据。对形式规约一般要讨论其一致性( 自身无矛盾) 及完备性( 是否完全、无遗漏地刻画所要描述的对象) 等性质。形式规约方法主要可分为两类：一类是面向模型的方法，该方法是通过构造系统的计算模型来刻画系统的不同行为特征；另一类是面向性质的方法，此方法通过定义系统必须满足的一些性质来描述一个系统。不同的形式规约方法要求不同的形式规约语言，即用于书写形式规约的语言，如代数语言o b j 、c l e a r 、a s l 等；进程代数语言c s p 、c c s 、丌演算等；时序逻辑语言p l t l 、c t l 、x y z e 、u n i t y 、t l a 等；由于这些规约语言基于不同的一7 -2 1 形式化技术发展回顾数学理论及规约方法，因而千差万别，但它们有一个共同的特点，即每种规约语言均由基本成分和构造成分两部分构成。前者用来描述基本( 原子) 规约，后者把基本部分组合成大规约。构造成分是形式规约研究和设计的重点，也是衡量规约语言优劣的主要依据。下面给出用于顺序和并发程序形式规约的常见方法及语言：形式验证形式化方法的另一重要研究内容是形式验证。形式验证与形式规约之间具有紧密的联系，形式验证就是验证已有的程序( 系统) p 是否满足其规约( 妒，妒) 的要求( h p p ( q o ，矽) ) ，它们也是形式化方法所要解决的核心问题。传统的验证方法主要包括模拟和测试，这是通过实验方法对系统进行查错。模拟和测试分别在系统抽象模型和实际系统上进行，一般的方法是在系统的某个点上给予输入，观察在另一点的输出情况，这些方法花费很大，而且由于实验所能涵盖的系统行为有限，很难找出所有可能存在的错误。基于这个原因，早期的形式验证主要研究如何使用数学方法，严格证明一个程序的正确性。2 1 4 形式化方法分类根据说明目标软件系统的方式，形式化方法可以分为两类：面向模型的形式化方法：面向模型的方法通过构造一个数学模型来说明系统的行为。面向属性的形式化方法：面向属性的方法通过描述目标软件系统的各种属性来间接定义系统行为。根据表达能力不同，形式化方法可以分为以下五类：基于模型的方法：通过明确定义状态和操作来建立一个系统模型( 系统从一个状态迁移到另一个状态) 。用这种方法虽可以表示非功能性需求如时间需求，但不能很好地表示并发性。如：z 语言，v d m ，b 方法等。基于逻辑的方法：用逻辑描述系统预期的性能，包括底层规约、时序和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编程构造扩充逻辑从而得到一种通用的形式化方法，通过保持正确性的细化步骤集来开发系统。如：区间时序逻辑，区段演一8 一第二章c c s 的发展历程算，h o a r e 逻辑，模态逻辑，时序逻辑，时序代理模型，实时时序逻辑等。代数方法：通过将未定义状态下不同的操作行为相联系，给出操作的显式定义。与基于模型的方法一样，该方法没有给出并发的显式表示。如：o b j ，l a r c h 族代数规约语言等；过程代数方法：通过限制所有允许的可观察的过程间通信来表示系统行为。此类方法允许并发过程的显式表示。如：通信顺序过程( c s p ) ，通信系统演算( c c s ) ，通信过程代数( a c p ) ，时序排序规约语言( l o t o s ) ，计时c s p ( t c s p ) ，通信系统计时可能性演算( t p c c s ) 等。基于网络的方法：由于图形化表示法易于理解，而且非专业人员能够使用，因此是一种通用的系统确定表示法。该方法采用具有形式语义的图形语言，为系统开发和再工程带来极大的好处。如p e t r i 图，计时p e t r i 图，状态图等。2 2 进程代数分类进程代数是关于通信并发系统的代数理论的统称。2 0 世纪7 0 年代后期，英国爱丁堡大学学者r o b i n m i l n e r 和c a r h o a r e ，分别提出了通信系统演算和通信顺序进程，开创了用代数方法研究通信并发系统的先河。此后这一研究方向兴盛不衰，出现了众多类似而又相互区别的演算系统，女h a c p ，a t p 和l o t c 6 等，统称为进程代数。这些代数理论都使用通信，而不是共享存储，作为进程之间相互作用的基本手段，表现出面向分布式系统的特征。在语法上，进程代数用一组算子作为进程的构件。算子的语义通常用结构化操作语义方法定义，这样进程就可看成是带标号的变迁系统。进程代数的一个显著特征是把并发性归结为非确定性，将并发执行的进程的行为看成是各单个进程的行为的所有可能的交错合成，即所谓交错语义。进程代数研究的核心问题是进程的等价性，即在什么意义下两个进程的行为相同? 在进程代数领域使用的最为广泛的等价关系有互模拟、测试等价、失败等价( 参见通信顺序进程) 等。对这些语义等价关系均建立了相应的公理系统。对于公理系统的研究不仅加深了对语义理论的理解，而且使对语义等价关系进行形式推理成为可能。为了将进程代数的理论成果应用+ r j ：解决实际问题，2 0 世纪8 0 年代后期出现9 一2 3c c s 及其相关技术了许多计算机支持工具。用这些工具可对进程的行为进行推理或模拟。2 3c c s 及其相关技术c c s 是一种普适并发进程模型，它所需要的条件比较弱，是一种操作语义。c c s 主要的贡献在于并发系统的等价性研究，主要是建立在互模拟上的观察等价，互模拟包括弱等价和强等价两种。c c s 理论认为两个动态的系统之间存在一种不变性，通过建立这种不变性的模型，可以证明这个两个系统的等价关系。c c s 中存在外部动作和内部动作，外部动作是外部观察者所能看到的，而内部动作是系统内部的行为，外部观察者看不到，其实也不必要关注。从外部观察者来看，只要知道两个系统的外部行为是否相同即可，而不必关注其内部行为，这正符合人类的行为习惯。观察等价的概念具有严格的数学形式，是一套完备的并发系统理论。2 3 1c c s 的基本计算下面介绍一下c c s 的基本运算。设集合= q ，卢，y ) ，其补集丕= 西iq ) ，标号集合7 = au 五，还引入一个不可知( c c s 中称为沉默的，s i l e n t ) 的作用7 _ ，并定义a c t = 7u 丁) 。k = aia 是事件) 表示事件常量集合，x = zlz 是事件变量) 表示动作集合。用= b ) 表示表达式集合。一个类( s d 庀) 是子集1 a c t ，使事件( 或称为系统) p 有类7 ，p ：1 指p 的所有动作都在- 1 中。c c s 符号表达式由如下规则构成：前缀规则：a ( z ) e ，7 _ e ，a ( z ) 。7 a c t i ，o ( z ) ，1 表示动作，口 ) ，7 - 动作发生后e 的行为变为o ( z ) e 和7 - e ，可以用e 7 和e ”来代替，可以表示爽e 墼e lw e 与eo选择( 求和) 规则：涮局，i 是动作集合：最表示任意最之一的行为，若i = 0 时，它为0 ；若i = 2 ，它是尻+ 岛。并行规则：e 1i 饬：表示易岛是并行的行为，他们通过互补的作用进行通信。一1 0 第二章c c s 的发展历程限制规则：e l ，l 1 ：e 的行为只是事件e 的行为，只是事件e 中的所有动作都不在l 中或l 的补集中。重标号规则：e 【门，f 是重标号函数( r e l a b e l ) ：e 门的行为只是e 的行为，但其作用有，重新标号。递归规则：f i ( 翰= e ：i ，) ) ，j ，：它指由甄= e j ，i ，) 定义的事件集合的第j 个分量。一般记 f iq ( z = 秀) ：j ，) 。还有一个条件规则，如果布尔型变量b 为真，则e ，还可以把常量任意个常量a 定义为：a ( x 1 ，z n ) d = e fe 下面在标号系统上给出上述规则的迁移语义2 ：a 以a e - - - 与fs u 叻毫盏( 歹，)c o m l 岛c 。仇2 而f - f c a m 3 唏鸟影胍瓣e - - - e ( 叩譬l ) 觑。赫c o n 影( a 型p )r e 勺鬻群( 歹，)2 3 2c c s 基本定律由c c s 的定义可以证明组合子的一些基本运算性质，把它们分成三组定律，即静杰律绢动杰律组和扩展律绸。静态律组：它主要与并发，限制，重标号组合算子有关，可以把它看成流程图上的代数。p i q = q i 尸；合成律：p ( q r ) = ( p l q ) i 冗；r i o = pp l = p ，i yr ( p ) n ( lu 劲= 妒；限制律：嚣& ：￥掣乏( p i q ) l = p l q l ，i fr ( p ) n f 泵万n ( lu - ) = 垆2 r o b i nm i l n e rc o m m u n i c a t i o na n dc o n c u r r e n c y 只6 一p 5 8p r e n t i c eh a l l1 9 8 91 l 一2 3c c s 及其相关技术p i a 日= p ：重标号律：；够 i 】! 翠i 鼻f ，r p = 厂。r p k( p i q ) f 】= p f lj q f 】i ，f ( luz ) 为一对一，这里l = r ( p i q )动态律组：动态定律主要与前缀，并行及常事件行为有关，由于这些组合算子的出现仅在作用发生之前，故称为动态律。由于我们经常把常事件视为一元组合算子，递归组合算子是有选择地使用常事件，也是。种动态组合算子。p + q = q + p ；单子律：；：譬加h 冠p + 0 = p ：q 丁p = 口p ：丁律：p + 7 p = 7 - p ；q ( p + 7 - q ) + q q = q ( p + 7 - q )扩展律组：它把两种组合算子联系起来。令p = ( p 1 1 i r ) l ，礼1 ，则p = q ( p 1i 1 只i - ir ) l ：只与只，q 譬luz ) + 丁( p 1i i 爿| 巧i ir ) l ：只与只，只与巧，i 歹)对于扩展律的一些特殊情况，还可以得到：( q q ) l 一 q 0 q li fq 三ul ，( a q ) ( ，) = 厂( a ) q ( ，) ；( q + r ) l = q l + r l ；( q + 兄) ( ，) = q ( f ) + r ( f ) 2 3 3 等价性理论等价性的研究在c c s 理论中处于中心地位，也是c c s 理论所要的表达的核心所在。等价性分为强等价性和弱等价性，下面做一下通俗的解释。强等价性要求极为严格，假设两个系统a 和b ，如果系统a 能做任意一个动作a c t i o n 使得系统由状态x 到状态y ，那么系统b 同样要做一个动作使得系- 1 2 第二章c c s 的发展历程统从状态x n 状态y ，而且当中不存在任何的不可见动作状态7 - ；反过来，如果系统b 能做任意一个动作a c t i o n 使得系统由状态x n 状态y ，那么系统a 同样要做一个动作使得系统从状态x n 状态y ，而且当中不存在任何的不可见动作状态7 - 。此之谓强等价性。下面给出定义，如果二元关系s 0 0 ，且( p ，o ) s ，a a c t 满足下列关系就是强等价的互模拟。( 1 ) 如果p 与p 7 ，则存在q 7 使q 与q 7 且( p ，q 7 ) s( 2 ) 如果o 与q ，则存在p 7 使p 与p 且( p 7 ，q ) sp 和q 的强互模拟表示为p q 。可以证明强互模拟是同余关系( 自反闭包，传递闭包和对称闭包) ，这是个非常好的数学性质。所有的动作在表达式中具有平等的地位，包括内部动作。我们知道内部动作从外部观察者的角度来看是无法看到的，因此一般不把内部动作和外部动作平等的看待。如：7 - q 0 和7 - 口但是从外部来看却无法看出两个进程的区别，因为丁动作是不可见的。如果忽略丁动作，就可以得到弱互模拟关系。弱等价性没有强等价性要求严格，假设两个系统a 和b ，如果系统a 能做任意一个动作a c t i o n 使得系统由状态x n 状态y ，那么系统b 同样要做一个动作使得系统从状态x n 状态y ，当中可以存在不可见动作状态7 - ，也就说系统b 可以经过若干动作( 而这些动作对a 来说不是必须的) 也能到相同的效果；反过来，如果系统b h r , 做任意一个动作a c t i o n 使得系统由状态x n 状态y ，那么系统a 同样要做一个动作使得系统从状态x n 状态y ，而且当巾可以存在不可见动作状态丁。此之谓弱等价性。满足下列关系就是弱互模拟。( 1 ) 如果尸与p ，则存在q 7 使q 导0 7 且( p ，0 7 ) s( 2 ) 如果q 与q 7 ，则存在p 7 使p 导p 且( p ，q 7 ) sp 和q 的弱互模拟关系表示为p q 。弱互模拟关系不是同余关系，m i l n e r 提出了一种新的同余关系一观察同余，他给出了观察同余的定义：_ 13 2 4c c s 模型的验证方式( 1 ) 如果p 与p 7 ，则存在q 7 使q 导q 7 且p 7 q 7 。( 2 ) 如果q 与q 7 ，则存在p 7 使p 导p 7 且p q 。p 与q 的观察同余关系表示为：p 竺q 。2 4c c s 模型的验证方式c c s 的验证方式分为两种，一种是手工验证，另一种是自动化验证。2 4 1 手工证明由于c c s 是采用双模拟的方式来刻画系统的等价性。系统从一种状态到另一种状态可能有很多种方式，而这些方式又是我们所不能唯一确定的，所以唯一的办法用数学形式进行展开，进行穷举。事实上，证明c c s 模型的等价性问题也只能展开代数式子穷举证明。2 4 2e c w 自动化证明由上一小节可知，c c s 模型的证明需要等价性穷举测试，这样来说，工作量极大，而且有时候极有可能不能覆盖所有的路径。爱丁堡大学提供t c c s 模型验证工具e c w ( e d i n b u r g hc o n c u r r e n c yw o r k b e n c h ) 。具体情况可以参考爱丁堡大学e c w 的官方网站3 。1 4 第三章对多路访问协议的研究第三章对多路访问协议的研究3 1 载波侦听多路访问协议在以太网中，所有的节点共享传输介质。如何保证传输介质有序、高效地为许多节点提供传输服务，就是以太网的介质访问控制协议要解决的问题。下面介绍一下多路访问协议的发展历程。多路访问协议是一种争用型的介质访问控制协议。它起源于美国夏威夷大学开发的a l o h a 网所采用的争用型协议，并进行了改进，使之具有l t a l o h a 协议更高的介质利用率。另一个改进是，对于每一个站而言，一旦它检n - n 有冲突，它就放弃它当前的传送任务。换句话说，如果两个站都检测到信道是空闲的，并且同时开始传送数据，则它们几乎立刻就会检测到有冲突发生。它们不应该再继续传送它们的帧，因为这样只会产生垃圾而已；相反一旦检测到冲突之后，它们应该立即停止传送数据。快速地终止被损坏的帧可以节省时间和带宽。3 2c s m a c d 协议原理当一个节点要发送数据时，首先监听信道；如果信道空闲就发送数据，并继续监听；如果在数据发送过程中监听到了冲突，则立刻停止数据发送，等待一段随机的时问后，重新开始尝试发送数据。一1 5 3 3c s m a c d 协议控制流程3 3c s m a c d 协议控制流程结束一7一。：一_ _ ：，。t ? 一一? e j i “? 。；一图3 - 1c s m a c d 协议控制流程图c s m a c d 控制流程：控制流程的核心问题：解决在公共通道上以广播方式传送数据中可能出现的问题( 主要是数据碰撞问题) 。控制过程包含四个处理内容：侦听、发送、检测、冲突处理。侦听：通过专门的检测机构，在站点准备发送前先侦听一下总线上是否有数据正在传送( 线路是否忙) ? 若“忙”则进入后述的“退避”处理程序，并进一步反复进行侦听工作。若“闲”，则按照一定算法原则( “x 坚持 算法) 决定如何发送。发送：当确定要发送后，通过发送机构，向总线发送数据。检测：数据发送后，也可能发生数据碰撞。因此，要对数据边发送，边接收，以判断是否冲突了。一】6 一第三章对多路访问协议的研究冲突处理：当确认发生冲突后，进入冲突处理程序。有两种冲突情况：( 1 ) 侦听中发现线路忙，则等待一个延时后再次侦听，若仍然忙，则继续延迟等待，一直到可以发送为止。每次延时的时间不一致，由退避算法确定延迟时间值。( 2 ) 送过程中发现数据碰撞，先发送阻塞信息，强化冲突，再进行侦听工作，以待下次重新发送。3 4 多路访问协议本质问题通过分析上述内容，可以知道，多路访问协议的本质问题在于多个进程的并发。而且各个客户端之间是对等的。多个进程运行过程中不存在优先级的关系，而且客户端向信道发送数据的过程是随机的，无序的。一1 7 -第四章利用形式化语义构建通用模型4 1 构建通用模型4 1 1 单一进程模型在操作系统出现之前，一般只有一个进程运行在计算机上( 其实主要是硬件上) 。这时的进程是独占计算机的，不存在并发概念的。因此模型也简单。独占性的进程访问计算机的资源是实时的，没有任何的延误。图4 _ 1 单一进程访问资源模型图i n 和o u t 是两个通道( c h a n n e l ) ，果从o u t 通道出来，假设数据是d a t a ，a g e n t 些i n ( d a t a ) a g e n t ，( d a t a )用来传输数据的。数据从通道i 扎，处理结传入通道的过程为：1 8 第四章利用形式化语义构建通用模型a g e n t 的状态发生了变化，从最初始态到状态s ( 巨p a g e n t 7 ，也就是a g e n t 接受了数据d a t a ，状态发生了跃迁) 。a 9 e n 放理完数据d a t a 恢复到初始状态为：a g e n t r ( d a t a ) 鬯- o - 五( d a t a ) a g e n t把两个过程整合起来就是：a g