Think Stitch
  最近の更新


CSP (Communicating Sequential Processes) の紹介資料

並行システムの理論 CSP (Communicating Sequential Processes) についての紹介資料を作成しました.並行システムの開発でポイントになる概念,逐次システムとの対比,CSP 理論の概要,検証手法とツールの紹介からなります.

2016/11/19 に行われた「静的コード解析の会 第0回」で発表しました.

ビデオを撮っていただいたのですが,残念ながら音声がうまくとれなかったようです.再度紹介する機会があれば撮り直したいと思いますが...

Q & A

静的コード解析の会 第0回 でいただいた質問(一部)

並行合成とはなんですか

相互作用する2つ以上のプロセスを並行に動作させると,それ全体が1つのプロセスとして見えます.この全体としてのプロセスを得る理論的な操作を並行合成といいます.

2つの状態遷移系 A, B があるとして,これを並行に動作させるとします.A の状態を a,B の状態を b とすると,合成した全体としての系の状態は各部分状態系 A, B の状態のペア (a, b) と考えることができます.ここから A, B が持つ遷移をたどることで,合成系の遷移を求めることができ,結果は1つの状態遷移系になるわけです.もし A の遷移が B とは独立の起こるのであれば (a, b) -> (a', b) と遷移し,同時に起こる,つまり相互作用があるときは (a, b) -> (a', b') と遷移します.(元気のあるときに図式説明を資料に追加しようと思います)

同期的相互作用の場合は,ここでいう並行合成のことを同期積(synchronized product)ということもあります.

イベントのスコープはグローバルですか

イベントそのものの名前はモデル全体がスコープとなるので,その意味でグローバルです.システムを構成するコンポーネント(サブプロセス)群の中でだけスコープを切りたい場合は隠蔽演算子を使います.

一方,今回紹介はしませんでしたが,CSP の実行系では局所的なイベントやチャネルを生成できるものが多いと思います.理論的には隠蔽とほぼ同じ意味を表すことになります(少し違うところがあるのですが,込み入った話なので省略します).

2つのプロセスが同じイベントを提示しているときに同期する場合としない場合があるのはなぜですか

2つのプロセスを並行合成したときに,あるイベント e で同期するかどうかは,並行合成演算子で指定するイベントの集合に e が含まれているかどうかで決まります.含まれている場合は同期します.含まれていない場合は同期せず,それぞれが独立して e を出せることになります.これをインターリーブ結合ということがあります.

例えばなんらかのサービスを提供しているプロセス M と,そのクライアント P, Q があるとします.インターリーブ結合を使うと,プロセス M が提供しているサービスのためのイベント(インタフェイス)を,クライアントを区別しない抽象的なものとしてモデル化することができます.P と Q を並行合成する際にはイベント集合を空集合にして,その合成結果とサービスプロセス M をインタフェイスを指定して並行合成します.

イベントの送信と受信の区別はないのですか

理論としては相互作用は対称なので,送受信の区別はありません.イベント同期とそれによる選択があるだけです.

しかしモデル化する問題領域では送受信の区別があることも多いですから,糖衣構文として送受信が用意されています.便宜上,1つのイベントだけを提示することを送信,複数のイベントを選択の形で待つことを受信としているだけです.したがって原理的には送信どうし,受信どうしで同期することも可能です.

例えば2つのプロセスがどちらも2つのイベント a, b を提示している場合は,どちらも受信とみなすことができます.どちらが発生するかは非決定的になります.

はじめはちょっととっつくにくく感じられるかもしれませんが,モデルを書いているうちにこの方が楽だとわかってきます.実際,対称性の高いモデルを書く場合は,逆に送受信の区別がある理論の方が煩わしく感じます.無理に送受信を決めなければならないからです.

加えて,CSP ではマルチ同期といって3つ以上のプロセスが1つのイベントで同時に遷移することが可能です.この場合もどれが送信でどれが受信ということにはあまり意味がありません.対称に扱う方が明快です.

3つの意味論の中でもっともよく使われているものはどれですか

どれがよく使われているかはわかりませんが,検証との関係でいうと以下のようになると思います:

詳細化検査ツールで状態数が無限にあるシステムを検査できますか

できません.状態数が有限の場合だけです.それも規模が大きいものはメモリや外部記憶に入りきらないので検査できません.

3本線の演算子 P ||| Q はどういう意味ですか

並行合成において,イベントの集合として空集合を指定した場合の省略形です.つまり合成するプロセスは相互作用を行わないということです.状態遷移の言葉でいえば,それぞれの遷移が独立して発生し,同時に発生する(同期する)ことはないということです.インターリーブ合成(結合)ともいいます.

コンポーネントの1つがブラックボックスだったとしても検証できますか

コンポーネントの振る舞いを仮定してモデル化できるならば検証できます.

少し話はずれますが,既存のコンポーネントやオペレーティングシステムが提供しているサービスの振る舞いはいつでも厳密にわかっているわけでないので,その場合はマニュアル等から振る舞いをモデル化して使うことになります.これは人間がマニュアルを読んで理解して使うのと同じですね.

ソースコードがある場合は,それを抽象化してモデル化することもあります.これをリバースモデリングと呼ぶことがあります.UML 系のツールなどはあると聞いていますが,CSP のツールがあるかどうかは知りません.一般の相互作用から自動的にリバースモデルを作るのはとても難しいと思います.

ついでにもう1つ脱線させてください.コンポーネントが行うある仕事を考えたとき,もっとも一般的な仕様というのを想像することができます.例えばマニュアルを読むときちんと細かいところまで書いていないことがあります.実装がある場合は実験をすることもありますが,その結果に依存して作ることが危険なことはいうまでもありません.その場合はいくつかある選択肢のうちどれが実装されているのかを非決定的にモデル化します.これが一般的な仕様といったものです.これに基づいて検証を行えば,実装がどのようなものであっても想定している範囲内にあれば正しく振る舞うシステムが得られることになります.つまりブラックボックスを扱う場合は,非決定性を使って未知の部分をモデル化するとよいということです.

master-q さんよりいただいたリスト

https://gist.github.com/master-q/3f461930cb5264f8c6b8b8688d0ff4a2

5ページ目: 口頭で簡単に、domや△のついたイコールなどの数式の意味の説明があると良いと思いました

ここでは仕様も実装も入出力の関係として表しています(表示).\(\mathrm{dom}\,R\) は関係 \(R\) の定義域です.定義は次のとおりです:

\[\mathrm{dom}\ R = \{x \,|\, \exists y. (x, y) \in R\}\]

計算システムの文脈における意味としては,受けつけることが可能な入力の集合ということになります.仕様の場合であれば,実装に対する要求として受けつけなければならない入力の集合,実装の場合は実際に受けつけることが可能な入力の集合ということになります.

したがって

\[\mathrm{dom}\ S \subseteq \mathrm{dom}\ R\]

であるということは,実装が確かに仕様で要求されている範囲の入力を受けつける,という意味になります.これはあとで出てくる並行システムの正当性の条件のうち,活性 (liveness) に対応するものと考えられます.

定義域制限演算子 \(A \triangleleft R\) については資料の方にも定義がありますが,再度書いておきます:

\[A \triangleleft R = \{(x, y) \,|\, x \in A \land (x, y) \in R \}\]

この演算子の使用はあまり本質的なことではなく,単に実装の定義域が仕様の定義域よりも広い場合があるので,はみだしている部分を切り取るためです.そうして仕様の入力範囲にそろえた実装の表示を

\[R' = \mathrm{dom}\ S \triangleleft R\]

とすると,2番目の条件は

\[R' \subseteq S\]

となります.この式の意味は,各入力に対応する出力は仕様が規定する範囲から選ばなければならないということです.たとえば

\[S = \{(0, 0), (1, 2), (2, 4)\}\]

という仕様が与えられた場合,実装は \(1\) に対して \(2\) を返さなければならないということです.これは並行システムの正当性条件のもう1つである安全性 (safety) に対応していると考えられます.

仕様は1つの入力に対して複数の出力を指定する場合があります.これは仕様としての許容を表します.例えば次のような仕様があるとします:

\[S = \{(0, 0), (1, 2), (1, -2), (2, 4)\}\]

この場合,実装は \(1\) に対して \(2\) を返してもよいし \(-2\) を返してもよいという意味になります.実行されるたびに交互に換えてもよいし,ランダムでもよいし,\(2\) に固定しても構わないということです.しかし \(1\) を受けつけないことは許されません.それは1番目の条件に抵触するからです.

このように,実装をするということは非決定性を減らすという意味を含んでいます.同じことが並行システムの正当性にもいえます.

10ページ目: このスライドではCSPは「イベントによる同期型相互作用」のみを扱うと主張しているのでしょうか?

ストレートな答えは YES です.

より正確には,CSP は相互作用のプリミティブとしてイベントによる同期型相互作用を採用している,ということです.その中には,他の実用上重要な相互作用は,イベントによる同期型相互作用で記述(モデル化,シミュレート)可能だという意味が含まれています.しかし今回の資料の中ではそれについては書いていません.例の中にキュー,共有変数,ミューテックス,条件変数,シーケンサ,イベントカウントがあるだけです.

その他の相互作用をプリミティブとして採用することに比べて優れているという主張をしているわけではありません.資料にある相互作用に期待される諸条件を満たすものとして,私はそれしか知らないというだけです.

相互作用プリミティブの選択については Hoare さんの本にも記述があります: "7.3.4 Unbuffered communication", p.222

13ページ目: 「prefix-choice」というのはAの内どれか1つにだけイベント同期を行なうことを表わしているのでしょうか?

そうです.

14ページ目: □演算子を使ってinとSTOPを結合していますが、STOPを単位元とした□演算子のプロセス代数の結合のイメージが実行モデルとして想像できませんでした

質問の意味がわからなかったので,当日お話したいと思います.

ただ,もしかしたら関係するかもしれないと思うことがあります.やや乱暴にいうと,選択演算子が結合しているのは状態ではなくて遷移の束だということです.STOP には遷移がないのでまとめるものがなく変わらないということです.p.13 右下の絵はそういうイメージです.

22ページ目: プロセス代数における再帰定義は必ず不動点になるのですか?通常のプログラミング言語では停止する再帰を書くために混乱しました

正確にいうと,任意の再帰的定義に対して不動点が存在します.CSP の演算子から定義される任意の式に対して,そこから導出される表示の変換関数が単調であることを証明できるからです.

プログラミング言語の意味論については説明できるほど知らないので主観的な感想だけで許していただきたいのですが,再帰的定義の解としての不動点の存在と再帰の停止性は別の問題だと思います.たとえば次のような再帰的定義を考えます:

\[f(x) = \mathbf{if}\ x \ge 0 \ \mathbf{then}\ 0 \ \mathbf{else}\ f(x)\]

この再帰は停止しませんが,不動点としての解は無数にあります.負の入力に対して任意の定義をしてもかまわないからです.ここでも並行システムとの類似性が見て取れます.この定義は発散しているということです.

発散やエラーの扱いにはいくつか流儀があるようなので,これ以上の深入りはやめておきます.

30ページ目: 「構成要素の交換」が成立することは自明ではないように思いました

自明ではありません.単調性が成り立つ理由がみえるような証明の例を Appendix に加えておきました.

35ページ目: 「弱模倣」というはつまり、外部から観測できるイベント列だけを比較してプロセスが同値であることを主張するのでしょうか?これはユニットテストと比較した場合の利点は何でしょうか?

まず細かいところを先に確認させてもらうと,弱模倣は非対称なので同値関係ではありません.この確認の上で「外から観測できるイベント列だけを比較して」は正しいと思います.資料では弱模倣の定義を省略しましたが,検索すればすぐに見つかります.書かない理由は複数の定義があるからです.

後半はよくわからないのですが,弱模倣は単にプロセス間の関係の1定義で,ユニットテストと比較されるものではないと思われます.たとえば弱模倣が成り立つかどうかをユニットテストで確認する,というようなことがいえます.プロセスが2つ必要ですからユニットではないかもしれませんが,模倣される方を仕様と考えればいいのかとも思います.

40ページ目: guardedfun_exは仕様PNfunSpecと実装PNfunImplが等しいことを証明しているのでしょうか?これは同値性の証明なのでしょうか?それとも弱模倣の証明なのでしょうか?

これはプロセスの定義が構成的であることを証明しています.構成的であることの定義は資料では説明していませんが,おおまかにはイベントの発生を経由せずに再帰しないということで,発散していないということに近い感じです.これ以上厳密なことをお知りになりたい場合は,参考文献にある理論を調べる必要があると思います.

ここでこの証明が必要な理由は,次ページにある逆方向の不動点帰納法を使うためです.そのためには不動点が unique でなければならないからです.

全体: 実際のコードとCSPで言う実装を同期させながら開発する方法は何かあるでしょうか?

「同期」が例えば B-method のようにツールが対応関係を管理してくれる手法のことを意味しているのであれば,私は知りません.

そうではなくて,モデルの性質をできるだけ壊さないように実装する,という意味であれば(そうであれば質問にはならないと思うので違うのでしょうけどれども),言語やライブラリの支援があります.

全体: 既存のソフトウェア実装を少しずつCSPで検証するような段階的な手法はあるでしょうか?

検証された範囲を徐々に広げていく,という意味だと解釈しました.違っていたら指摘してください.

対象のシステムがイベントによる同期型の相互作用を基礎にしている場合,実際の実装のリバースモデル化も仕様記述も原理的には可能だと思います.実際に検証できるかというと,ある規模までの部分はできますが,規模が大きくなると,あるところを境にできなくなると思います.実用規模のシステム全体を検証することは不可能でしょう.モデル検査的な手法では状態爆発に対処することができませんし,証明による方法も規模が大きくなれば事実上不可能になってしまうと思います.

抽象化を行うと検証範囲を広げられますが,実実装の検証をしたい場合は関係が切れてしまうので期待しているものではないと思います.部分仕様のセットを用意して検証するという方法が考えられますが,ツールがあるかどうかは知りません.

採用している相互作用がメッセージ通信ならば非同期であったとしても仕様を書けるだろうと推測します.それ以外の相互作用については正当性の定義すら私は知りません.これは CSP の問題ではありません.確かに CSP で記述することはできますが,何をもって正しいとするかは別に決めなければいけません.

将来の可能性としては自動証明を強力にするしかないと個人的には思っています.

全体: 実はCSPはソフトウェアよりもハードウェア記述言語(Verilog,VHDLなど)と相性が良いのでしょうか?

ハードウェア記述言語については私は本を読んだことしかないので正確なことはわかりません.ですが,感想としては似ていると思います.接続のための存在があり,各コンポーネントの振る舞いを記述し,合成するというだけでも似ています.

実際少し検索してみると,HDL と CSP を統合したものや,CSP の影響を強く受けている仕様記述言語 LOTOS の記述を HDL に変換する等の話が見つかりました.

© 2013-2016 PRINCIPIA Limited