交談循序程式

计算机科学中,交談循序程式(英語:Communicating sequential processes,縮寫為CSP),又譯為通信顺序进程交換訊息的循序程式,是一種形式語言,用來描述並行性系統間進行互動的模式[1]。它是叫做进程代数或进程演算的关于并发的数学理论家族的一员,基于了通过通道消息传递。CSP高度影響了Occam的設計[1][2],也影響了程式語言如Limbo[3]RaftLibGo[4]CrystalClojure的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):

事件
事件表示通信或交互。它们被假定为是不可分的和瞬时的。它们可以是原子名字(比如on、off),复合名字(比如valve.open、valve.close),输入/输出事件(比如mouse?xy、screen!bitmap)。
原语进程
原语进程表示基本的行为:例子包括STOP(什么都不通信的进程,也叫作死锁)和SKIP(它表示成功终止)。

代数算符编辑

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

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

例子编辑

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

 

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

 

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

 

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

 

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

 

我们得到非确定性进程:

 

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

形式定义编辑

语法编辑

CSP的语法定义了进程和事件可以组合的“合法”方式。设e是一个事件,X是一个事件集合。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. , INMOS document 72 occ 45 03
  3. ^ Resources about threaded programming in the Bell Labs CSP style. [2010-04-15]. 
  4. ^ Language Design FAQ: Why build concurrency on the ideas of CSP?. 
  5. ^ Clojure core.async Channels. 
  6. ^ 6.0 6.1 Hoare, C. A. R. Communicating sequential processes (PDF). Communications of the ACM. 1978, 21 (8): 666–677. doi:10.1145/359576.359585. 
  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. doi:10.1109/52.976937. 
  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. doi:10.1145/828.833. 
  14. ^ ISO 8807,时态次序规定语言英语Language Of Temporal Ordering Specification

延伸阅读编辑

外部链接编辑

  • WoTUG, CSP和occam风格系统的用户组,包含了关于CSP和有用链接的一些信息。
  • Go语言原本-2.6顺序进程通讯CSP,解读了对贝尔实验室并发编程语言系列实践有重大影响的1978年版CSP论文。