第4章 进程代数

1第4章进程代数通信顺序进程(CommunicationSequentialProcesses--CSP)和通信系统演算（ACalculusofCommunicatingSystems---CCS）是分布式并发软件系统规格和设计的进程代数方法。CCS是最早建立的并发系统模型，是进程代数的基础。讨论CSP的相关概念、分布式并发系统规格等对CCS进行简要的介绍24.1通信顺序进程CSP4.1.1进程及其表示CSP是Hoare于1978年建立的一种适合于分布式并发软件规格和设计的形式化方法。TonyHoare出生于1934年于斯里兰卡，其父母为英国人。Hoare于1956年从牛津大学获得学士学位。1977年，Hoare回到牛津大学担任计算机科学程序语言研究小组的教授。Hoare对程序设计语言的主要贡献为：HoareLogic,快速排序算法(Quicksort)和CSP。他是第十五位图灵奖(1980年)获得者。在分布式并发软件系统开发中，存在一些相关而又不完全一致的概念：不确定性、平行性、分布性、并发性。34.1.1进程及其表示不确定性指一个程序的运行可能会有两种或两种以上的方式平行性指一个程序的几个分量在某一时间段内可以相对独立地运行，平行分量共享一片存储区域。平行性的背景是多处理机。分布性指一个程序的几个分量在某一时间段内可以相对独立地运行，分量之间通过交换信息，而不是共享一片存储区域，来协同工作。分布性的背景是计算机网络。并发性指一个系统内部发生的两个事件之间没有因果关系。44.1.1进程及其表示在一个存在着并发性行为的系统中没有统一的时钟。平行性、分布性、并发性是造成不确定性的根源，不确定性只是一种现象。CSP的基本成分是事件和进程进程是事件或者活动的序列54.1.1进程及其表示约定：由小写字母组成的字符串表示事件；由大写字母组成的字符串表示进程；小写字母x、y、z等表示事件变量；大写字母A、B、C等表示事件集；大写字母X、Y、Z等表示进程变量；为一运算子，将每一个进程映射为它的事件集。6•进程基本表示法进程的基本表示法是前缀表示法设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)))都是进程的合法表示。进程表达式中的括号也可以省略7•进程基本表示法一个进程中活动或者事件的出现可能是有限的--有限进程，也可能是无限的--无限进程。有限进程的合法结尾是一个特殊进程STOP，表示不执行任何事件或活动。有时为了加以区别，把进程的名字作为STOP的下标STOPA表示不执行事件集A中的任何事件。对于无限进程，将以递归形式进行描述。8•进程的递归方程表示法设X是一个进程变量，A=X，则进程的递归方程表示为：X=F(X)F(X)是包含有进程变量X的一个前缀表达式，即F(X)=(x:AX)，且该递归方程具有事件符号集A上的唯一解。也可表示为：X：AF(X)，表达式中的A可以省略，即表示为XF(X)为保证递归方程有唯一确定解，要求F(X)包含有进程变量X的一个前缀表达式，从而给出进程的确切描述。例如，对于X=X，任何X都是该方程的解，描述的是任何进程，也就不能给出给定进程的确切描述。具有前缀表达形式的进程描述，又称为是监督的（guarded）。前缀表达式也称为监督表达式。9•进程的递归方程表示法例如，时钟行为的进程描述如下：CLOCK={tick}CLOCK=tickCLOCK或者CLOCK=X：{tick}(tickX)或者CLOCK=X(tickX)进程的前缀表示和递归方程表示，可以给出具有单一线程特征的顺序执行事件和活动的描述。实际中，存在进程和环境的交互作用，即事件执行的可选择性。下面引入进程选择表达式。10•进程的选择表达式选择表达式给出了从多个前缀事件中选择执行一个的行为描述从事件x或y中选择一个，并执行相应的剩余进程部分R或Q的情形，可表示为：(x→R|y→Q)符号“|”称为选择算子选择可以是多者取一，即(x→R|y→Q|…|z→S)对于多者取一的情形，也可以用如下简单形式表示：(x：A→G(x))A是进程全体事件集合的一个子集；x：A表示A中任一事件均可为该进程的第一个事件；G(x)表示执行事件x后的剩余进程部分。11•进程的选择表达式-举例下面给出了在超级商场购物的进程描述，假定可以任意次序分别购进鸡(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))；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.12•进程的树结构图表示树中结点表示状态，联系结点之间的有向弧线表示状态之间的迁移。树根结点为进程的初始状态；进程沿着弧线执行。弧线旁标注引起该迁移发生变化的事件。始于同一结点的弧线必须有不同的事件标记。STOP在图中用没有输出弧线的结点表示为了表示进程的无限行为，可在图中增加一条从叶结点到任一非叶结点的无标记弧。见下页图4.113coin--将一枚硬币投入自动售货机的硬币槽choc—由机器的发货器送出一块巧克力toffee--由机器的发货器送出一块太妃糖144.1.2事件迹及其操作进程行为就是进程执行所发生的事件序列事件迹是一个进程所执行事件的历史行为的符号记录，简称为迹。迹表示为用尖括号“”和“”括起来的用逗点“,”分开的事件符号序列。用traces(P)表示进程P的所有可能迹的集合，并称为进程P的迹。打电话进程PHONE=ring→answer→STOP，（空迹）、ring和ring,answer都是其可能的迹，即，traces(P)={,ring,ring,answer}15•迹的连接CSP中定义了一系列关于迹的操作运算连接运算、投影运算、首/尾运算、星运算等约定：小写字母s、t、u表示迹；大写字母S、T、U表示迹的集合；小写字母f、g、h表示定义在迹集合上的函数或映射。迹的连接---对于迹s和t，将它们中的事件符号依次序排放在一起所得到的迹，称为s和t的连接，记为s^t，符号“^”称为连接运算或连接算子。对于迹s和非负整数n，以sn表示迹s的n次重复连接（规定s0=（空迹））。16•迹的投影对于迹s和事件集合A，保留迹s中所有属于A中的事件符号后所得到符号串，称为s在A中的投影，记为(sA)。符号“”称为投影运算或投影算子。投影运算性质：A=；(t^s)A=(tA)^(sA)；xA=x如果xA；xA=如果xA；s{}=；{}表示空集（无元素集）(sA)B=s(AB)17•迹的运算迹的首/尾--设迹s是一个非空事件序列，s中的第一个事件称为s的首，记为s；s中删除第一个事件剩余的部分符号称为s的尾，记为s。符号“”和“”分别称为首运算和尾运算星运算--事件集A上所有有限事件符号形成的迹（包括）组成的集合，记为A*。符号“*”称为星运算。A*可递归定义为A*={t|t=(tAtA)}18•迹的运算迹函数--迹到迹的映射，又称迹映射。迹函数f，如果f()=，则称f是严格的s，t，若f(s^t)=f(s)^f(t)，则称f满足分配律。迹长度--迹s中事件符号的出现个数，称为迹s的长度，记为#s。符号“#”称为迹的长度运算。对于迹s和事件x，x在s中的出现次数为#(s{x})19•迹的运算迹的逆--对于迹s，将其中的事件逆序排列后所得到的迹，称为迹s的逆，记为s-1。迹的交替--对于迹s和t，将各自的事件依次序交替排列所得到的迹，称为s和t的交替迹，记为s⊕t。例如，a,b,c⊕1,2,3=a,1,b,2,c,3迹的后进程--对于进程P的一个迹s，如果Q为P在s以后的行为，那么称进程Q为进程P的s后进程，记为P\s。例如，a,1,b,2,c,3\a,1=b,2,c,320•迹的运算迹的偏序关系--对于迹s和t，如果存在迹u，使得s^u=t，则称迹s和t存在偏序关系，记为≤。并称s为t的前缀。例如，a,1≤a,1,b,2,c,3性质：x^s≤tifft≠x=ts≤t进程的迹和进程的树描述有着紧密的联系对于树中任一结点，进程到达此结点的行为的迹是：从根结点到达该结点的路径上弧线的标号序列。例如，下图4.2中对应于涂黑结点的迹为：in2p,small,out1pin1p–向自动售货机投入一枚一便士的硬币in2p–向自动售货机投入一枚二便士的硬币Small–送出一块小饼干或小甜饼large–送出一块大饼干或大甜饼Out1p–送出一便士的找头224.1.3进程的复合操作进程之间可以通过运算操作进行复合，实现复杂问题的描述。CSP提供并发进程、或进程、选择进程、屏蔽进程、混合进程、顺序进程等描述的运算操作。并发进程–给定进程P和Q，对PQ中事件同时执行，其它事件交替执行的进程，称为进程P和Q的并发进程，记为P||Q。符号“||”称为进程的并发复合算子。23•并发复合算子举例对于进程CUST={curse,money,food}CUST=curse→money→food→CUSTSHOP={chat,money,food}SHOP=chat→money→food→SHOP有CUST||SHOP=X(curse→chat→money→food→X|chat→curse→money→food→X)24•并发复合算子性质设aP-Q，bQ-P，c、dPQ：P||Q=Q||P；P||(Q||R)=(P||Q)||R；(c→P)||(c→Q)=c→(P||Q)；(c→P)||(d→Q)=STOPif(c≠d)；(a→P)||(c→Q)=a→(P||(c→Q))；(c→P)||(b→Q)=b→((c→P)||Q)；(a→P)||(b→Q)=(a→(P||(b→Q))|b→((a→P)||Q))；traces(P||Q)={t|(tP)traces(P)(tQ)traces(Q)t(PQ)*}；(P||Q)\s=(P\(sP))||(Q\(sQ))；traces(P||Q)=traces(P)traces(Q)if(P=Q)；traces(P||Q)={s⊕t|straces(P),ttraces(Q)}if(PQ={})25•并发复合算子性质应用示例下列进程P和进程QP={a,c}