Understand Communicating Sequencial Processes

主要內(nèi)容為論文解讀：1978年ACM Communicating Sequential Process
此論文主要是一個(gè)編程語(yǔ)言的實(shí)現(xiàn)，并通過(guò)程序樣例來(lái)舉例不同的問(wèn)題如何解決厢拭。

背景

程序的常見(jiàn)結(jié)構(gòu)

• 常見(jiàn)的三種構(gòu)造結(jié)構(gòu)：循環(huán)重復(fù)(for)、條件選擇(if)徘跪、順序執(zhí)行(;)
• Fortran: Subroutine
• Algol 60: Procedure
• PL/I: Entry
• UNIX: Coroutine
• SIMULA 64: Class
• Concurrent Pascal: Process and monitor
• CLU: Cluster
• ALPHARD: Form
• Hewitt: Actor
• 程序演進(jìn)史

并行的興起

• 引入并行：硬件（CDC 6600 并行單元）到軟件（I/O 控制包、多編程操作系統(tǒng)）
• semaphore（ Dutch computer scientist Edsger Dijkstra in 1962 or 1963 提出）
• 公共存儲(chǔ)的檢查與更新：Algol 68, PL/I, 各種不同的機(jī)器碼（開(kāi)銷較大）
• events: PL/I
• 條件臨界區(qū)
• monitors and queues: Concurrent Pascal
• path expression

Motivation: 并行的實(shí)現(xiàn)太多且繁雜汉柒，以上多種方法沒(méi)有一個(gè)統(tǒng)一的選擇標(biāo)準(zhǔn)千埃，因此論文作者提出此編程語(yǔ)言來(lái)整合這些并行的實(shí)現(xiàn)（通過(guò)6個(gè)結(jié)構(gòu)囊括并行的實(shí)現(xiàn)）

內(nèi)容

一種新的設(shè)計(jì)

• Dijkstra's guarded command
  • 條件分支，類似 Go 的 Select 語(yǔ)句
  • 主要的區(qū)別：如果多個(gè)條件為真噪矛，則隨機(jī)選擇一個(gè)分支執(zhí)行
• Dijkstra's parbegin parallel command
  • 啟動(dòng)并發(fā)過(guò)程
• input and output command
  • 過(guò)程間通信手段量蕊；通信值通過(guò)復(fù)制進(jìn)行，而不是共享艇挨；沒(méi)有緩存残炮；指令推遲到其他的過(guò)程能夠處理該消息
  • 等價(jià)于 Go 的無(wú)緩存的 channel
• input + guarded command
  • 等價(jià)于 Go 的 select 語(yǔ)句，條件分支僅當(dāng) input 源 ready 時(shí)開(kāi)始執(zhí)行
  • 多個(gè) input guards 同時(shí)就緒缩滨，只隨機(jī)選擇一個(gè)執(zhí)行势就，其他 guards 沒(méi)有影響
• repetitive command
  • 循環(huán)；終止性取決于所有的 guards 是否已經(jīng)終止
• pattern-matching
  • 做條件判斷使用（比如如何判斷兩個(gè) bool 是否相等）

概念與記號(hào)

程序結(jié)構(gòu)指令

<cmd>            ::= <simple cmd> | <structured cmd>
<simple cmd>     ::= <assignment cmd> | <input cmd> | <output cmd>
<structured cmd> ::= <alternative cmd> | <repetitive cmd> | <parallel cmd>
<null cmd>       ::= skip
<cmd list>       ::= {<declaration>; | <cmd>; } <cmd>

并行指令

<parallel cmd>     ::= [<proc>{||<proc>}]
<proc>             ::= <proc label> <cmd list>
<proc label>       ::= <empty> | <identifier> :: | <identifier>(<label subscript>{,<label subscript>}) ::
<label subscript>  ::= <integer const> | <range>
<integer constant> ::= <numeral> | <bound var>
<bound var>        ::= <identifier>
<range>            ::= <bound variable>:<lower bound>..<upper bound>
<lower bound>      ::= <integer const>
<upper bound>      ::= <integer const>

并行語(yǔ)句舉例——循環(huán)構(gòu)造并行語(yǔ)句

• 其他并行語(yǔ)句舉例

