CSPとはCommunicating Sequential Processesの訳でOxford大学のTony Hoareが1979年に考案したもので、並列処理で必要とされる基本的な動作を記述するプロセス代数です。詳しくはWikiのサイトに記載されています。CSPモデルに基づく並列処理プログラミング言語occamは1980年代初めに考案され、ハードウェアとしてTransputerが作られました。Transputerが無くなった今でも、occamの思想はC,C#,C++,Java,Haskell,Python, Handel-C, XCなど多くのプログラミング言語にCSPモデルがライブラリとして準備されました。従って通常のプログラミング環境でもCSPモデルの恩恵を受ける事ができます。
CSP/occamのプロセスモデルは以下の様に表わす事ができます。丸い印がプロセス、矢印が通信チャネルを表わします。メッセージ交換とプロセスの相互作用によって並列動作が実現されます。つまりイベント駆動の仕組みになります。CSPモデルには代数的法則があり、プロセスの動作はその代数的法則に沿った動きをします。マルチスレッドのように共有メモリを排他的にアクセスする手法では無いので、安全で確実な結果が得られます。
CSPモデルはハードウェア、OS、ミドルウェア、プログラミング言語、アプリケーションと幅広い分野に適応されています。
| 正常終了 | SKIP |
| 停止 | STOP |
| 代入 | Var := Exp |
| チャネル入力 | CHAN ? Var |
| チャネル出力 | CHAN ! Exp |
| 逐次処理 | SEQ(P0, ..., Pn) |
| 条件 | IF((b0, P0), ...(bn,Pn)) |
| ループ | WHILE(b, P) |
| 選択 | CASE e (e1 P1, e2 P2, ..., ELSE Pn ) |
| 並列処理 | PAR(P0, ..., Pn) |
| プロセス選択 | ALT((g0, P0), ...(gn, Pn)) |
| 優先度 | PRI(P1, P2, .., Pn) |
| タイマー | TIMER ? tim , TIMER ? AFTER tim |
| 他 |
【何故必要とされているのか？】
CSPモデルが必要とされる背景には幾つかの理由があります。以下に代表的な理由を記します。
- C/C++/Javaのような逐次処理プログラミング技法では複雑でリアルタイム性の高い並列処理（特に入出力）、更に割り込み処理にイベント駆動、時間駆動等を実現するには非常に難しい。
- POSIX Threadによるマルチスレッド並列プログラミングは排他制御をするために各スレッドはメモリー間で競合が生じ、異なった結果を発生させる。
- マルチコアでサポートされているOpenMPはFortranの流れを受け継いでおり、組み込みシステムで必要とされる機能が十分でない。
- 形式手法は大きな関心ではあるが、大半のモデル検証ツールとプログラミング言語(C/C++/Javaなど)の間に大きなギャップがあり、効果は少ない。
とりわけ、マルチスレッドによる誤動作はシステム設計に大きな問題となっている。マルチスレッドの問題点は1997年頃にCSP/occamコミュニティがIEEE Editorに潜在的な問題点に関して警告している。しかしビジネス優先であり問題解決は放置されたままである。安全性の高いプログラミングを実現するためには、こういった問題点を回避する事にあります。
【他の形式手法ツールとの関係】
安全なシステム設計を実現するにあたり、形式手法は産業界の大きな関心事です。形式手法のツールは(Z, B, VDMなど)数多くありますが、これらは仕様記述言語であります。これに対してCSPは動的な振る舞いのモデリングに有効です。多くの論文にはCSPモデルと異なった形式手法の融合が報告されています(CSP-Z, CSP-OZ, TCOS, B+CSP, CSP+VDM, LOTOS, HOL-CSP, CSP-Isabelle, RT-CSP, CSP-OZ-DC, CSP-LTLなど)。従ってCSPモデルは広範囲のモデルに適応する事ができます。設計方法も上位設計から実装まで直結しています。
【関連団体】
【CSPに関連するプロジェクト、教育】
- UK Grand Challenges
- CoSMoS
- Grid-occam Project
- 国立情報学研究所 Top SE講座
【関連するモデル検証ツール】
【関連するサイト】