通信顺序进程

在计算机科学中，通信顺序进程（英语：Communicating sequential processes，缩写为CSP），又译为交谈循序程序、交换消息的循序程序，是一种形式语言，用来描述并发性系统间进行交互的模式。它是叫做进程代数或进程演算的关于并发的数学理论家族的一员，基于了通过通道的消息传递。CSP高度影响了Occam的设计，也影响了编程语言如Limbo、RaftLib、Go、 Crystal和Clojure的core.async等。

CSP最早出现于东尼·霍尔在1978年发表的论文，但在之后又经过一系列的改善。CSP已经实际的应用在工业之中，作为一种工具去规定和验证各种不同系统的并发状况，比如T9000 Transputer，还有安全电子商务系统。CSP的理论自身仍是活跃研究的主题，包括了增加它的实际可应用性的范围（比如增大可以跟踪分析的系统的规模）。

历史

在Hoare的1978年论文中提出的CSP版本在本质上不是一种进程演算，而是一种并发编程语言，它有四类命令：并行命令，赋值命令，输入和输出命令，交替（alternation）和重复命令。它有着与后来版本的CSP在实质上不同的语法，不拥有数学上定义的语义，不能体现无界非确定性。最初的CSP程序被写为一组固定数目的顺序进程的并行复合（composition），它们相互之间严格通过同步消息传递来进行通信。与后来版本的CSP相对比，每个进程都被赋予了一个显式的名字，通过指定意图发送或接收的进程的名字，定义消息的来源和目标，没有采用等价的命名的通道方式。例如，定义进程：

COPY = *[c:character; west?c → east!c]

它是重复的从叫作west的进程接收一个字符，再将这个字符发送到叫作east的进程。接着定义逐行读取打孔卡再输出字符流到叫作X的进程的DISASSEMBLE进程，和从叫作X的进程读取字符串流再逐行打印到行式打印机的ASSEBLE进程。并行复合：

[west::DISASSEMBLE || X::COPY || east::ASSEMBLE]

它赋予名字west至DISASSEMBLE进程，名字X至COPY进程，名字east至ASSEMBLE进程，并发的执行这三个进程。

在最初版本的CSP出版之后，Hoare、Stephen Brookes和A. W. Roscoe发展并精炼了CSP的理论，使之成为现代的进程代数形式。将CSP发展成进程代数的方式受到Robin Milner关于通信系统演算（CCS）的工作的影响，反之亦然。最初提出CSP的理论上的版本的是Brookes、Hoare和Roscoe的1984年的文章，和后来Hoare的1985年出版的书籍《通信顺序进程》。CSP的理论在Hoare的书籍出版之后仍继续有细小的变更。这些变更大多由CSP进程分析和验证的自动工具的出现所推动。Roscoe在1997年出版的《并发的理论和实践》描述了更新版本的CSP。

非形式描述

如其名字所提示的那样，CSP允许依据构件进程来描述系统，它们独立运作，并只通过消息传递通信来相互交互。但是CSP名字中“顺序”这个词有时导致误解，因为现代CSP允许构件进程被定义为二者：顺序进程和多个更原始的进程的并行复合。在不同进程之间的关系，和每个进程与它的环境通信的方式，是使用各种进程代数算符（operator）描述的。使用这种代数方式，可以从原始元素轻易的构造出非常复杂的进程描述。

原语

CSP在它的进程代数中提供两类原语（primitive）：

事件

事件表示通信或交互。它们被假定为是不可分的和瞬时的。它们可以是原子名字（比如$\,\mathrm {on} \,$、$\,\mathrm {off} \,$），复合名字（比如$\,\mathrm {valve.open} \,$、$\,\mathrm {valve.close} \,$），输入/输出事件（比如$\,\mathrm {mouse?xy} \,$、$\,\mathrm {screen!bitmap} \,$）。

原始进程

原始进程表示基本的行为：例子包括$\,\mathrm {STOP} \,$（什么都不通信的进程，也叫作死锁）和$\,\mathrm {SKIP} \,$（它表示成功终止）。

代数算符

CSP有范围广泛的代数算符。主要的有：

前缀

前缀算符，将一个事件和一个进程结合起来产生一个新进程。例如：

$a\rightarrow P$

是想要与它的环境通信$a$的进程，而且在$\,a\,$之后，表现得如同进程$\,P\,$。