(1) [cardreader ? cardimage || lineprinter ! lineimage]
    // 兩個(gè)并行過(guò)程
(2) [west::DISASSEMBLE || X::SQUASH || east::ASSEMBLE]
    // 三個(gè)并行過(guò)程
(3) [room::ROOM || fork(i:0..4)::FORK || phil(i:0..4)::PHIL]
    // 十一個(gè)個(gè)并行過(guò)程脉漏，其中第二個(gè)和第三個(gè)并行過(guò)程分別包含五個(gè)并行的子過(guò)程

賦值指令

<assignment cmd>    ::= <target var> := <expr>
<expr>              ::= <simple expr> | <structured expr>
<structured expr>   ::= <constructor> ( <expr list> )
<constructor>       ::= <identifier> | <empty>
<expr list>         ::= <empty> | <expr> {, <expr> }
<target var>        ::= <simple var> | <structured target>
<structured target> ::= <constructor> ( <target var list> )
<target var list>   ::= <empty> | <target var> {, <target var> }

• 舉例

(1) x := x + 1                  // 普通的賦值
(2) (x, y) := (y, x)            // 普通的賦值
(3) x := cons(left, right)      // 結(jié)構(gòu)體賦值
(4) cons(left, right) := x      // 如果 x 是一個(gè)結(jié)構(gòu)體 cons(y, z)苞冯，則賦值成功 left:=y, right:=z，否則失敗
(5) insert(n) := insert(2*x+1)  // 等價(jià)于 n := 2*x + 1
(6) c := P()                    // 空結(jié)構(gòu)體, 或稱‘信號(hào)’（比如Go里面的 struct{}{} 充當(dāng)一個(gè)信號(hào)侧巨，并不會(huì)實(shí)際占用內(nèi)存）
(7) P() := c                    // 如果 c 同為信號(hào)舅锄，則無(wú)實(shí)際效果，否則失敗
(8) insert(n) := has(n)         // 失敗司忱。不允許不匹配的結(jié)構(gòu)體之間進(jìn)行賦值

輸入與輸出指令

<input cmd>   ::= <source> ? <target var>
<output cmd>  ::= <destination> ! <expr>
<source>      ::= <proc name>
<destination> ::= <proc name>
<proc name>   ::= <identifier> | <identifier> ( <subscripts> )
<subscripts>  ::= <integer expr> {, <integer expr> }

• 舉例

(1) cardreader?cardimage      // 類似于 cardimage <- cardreader
(2) lineprinter!lineimage     // 類似于 lineprinter := <- lineimage
(3) X?(x,y)                   // 從過(guò)程 X 接受兩個(gè)值皇忿，并賦值給 x 和 y
(4) DIV!(3*a + b, 13)         // 向過(guò)程 DIV 發(fā)送兩個(gè)值，分別為 3*a+b 和 13  
(5) console(i)?c              // 向第 i 個(gè) console 發(fā)送值 c
(6) console(j-1)!"A"          // 向第 j-1 個(gè) console 發(fā)送字符 "A"
(7) X(i)?V()                  // 從第 i 個(gè) X 接受一個(gè)信號(hào) V
(8) sem!P()                   // 向 sem 發(fā)送一個(gè)信號(hào) P

通過(guò) (3) 和 (4)烘贴，思考：[X :: DIV!(3*a+b, 13) || DIV :: X?(x,y)] 表達(dá)什么意思？
X被定義為 DIV 指令撮胧，DIV 被定義為 X 指令桨踪；X是圖個(gè)輸出指令，DIV 是一個(gè)輸入指令芹啥；看上去是并發(fā)執(zhí)行锻离，但是實(shí)際上是順序執(zhí)行，X 首先執(zhí)行完墓怀，把 3*a+b, 13 輸出給 DIV汽纠，然后 DIV 再接受 X 的兩個(gè)值 x y。

選擇與重復(fù)指令

<repetitive cmd>  ::= * <alternative cmd>
<alternative cmd> ::= [<guarded cmd> { □ <guarded cmd> }]
<guarded cmd>     ::= <guard> → <cmd list> | ( <range> {, <range> }) <guard> → <cmd list>
<guard>           ::= <guard list> | <guard list>;<input cmd> | <input cmd>
<guard list>      ::= <guard elem> {; <guard elem> }
<guard elem>      ::= <boolean expr> | <declaration>

