Communicating_Sequential_Processes

ウィキペディア

Communicating Sequential Processes

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/06/28 04:45 UTC 版)

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種類のプリミティブのクラスを提供する。

イベント

イベントとは、通信あるいは相互作用を意味する。不可分で瞬間的なものと見なされる。不可分名（たとえば、${\displaystyle {\mathit {on}}}$

この節の加筆が望まれています。

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

表示的意味論

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

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

• ${\displaystyle traces\left(STOP\right)=\left\{\langle \rangle \right\}}$
  この節の加筆が望まれています。

  長年に渡って、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

  関連する形式手法

  CSP の影響を受けているその他の形式手法や仕様記述言語として、以下のものがある。

  • Timed CSP, リアルタイムシステム用にタイミング情報を追加したCSP
  • Receptive Process Theory, 非同期（ブロックしない）送信操作を追加したCSP
  • Wright, アーキテクチャ記述言語
  • TCOZ, Timed CSP と Object Z（オブジェクト指向を導入したZ言語）を統合したもの
  • Circus, Z言語 と CSP を統合したもの
  • CspCASL, CASL に CSP を統合したもの

  関連項目

  • Limbo (プログラミング言語) - Inferno オペレーティングシステム内で並行性を実装した言語。CSPに影響を受けている。
  • Plan 9 from Bell Labs - C言語でCSP風の並行性を記述できるスレッドライブラリがある。

  脚注

  1. ^ ^{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 のこちらのリストからダウンロード可能。
  2. ^ INMOS (1995年5月12日). occam 2.1 Reference Manual. SGS-THOMSON Microelectronics Ltd.. http://www.wotug.org/occam/documentation/oc21refman.pdf , INMOS document 72 occ 45 03
  3. ^ ^{a b} Hoare, C. A. R. (1978年). “Communicating sequential processes”. Communications of the ACM 21 (8): 666-677. doi:10.1145/359576.359585. 
  4. ^ ^{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. 
  5. ^ ^{a b} Hall, A; R. Chapman (2002年). “Correctness by construction: Developing a commercial secure system”. IEEE Software 19 (1): 18-25. http://www.anthonyhall.org/c_by_c_secure_system.pdf. 
  6. ^ Creese, S. (2001年). Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks. D. Phil.. Oxford University. 
  7. ^ ^{a b} Hoare, C. A. R.. Communicating Sequential Processes. Prentice Hall. ISBN 0-13-153289-8 
     • この本はオックスフォード大学コンピュータ研究所の Jim Davis が改版しており、新版は Using CSP というサイトでPDF形式でダウンロード可能。
  8. ^ William Clinger (1981年6月). Foundations of Actor Semantics. Mathematics Doctoral Dissertation. MIT. https://dspace.mit.edu/handle/1721.1/6935. 
  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. 

  外部リンク

  • 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風の機能を追加するマクロ