确定性选择

确定性（或外部）选择算符，允许将进程的将来演变定义为，在两个构件进程之间进行选择，并允许环境通过通信这两进程之一的初始事件，来解决这个选择。例如：

$\left(a\rightarrow P\right)\Box \left(b\rightarrow Q\right)$

是想要通信初始事件$\,a\,$和$\,b\,$的进程，并依据环境决定与之通信的是哪个初始事件，随后表现为要么$\,P\,$要么$\,Q\,$。如果$\,a\,$和$\,b\,$二者同时被通信，则选择将被非确定性的解决。

非确定性选择

非确定性（或内部）选择算子，允许将进程的将来演变定义为，在两个构件进程之间的选择，但是不允许环境对哪个构件进程将被选择的任何控制。例如：

$\left(a\rightarrow P\right)\sqcap \left(b\rightarrow Q\right)$

可以表现得如同要么$\,\left(a\rightarrow P\right)\,$要么$\,\left(b\rightarrow Q\right)\,$。它可以拒绝接受$\,a\,$或$\,b\,$，并只在环境提供了$\,a\,$和$\,b\,$二者时，被强制去通信。如果要选择的两边的初始事件是同一的，非确定性也可能被介入到确定性选择中。例如：

$\left(a\rightarrow a\rightarrow \mathrm {STOP} \right)\Box \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)$

等价于

$a\rightarrow \left(\left(a\rightarrow \mathrm {STOP} \right)\sqcap \left(b\rightarrow \mathrm {STOP} \right)\right)$

交错

交错（interleaving）算符，代表完全独立的并发活动。进程：

$P\;\vert \vert \vert \;Q$

表现为$\,P\,$和$\,Q\,$二者同时。来自二者进程的事件在时间上是任意交错的。

接口并行

接口（interface）或广义（generalized）并行算符，代表并发活动要求在构件进程之间的同步：在接口集合中的任何事件，只能在所有进程都能应允（engage）这个事件的时候出现。例如，进程：

$P\left\vert \left[\left\{a\right\}\right]\right\vert Q$

要求$\,P\,$和$\,Q\,$必须在事件$\,a\,$可以发生前能够进行这个事件。例如，进程：

$\left(a\rightarrow P\right)\left\vert \left[\left\{a\right\}\right]\right\vert \left(a\rightarrow Q\right)$

可以应允事件$\,a\,$，而变成进程：

$P\left\vert \left[\left\{a\right\}\right]\right\vert Q$

然而

$\left(a\rightarrow P\right)\left\vert \left[\left\{a,b\right\}\right]\right\vert \left(b\rightarrow Q\right)$

将会简单的死锁。

隐藏

隐藏算符，通过使某些事件不可察见，提供了一种抽象进程的方式。隐藏的一个平凡的例子是：

$\left(a\rightarrow P\right)\setminus \left\{a\right\}$

假定事件$\,a\,$不出现在$\,P\,$中，它简单的归约成：

$P$

例子

一个原型的CSP例子是，一个巧克力售货机和它与一个想要买巧克力的人之间交互的抽象表示。这个售货机可以执行两个不同事件，$\,\mathrm {coin} \,$和$\,\mathrm {choc} \,$，分别表示插入硬币和投递巧克力。这个机器在提供巧克力之前想要货款（现金）可以写为：

$\mathrm {VendingMachine} =\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP}$

一个人可以选择投币或刷卡支付可以建模为：

$\mathrm {Person} =(\mathrm {coin} \rightarrow \mathrm {STOP} )\Box (\mathrm {card} \rightarrow \mathrm {STOP} )$

这两个进程可以放置为并行，这样它们可以相互交互。这种复合进程的行为依赖于这两个进程必须同步于其上的那些事件。因此：

$\mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} ,\mathrm {card} \right\}\right]\right\vert \mathrm {Person} \equiv \mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP}$

然而如果同步只要求$\,\mathrm {coin} \,$，我们会得到：

$\mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} \right\}\right]\right\vert \mathrm {Person} \equiv \left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)$

如果我们通过隐藏$\,\mathrm {coin} \,$和$\,\mathrm {card} \,$来抽象后者这个复合进程，也就是：

$\left(\left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)\right)\setminus \left\{\mathrm {coin,card} \right\}$

