通信顺序进程

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

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

然而如果同步只要求 $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)$

如果我們通過隱藏 $coin$ 和 $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 已經衍生出一些其他的規定語言和形式化，包括：

## 參見

## 延伸閱讀

* Hoare, C. A. R. Communicating Sequential Processes. Prentice Hall International. 2004 [1985] [2011-08-13]. ISBN978-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]. ISBN978-0-13-674409-2. （原始內容存檔於 2022-01-18）. 
  * 一些與本書有關的連結可見於網站。全文可從 Bill Roscoe 的學術出版列表下載取得為 PS 或 PDF 檔案。

## 參照

## 外部連結

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