进程代数是关于通信并发系统的代数理论的统称。 20世纪70年代后期,英国学者RMnner和C. A.R,分别提出了通信系统演算和通信顺序进程,开创了用代数方法研究通信并发系统的先河。 此后这一研究方向兴盛不衰,出现了众多类似而又 相互区别的演算系统,如ACP(提出者J.A.Ber郎tra 和J.W.K10p),ATp(提出者M.H即n樱y),Meije(提出者G.Eudol,R.desi~),LOTC6等,统称为进程代数。
简介
计算机科学是个非常年轻的科学,非常多的研究至今可能都不超过50年,很多研究的都可以追溯到20世纪50年代,而那个时候从事计算机事业的大师们很多今天仍健在。所以相对而言,我们对与一些事情的历史可以更加细致地但不会过于冗长地进行介绍。通过本文,我希望读者了解到进程代数是什么,并可以在脑中形成一条简单的时间线,清楚地看到进程代数发生的历史。
这些代数理论都使用通信,而不是
共享存储,作为进程之间相互作用的基本手段,表现出面向分布式系统的特征。 在语法上,进程代数用一组算子作为进程的构件。算子的语义通常用结构化操作语义方法定义, 这样进程就可看成是带标号的变迁系统。进程代数 的一个显著特征是把并发性归结为非确定性,将并 发执行的进程的行为看成是各单个进程的行为的所 有可能的交错合成,即所谓交错语义。 进程代数研究的核心问题是进程的等价性,即在什么意义下两个进程的行为相同?在进程代数领域使用的最为广泛的等价关系有互模拟、测试等价、 失败等价(参见通信顺序进程)等。对这些语义等价 关系均建立了相应的公理系统。关于公理系统的研 究不仅加深了对语义理论的理解,而且使得有可能 对语义等价关系进行形式推理。 为了将进程代数的理论成果应用于解决实际问题,20世纪80年代后期出现了许多计算机支持工具。用这些工具可对进程的行为进行推理或模拟。
历史
谈到进程代数,很多人会想到Petri-net,在进程代数之前,这个1962年由Petri发明的形式化方法是并行理论的唯一工具,用来研究并行和分布式系统。
1970年的时候,世界上关于计算(computation)的形式化推理方法,基本分为三种:
定义
进程代数英文为:process algebra,在英文中,这个词组中的process代表一个system(系统的)behavior(行为);一个系统就是一个能表现出各种行为的事物,在计算机世界,process主要指一个软件系统的行为;这句话很抽象,说白了就是,一个软件系统可以表现为一个动作(action),比如转换一个文件的格式,也可以发生一个个事件(event),比如格式转换完毕,另外,一个软件系统也可以在一定的序列下完成一系列动作(action);我们可以从各个角度(aspect)去观察一个系统的行为。研究者往往会关注一个角度的系统行为,这是他们会把系统进行抽象,称这种抽象为对系统行为的一种观察(observation)。
有一些研究人员,以这样的一个角度观察系统的行为:
系统由一大堆动作(action)组成;
动作之间都是离散的(discrete),独立的;
离散的意思是action发生在某一时间,各个action发生的时间是独立的,不相关的。
离散数学中,群(Group)是一个代数结构,它的运算符特性满足该群的约束要求,比如群(G,*)是一个代数系统,其中运算符*要满足结合律的要求,从群论的角度来看,进程代数是一个以进程为基本元素,并且进程上的运算符满足特定的约束的代数结构。
进程代数理论中提出了许多种模型,其中最早的(大约是20世纪中期)、最简单的模型是:将行为看做是一个带有输入/输出的函数,在进程开始时,给予一个输入值,在进程的执行过程中的某个时刻会给予外界它的某个输出值。这个模型是基于有穷自动机理论的,即每个process被看做一个自动机(automaton)【注:今天仍然有人将一个process看作自动机,进行研究】,一个自动机有很多状态(state)和迁移(transition),状态通过迁移进行状态之间之间的转换,这样,用自动机代表一个进程时,状态之间的迁移就代表进程执行了一个动作,所以迁移描述了进程的最基本行为,另外,一个自动机还可以有一个初始状态和多个终止状态。一次行为(behiour)就是一个自动机迁移的实例,即从初始态到达某一个终止态的具体路径过程。
但是后来,人们发现这种自动机模型并不能完全表达一个系统的行为,它无法描述两个系统之前的交互行为,也就是说自动机无法用来描述并行系统或分布式系统,或者说反应系统(reactive system)的行为。因此人们开始了并发理论(concurrency theory)研究,所以说并发理论是针对反应式、并行式或分布式系统的,这些系统与云计算也有重要的相关之处。
那么进程代数可以说是并行理论中的一个研究方向,所以我们在后面会看到,一种进程代数通常都会有一个基本的运算符——并行组合(parallel composition),这里组合(compostion)是指多个离散的动作的组合。除了并行的组合,还有带有选择分支的组合(alternative composition--choice)和按顺序组合(sequential composition--sequencing),这样,我们就可以对系统使用进程代数建模,然后通过代数的运算,方程推导进行分析和验证以判断系统是否满足我们所希望的特性。
我们使用加号“ +” 作为 alternative composition, 分号“;” 作为sequential composition,而双竖线“||” 表示 parallel composition.那么我们定义以下法则:
如果任何带有三个运算符的代数结构满足以上七条法则,那么就称这个代数为进程代数,这就是一个简单的进程代数的概念定义。
方法
Bekič
奥地利维也纳的IBM实验室在整个60年代和70年代都以其程序语言的定义和语义方面的研究而著称,这个期间Hans Bekič就工作在这里,他主要从事ALGOL和PL/I(相信学过计算机的同志对这些名词都有点眼熟)的指称语义方面的研究,但是针对PL/I的parallel composition运算符如何指定指称语义遇到了困难,他提出了一个类并行组合运算符(quasi-parallel composition operator),后来更正为并行组合运算符,并提出了一些其他的基本运算和概念,使得进程代数的一些基本概念开始浮现,但是还不成熟。
CCS
进程代数历史上最重要的人物是Robin Milner,1973至1980年间发明了CCS(Calculus of Communicating Systems,通信系统演算),是用于描述通信并发系统的代数理论。
CSP
中国的研究者
林惠民
林惠民院士主要从事软件的基础性研究。计算机是一种工具,大部分的人是在进行应用研究,即如何利用现有的理论和模型来开发出更有用的东西。而基础性研究与应用研究不同,它不仅要关心怎么样,还要知道为什么这样,要能够提出新的模型和方法。计算机软件科学的特点是基础研究和应用研究是紧密结合的,而且时效性非常强,基础研究的最新成果很快就会应用到工程中去。
林惠民院士从事的一项工作是关于
并发程序的
形式语义学及
形式化方法的研究。他和他的同事设计并实现了世界上第一个通用的进程代数验证工具。进程代数的实际应用离不开计算机辅助工具的支持。八十年代后期,一批进程代数验证工具应运而生(如CWB, PSF, LOTOSphere等),其共同局限性是每一工具只适用于某一特定的进程演算。这种局限性妨碍了验证工具的推广应用。如何克服这种局限性是当时国际进程代数界面临的一个重大挑战。这些验证工具无法做到通用,根本原因在于缺乏既能描述不同进程演算的语义,又能为计算机所理解的通用语言。经过对不同演算的反复比较,并考虑到在计算机上实现的可能性,他提炼出了一个元语言,用它可以描述各种进程演算的公理化语义,并且具有良好的可读性。在此基础上实现了通用的交互式进程代数验证工具PAM,只要将这个元语言描述的进程演算定义输入PAM,就得到该演算的证明器。PAM可同时接受多个不同的演算,对每个演算又可生成多个证明窗口。这是世界上第一个通用的进程代数证明工具。1993年他又利用当时刚刚取得的关于
消息传送进程证明系统的理论结果,对PAM加以扩充,研制成迄今世界上唯一能对付
消息传送进程的验证工具VPAM。PAM和VPAM都是通过ftp在Internet上公开发行的,其用户遍布各大洲,包括美国、加拿大、英、法、德、意、荷兰、丹麦、瑞典、斯洛伐克、巴西、印度、新西兰、南非等十几个国家,其中既有来自大学的,也有来自菲利普、惠普和贝尔等著名公司实验室的。