Communicating Sequential Processes

Communicating Sequential Processes（CSP）とは、並行性に関するプロセス計算の理論のひとつである^[1]。プログラミング言語Occamにも影響を与えた^[2]^[1]。

CSPは1978年、アントニー・ホーアが最初に考案し^[3]、その後かなり改良されていった。CSPは様々なシステムにおける並行性を記述し検証する、形式仕様記述ツールとして産業で利用されてきた。たとえば、T9000トランスピュータ^[4]やセキュアな電子商取引システム^[5]などの例がある。理論としても、応用範囲を広げる（より大規模なシステムの解析に使えるようにする^[6]）などの研究が行われている。

歴史

ホーアの1978年の論文で提示されたCSPは、プロセス計算というよりも本質的には並行プログラミング言語であった。後のCSPとは構文が著しく異なり、数学的に定義された意味論を持っておらず^[7]、無制限の非決定性を表現することはできなかった^[8]。本来のCSPでは、並列に動作する有限個の逐次プロセスが同期式のメッセージパッシングで相互に通信するという形式でプログラムを記述していた。その後のCSPとは対照的に、各プロセスには名前が付けられ、メッセージには送信元と送信先の名前が指定されている。たとえば次のプロセス

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

は、west という名前のプロセスから文字を繰り返し受信し、その文字を east という名前のプロセスに送信する。並列合成

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

では、west という名前を DISASSEMBLE プロセスに割り当て、X という名前を COPY プロセスに割り当て、east という名前を ASSEMBLE プロセスに割り当て、これらを並行に実行する^[3]。

その後、ホーアは Stephen Brookes や Bill Roscoe らと共に理論面の改良に取り組み、CSPをプロセス代数的にしていった。この方向性は、同時期にロビン・ミルナーが行っていた Calculus of Communicating Systems（CCS）の研究と相互に影響しあっている。CSPの理論面は1984年に発表され^[9]、1985年に出版されたホーアの著書 Communicating Sequential Processes^[7] で一般に知られるようになった。2006年9月現在でも、Citeseer によればこの本は計算機科学分野での引用回数第3位とされている（ただし、サンプリング方式であるため信頼性は高くない）。このホーアの著書以降、CSPの理論は若干変更されただけである。変更のほとんどは、CSPプロセス解析と検証のための自動化ツールの出現に対応するものである。Roscoe の The Theory and Practice of Concurrency^[1] ではこの新たなCSPが解説されている。

概要

名前が示すとおり、CSPは独立したプロセス群がメッセージパッシングによって通信することで相互にやり取りしているものとしてシステムを記述する。しかし、CSPの名称に含まれる "Sequential"（逐次的）という部分は誤解を生じる可能性がある。というのも最近のCSPでは、プロセスは単なる逐次的プロセスだけでなく、より基本的なプロセス群の並列合成で生成されるプロセスも含まれるからである。プロセス間の関係やプロセスが周囲と通信する方法は、各種プロセス代数演算子を使って表される。このような代数的手法を使うことで、少数のプリミティブ要素から容易に極めて複雑なプロセスを構築できる。

プリミティブ

CSP は、そのプロセス代数における2種類のプリミティブのクラスを提供する。

イベント: イベントとは、通信あるいは相互作用を意味する。不可分で瞬間的なものと見なされる。不可分名（たとえば、 ${\mathit {on}}$ 、 ${\mathit {off}}$ ）、複合名（たとえば、 $valve.open$ 、 $valve.close$ ）、入出力イベント（たとえば、 $mouse?xy$ 、 $screen!bitmap$ ）などがある。
プリミティブプロセス: プリミティブプロセスとは、基本的振る舞いを表したものである。たとえば、 ${\mathit {STOP}}$ （まったく通信しないプロセスであり、デッドロックとも言う）や ${\mathit {SKIP}}$ （成功裡に終了することを表す）がある。

代数演算子

CSP には様々な代数演算子がある。主なものを以下に挙げる。

プレフィックス: プレフィックス演算子は、イベントとプロセスを結合して新たなプロセスを生成する。たとえば、

a\rightarrow P

は、

{\mathit {a}}

にその環境と通信させようとするプロセスであり、

{\mathit {a}}

の後では、プロセス

{\mathit {P}}

として振舞う。