我们得到非确定性进程：

$\left(\mathrm {choc} \rightarrow \mathrm {STOP} \right)\sqcap \mathrm {STOP}$

这是一个要么提供$\,\mathrm {choc} \,$事件并接着停止，或者就地停止的进程。换句话说，如果我们把这个抽象当作对这个系统的外部查看（比如未看到这个人的做出如何决定的某个人），非确定性就已经介入了。

形式定义

语法

CSP的语法定义了进程和事件可以组合的“合法”方式。设$\,e\,$是一个事件，$\,X\,$是一个事件集合。CSP的基本语法可以定义为：

${\begin{array}{lcll}{Proc}&::=&\mathrm {STOP} &\;\\&|&\mathrm {SKIP} &\;\\&|&e\rightarrow {Proc}&({\text{prefixing}})\\&|&{Proc}\;\Box \;{Proc}&({\text{external}}\;{\text{choice}})\\&|&{Proc}\;\sqcap \;{Proc}&({\text{nondeterministic}}\;{\text{choice}})\\&|&{Proc}\;\vert \vert \vert \;{Proc}&({\text{interleaving}})\\&|&{Proc}\;|[\{X\}]|\;{Proc}&({\text{interface}}\;{\text{parallel}})\\&|&{Proc}\setminus X&({\text{hiding}})\\&|&{Proc};{Proc}&({\text{sequential}}\;{\text{composition}})\\&|&\mathrm {if} \;b\;\mathrm {then} \;{Proc}\;\mathrm {else} \;Proc&({\text{boolean}}\;{\text{conditional}})\\&|&{Proc}\;\triangleright \;{Proc}&({\text{timeout}})\\&|&{Proc}\;\triangle \;{Proc}&({\text{interrupt}})\end{array}}$

注意：为得到简要性，上述提供的语法省略了$\,\mathbf {div} \,$进程，它表示分岐，还有各种算符，比如字母化并行、管道、索引选择。

有关的形式化

从经典无时序的CSP已经派生出一些其他的规定语言和形式化，包括：

• Timed CSP，它结合了时序信息用于关于实时系统的推理。
• Receptive Process Theory，专门化的CSP，假定了异步（就是非阻塞）发送操作。
• CSPP
• HCSP
• TCOZ，集成有时序的CSP于对象Z。
• Circus，集成CSP和基于编程的统一理论的Z表示法。
• CML（COMPASS建模语言），合并了为多系统的系统（SoS）开发的Circus和VDM。
• CspCASL，集成了CSP的CASL扩展。
• LOTOS，结合了CSP与CCS特征的国际标准。

参见

• 跟踪理论，跟踪的一般性理论。
• 跟踪幺半群和历史幺半群
• Ease
• XC
• VerilogCSP，向Verilog HDL增加的一组宏，用来支持通信顺序进程通道通信。
• Joyce，是Brinch Hansen在大约1989年开发的基于CSP原理的编程语言。
• SuperPascal，是Brinch Hansen开发的编程语言，受到CSP和他早期创作的Joyce的影响。
• Ada，实现了CSP特征比如约会。
• DirectShow，是DirectX内的视频框架，它使用了CSP概念来实现音频和视频过滤器。
• OpenComRTOS，是正式开发的网络为中心分布式RTOS，基于了CSP的务实超集。
• 输入/输出自动机
• 并行编程模型

延伸阅读

• Hoare, C. A. R. Communicating Sequential Processes. Prentice Hall International. 2004 [1985] [2011-08-13]. ISBN 978-0-13-153271-7. （原始内容存档于2021-02-01）. 
  • 本书已经被牛津大学计算实验室的Jim Davies更新，新版可以于网站Using CSP自由的下载获取为PDF文件。应用了著作权限制，下载前参看页面文本。
• Roscoe, A. W. The Theory and Practice of Concurrency. Prentice Hall. 1997 [2022-01-18]. ISBN 978-0-13-674409-2. （原始内容存档于2022-01-18）. 
  • 一些与本书有关的链接可见于网站。全文可从Bill Roscoe的学术出版列表下载获取为PS或PDF文件。

外部链接

• WoTUG （页面存档备份，存于互联网档案馆）, CSP和occam风格系统的用户组，包含了关于CSP和有用链接的一些信息。