从Rchain项目中学习“进程代数”
并发性(concurrency)
并发性(concurrency)是现实生活中普遍存在的现象,包括并行性(parallel)和分布性(distribution)。事实上,现实中的绝大多数的系统在本质上都是具有并行性或是分布性,纯顺序的系统很少,这样的系统称为并发系统(concurrent systems),例如并行计算机系统、计算机网络系统、移动通信系统、通信协议、集成电路系统等等。研究并发系统的行为是最近二十多年理论计算机科学中一个重要的课题,由于并发系统的复杂性,对它的研究,人们通常采用的都是形式化方法(formal methods)。形式化方法是基于严格数学框架的一种对系统进行刻画、分析和推理的方法,它通过对系统进行严格的语法和语义定义,使得系统的分析和推理能够精确化、数学化,从而保证系统刻画和分析的正确性。
进程代数(process algebra)
目前,在并发系统的理论研究领域,普遍采用一种形式化方法是进程代数(process algebra)方法。进程代数是一种抽象描述语言,它提供了用于并发系统建模的严格式化数学框架。在进程代数方法中,系统的行为用进程来描述,进程由系统所能执行的动作所组成,这里,动作是一个抽象概念,它的含义不需要具体解释,用来表示一个抽象的活动或行为,例如发送一条消息、接收一条消息等等。因此,以进程代数为框架的并发系统分析都是建立在动作这个基本概念上的。以动作为基础,进程代数用算子的形式义了进程间的各种相互作用,例如前缀操作(.)、顺序操作(;)、选择操作(+)、并发操作(||)等,进程代数就能以一种组合化的方式来描述复杂并发系统的行为,这种组合化的系统描述方式将一个大的系统看作是很多小的子系统组合而成,所以特别适合于描述大规模复杂并发系统,进程代数也因此成为了当今复杂并发系统形式刻画与分析的主要工具。比较著名的进程代数有R.Milner提出的CCS(calculus of communication systems),Hoare CAR提出的CSP(communicating sequential process),以及其后在这两种进程代数基础上由国际标准化组织(ISO)标准化的LOTOS(language of temporal ordering specifications)。
并发系统的研究可以从很多不同的角度进行,但所有的研究都集中在两方面,一方面是研究如何对系统的功能特征进行刻画分析,另一方面是研究如何对系统的性能特征进行刻画分析。另外,在系统的设计开发过程中,层次化设计技术是一种非常重要的设计方法,因此并发系统的层次化设计分析技术也是这个领域中的重要研究内容。
pi-演算
在网络时代之前,人们关心的主要是顺序计算。在这种模式下,计算被看作是从输入到输出的函数;永远不终止的计算被认为是没有意义的,因为它不产生任何输出。而在网络出现之后,人们关心更多的是并发计算。在并发计算中,计算主体(进程)在于外界不断的交互中完成所制定的计算任务;而在移动计算中,进程所与之交互的外部环境也在动态地改变。对于这类计算现场,传统的基于"函数"的理论不再适用。如何理解并发、移动计算,为其建立严格的数学模型,从而为实际并发系统的设计与分析提供坚实的理论基础,是近30年来计算机科学面临的重大挑战-----由图灵奖获得者Milner教授与其合作者提出的pi-演算,代表了迄今为止学术界对这一挑战的最为成功的回应。