通信顺序进程
发布时间:2026-08-06 | 浏览:1
在 计算机科学 中, 通信顺序进程 (英語: 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相对比,每个进程都被赋予了一个显式的名字,通过指定意图发送或接收的进程的名字,定义消息的来源和目标,没有采用等价的命名的 通道 方式。例如,定义进程:
它是重复的从叫作 west 的进程接收一个字符,再将这个字符发送到叫作 east 的进程。接着定义逐行读取 打孔卡 再输出字符 串流 到叫作 X 的进程的 DISASSEMBLE 进程,和从叫作 X 的进程读取字符串流再逐行打印到 行式打印机 的 ASSEBLE 进程。并行复合:
它赋予名字 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):
CSP有范围广泛的代数算符。主要的有:
一个原型的CSP例子是,一个巧克力售货机和它与一个想要买巧克力的人之间交互的抽象表示。这个售货机可以执行两个不同事件, c o i n {\displaystyle \,\mathrm {coin} \,} 和 c h o c {\displaystyle \,\mathrm {choc} \,} ,分别表示插入硬币和投递巧克力。这个机器在提供巧克力之前想要货款(现金)可以写为:
一个人可以选择投币或刷卡支付可以建模为:
这两个进程可以放置为并行,这样它们可以相互交互。这种复合进程的行为依赖于这两个进程必须同步于其上的那些事件。因此:
然而如果同步只要求 c o i n {\displaystyle \,\mathrm {coin} \,} ,我们会得到:
如果我们通过隐藏 c o i n {\displaystyle \,\mathrm {coin} \,} 和 c a r d {\displaystyle \,\mathrm {card} \,} 来抽象后者这个复合进程,也就是:
这是一个要么提供 c h o c {\displaystyle \,\mathrm {choc} \,} 事件并接着停止,或者就地停止的进程。换句话说,如果我们把这个抽象当作对这个系统的外部查看(比如未看到这个人的做出如何决定的某个人), 非确定性 ( 英语 : Nondeterministic algorithm ) 就已经介入了。
CSP的语法定义了进程和事件可以组合的“合法”方式。设 e {\displaystyle \,e\,} 是一个事件, X {\displaystyle \,X\,} 是一个事件集合。CSP的基本语法可以定义为:
注意:为得到简要性,上述提供的语法省略了 d i v {\displaystyle \,\mathbf {div} \,} 进程,它表示 分岐 ( 英语 : Divergence (computer science) ) ,还有各种算符,比如字母化并行、管道、索引选择。
从经典无时序的CSP已经派生出一些其他的规定语言和形式化,包括:
Timed CSP [ 14 ] ,它结合了时序信息用于关于实时系统的推理。
Receptive Process Theory [ 15 ] ,专门化的CSP,假定了异步(就是 非阻塞 ( 英语 : Non-blocking algorithm ) )发送操作。
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) )
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文件。应用了版权限制,下载前参看页面文本。
本书已经被 牛津大学计算实验室 ( 英语 : Department of Computer Science, University of Oxford ) 的 Jim Davies ( 英语 : Jim Davies (computer scientist) ) 更新,新版可以于网站Using CSP [ 23 ] 自由的下载获取为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). 一些与本书有关的链接可见于网站 [ 24 ] 。全文可从Bill Roscoe的学术出版列表 [ 25 ] 下载获取为PS [ 26 ] 或PDF [ 27 ] 文件。
一些与本书有关的链接可见于网站 [ 24 ] 。全文可从Bill Roscoe的学术出版列表 [ 25 ] 下载获取为PS [ 26 ] 或PDF [ 27 ] 文件。
^ 1.0 1.1 1.2 Roscoe, A. W. The Theory and Practice of Concurrency . Prentice Hall . 1997. ISBN 978-0-13-674409-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
^ Resources about threaded programming in the Bell Labs CSP style . [ 2010-04-15 ] . ( 原始内容 存档于2013-04-26).
^ Language Design FAQ: Why build concurrency on the ideas of CSP? . [ 2020-05-03 ] . (原始内容 存档 于2013-01-02).
^ Clojure core.async Channels . [ 2020-05-03 ] . (原始内容 存档 于2019-07-05).
^ 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).
^ Abdallah, Ali E.; Jones, Cliff B.; Sanders, Jeff W. Communicating Sequential Processes: The First 25 Years . LNCS 3525 . Springer. 2005. ISBN 9783540258131 .
^ 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 .
^ 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).
^ Creese, S. Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks. D. Phil. Oxford University . 2001.
^ 11.0 11.1 Hoare, C. A. R. Communicating Sequential Processes. Prentice Hall. 1985. ISBN 978-0-13-153289-2 .
^ Clinger, William . Foundations of Actor Semantics. Mathematics Doctoral Dissertation. MIT. June 1981. hdl:1721.1/6935 .
^ 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).
^ Timed CSP ( 页面存档备份 ,存于 互联网档案馆 )
^ Receptive Process Theory
^ TCOZ ( 页面存档备份 ,存于 互联网档案馆 )
^ 19.0 19.1 Circus ( 页面存档备份 ,存于 互联网档案馆 )
^ CML ( 页面存档备份 ,存于 互联网档案馆 )
^ ISO 8807,时态次序规定语言 ( 英语 : Language Of Temporal Ordering Specification )
^ Using CSP ( 页面存档备份 ,存于 互联网档案馆 )
^ The Theory and Practice of Concurrency ( 页面存档备份 ,存于 互联网档案馆 )
^ Bill Roscoe : Publications . [ 2022-04-05 ] . ( 原始内容 存档于2022-02-18).
^ PS ( 页面存档备份 ,存于 互联网档案馆 )
^ PDF ( 页面存档备份 ,存于 互联网档案馆 )
WoTUG ( 页面存档备份 ,存于 互联网档案馆 ), CSP和occam风格系统的用户组,包含了关于CSP和有用链接的一些信息。
大型与小型编程 ( 英语 : Programming in the large and programming in the small )
部分应用 ( 英语 : Partial application )
广义代数数据类型 ( 英语 : Generalized algebraic data type )
信号 ( 英语 : Signals and slots )
概率逻辑 ( 英语 : Probabilistic logic programming )
交互式 ( 英语 : Interactive programming )
符号 ( 英语 : Symbolic programming )
程序合成 ( 英语 : Program synthesis )
多阶段 ( 英语 : Multi-stage programming )
结构化并发 ( 英语 : Structured concurrency )
面向服务 ( 英语 : Service-oriented programming )
面向表达式 ( 英语 : Expression-oriented programming language )
基于组件 ( 英语 : Component-based software engineering )
块 嵌套函数 ( 英语 : Nested function ) 回调函数
嵌套函数 ( 英语 : Nested function )
多态 运算符重载 泛型 多分派