• 舉例

(1) [x ≥ y → m := x □ y ≥ x → m := y] 
    // 如果某個(gè)條件成立傀履，則執(zhí)行 → 后的語(yǔ)句虱朵；若均成立則隨機(jī)選擇一個(gè)執(zhí)行
(2) i := 0; *[i < size; content(i) ≠ n → i := i+1] 
    // 依次檢查 content 中的值是否與 n 相同
(3) *[c:character; west?c → east!c] 
    // 從 west 復(fù)制一個(gè)字符串并輸出到 east 中
(4) *[(i:1..10)continue(i); console(i)?c → X!(i,c); console(i)!ack(); continue(i) := (c ≠ sign off)]
    // 監(jiān)聽(tīng)來(lái)自 10 個(gè) console 的值，并將其發(fā)送給 X钓账，當(dāng)收到 sign off 時(shí)終止監(jiān)聽(tīng)
(5) *[n:integer; X?insert(n) → INSERT □ n:integer; X?has(n) → SEARCH; X!(i<size)]
    // insert 操作: 執(zhí)行 INSERT
    // has 操作: 執(zhí)行 SEARCH碴犬，并當(dāng) i < size 時(shí)，向 X 發(fā)送 true梆暮，否則發(fā)送 false
(6) *[X?V() → val := val+1 □ val > 0; Y?P() → val := val-1]
    // V 操作: val++
    // P 操作: val > 0 時(shí), val--服协，否則失敗

算符

順序算符 ; 
并行算符 ||  
賦值算符 := 
輸入算符 ? （發(fā)送）
輸出算符 ! （接受）
選擇算符 □ 
守衛(wèi)算符 → 
重復(fù)算符 *

協(xié)程（Coroutine）

S31 COPY

程序描述：編寫(xiě)一個(gè)過(guò)程 X，復(fù)制從 west 過(guò)程輸出的字符到 east 過(guò)程

COPY :: *[c:character; west?c → east!c]

該語(yǔ)句等價(jià)于以下 go 語(yǔ)句：

func S31_COPY(west, east chan rune) {
    for c := range west {
        east <- c
    }
    close(east)
}

S32 SQUASH

程序描述：調(diào)整前面的程序啦粹，替換成對(duì)出現(xiàn)的「**」為「↑」偿荷，假設(shè)最后一個(gè)字符不是「*」窘游。

SQUASH :: *[c:character; west?c → 
   [ c != asterisk → east!c
    □ c = asterisk → west?c;
          [ c != asterisk → east!asterisk; east!c
           □ c = asterisk → east!upward arrow
   ] ]    ]

練習(xí)：調(diào)整上面的程序，處理最后以奇數(shù)個(gè)「*」結(jié)尾的輸入數(shù)據(jù)跳纳。
SQUASH_EX :: *[c:character; west?c → 
   [ c != asterisk → east!c
    □ c = asterisk → west?c;
          [ c != asterisk → east!asterisk; east!c
           □ c = asterisk → east!upward arrow
+         ] □ east!asterisk
   ]    ]

該程序等價(jià)于以下 Go 程序：

func S32_SQUASH_EX(west, east chan rune) {
    for {
        c, ok := <-west
        if !ok {
            break
        }
        if c != '*' {
            east <- c
        }
        if c == '*' {
            c, ok = <-west
            if !ok {
+               east <- '*'
                break
            }
            if c != '*' {
                east <- '*'
                east <- c
            }
            if c == '*' {
                east <- '↑'
            }
        }
    }
    close(east)
}

S33 DISASSEMBLE

程序描述：從卡片盒中讀取卡片上的內(nèi)容忍饰，并以流的形式將它們輸出到過(guò)程 X ，并在每個(gè)卡片的最后插入一個(gè)空格棒旗。

DISASSEMBLE::
*[cardimage:(1..80)characters; cardfile?cardimage →
    i:integer; i := 1;
    *[i <= 80 → X!cardimage(i); i := i+1 ]
    X!space
]

等價(jià)于以下 Go 語(yǔ)言程序：

