进程代数

第4章进程代数报告人：。。。专业：计算数学1目录4.1通信顺序进程CSP4.1.1进程及其表示4.1.2事件迹及其操作4.1.3进程的复合操作4.1.4进程的模型4.1.5进程之间的通信4.1.6CSP规格的例24.1通信顺序进程CSP通信顺序进程(CommunicationSequentialProcesses--CSP)是分布式并发软件系统规格和设计的进程代数方法。本章讨论CSP的相关概念、分布式并发系统规格等。34.1通信顺序进程CSPCSP是Hoare于1978年建立的一种适合于分布式并发软件规格和设计的形式化方法。TonyHoare出生于1934年于斯里兰卡，其父母为英国人。Hoare于1956年从牛津大学获得学士学位。1977年，Hoare回到牛津大学担任。计算机科学程序语言研究小组的教授。Hoare对程序设计语言的主要贡献为：HoareLogic,快速排序算法(Quicksort)和CSP。他是第十五位图灵奖(1980年)获得者44.1.1进程及其表示在分布式并发软件系统开发中，存在一些相关而又不完全一致的概念：不确定性、平行性、分布性、并发性。不确定性指一个程序的运行可能会有两种或两种以上的方式平行性指一个程序的几个分量在某一时间段内可以相对独立地运行，平行分量共享一片存储区域。平行性的背景是多处理机。分布性指一个程序的几个分量在某一时间段内可以相对独立地运行，分量之间通过交换信息，而不是共享一片存储区域，来协同工作。分布性的背景是计算机网络。并发性指一个系统内部发生的两个事件之间没有因果关系。54.1.1进程及其表示在一个存在着并发性行为的系统中没有统一的时钟。平行性、分布性、并发性是造成不确定性的根源，不确定性只是一种现象。CSP的基本成分是事件和进程。进程是事件或者活动的序列。64.1.1进程及其表示为了表述方便，进行如下约定：由小写字母组成的字符串表示事件；由大写字母组成的字符串表示进程；小写字母x、y、z等表示事件；大写字母A、B、C等表示事件集；大写字母X、Y、Z等表示进程；为一运算子，将每一个进程映射为它的事件集。74.1.1进程及其表示例：SHOPPING是一个进程，它由事件goout,paymoney,getaway,comeback组成，于是有：SHOPPING={goout,paymoney,getaway,comeback}。8•进程基本表示法进程的基本表示法是前缀表示法。设P是一个进程，第一个事件是x，且x执行后，P的剩余部分为Q，则进程P可表示为：xQ，其中x称为前缀；xP、(xQ)=P。并称xQ为前缀表达式。算子“”称为顺序算子。顺序算子的右部总为一个进程，左部总为一个事件。x(yP)、x(y(aQ))、x(y(c(zP)))都是进程的合法表示。PQ和xa是合法表示吗？(不合法)9•进程基本表示法实际使用时进程表达式中的括号也可以省略xyP、xyaQ、xyczP上例中的进程SHOPPING可表示为：SHOPPING=gooutpaymoneygetawaycomebackSTOP。10•进程基本表示法一个进程中活动或者事件的出现可能是有限的--有限进程，也可能是无限的--无限进程。有限进程合法的结尾应该是进程STOP。STOP是一个特殊进程，该进程不执行任何事件或活动。有时为了加以区别，把进程的名字作为STOP的下标如STOPA、STOPSHOPPING。STOPA表示不执行事件集A中的任何事件。对于无限进程，将以递归形式进行描述。11•进程的递归方程表示法设X是一个进程变量，A=X，则进程的递归方程表示为：X=F(X)其中，F(X)是包含有进程变量X的一个前缀表达式，且该递归方程具有事件符号集A上的唯一解。也可表示为：X：AF(X)，表达式中的A可以省略，即表示为XF(X)。12•进程的递归方程表示法要求F(X)包含有进程变量X的一个前缀表达式，为了保证递归方程有唯一确定解，从而给出进程的确切描述。例如，对于X=X，任何X都是该方程的解，描述的是任何进程，也就不能给出给定进程的确切描述。13•进程的递归方程表示法具有前缀表达形式的进程描述，又称为监督的（Guarded）。前缀表达式也称为监督表达式。14•进程的递归方程表示法例如，时钟行为的进程描述如下：CLOCK={tick}CLOCK=tickCLOCK或者CLOCK=X：{tick}(tickX)或者CLOCK=X(tickX)进程的前缀表示和递归方程表示，可以给出具有单一线程特征的顺序执行事件和活动的描述。实际中，存在进程和环境的交互作用，即事件执行的可选择性。下面引入进程选择表达式。15•进程的选择表达式选择表达式给出了从多个前缀事件中选择执行一个的行为描述。从事件x或y中选择一个，并执行相应的剩余进程部分R或Q的情形，可表示为：(x→R|y→Q)符号“|”称为选择算子。16•进程的选择表达式选择不限于两者取一，可以是多者取一，即(x→R|y→Q|…|z→S)对于多者取一的情形，也可以用如下简单形式表示：(x：A→G(x))17•进程的选择表达式其中，A是进程全体事件集合的一个子集；x：A表示A中任一事件均可为该进程的第一个事件；G(x)表示执行事件x后的剩余进程部分。18•进程的选择表达式-举例下面给出了在超级商场购物的进程描述，假定可以任意次序分别购进鸡(getchicken)、购进鱼(getfish)、购进蛋(getegg)，并付款(paymoney)：SHOPPING=goin→(x:{getchicken,getfish,getegg}→G(x))；G(getchicken)=(x：{getfish,getegg}→H1(x))；G(getfish)=(x：{getchicken,getegg}→H2(x))；G(getegg)=(x：{getchicken,getfish}→H3(x))；19•进程的选择表达式-举例H1(getfish)=getegg→paymoney→comeback→STOP；H1(getegg)=getfish→paymoney→comeback→STOP；H2(getchicken)=getegg→paymoney→comeback→STOP；H2(getegg)=getchicken→paymoney→comeback→STOP；H3(getchicken)=getfish→paymoney→comeback→STOP；H3(getfish)=getchicken→paymoney→comeback→STOP.20•进程的选择表达式-举例事实上，许多进程都可以表示成选择表达式的形式。例：x→Q可以表示为（x:{x}→Q（x））；STOP可表示为（x：{}→Q（x）），这里{}表示空集；（tick→CLOCK）可表示为（x:{tick}→Q（x）），Q（x）=（tick→CLOCK）。21•进程的树结构图表示进程也可以树结构图直观地表示。树中结点表示状态，联系结点之间的有向弧线表示状态之间的迁移。树根结点为进程的初始状态；进程沿着弧线执行。弧线旁标注引起该迁移发生变化的事件。始于同一结点的弧线必须有不同的事件标记。22•进程的树结构图表示进程的每一个分支都终止于STOP,STOP在图中用没有输出弧线的结点表示，如图4.1的a，b。为了表示进程的无限行为，可在图中增加一条从叶结点到任一非叶结点的无标记弧，如图4.1的c。23coin--将一枚硬币投入自动售货机的硬币槽choc—由机器的发货器送出一块巧克力toffee--由机器的发货器送出一块太妃糖244.1.2事件迹及其操作从观测者角度所能看到的进程行为就是进程执行所发生的事件序列，下面讨论描述事件序列相关的事件迹以及事件迹之间的操作运算。事件迹是一个进程所执行事件的历史行为的符号记录，简称为迹。迹表示为用尖括号“”和“”括起来的用逗点“,”分开的事件序列。254.1.2事件迹及其操作对于进程P，用traces(P)表示进程P的所有可能迹的集合，并称为进程P的迹。例如：迹x,y包含两个事件，事件y应紧跟事件x之后；迹x是一个仅包含一个事件x的序列；迹是一个空序列，他没有包含任何事件，它是每一个进程的事件迹，因为它对应进程没有事件发生时的情况。264.1.2事件迹及其操作对于打电话进程：PHONE=ring→answer→STOP，、ring和ring,answer都是其可能的迹，即，traces(PHONE)={,ring,ring,answer}；对于STOP进程，它的迹traces（STOP）={}。27•迹的连接CSP中定义了一系列关于迹的操作运算连接运算、投影运算、首/尾运算、星运算等约定：小写字母s、t、u表示迹；大写字母S、T、U表示迹的集合；小写字母f、g、h表示定义在迹集合上的函数或映射。迹的连接---对于迹s和t，将它们中的事件符号依次序排放在一起所得到的迹，称为s和t的连接，记为s^t，符号“^”称为连接运算或连接算子。对于迹s和非负整数n，以sn表示迹s的n次重复连接（规定s0=（空迹））。28•迹的连接例如：ring^answer=ring,answer;tick3=tick,tick,tick。29•迹的投影对于迹s和事件集合A，保留迹s中所有属于A中的事件符号后所得到符号串，称为s在A中的投影，或者s的A限序列，记为(sA)。符号“”称为投影运算或投影算子。例：start,execute,fault,start,repair,end{start,end}=start,start,end;30•迹的投影投影运算性质：A=；(t^s)A=(tA)^(sA)；xA=x如果xA；xA=如果xA；s{}=；{}表示空集（无元素集）(sA)B=s(AB)31•迹的首尾迹的首/尾：设迹s是一个非空事件序列，s中的第一个事件称为s的首，记为s；s中删除第一个事件剩余的部分符号称为s的尾，记为s。符号“”和“”分别称为首运算和尾运算例如：start,execute,fault,start,repair,end’=start;start,execute,fault,start,repair,end’’=execute,fault,start,repair,end。32•星运算星运算：事件集A上所有有限事件符号形成的迹（包括）组成的集合，记为A*。符号“*”称为星运算。A*可递归定义为A*={t|t=(tAtA)}对于进程P，traces(P)(P)*33•迹函数迹函数：迹函数是迹到迹的映射，又称迹映射。对于迹函数f，如果f()=，则称f是严格的；s，t，若f(s^t)=f(s)^f(t)，则称f满足分配律。34•迹的长度迹长度：迹s中事件符号的出现个数，称为迹s的长度，记为#s。符号“#”称为迹的长度运算。例如：#start,execute,fault,repair,end=6对于迹s和事件x，x在s中的出现次数为#(s{x})。35•迹的逆迹的逆：对于迹s，将其中的事件逆序排列后所得到的迹，称为迹s的逆，记为s-1。例如：start,execute,fault,start,repair,end-1=end,repair,start,fault,execute,start36•迹的交替迹的交替：对于迹s和t，将各自的事件依次序交替排列所得到的迹，称为s和t的交替迹，记