CSP 並發編程入門：為什麼 Java 需要 Communicating Sequential Processes (第 1 部分)

前言：多執行緒的痛苦與逃避

Java 多執行緒編程以困難著稱。Sun 官方在 EJB 規格中甚至明確宣稱：

「應用程式開發人員不必理解低層交易、狀態管理、多執行緒、連線池或其他複雜的低層 API。」

這種「隱藏複雜度」的思維導致大多數開發者選擇避開多執行緒，或完全依賴框架。但現實是：許多企業級問題本質上需要並發解決，而 EJB 等框架並非萬靈丹。本系列介紹一種承認複雜度、提供數學嚴謹解決方案的範式：CSP (Communicating Sequential Processes)。

一、Java 平台並發編程基礎回顧

執行緒建立兩種方式

1. 繼承 java.lang.Thread，覆寫 run()，呼叫 start()。
2. 實作 Runnable 介面，傳入 new Thread(runnable).start()。

同步機制：監視器模式

• Hoare (1974) 提出 Monitor：受互斥鎖保護的程式碼區塊。
• Java synchronized 關鍵字直接對應：執行緒爭取物件關聯的唯一互斥鎖，成功者執行區塊，離開時釋放。

等待/通知機制

• wait()：釋放鎖並進入物件等待集；notify()/notifyAll()：喚醒等待執行緒。
• 難點：需掌握所有使用同一鎖的方法邏輯才能推理正確性，複雜度隨方法數爆炸增長。

執行緒狀態機

NEW → RUNNABLE → (OS 排程) RUNNING → BLOCKED (I/O、鎖等待) → RUNNABLE → DEAD (run() 結束或未捕獲異常)。

排程模型

• 協作式：執行緒自願放棄 CPU (易發生飢餓)。
• 搶佔式：OS 依時鐘中斷強制切換，支援優先級、時間片等策略 (現代主流)。

二、四大經典並發缺陷

三、飢餓哲學家問題：資源耗盡的經典展示

Peter Welch 教授改編「五哲學家進餐」：

• 5 位哲學家，4 份雞肉/批，廚師循環供應。
• 4 位正常：思考 3 秒 → 取餐。
• 1 位貪婪：不思考、持續搶餐。
• 結果：貪婪者第一次太早到達 → wait()；開飯時 notify() 喚醒，但已有 4 位正常哲學家排隊在前，搶光雞肉 → 貪婪者永遠在等待集尾部，永遠吃不到。

揭示 wait/notify + 等待集隊列 的非公平性：被喚醒執行緒不一定能立即獲鎖，條件可能再次失效，導致無限重試。

四、驗證困境：為什麼傳統多執行緒難以證明正確？

1. 狀態空間爆炸：N 個執行緒、M 個鎖、K 個條件變數 → 組合狀態數天文級。
2. 非確定性排程：同樣輸入，不同執行順序產生不同結果。
3. 缺乏形式模型：Java 語言規格未提供並發語義的數學模型。
4. Heisenbug：除錯器改變時序導致 Bug 消失/無法重現。

現有對策皆有限：

• 長時間壓力測試：覆蓋率未知，無法證明無 Bug。
• 設計模式/守則：僅在全系統遵守時有效，無法強制執行。

五、CSP：第三條路 — 數學嚴謹的並發範式

歷史淵源

• C.A.R. Hoare (1978) 提出 CSP，將平行組合視為基本程式結構。
• 影響了 Occam 語言、Ada 設計，成為並發理論基石。

核心思想

1. Process：封裝資料與演算法，擁有獨立控制流，無公開方法。
2. Channel：進程間唯一通訊方式，同步、無共享記憶體。
3. Composition：進程透過 Channel 組合為網絡，網絡本身又是進程 (遞歸)。
4. Formal Verification：CSP 擁有完整數學理論 (Traces, Failures, Refusal 等)，可用模型檢查器 (FDR2) 證明無死鎖、活鎖、飢餓。

六、JCSP：CSP 在 Java 的落地實作

• 由 Kent 大學 Peter Welch 教授與 Paul Austin 開發。
• 內部使用 Java 原生 synchronized/wait/notify 實作 CSP 語義。
• 提供 CSProcess、ChannelInput/Output、Parallel、Guard/Alternative 等高階 API。
• 開發者無需理解底層監視器機制，直接用 CSP 抽象編程，仍獲形式化驗證保障。

七、本系列路線圖

1. 第 1 部分 (本文)：Java 多執行緒痛點、四大缺陷、驗證困境、CSP 理論優勢。
2. 第 2 部分：CSP 理論深入、JCSP 核心構造實作、確定性/非確定性範例 (IntegrateInt、SquaresInt、ScaleInt)。
3. 第 3 部分：CSP 與 AOP 相似性、高級同步 (Barrier/Bucket/CREW)、ProcessManager、JCSP.Net 分布式、vs java.util.concurrent。

八、結語

CSP 不隱藏並發複雜度，而是提供嚴謹的數學框架讓開發者在設計階段即能推理並發行為。JCSP 將這套理論帶入 Java 生態，配合形式化驗證工具，為安全關鍵、高併發系統提供了超越傳統鎖同步的解決方案。

下一部分將動手實作 JCSP 核心構造，體驗「以通道連接進程，而非鎖保護共享物件」的編程範式轉換。

參考資源

• Brian Goetz, Threading Lightly 三部曲 / Java Theory and Practice 專欄
• Allen Holub, Programming Java Threads in the Real World / If I Were King
• C.A.R. Hoare, Communicating Sequential Processes (1978) / Monitors (1974) — 免費 PDF
• Bill Roscoe, Theory and Practice of Concurrency (1997)
• Peter Welch, Formal Analysis of Concurrent Java Systems (2000)
• JCSP 官網 / FDR2 / Occam-pi / CTJ 替代實作

作者簡介

Abhijit Belapurkar，IIT Delhi 計算機科學學士，11 年分布式架構與資安經驗，6 年 Java N-tier 開發，現任 Infosys 班加羅爾高級技術架構師 (J2EE 領域)。