func S33_DISASSEMBLE(cardfile chan []rune, X chan rune) {
    cardimage := make([]rune, 0, 80)
    for tmp := range cardfile {
        if len(tmp) > 80 {
            cardimage = append(cardimage, tmp[:80]...)
        } else {
            cardimage = append(cardimage, tmp[:len(tmp)]...)
        }
        for i := 0; i < len(cardimage); i++ {
            X <- cardimage[i]
        }
        X <- ' '
        cardimage = cardimage[:0]
    }
    close(X)
}

S34 ASSEMBLE

程序描述：將一串流式字符串從過(guò)程 X 打印到每行 125 個(gè)字符的 lineprinter 上喘批。必要時(shí)將最后一行用空格填滿。

ASSEMBLE::
lineimage:(1..125)character;
i:integer, i:=1;
*[c:character; X?c →
    lineimage(i) := c;
    [i <= 124 → i := i+1
    □ i = 125 → lineprinter!lineimage; i:=1
]   ];
[ i = 1 → skip
□ i > 1 → *[i <= 125 → lineimage(i) := space; i := i+1];
  lineprinter!lineimage
]

等價(jià)于以下 Go 語(yǔ)言程序：

func S34_ASSEMBLE(X chan rune, lineprinter chan string) {
    lineimage := make([]rune, 125)

    i := 0
    for c := range X {
        lineimage[i] = c
        if i <= 124 {
            i++
        }
        if i == 125 {
            lineimage[i-1] = c
            lineprinter <- string(lineimage)
            i = 0
        }
    }
    if i > 0 {
        for i <= 124 {
            lineimage[i] = ' '
            i++
        }
        lineprinter <- string(lineimage)
    }

    close(lineprinter)
    return
}

S35 REFORMAT

程序描述：從長(zhǎng)度為 80 的卡片上進(jìn)行讀取铣揉，并打印到長(zhǎng)度為 125 個(gè)字符的 lineprinter 上饶深。每個(gè)卡片必須跟隨一個(gè)額外的空格，最后一行須使用空格進(jìn)行填充逛拱。

REFORMAT::
[west::DISASSEMBLE || X::COPY || east::ASSEMBLE]

等價(jià)于以下 Go 語(yǔ)言程序：

func S35_Reformat(cardfile chan []rune, lineprinter chan string) {
    west, east := make(chan rune), make(chan rune)
    go S33_DISASSEMBLE(cardfile, west)
    go S31_COPY(west, east)
    S34_ASSEMBLE(east, lineprinter)
}

S36 Conway's Problem

程序描述：調(diào)整前面的程序敌厘，使用「↑」替換每個(gè)成對(duì)出現(xiàn)的「*」。

CONWAY::
[west::DISASSEMBLE || X::SQUASH || east::ASSEMBLE]

等價(jià)于以下 Go 語(yǔ)言程序：

func S35_ConwayProblem(cardfile chan []rune, lineprinter chan string) {
    west, east := make(chan rune), make(chan rune)
    go S33_DISASSEMBLE(cardfile, west)
    go S32_SQUASH_EX(west, east)
    S34_ASSEMBLE(east, lineprinter)
}

子程朽合、數(shù)據(jù)表示與遞歸（Subroutine\Data Representation\Recursive）

不展開(kāi)闡述例子俱两，可以直接看論文，以及對(duì)應(yīng)的Go實(shí)現(xiàn)

子程

[subr:SUBROUTINE || X::USER] // 子程和用戶程序并行執(zhí)行

SUBROUTINE::[X?(value params) → …; X!(result params)]
// 子程從用戶程序讀取一個(gè)輸入曹步，執(zhí)行對(duì)應(yīng)分支宪彩，最后輸出給用戶程序結(jié)果
USER::[ …; subr!(arguments); …; subr?(results)]
// 用戶程序輸出給子程一個(gè)參數(shù)，從子程讀取一個(gè)輸入（即返回的結(jié)果）

子程分為一個(gè)子程序和一個(gè)用戶程序讲婚。用戶往子程發(fā)送一個(gè)輸入尿孔，監(jiān)聽(tīng)子程獲取輸出；子程則監(jiān)聽(tīng)用戶程序的輸入筹麸，并執(zhí)行語(yǔ)句活合，最后輸出給用戶程序。
可以視為Go語(yǔ)言里面物赶，子程序和用戶程序通過(guò) channel 來(lái)傳遞數(shù)據(jù)白指。

