通信順序進程

在計算機科學中，通信順序進程（英語：Communicating sequential processes，縮寫為CSP），又譯為交談循序程式、交換訊息的循序程式，是一種形式語言，用來描述並行性系統間進行互動的模式。它是叫做進程代數或進程演算的關於並發的數學理論家族的一員，基於了通過通道的消息傳遞。CSP高度影響了Occam的設計，也影響了程式語言如Limbo、RaftLib、Go、 Crystal和Clojure的core.async等。

CSP最早出現於東尼·霍爾在1978年發表的論文，但在之後又經過一系列的改善。CSP已經實際的應用在工業之中，作為一種工具去規定和驗證各種不同系統的並發狀況，比如T9000 Transputer，還有安全電子商務系統。CSP的理論自身仍是活躍研究的主題，包括了增加它的實際可應用性的範圍（比如增大可以跟蹤分析的系統的規模）。

歷史

在Hoare的1978年論文中提出的CSP版本在本質上不是一種進程演算，而是一種並發編程語言，它有四類命令：並行命令，賦值命令，輸入和輸出命令，交替（alternation）和重複命令。它有着與後來版本的CSP在實質上不同的語法，不擁有數學上定義的語義，不能體現無界非確定性。最初的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進程，並發的執行這三個進程。

在最初版本的CSP出版之後，Hoare、Stephen Brookes和A. W. Roscoe發展並精煉了CSP的理論，使之成為現代的進程代數形式。將CSP發展成進程代數的方式受到Robin Milner關於通信系統演算（CCS）的工作的影響，反之亦然。最初提出CSP的理論上的版本的是Brookes、Hoare和Roscoe的1984年的文章，和後來Hoare的1985年出版的書籍《通信順序進程》。CSP的理論在Hoare的書籍出版之後仍繼續有細小的變更。這些變更大多由CSP進程分析和驗證的自動工具的出現所推動。Roscoe在1997年出版的《並發的理論和實踐》描述了更新版本的CSP。

非形式描述

如其名字所提示的那樣，CSP允許依據構件進程來描述系統，它們獨立運作，並只通過消息傳遞通信來相互交互。但是CSP名字中「順序」這個詞有時導致誤解，因為現代CSP允許構件進程被定義為二者：順序進程和多個更原始的進程的並行複合。在不同進程之間的關係，和每個進程與它的環境通信的方式，是使用各種進程代數算符（operator）描述的。使用這種代數方式，可以從原始元素輕易的構造出非常複雜的進程描述。

原語

CSP在它的進程代數中提供兩類原語（primitive）：

事件

事件表示通信或交互。它們被假定為是不可分的和瞬時的。它們可以是原子名字（比如$\,\mathrm {on} \,$、$\,\mathrm {off} \,$），複合名字（比如$\,\mathrm {valve.open} \,$、$\,\mathrm {valve.close} \,$），輸入/輸出事件（比如$\,\mathrm {mouse?xy} \,$、$\,\mathrm {screen!bitmap} \,$）。

原始進程

原始進程表示基本的行為：例子包括$\,\mathrm {STOP} \,$（什麼都不通信的進程，也叫作死鎖）和$\,\mathrm {SKIP} \,$（它表示成功終止）。

代數算符

CSP有範圍廣泛的代數算符。主要的有：

前綴

前綴算符，將一個事件和一個進程結合起來產生一個新進程。例如：

$a\rightarrow P$

是想要與它的環境通信$a$的進程，而且在$\,a\,$之後，表現得如同進程$\,P\,$。

確定性選擇

確定性（或外部）選擇算符，允許將進程的將來演變定義為，在兩個構件進程之間進行選擇，並允許環境通過通信這兩進程之一的初始事件，來解決這個選擇。例如：

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

是想要通信初始事件$\,a\,$和$\,b\,$的進程，並依據環境決定與之通信的是哪個初始事件，隨後表現為要麼$\,P\,$要麼$\,Q\,$。如果$\,a\,$和$\,b\,$二者同時被通信，則選擇將被非確定性的解決。

非確定性選擇

非確定性（或內部）選擇算子，允許將進程的將來演變定義為，在兩個構件進程之間的選擇，但是不允許環境對哪個構件進程將被選擇的任何控制。例如：

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

可以表現得如同要麼$\,\left(a\rightarrow P\right)\,$要麼$\,\left(b\rightarrow Q\right)\,$。它可以拒絕接受$\,a\,$或$\,b\,$，並只在環境提供了$\,a\,$和$\,b\,$二者時，被強制去通信。如果要選擇的兩邊的初始事件是同一的，非確定性也可能被介入到確定性選擇中。例如：

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

