通信顺序进程

电脑科学中,通信顺序进程(英语:Communicating sequential processes,缩写为CSP),又译为交谈循序程序交换消息的循序程序,是一种形式语言,用来描述并发性系统间进行交互的模式[1]。它是叫做进程代数或进程演算的关于并发的数学理论家族的一员,基于了通过通道消息传递。CSP高度影响了Occam的设计[1][2],也影响了编程语言如Limbo[3]RaftLib英语RaftLibGo[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]

它赋予名字westDISASSEMBLE进程,名字XCOPY进程,名字eastASSEMBLE进程,并发的执行这三个进程[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):

事件
事件表示通信或交互。它们被假定为是不可分的和瞬时的。它们可以是原子名字(比如  ),复合名字(比如  ),输入/输出事件(比如  )。
原始进程
原始进程表示基本的行为:例子包括 (什么都不通信的进程,也叫作死锁)和 (它表示成功终止)。

代数算符

编辑

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

前缀
前缀算符,将一个事件和一个进程结合起来产生一个新进程。例如:
 
是想要与它的环境通信 的进程,而且在 之后,表现得如同进程 
确定性选择
确定性(或外部)选择算符,允许将进程的将来演变定义为,在两个构件进程之间进行选择,并允许环境通过通信这两进程之一的初始事件,来解决这个选择。例如:
 
是想要通信初始事件  的进程,并依据环境决定与之通信的是哪个初始事件,随后表现为要么 要么 。如果  二者同时被通信,则选择将被非确定性的解决。
非确定性选择
非确定性(或内部)选择算子,允许将进程的将来演变定义为,在两个构件进程之间的选择,但是不允许环境对哪个构件进程将被选择的任何控制。例如:
 
可以表现得如同要么 要么 。它可以拒绝接受  ,并只在环境提供了  二者时,被强制去通信。如果要选择的两边的初始事件是同一的,非确定性也可能被介入到确定性选择中。例如:
 
等价于
 
交错
交错(interleaving)算符,代表完全独立的并发活动。进程:
 
表现为  二者同时。来自二者进程的事件在时间上是任意交错的。
接口并行
接口(interface)或广义(generalized)并行算符,代表并发活动要求在构件进程之间的同步:在接口集合中的任何事件,只能在所有进程都能应允(engage)这个事件的时候出现。例如,进程:
 
要求  必须在事件 可以发生前能够进行这个事件。例如,进程:
 
可以应允事件 ,而变成进程:
 
然而
 
将会简单的死锁。
隐藏
隐藏算符,通过使某些事件不可察见,提供了一种抽象进程的方式。隐藏的一个平凡的例子是:
 
假定事件 不出现在 中,它简单的归约成:
 

例子

编辑

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

 

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

 

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

 

然而如果同步只要求 ,我们会得到:

 

如果我们通过隐藏  来抽象后者这个复合进程,也就是:

 

我们得到非确定性进程:

 

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

形式定义

编辑

语法

编辑

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

 

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

有关的形式化

编辑

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

参见

编辑

延伸阅读

编辑

引用

编辑
  1. ^ 1.0 1.1 1.2 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. ^ Resources about threaded programming in the Bell Labs CSP style. [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. ^ 6.0 6.1 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. ^ 11.0 11.1 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. A Theory of Communicating Sequential Processes. 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
  16. ^ CSPP
  17. ^ HCSP
  18. ^ TCOZ页面存档备份,存于互联网档案馆
  19. ^ 19.0 19.1 Circus页面存档备份,存于互联网档案馆
  20. ^ CML页面存档备份,存于互联网档案馆
  21. ^ CspCASL
  22. ^ ISO 8807,时态次序规定语言英语Language Of Temporal Ordering Specification
  23. ^ Using CSP页面存档备份,存于互联网档案馆
  24. ^ The Theory and Practice of Concurrency页面存档备份,存于互联网档案馆
  25. ^ Bill Roscoe : Publications. [2022-04-05]. (原始内容存档于2022-02-18). 
  26. ^ PS页面存档备份,存于互联网档案馆
  27. ^ PDF页面存档备份,存于互联网档案馆

外部链接

编辑