例子：

• S41 帶余除法
• S42 階乘
• S43 S44 S45 S46 集合：實(shí)現(xiàn)一個(gè)集合的 insert 與 has 方法

數(shù)據(jù)表示

*[X? method1(value params) → … 
□ X? method2(value params) → … ]

數(shù)據(jù)表示可以視為一個(gè)具有多入口的子過(guò)程，根據(jù) guarded command 進(jìn)行分支選擇酵紫。
可以參考 Go 的 Select 實(shí)現(xiàn)：滿足 case 條件告嘲，則執(zhí)行一個(gè)分支。

遞歸

[recsub(0)::USER || recsub(i:1..reclimit):: RECSUB]
USER::recsub(1)!(arguments); … ; recsub(1)?(results);

遞歸可以通過(guò)一個(gè)子程數(shù)組進(jìn)行模擬奖地，用戶過(guò)程（零號(hào)子程）向一號(hào)子程發(fā)送必要的參數(shù)状蜗，再?gòu)囊惶?hào)子程接受遞歸后的結(jié)果。
用戶程序輸出給一號(hào)子程鹉动，一號(hào)子程獲取輸入后轧坎，處理并輸出給二號(hào)子程，二號(hào)子程輸出給三號(hào)子程泽示，...缸血，最后reclimit號(hào)子程輸出給reclimit-1號(hào)子程蜜氨，...，二號(hào)子程輸出給一號(hào)子程捎泻，一號(hào)子程輸出給用戶程序

監(jiān)控與調(diào)度（Subroutine\Data Representation\Recursive）

監(jiān)控可以被視為與多個(gè)用戶過(guò)程通信的單一過(guò)程飒炎，且總是能跟用戶過(guò)程進(jìn)行通信。例如：

*[(i:1..100)X(i)?(value param) → …; X(i)!(results)]

當(dāng)兩個(gè)用戶過(guò)程同時(shí)選擇一個(gè) X(i) 時(shí)笆豁，guarded cmd(順序執(zhí)行) 保護(hù)了監(jiān)控結(jié)果不會(huì)被錯(cuò)誤地發(fā)送到錯(cuò)誤的用戶過(guò)程中郎汪。
例子：S51 Buffered Channel；S52 信號(hào)量闯狱；S53 哲學(xué)家進(jìn)餐問(wèn)題

算法（algorithom）

例子：S61 Eratosthenes 素?cái)?shù)篩法煞赢；S62 矩陣乘法

反思和總結(jié)

這篇論文中討論的 CSP 設(shè)計(jì)是 Tony Hoare 的早期提出的設(shè)計(jì)，與隨后將理論完整化后的 CSP（1985）存在兩大差異：

缺陷1: 未對(duì) channel 命名

并行過(guò)程的構(gòu)造具有唯一的名詞哄孤，并以一對(duì)冒號(hào)作為前綴：[a::P || b::Q || … || c::R]
在過(guò)程 P 中照筑，命令 b!v 將 v 輸出到名為 b 的過(guò)程。該值由在過(guò)程 Q 中出現(xiàn)的命令 a?x 輸入瘦陈。
過(guò)程名稱對(duì)于引入它們的并行命令是局部的凝危，并且組件過(guò)程間的通信是隱藏的。
雖然其優(yōu)點(diǎn)是不需要在語(yǔ)言中引入任何 channel 或者 channel 聲明的概念晨逝。

缺點(diǎn)：

1. 子過(guò)程需要知道其使用過(guò)程的名稱蛾默，使得難以構(gòu)建封裝性較好的子過(guò)程庫(kù)
2. 并行過(guò)程組合本質(zhì)上是具有可變數(shù)量參數(shù)的運(yùn)算，不能進(jìn)行簡(jiǎn)化（見(jiàn) CSP 1985）

缺陷2: 重復(fù)指令的終止性模糊