決定的選択: 決定的（または外部）選択演算子は、プロセスの将来を2つのコンポーネントプロセス間の選択で定義可能とするもので、プロセス群と初期イベントとのやり取りによって環境が選択を行うことを可能にする。たとえば

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

は、初期イベント

{\mathit {a}}

および

{\mathit {b}}

とやり取りしようとするプロセスであり、環境がどちらの初期イベントとやり取りすることを選択したかによって、

{\mathit {P}}

または

{\mathit {Q}}

として振舞うようになる。

{\mathit {a}}

および

{\mathit {b}}

と同時にやり取りする場合、選択は非決定的となる。

非決定的選択: 非決定的（または内部）選択演算子は、プロセスの将来を2つのコンポーネントプロセス間の選択で定義可能とするものだが、環境がどちらのコンポーネントプロセスを選択するかを制御できない。たとえば

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

は、

\left(a\rightarrow P\right)

または

\left(b\rightarrow Q\right)

のどちらかとして振舞う。

{\mathit {a}}

または

{\mathit {b}}

を受容することを拒否でき、環境が

{\mathit {a}}

と

{\mathit {b}}

の両方を提供する場合にそれとやり取りするだけである。決定的選択で選択肢である2つの初期イベントが同一である場合、非決定性が生じる。したがってたとえば、

\left(a\rightarrow a\rightarrow STOP\right)\Box \left(a\rightarrow b\rightarrow STOP\right)

は次と等価である。

a\rightarrow \left(\left(a\rightarrow STOP\right)\sqcap \left(b\rightarrow STOP\right)\right)

インターリーブ: インターリーブ演算子は、完全に独立した並行動作を表す。次のプロセス

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

は、

{\mathit {P}}

と

{\mathit {Q}}

が同時並行に動作することを意味する。両方のプロセスが発生するイベントは時系列上でインターリーブされる。

インタフェース並列: インタフェース並列演算子は、コンポーネントプロセス間で同期を必要とする並行動作を表す。インタフェースにおけるイベントは、全コンポーネントプロセスがそのイベントに関わることが可能な場合にのみ発生する。たとえば、次のプロセス

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

は、イベント

{\mathit {a}}

が発生する前に

{\mathit {P}}

と

{\mathit {Q}}

が共にそのイベントを扱える状態になっている必要があることを意味する。したがって例えば、次のプロセス

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

は、イベント

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

は、イベント

{\mathit {a}}

が

{\mathit {P}}

の中で出現しないものとすると、以下のように省略可能である。

{\mathit {P}}

例

簡単なCSPの例として、チョコレートの自動販売機の抽象表現とチョコレートを購入しようとしている人との相互作用を考える。この自動販売機は2つのイベント "coin" と "choc" を扱う。"coin" は代金の投入を表し、"choc" はチョコレートの引渡しを表す。チョコレートを渡す前に代金の支払いを要求する機械は次のように記述される。

VendingMachine=coin\rightarrow choc\rightarrow STOP

支払いに硬貨またはカードを使う人は、以下のようにモデル化される。

Person=(coin\rightarrow STOP)\Box (card\rightarrow STOP)

これら2つのプロセスを並列に置くことで、互いにやり取りできるようにする。合成プロセスの振る舞いは、2つのプロセスが同期しなければならないイベント依存する。すなわち、

VendingMachine\left\vert \left[\left\{coin,card\right\}\right]\right\vert Person\equiv coin\rightarrow choc\rightarrow STOP

ここで、同期が "coin" についてのみ必要とされる場合、以下が得られる。

VendingMachine\left\vert \left[\left\{coin\right\}\right]\right\vert Person\equiv \left(coin\rightarrow choc\rightarrow STOP\right)\Box \left(card\rightarrow STOP\right)

この合成プロセスを "coin" と "card" というイベントを隠蔽することで抽象化すると、次のようになる。

\left(\left(coin\rightarrow choc\rightarrow STOP\right)\Box \left(card\rightarrow STOP\right)\right)\setminus \left\{coin,card\right\}

以上から、次の非決定性プロセスが得られる。

\left(choc\rightarrow STOP\right)\sqcap STOP

これは、"choc" イベント後に停止するか、単に停止するプロセスである。言い換えれば、システムを外部から見たものとして上記抽象化を扱えば（すなわち、人間が行った決定を無視すれば）、非決定性が生じる。

形式的定義

構文

