通信顺序进程

在计算机科学中，通信顺序进程（英語：Communicating sequential processes，縮寫為CSP），又譯為交談循序程式、交換訊息的循序程式，是一種形式語言，用來描述並行性系統間進行互動的模式^[1]。它是叫做进程代数或进程演算的关于并发的数学理论家族的一员，基于了通过通道的消息传递。CSP高度影響了Occam的設計^[1][2]，也影響了程式語言如Limbo^[3]、RaftLib（英语：RaftLib）、Go^[4]、 Crystal（英语：Crystal (programming language)）和Clojure的core.async^[5]等。

CSP最早出現於東尼·霍爾在1978年發表的論文^[6]，但在之後又經過一系列的改善^[7]。CSP已经实际的应用在工业之中，作为一种工具去规定和验证（英语：Formal specification）各种不同系统的并发状况，比如T9000 Transputer^[8]，还有安全电子商务系统^[9]。CSP的理论自身仍是活跃研究的主题，包括了增加它的实际可应用性的范围（比如增大可以跟踪分析的系统的规模）^[10]。

历史

在Hoare的1978年论文中提出的CSP版本在本质上不是一种进程演算，而是一种并发编程语言，它有四类命令：并行命令，赋值命令，输入和输出命令，交替（alternation）和重复命令。它有着与后来版本的CSP在实质上不同的语法，不拥有数学上定义的语义^[11]，不能体现无界非确定性（英语：unbounded nondeterminism）^[12]。最初的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进程，并发的执行这三个进程^[6]。

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

非形式描述

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

原语

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

事件

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

原始进程

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

代数算符

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

前缀

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

${\displaystyle a\rightarrow P}$ 

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

确定性选择

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

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

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

非确定性选择

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

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

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

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

等价于

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

交错

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

${\displaystyle P\;\vert \vert \vert \;Q}$ 

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

接口并行

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

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

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

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

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

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

然而

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

将会简单的死锁。

隐藏

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

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

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

${\displaystyle P}$ 

例子

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

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

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

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

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

${\displaystyle \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} }$ 

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

${\displaystyle \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)}$ 

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

${\displaystyle \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\}}$ 

我们得到非确定性进程：

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

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

形式定义

语法

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

${\displaystyle {\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}}}$ 

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

有关的形式化

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

• Timed CSP^[14]，它结合了时序信息用于关于实时系统的推理。
• Receptive Process Theory^[15]，专门化的CSP，假定了异步（就是非阻塞（英语：Non-blocking algorithm））发送操作。
• CSPP^[16]
• HCSP^[17]
• TCOZ^[18]，集成有时序的CSP于对象Z（英语：Object-Z）。
• Circus^[19]，集成CSP和基于编程的统一理论（英语：Unifying Theories of Programming）的Z表示法（英语：Z notation）。
• CML^[20]（COMPASS建模语言），合并了为多系统的系统（英语：System of systems）（SoS）开发的Circus^[19]和VDM（英语：Vienna Development Method）。
• CspCASL^[21]，集成了CSP的CASL（英语：Common Algebraic Specification Language）扩展。
• LOTOS（英语：Language Of Temporal Ordering Specification），结合了CSP与CCS（英语：Calculus of Communicating Systems）特征的国际标准^[22]。

参见

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

延伸阅读

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

引用

1. Roscoe, A. W. The Theory and Practice of Concurrency. Prentice Hall. 1997. ISBN 978-0-13-674409-2. 
2. INMOS. occam 2.1 Reference Manual (PDF). SGS-THOMSON Microelectronics Ltd. 1995-05-12 [2020-05-03]. （原始内容 (PDF)于2020-08-01）. , INMOS document 72 occ 45 03
3. . [2010-04-15]. （原始内容存档于2013-04-26）. 
4. Language Design FAQ: Why build concurrency on the ideas of CSP?. [2020-05-03]. （原始内容于2013-01-02）. 
5. Clojure core.async Channels. [2020-05-03]. （原始内容于2019-07-05）. 
6. Hoare, C. A. R. Communicating sequential processes (PDF). Communications of the ACM. 1978, 21 (8): 666–677 [2020-05-03]. doi:10.1145/359576.359585. （原始内容 (PDF)于2020-12-30）. 
7. Abdallah, Ali E.; Jones, Cliff B.; Sanders, Jeff W. Communicating Sequential Processes: The First 25 Years. LNCS 3525. Springer. 2005. ISBN 9783540258131. 
8. Barrett, G. Model checking in practice: The T9000 Virtual Channel Processor. IEEE Transactions on Software Engineering. 1995, 21 (2): 69–78. doi:10.1109/32.345823. 
9. Hall, A; Chapman, R. Correctness by construction: Developing a commercial secure system (PDF). IEEE Software. 2002, 19 (1): 18–25 [2020-05-03]. doi:10.1109/52.976937. （原始内容 (PDF)于2020-12-02）. 
10. Creese, S. Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks. D. Phil. Oxford University. 2001. 
11. Hoare, C. A. R. Communicating Sequential Processes. Prentice Hall. 1985. ISBN 978-0-13-153289-2. 
12. Clinger, William. Foundations of Actor Semantics. Mathematics Doctoral Dissertation. MIT. June 1981. hdl:1721.1/6935. 
13. Brookes, Stephen; Hoare, C. A. R.; Roscoe, A. W. . Journal of the ACM. 1984, 31 (3): 560–599 [2020-05-03]. doi:10.1145/828.833. （原始内容存档于2021-06-23）. 
14. Timed CSP （页面存档备份，存于互联网档案馆）
15. Receptive Process Theory
18. TCOZ（页面存档备份，存于互联网档案馆）
19. Circus（页面存档备份，存于互联网档案馆）
20. CML （页面存档备份，存于互联网档案馆）
22. ISO 8807，时态次序规定语言（英语：Language Of Temporal Ordering Specification）
23. Using CSP （页面存档备份，存于互联网档案馆）
24. The Theory and Practice of Concurrency （页面存档备份，存于互联网档案馆）
25. . [2022-04-05]. （原始内容存档于2022-02-18）. 
26. PS （页面存档备份，存于互联网档案馆）
27. PDF （页面存档备份，存于互联网档案馆）

外部链接

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