重復(fù)指令默認(rèn)當(dāng)每個(gè) guard 均已終止則指令中終止捉貌，這一假設(shè)過(guò)強(qiáng)支鸡。具體而言，對(duì)于 *[a?x → P □ b?x → Q □ ...]
要求當(dāng)且僅當(dāng)輸入的所有過(guò)程 a,b,… 均終止時(shí)整個(gè)過(guò)程才自動(dòng)終止昏翰。

缺點(diǎn)：

1. 定義和實(shí)現(xiàn)起來(lái)很復(fù)雜
2. 證明程序正確性的方法似乎比沒(méi)有簡(jiǎn)單苍匆。

一種可能的弱化條件為：直接假設(shè)子過(guò)程一定會(huì)終止刘急。

一些要點(diǎn)

CSP 1978 中描述的編程語(yǔ)言（與 Go 所構(gòu)建的基于通道的 channel/select 同步機(jī)制進(jìn)行對(duì)比）：

1. channel 沒(méi)有被顯式命名（作者描述了過(guò)程之間通信棚菊，但是隱藏了具體實(shí)現(xiàn)，沒(méi)有明確命名出channel）
2. channel 沒(méi)有緩沖叔汁，對(duì)應(yīng) Go 中 unbuffered channel
3. buffered channel 不是一種基本的編程源語(yǔ)统求，并展示了一個(gè)使用 unbuffered channel 實(shí)現(xiàn)其作用的例子
4. guarded command 等價(jià)于 if 與 select 語(yǔ)句的組合，分支的隨機(jī)觸發(fā)性是為了提供公平性保障
5. guarded command 沒(méi)有對(duì)確定性分支選擇與非確定性（即多個(gè)分支有效時(shí)隨機(jī)選擇）分支選擇進(jìn)行區(qū)分
6. repetitive command 的本質(zhì)是一個(gè)無(wú)條件的 for 循環(huán)据块，但終止性所要求的條件太苛刻码邻，不利于理論的進(jìn)一步形式化
7. CSP 1978 中描述的編程語(yǔ)言對(duì)程序終止性的討論幾乎為零（作者自己在論文中也還沒(méi)想清楚）
8. 此時(shí)與 Actor 模型進(jìn)行比較，CSP 與 Actor 均在實(shí)體間直接通信另假，區(qū)別在于 Actor 支持異步消息通信像屋，而 CSP 1978 是同步通信
   …

Q&A

Q: Tony Hoare 提出 CSP 的時(shí)代背景是什么？
A: 并行計(jì)算的興起边篮、需要一種形式化的并行編程語(yǔ)言

Q: CSP 1978 理論到底有哪些值得我們研究的地方己莺？
A: 一種面向并行過(guò)程的演算代數(shù)

Q: CSP 1978 理論是否真的就是我們目前熟知的基于通道的同步方式奏甫？
A: 不是，早期的設(shè)計(jì)中沒(méi)有顯式的對(duì)通道進(jìn)行命名凌受。

Q: CSP 1978 理論的早期設(shè)計(jì)存在什么樣的缺陷阵子？
A: 早期設(shè)計(jì)中沒(méi)有對(duì)通道進(jìn)行命名是設(shè)計(jì)的一個(gè)主要缺陷，此外胜蛉，對(duì)程序終止性的條件描述過(guò)于模糊挠进，形式化程度不夠完善。

進(jìn)一步閱讀的參考文獻(xiàn)

完成閱讀此論文之后誊册，就可以繼續(xù)看之后的理論發(fā)展领突。

[Hoare 78]
Hoare, C. A. R. (1978). Communicating sequential processes. Communications of the ACM, 21(8), 666–677.

[Brookes 84]
S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. 1984. A Theory of Communicating Sequential Processes. J. ACM 31, 3 (June 1984), 560-599.

[Hoare 85]
C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice-Hall, Inc., Upper Saddle River, NJ, USA.

[Milner 82]
R. Milner. 1982. A Calculus of Communicating Systems. Springer-Verlag, Berlin, Heidelberg.

[Fidge 94]
Fidge, C., 1994. A comparative introduction to CSP, CCS and LOTOS. Software Verification Research Centre, University of Queensland, Tech. Rep, pp.93-24.

推薦書(shū)籍

相關(guān)鏈接

講稿PPT；Youtube Go夜讀 演講