CSPの構文は、プロセスとイベントの結合の「正当な」方法を定義する。 ${\mathit {e}}$ をイベント、 ${\mathit {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}}

註：上記の構文では簡潔にするため、発散 (計算機科学)（英語版）^[10]を表す $\mathbf {div}$ プロセスや、アルファベット付き並列、パイピング、インデックス付き選択などの様々な演算子を省略している。

形式意味論

文法的に正しいCSPの表現の意味を定義する形式意味論はいくつかある。CSPの理論には、相互に一貫した表示的意味論、代数的意味論、操作的意味論がある。

表示的意味論

CSPの主な表示的モデルとして、トレースモデル、安定失敗モデル、失敗/発散モデルの3つがある。プロセス表現とこれらモデルとの意味論的マッピングがCSPの表示的意味論となる^[1]。

トレースモデルは、そのプロセスが扱う一連のイベント（トレース）でプロセス表現の意味を定義する。例えば、

$traces\left(STOP\right)=\left\{\langle \rangle \right\}$ 何故なら $STOP$ は何のイベントも扱わないから
$traces\left(a\rightarrow b\rightarrow STOP\right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ 何故ならプロセス $(a\rightarrow b\rightarrow STOP)$ は、何のイベントも扱わない場合、イベント $a$ を受け付ける場合、イベント $a$ を受け付けた後でイベント $b$ を受け付ける場合の3つのケースがありうるから

より形式的に表せば、プロセス $P$ のトレースモデルでの意味は $traces\left(P\right)\subseteq \Sigma ^{\ast }$ として定義される。すなわち、

$\langle \rangle \in traces\left(P\right)$ （ $traces\left(P\right)$ は空のシーケンスを含む）
$s_{1}\smallfrown s_{2}\in traces\left(P\right)\implies s_{1}\in traces\left(P\right)$ （ $traces\left(P\right)$ はプレフィックスで閉じている）

ここで、 $\Sigma ^{\ast }$ は考えられる全てのイベントの有限な並びの集合である。

安定失敗モデルはトレースモデルを拒絶集合（refusal set）で拡張したものである。拒絶集合とは、プロセスが実行を拒絶できるイベントの集合 $X\subseteq \Sigma$ である。失敗（failure）は $\left(s,X\right)$ という対で表される。ここで $s$ はトレース、 $X$ は拒絶集合であり、トレース $s$ が実行されたときそのプロセスが拒絶するイベント群を表す。安定失敗モデルにおけるプロセスの観測された振る舞いは、 $\left(traces\left(P\right),failures\left(P\right)\right)$ という対で表される。例えば、

$failures\left(\left(a\rightarrow STOP\right)\Box \left(b\rightarrow STOP\right)\right)=\left\{\left(\langle \rangle ,\emptyset \right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}$
$failures\left(\left(a\rightarrow STOP\right)\sqcap \left(b\rightarrow STOP\right)\right)=\left\{\left(\langle \rangle ,\left\{a\right\}\right),\left(\langle \rangle ,\left\{b\right\}\right),\left(\langle a\rangle ,\left\{a,b\right\}\right),\left(\langle b\rangle ,\left\{a,b\right\}\right)\right\}$

失敗/発散モデルは、失敗モデルを発散（divergence）を扱えるよう拡張したものである。失敗/発散モデルにおけるプロセスは $\left(failures_{\perp }\left(P\right),divergences\left(P\right)\right)$ という対で表され、 $divergences\left(P\right)$ は発散を生じさせる全トレースの集合である。また、 $failures_{\perp }\left(P\right)=failures\left(P\right)\cup \left\{\left(s,X\right)\vert s\in divergences\left(P\right)\right\}$ が成り立つ。

応用

初期の重要なCSPの応用例として、INMOS T9000 トランスピュータの仕様記述と検証に使われた例がある。T9000 は複雑なスーパースケーラ型パイプラインプロセッサであり、大規模マルチプロセッシング可能なように設計されている。CSP はパイプラインの正当性検証と、Virtual Channel Processor というチップ間通信管理機能の検証に使われた^[4]。

ソフトウェア設計におけるCSPの応用は、主に人命に関わるような重要なシステムでなされている。例えば、Bremen Institute for Safe Systems と Daimler-Benz Aerospace は、国際宇宙ステーションで使用予定のシステム（約23,000行のコード）をCSPでモデル化し、デッドロックやライブロックが起きないことを検証した^[11]^[12]。このモデル化と解析によって、通常のソフトウェアテストでは検出が困難な問題をいくつか発見した。同様に Praxis High Integrity Systems でもセキュアなスマートカード認証システム（約100,000行のコード）の開発でCSPを使い、セキュリティとデッドロックが発生しないことの検証を行った。Praxis はシステムの欠陥率が他の同等のシステムよりも低くなったと主張している^[5]。

CSP はメッセージ交換を行う複雑なシステムのモデル化と解析に適しているため、通信プロトコルやセキュリティプロトコルの検証にも応用されてきた。特筆すべき応用例として、Needham-Schroeder 公開鍵認証プロトコルをCSPを使って検証し、未知の脆弱性を発見し、それに対処した新たなプロトコルを開発した例がある^[13]。

ツール

長年に渡って、CSPを使ってシステムを表現することで解析するツールがいくつも生み出されてきた。初期のツールはコンピュータが理解できるCSPの表現もまちまちだったため、ツール間で情報を共有できなかった。しかし最近では Bryan Scattergood の記法 CSP_M^[14] が多くのCSPツールで使われている。CSP_M には操作的意味論の形式定義があり、組み込みの関数型言語が含まれる。

もっとも有名なCSPツールとして Formal Systems Europe Ltd. が開発した商用製品である Failures/Divergence Refinement 2 (FDR2) がある。FDR2 はモデルチェッカとされることが多いが、技術的には改良チェッカである。すなわち、2つのCSPプロセス表現をラベル付き遷移系に変換し、指定された意味論モデル（トレース、失敗、失敗/発散）において、一方がもう一方の改良となっているかを調べる^[15]。

他にも以下のようなCSPツールがある。

ProBE
ARC
Casper

脚注

^ ^a ^b ^c ^d
Roscoe, A. W. (1997年). The Theory and Practice of Concurrency. Prentice Hall. ISBN 0-13-674409-5
- この書籍に関連したリンクはこちらにある。全文は PS形式かPDF形式で Bill Roscoe のこちらのリストからダウンロード可能。
^ INMOS (1995年5月12日). occam 2.1 Reference Manual. SGS-THOMSON Microelectronics Ltd. , INMOS document 72 occ 45 03
^ ^a ^b Hoare, C. A. R. (1978年). “Communicating sequential processes”. Communications of the ACM 21 (8): 666-677. doi:10.1145/359576.359585.
^ ^a ^b Barrett, G. (1995年). “Model checking in practice: The T9000 Virtual Channel Processor”. IEEE Transactions on Software Engineering 21 (2): 69-78. doi:10.1109/32.345823.
^ ^a ^b Hall, A; R. Chapman (2002年). “Correctness by construction: Developing a commercial secure system”. IEEE Software 19 (1): 18-25.
^ Creese, S. (2001年). Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks. D. Phil.. Oxford University.
^ ^a ^b
Hoare, C. A. R.. Communicating Sequential Processes. Prentice Hall. ISBN 0-13-153289-8
- この本はオックスフォード大学コンピュータ研究所の Jim Davis が改版しており、新版は Using CSP というサイトでPDF形式でダウンロード可能。
^ William Clinger (1981年6月). Foundations of Actor Semantics. Mathematics Doctoral Dissertation. MIT.
^ Brookes, Stephen; C. A. R. Hoare and A. W. Roscoe (1984年). “A Theory of Communicating Sequential Processes”. Journal of the ACM 31 (3): 560-599. doi:10.1145/828.833.
^ 計算機科学では、計算が終了しないか、例外的な状態で終了する場合、その計算は発散すると言われる、そうでない場合は収束すると言われる。プロセス計算など、計算が無限に続くことが予想される領域では、計算が生産的でない場合（すなわち、有限の時間内に行動を生み出し続けることができない場合）に、計算が発散すると言われる。
^ Buth, B.; Kouvaras, M.; Peleska, J.; Shi, H. (December 1997). "Deadlock analysis for a fault-tolerant system". Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97). pp. 60–75.
^ Buth, B.; Peleska, J.; Shi, H. (January 1999). "Combining methods for the livelock analysis of a fault-tolerant system". Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98). pp. 124–139.
^ Lowe, G. (1996年). "Breaking and fixing the Needham-Schroeder public-key protocol using FDR". Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer-Verlag. pp. 147–166.
^ Scattergood, J.B. (1998年). The Semantics and Implementation of Machine-Readable CSP. D.Phil.. Oxford University Computing Laboratory.
^ A.W. Roscoe (1994年). Model-checking CSP. In A Classical Mind: essays in Honour of C.A.R. Hoare. Prentice Hall.

