交談循序程式

在電腦科學中，通信順序行程（英語：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）：

事件

事件表示通訊或互動。它們被假定為是不可分的和瞬時的。它們可以是原子名字（比如${\displaystyle \,\mathrm {on} \,}$、${\displaystyle \,\mathrm {off} \,}$），複合名字（比如${\displaystyle \,\mathrm {valve.open} \,}$、${\displaystyle \,\mathrm {valve.close} \,}$），輸入/輸出事件（比如${\displaystyle \,\mathrm {mouse?xy} \,}$、${\displaystyle \,\mathrm {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 \,\mathrm {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 \,\mathrm {coin} \,}$和${\displaystyle \,\mathrm {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. 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]檔案。

參照

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. 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. 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. 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. 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 （頁面存檔備份，存於網際網路檔案館）

外部連結

• WoTUG （頁面存檔備份，存於網際網路檔案館）, CSP和occam風格系統的使用者群組，包含了關於CSP和有用連結的一些資訊。