等價於

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

交錯

交錯（interleaving）算符，代表完全獨立的並發活動。進程：

$P\;\vert \vert \vert \;Q$

表現為$\,P\,$和$\,Q\,$二者同時。來自二者進程的事件在時間上是任意交錯的。

接口並行

接口（interface）或廣義（generalized）並行算符，代表並發活動要求在構件進程之間的同步：在接口集合中的任何事件，只能在所有進程都能應允（engage）這個事件的時候出現。例如，進程：

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

要求$\,P\,$和$\,Q\,$必須在事件$\,a\,$可以發生前能夠進行這個事件。例如，進程：

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

可以應允事件$\,a\,$，而變成進程：

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

然而

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

將會簡單的死鎖。

隱藏

隱藏算符，通過使某些事件不可察見，提供了一種抽象進程的方式。隱藏的一個平凡的例子是：

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

假定事件$\,a\,$不出現在$\,P\,$中，它簡單的歸約成：

$P$

例子

一個原型的CSP例子是，一個巧克力售貨機和它與一個想要買巧克力的人之間交互的抽象表示。這個售貨機可以執行兩個不同事件，$\,\mathrm {coin} \,$和$\,\mathrm {choc} \,$，分別表示插入硬幣和投遞巧克力。這個機器在提供巧克力之前想要貨款（現金）可以寫為：

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

一個人可以選擇投幣或刷卡支付可以建模為：

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

這兩個進程可以放置為並行，這樣它們可以相互交互。這種複合進程的行為依賴於這兩個進程必須同步於其上的那些事件。因此：

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

然而如果同步只要求$\,\mathrm {coin} \,$，我們會得到：

$\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)$

如果我們通過隱藏$\,\mathrm {coin} \,$和$\,\mathrm {card} \,$來抽象後者這個複合進程，也就是：

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

我們得到非確定性進程：

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

這是一個要麼提供$\,\mathrm {choc} \,$事件並接着停止，或者就地停止的進程。換句話說，如果我們把這個抽象當作對這個系統的外部查看（比如未看到這個人的做出如何決定的某個人），非確定性就已經介入了。

形式定義

語法

CSP的語法定義了進程和事件可以組合的「合法」方式。設$\,e\,$是一個事件，$\,X\,$是一個事件集合。CSP的基本語法可以定義為：

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

注意：為得到簡要性，上述提供的語法省略了$\,\mathbf {div} \,$進程，它表示分岐，還有各種算符，比如字母化並行、管道、索引選擇。

有關的形式化

從經典無時序的CSP已經派生出一些其他的規定語言和形式化，包括：

• Timed CSP，它結合了時序信息用於關於實時系統的推理。
• Receptive Process Theory，專門化的CSP，假定了異步（就是非阻塞）發送操作。
• CSPP
• HCSP
• TCOZ，集成有時序的CSP於對象Z。
• Circus，集成CSP和基於編程的統一理論的Z表示法。
• CML（COMPASS建模語言），合併了為多系統的系統（SoS）開發的Circus和VDM。
• CspCASL，集成了CSP的CASL擴展。
• LOTOS，結合了CSP與CCS特徵的國際標準。

參見

• 跟蹤理論，跟蹤的一般性理論。
• 跟蹤幺半群和歷史幺半群
• Ease
• XC
• VerilogCSP，向Verilog HDL增加的一組宏，用來支持通信順序進程通道通信。
• Joyce，是Brinch Hansen在大約1989年開發的基於CSP原理的編程語言。
• SuperPascal，是Brinch Hansen開發的編程語言，受到CSP和他早期創作的Joyce的影響。
• Ada，實現了CSP特徵比如約會。
• DirectShow，是DirectX內的視頻框架，它使用了CSP概念來實現音頻和視頻過濾器。
• OpenComRTOS，是正式開發的網絡為中心分布式RTOS，基於了CSP的務實超集。
• 輸入/輸出自動機
• 並行編程模型

延伸閱讀

• Hoare, C. A. R. Communicating Sequential Processes. Prentice Hall International. 2004 [1985] [2011-08-13]. ISBN 978-0-13-153271-7. （原始內容存檔於2021-02-01）. 
  • 本書已經被牛津大學計算實驗室的Jim Davies更新，新版可以於網站Using CSP自由的下載獲取為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）. 
  • 一些與本書有關的鏈接可見於網站。全文可從Bill Roscoe的學術出版列表下載獲取為PS或PDF文件。

外部連結

• WoTUG （頁面存檔備份，存於網際網路檔案館）, CSP和occam風格系統的用戶組，包含了關於CSP和有用鏈接的一些信息。