外部リンク

WoTUG CSP や Occam のユーザーグループ
Formal Systems Europe, Ltd. CSPツールを開発しており、一部はフリーにダウンロード可能
JCSP CSPのコンセプトをJavaのスレッドAPIに導入した実装
CTJ CSP の Java での実装
C++CSP CSP の C++ での実装
JIBU .NET その他での CSP 実装（商用）
CSP++ CSP による仕様記述から C++ のコードを生成するツール
csp CSP風並行性モデルを記述可能なCommon Lisp用ライブラリ。
VerilogCSP VerilogにCSP風の機能を追加するマクロ

[roscoe-1] Roscoe, A. W. (1997年). The Theory and Practice of Concurrency. Prentice Hall. ISBN 0-13-674409-5
この書籍に関連したリンクはこちらにある。全文は PS形式かPDF形式で Bill Roscoe のこちらのリストからダウンロード可能。

[2] この書籍に関連したリンクはこちらにある。全文は PS形式かPDF形式で Bill Roscoe のこちらのリストからダウンロード可能。

[2] INMOS (1995年5月12日). occam 2.1 Reference Manual. SGS-THOMSON Microelectronics Ltd. , INMOS document 72 occ 45 03

[hoare1978-3] Hoare, C. A. R. (1978年). “Communicating sequential processes”. Communications of the ACM 21 (8): 666-677. doi:10.1145/359576.359585.

