CSP モデルの優位性 産業技術総合研究所情報技術研究部門磯部祥尚 0:40 第 9 回 CSP 研究会 (2012 年 3 月 17 日 ) 1
講演内容 1. CSPモデルの特徴 CSPモデルとは? 同期型メッセージパッシング通信 イベント駆動 通信相手 ( チャネル ) の自動選択 3. CSPモデルの検証 CSPモデルの記述例 検証ツール 振舞いの等しさ 2. CSPモデルの実装 ライブラリ / 言語 CSPモデルの実装例 ローカル / ネットワークチャネル 4. CSPモデルベース開発 並列プログラミングの難しさ CSPによるモデル化 検証 実装 まとめ 理論 CSP 検証 FDR 実装 JCSP 1:20 2
CSP モデルの特徴 CSPモデルとは? 同期型メッセージパッシング通信 イベント駆動 通信相手 ( チャネル ) の自動選択 1:20 3
CSP モデルとは? CSP モデル : 並行システムを表現する方法のひとつ 並行システムの構造 ( チャネルの接続関係 ) を表現できる 各プロセスの動作 ( 入出力 計算の順序関係 ) を表現できる 各プロセスの動作 並行システムの構造 com1 out1 in?x in s1 s2 out1!x out2!x com2 P3 out2 例 : 6 コア CPU Core i7-980x 2:10 4
CSP モデルの特徴 ( 同期型メッセージパッシング通信 ) CSP モデルはチャネルを用いた同期型メッセージパッシング通信方式を採用 確実に情報が相手に伝わる ( 動作がわかりやすい ) 共有メモリ通信よりも処理が重い 同期型メッセージパッシング通信 共有メモリ通信 com. AM 8:00 共有メモリ AM 8:00 x = AM 8:00 伝言板 AM 8:00 話したメッセージは確実に伝わる ( 不在ならば話せない ) 書いたメッセージが伝わるか不安 ( 読み書きのタイミングが難しい ) 3:40 5
CSP モデルの特徴 ( イベント駆動 ) CSP モデルはイベント駆動を採用 同期型メッセージパッシング通信 + イベント駆動 : 待ちの間の CPU 負荷はかからない 共有メモリ + ポーリング : 定期的に書込みの有無をチェックするため CPU 負荷がかかる イベント駆動 ポーリング com 共有メモリ zzz x = 伝言板 電話が鳴るまでは眠っていてよい 書込みの有無を定期的にチェック ( 何もしないのに忙しい ) 5:00 6
CSP モデルの特徴 ( 通信相手の自動選択 ) CSP モデルは通信可能な相手を自動的に選択して通信可能 P 119 119 P3 受信可能なプロセスを選択して送信する ( 全てが受信不可のときは ひとつが受信可能になるまで送信を延期 ) 代表電話 ( 手の空いている人が受ける ) 6:00 7
CSP モデルの特徴 ( 通信チャネルの自動選択 ) CSP モデルは通信可能なチャネルを自動的に選択 ( 外部選択 ) して通信可能 45892 45892 山田 P 46031 46031 佐藤 受信可能なプロセスが接続されているチャネルを選択して送信する 2 人に同時に電話をかけて出た方とだけ会話する ( このような電話はない?) 7:00 8
CSP モデルの実装 ライブラリ / 言語 実装例 ローカル / ネットワークチャネル 7:00 9
CSP モデルを実装するためのライブラリ / 言語 CSPモデルを実装するためのライブラリやプログラミング言語が公開されている ライブラリ 言語 研究開発元 JCSP Java ケント大学 (QuickStone) C++CSP C++ ケント大学 CHP Haskell ケント大学 PyCSP Python トロムソ大学 & コペンハーゲン大学 Python-CSP Python ウォルバーハンプトン大学 Go 言語 : 2009 年秋にGoogleが発表したプログラミング言語 コンパイル言語のように速く スクリプト言語のように使い易い CSPに基づく並列処理記述が言語レベルで可能 XMOS : 2008 年から XMOS 社が販売しているプロセッサ イベント駆動型マルチスレッドプロセッサ (XS1-G4, 4コア, 32スレッド ) CSPに基づくC 言語風の実装言語 XCによるハードウェア実装 8:40 10
CSP モデルの JCSP(Java) による実装例 Sender, Gate, Receiver から構成される並行システム Gate は Sender のデータを Receiver に転送する 転送の中断と再開を外部から制御できる Gate は input と cntl から通信可能なチャネルを選択して受信する Sender input cntl Sender output Gate disp Receiver start stop 20 秒ごとに転送の中断と再開を繰り返すと CPU 負荷は下記のようになる 20 秒 転送を中断中の CPU 負荷は 0 10:30, 11:30 11
ローカルチャネルとネットワークチャネル JCSP(Java) では複数のプロセスを複数の PC で分散実行することも簡単 ローカルチャネル :1 つのプログラム内の複数のプロセスを接続する ネットワークチャネル : 異なるプログラム (PC) 間の複数のプロセスを接続する net1 net2 R1 Q1 Q2 S1 S2 Q3 ローカルチャネルをネットワークチャネルに置き換えるだけで分散化が可能 12:40 12
CSP モデルの検証 CSP モデルの例 検証ツール 振舞いの等しさ 12:40 13
並行システムの CSP モデルの例 CSP では並行システムの構造や動作を 式 で表現する 動作 動作 動作 = in1?x com1! f(x) STOP = in2?x com2! g(x) STOP P3 = com1?x com2?y P (x,y) com2?y com1?x P (x,y) P (x,y) = out! h(x,y) STOP CSP モデル com1?x com2?y 動作 P3 com2?y com1?x P out! h(x,y) 構造 SYS = (( ) [ Com ] P3) \Com 動作 in1?x com1! f(x) 動作 in2?x com2! g(x) in1 in2 com1 com2 構造 P3 SYS out 14:20 Com = { com1, com2 } 14
CSP モデルの検証 CSP では並行システムの動作の等しさを証明できる in1 in2 com1 com2 P3 SYS out in1 in2 SPEC out = in1?x com1! f(x) STOP = in2?x com2! g(x) STOP P3 = com1?x com2?y P (x,y) com2?y com1?x P (x,y) P (x,y) = out! h(x,y) STOP 並行 SYS = (( ) [ Com ] P3) \Com 逐次 SPEC = in1?x in2?y Q(x,y) in2?y in1?x Q(x,y) Q(x,y) = out! h(f(x),g(y)) STOP この例では 下記の等しさを証明できる SYS = SPEC 16:00 15
CSP ベースのモデル検査ツール FDR(Oxford 大学 ) モデル検査ツール FDR を使うと SYS と SPEC の等しさ ( 詳細化関係 ) を自動判定できる = in1?x com1! f(x) STOP = in2?x com2! g(x) STOP 並行 P3 = com1?x com2?y P (x,y) com2?y com1?x P (x,y) P (x,y) = out! h(x,y) STOP SYS = (( ) [ Com ] P3) \Com 入力 SYS = SPEC? FDR 出力 True SPEC = in1?x in2?y Q(x,y) in2?y in1?x Q(x,y) Q(x,y) = out! h(f(x),g(y)) STOP 逐次 assert SYS = SPEC ( 検証項目 ) PAT 16::30 ( シンガポール大学のモデル検査ツール ) 16
CSP ベースの解析ツール CONPASU( 産総研 ) 解析ツール CONPASU を使うと SYS から SPEC ( に近い記述 ) を自動生成できる = in1?x com1! f(x) STOP = in2?x com2! g(x) STOP P3 = com1?x com2?y P (x,y) com2?y com1?x P (x,y) P (x,y) = out! h(x,y) STOP 並行 SYS = (( ) [ Com ] P3) \Com 入力 CONPASU SPEC = in1?x in2?y Q(x,y) in2?y in1?x Q(x,y) Q(x,y) = out! h(f(x),g(y)) STOP 逐次 出力 SYS = SPEC を保証 SYS の記述は比較的機械的に作成できるが SPEC の記述は意外と難しい 17:30 17
CSP モデルの等しさの特徴 CSP の等しさは決定的選択と非決定的選択を区別できる コインを入れた後に 珈琲か紅茶を購入できる自動販売機 珈琲 紅茶 購入者が選ぶ 紅茶決定的 tea VMD coffee coin VMD 珈琲 紅茶 販売機が選ぶ 残念 紅茶が良かった tea coin VMND1 VMND 非決定的 coin VMND2 coffee CSP では VMD VMND ( 注 : 実行トレースだけでは区別できない ) 19:00 18
CSP モデルの等しさの保存 CSP の等しさは合成後も保存される ( 部品単位での検証が可能 ) SEQ = SYS (SEQ [Out] SYS)\Out = (SYS [Out] SYS)\Out in1 in2 P SEQ out = in1 in2 SYS com1 P3 com2 out in1 in2 P SEQ out SYS2 out2 = in1 in2 SYS com1 P3 com2 out SYS2 out2 20:10 19
CSP モデルベース開発 並列プログラミングの難しさ CSP によるモデル化 検証 実装 まとめ 20:10 20
並列プログラミングの難しさ マルチコアシステムでの Java 並行性バグのパターン のウェブサイト (2010.12.21): http://www.ibm.com/developerworks/jp/java/library/j-concurrencybugpatterns/ Java 並行プログラミングにおける間違えやすい様々なバグのパターンとその回避策が紹介されている そのようなプログラムをモデル化して検査することは可能であるが 根本的なところに難しさがある CSP ベースの言語 / ライブラリを使うことで振舞いが明確になり このようなバグも抑えられる また 検証ツールも使える 22:00 21
CSP モデルの検証と実装 並行システムを CSP でモデル化し FDR で検証し JCSP で実装する 理論 CSP 検証 FDR 実装 JCSP Communicating Sequential Processes, Hoare, 1985 プロセス代数 CSP: 並行システムを記述 解析するための理論 モデル検査器 FDR: CSP モデルの詳細化関係を検証するツール Oxford 大学 Formal Systems ( アカデミックライセンスは無料 ) Java ライブラリ JCSP: CSP モデルを Java で実装するためのライブラリ Kent 大学 (2006 年秋からオープンソース ) 23:00 22
モデル化 検証 実装の流れ 並行システムを CSP でモデル化し FDR で検証し JCSP で実装する 逐次システムや仕様 モデル化 CSP モデル SRseq(K) = SendRec(0,0,0,K) SendRec(n,m,i,K) = i<k & disp!send.n SendRec((n+1)%N,m,i+1,K) i>0 & disp!receive.m SendRec(n,(m+1)%N,i-1,K) 検証 FDR スクリプト 並行システム逐次システム検証項目 実行 FDR 並行システムや仕様 モデル化 CSP モデル SRconc = (Sender(0) [ { chan } ] Receiver(0))\{ chan } Sender(n) = disp!send.n Sender'(n) Sender (n) = chan!n Sender((n+1)%N) Receiver(m) = chan?m Receiver'(m) Receiver (m) = disp!receive.m Receiver(m) 実装 JCSP プログラム プロセスの並行 Senderの動作 Receiverの動作 実行 Java 24:00 23
まとめ 並行システムの開発に CSP モデルを利用するありがたみ 設計の視点 設計コストを削減できる 同期チャネルによる通信 ( 例 : タイミング制御が容易 ) 通信相手 ( チャネル ) の自動選択 ( 例 : 複数の入出力処理が容易 ) Sensor1 Sensor2 s1 s2 in1 in2 P out Motor 検証の視点 実装前に不具合を発見できる モデル検査器 FDR, PAT による不具合発見 解析ツールCONAPSU( 開発中 ) による並行動作の可視化 実装の視点 CSP モデルを実装できる CSPモデルベースの言語 / ライブラリ (JCSP, Go, ) による実装 イベント駆動によるCPU 負荷の削減 25:00 24