[barrett-4] Barrett, G. (1995年). “Model checking in practice: The T9000 Virtual Channel Processor”. IEEE Transactions on Software Engineering 21 (2): 69-78. doi:10.1109/32.345823.

[hall-5] Hall, A; R. Chapman (2002年). “Correctness by construction: Developing a commercial secure system”. IEEE Software 19 (1): 18-25.

[6] Creese, S. (2001年). Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks. D. Phil.. Oxford University.

[hoare-7] Hoare, C. A. R.. Communicating Sequential Processes. Prentice Hall. ISBN 0-13-153289-8
この本はオックスフォード大学コンピュータ研究所の Jim Davis が改版しており、新版は Using CSP というサイトでPDF形式でダウンロード可能。

[9] この本はオックスフォード大学コンピュータ研究所の Jim Davis が改版しており、新版は Using CSP というサイトでPDF形式でダウンロード可能。

[clinger1981-8] William Clinger (1981年6月). Foundations of Actor Semantics. Mathematics Doctoral Dissertation. MIT.

[9] Brookes, Stephen; C. A. R. Hoare and A. W. Roscoe (1984年). “A Theory of Communicating Sequential Processes”. Journal of the ACM 31 (3): 560-599. doi:10.1145/828.833.

[10] 計算機科学では、計算が終了しないか、例外的な状態で終了する場合、その計算は発散すると言われる、そうでない場合は収束すると言われる。プロセス計算など、計算が無限に続くことが予想される領域では、計算が生産的でない場合（すなわち、有限の時間内に行動を生み出し続けることができない場合）に、計算が発散すると言われる。

[11] Buth, B.; Kouvaras, M.; Peleska, J.; Shi, H. (December 1997). "Deadlock analysis for a fault-tolerant system". Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97). pp. 60–75.

[12] Buth, B.; Peleska, J.; Shi, H. (January 1999). "Combining methods for the livelock analysis of a fault-tolerant system". Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98). pp. 124–139.

[13] Lowe, G. (1996年). "Breaking and fixing the Needham-Schroeder public-key protocol using FDR". Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer-Verlag. pp. 147–166.

[14] Scattergood, J.B. (1998年). The Semantics and Implementation of Machine-Readable CSP. D.Phil.. Oxford University Computing Laboratory.

[15] A.W. Roscoe (1994年). Model-checking CSP. In A Classical Mind: essays in Honour of C.A.R. Hoare. Prentice Hall.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

Communicating Sequential Processes

歴史

概要

プリミティブ

代数演算子

例

形式的定義

構文

形式意味論

表示的意味論

応用

ツール

関連する形式手法

関連項目

脚注

外部リンク