CSPの紹介

Size: px

Start display at page:

Download "CSPの紹介"

きみのしんこのえ
6 years ago
Views:

1 CSP モデルの優位性産業技術総合研究所情報技術研究部門磯部祥尚 0:40 第 9 回 CSP 研究会 (2012 年 3 月 17 日 ) 1

2 講演内容 1. CSPモデルの特徴 CSPモデルとは? 同期型メッセージパッシング通信イベント駆動通信相手 ( チャネル ) の自動選択 3. CSPモデルの検証 CSPモデルの記述例検証ツール振舞いの等しさ 2. CSPモデルの実装ライブラリ / 言語 CSPモデルの実装例ローカル / ネットワークチャネル 4. CSPモデルベース開発並列プログラミングの難しさ CSPによるモデル化検証実装まとめ理論 CSP 検証 FDR 実装 JCSP 1:20 2

3 CSP モデルの特徴 CSPモデルとは? 同期型メッセージパッシング通信イベント駆動通信相手 ( チャネル ) の自動選択 1:20 3

4 CSP モデルとは? CSP モデル : 並行システムを表現する方法のひとつ並行システムの構造 ( チャネルの接続関係 ) を表現できる各プロセスの動作 ( 入出力計算の順序関係 ) を表現できる各プロセスの動作並行システムの構造 com1 out1 in?x in s1 s2 out1!x out2!x com2 P3 out2 例 : 6 コア CPU Core i7-980x 2:10 4

5 CSP モデルの特徴 ( 同期型メッセージパッシング通信 ) CSP モデルはチャネルを用いた同期型メッセージパッシング通信方式を採用確実に情報が相手に伝わる ( 動作がわかりやすい ) 共有メモリ通信よりも処理が重い同期型メッセージパッシング通信共有メモリ通信 com. AM 8:00 共有メモリ AM 8:00 x = AM 8:00 伝言板 AM 8:00 話したメッセージは確実に伝わる ( 不在ならば話せない ) 書いたメッセージが伝わるか不安 ( 読み書きのタイミングが難しい ) 3:40 5

6 CSP モデルの特徴 ( イベント駆動 ) CSP モデルはイベント駆動を採用同期型メッセージパッシング通信 + イベント駆動 : 待ちの間の CPU 負荷はかからない共有メモリ + ポーリング : 定期的に書込みの有無をチェックするため CPU 負荷がかかるイベント駆動ポーリング com 共有メモリ zzz x = 伝言板電話が鳴るまでは眠っていてよい書込みの有無を定期的にチェック ( 何もしないのに忙しい ) 5:00 6

7 CSP モデルの特徴 ( 通信相手の自動選択 ) CSP モデルは通信可能な相手を自動的に選択して通信可能 P P3 受信可能なプロセスを選択して送信する ( 全てが受信不可のときはひとつが受信可能になるまで送信を延期 ) 代表電話 ( 手の空いている人が受ける ) 6:00 7

8 CSP モデルの特徴 ( 通信チャネルの自動選択 ) CSP モデルは通信可能なチャネルを自動的に選択 ( 外部選択 ) して通信可能山田 P 佐藤受信可能なプロセスが接続されているチャネルを選択して送信する 2 人に同時に電話をかけて出た方とだけ会話する ( このような電話はない?) 7:00 8

9 CSP モデルの実装ライブラリ / 言語実装例ローカル / ネットワークチャネル 7:00 9

研究開発元 JCSP Java ケント大学 (QuickStone) C++CSP C++ ケント大学

Python-CSP Python ウォルバーハンプトン大学 Go 言語 : 2009

スクリプト言語のように使い易い CSPに基づく並列処理記述が言語レベルで可能 XMOS : 2008

10 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

11 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

12 ローカルチャネルとネットワークチャネル JCSP(Java) では複数のプロセスを複数の PC で分散実行することも簡単ローカルチャネル :1 つのプログラム内の複数のプロセスを接続するネットワークチャネル : 異なるプログラム (PC) 間の複数のプロセスを接続する net1 net2 R1 Q1 Q2 S1 S2 Q3 ローカルチャネルをネットワークチャネルに置き換えるだけで分散化が可能 12:40 12

13 CSP モデルの検証 CSP モデルの例検証ツール振舞いの等しさ 12:40 13

並行システムの CSP モデルの例 CSP では並行システムの構造や動作を式で表現する

g(x) STOP P3 = com1?x com2?y P (x,y) com2?

h(x,y) STOP CSP モデル com1?x com2?y 動作 P3 com2?

$h(x,y) 構造 SYS = (( ) [ Com ] P3) \Com 動作 in1?$

14 並行システムの 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

15 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 の等しさ (

g(x) STOP 並行 P3 = com1?x com2?y P (x,y) com2?y com1?

$h(x,y) STOP SYS = (( ) [ Com ] P3) \Com 入力 SYS = SPEC?$

16 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

$] P3) \Com 入力 CONPASU SPEC = in1?$ x Q(x,y) Q(x,y) = out!

17 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

18 CSP モデルの等しさの特徴 CSP の等しさは決定的選択と非決定的選択を区別できるコインを入れた後に珈琲か紅茶を購入できる自動販売機珈琲紅茶購入者が選ぶ紅茶決定的 tea VMD coffee coin VMD 珈琲紅茶販売機が選ぶ残念紅茶が良かった tea coin VMND1 VMND 非決定的 coin VMND2 coffee CSP では VMD VMND ( 注 : 実行トレースだけでは区別できない ) 19:00 18

19 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

20 CSP モデルベース開発並列プログラミングの難しさ CSP によるモデル化検証実装まとめ 20:10 20

並列プログラミングの難しさマルチコアシステムでの Java 並行性バグのパターンのウェブサイト (2010.12.21): http://www.ibm.

21 並列プログラミングの難しさマルチコアシステムでの Java 並行性バグのパターンのウェブサイト ( ): Java 並行プログラミングにおける間違えやすい様々なバグのパターンとその回避策が紹介されているそのようなプログラムをモデル化して検査することは可能であるが根本的なところに難しさがある CSP ベースの言語 / ライブラリを使うことで振舞いが明確になりこのようなバグも抑えられるまた検証ツールも使える 22:00 21

22 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) =

n SendRec((n+1)%N,m,i+1,K) i>0 & disp!receive.

$SRconc = (Sender(0) [ { chan } ] Receiver(0))\{ chan } Sender(n) = disp!send.$

23 モデル化検証実装の流れ並行システムを 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

検証の視点実装前に不具合を発見できるモデル検査器 FDR, PAT による不具合発見解析ツールCONAPSU( 開発中 ) による並行動作の可視化

24 まとめ並行システムの開発に CSP モデルを利用するありがたみ設計の視点設計コストを削減できる同期チャネルによる通信 ( 例 : タイミング制御が容易 ) 通信相手 ( チャネル ) の自動選択 ( 例 : 複数の入出力処理が容易 ) Sensor1 Sensor2 s1 s2 in1 in2 P out Motor 検証の視点実装前に不具合を発見できるモデル検査器 FDR, PAT による不具合発見解析ツールCONAPSU( 開発中 ) による並行動作の可視化実装の視点 CSP モデルを実装できる CSPモデルベースの言語 / ライブラリ (JCSP, Go, ) による実装イベント駆動によるCPU 負荷の削減 25:00 24

TopSE並行システムはじめに

TopSE並行システムはじめにはじめに平成 23 年 9 月 1 日トップエスイープロジェクト磯部祥尚 ( 産業技術総合研究所 ) 2 本講座の背景と目標背景 : マルチコア CPU やクラウドコンピューティング等並列 / 分散処理環境が身近なものになっている複数のプロセス ( プログラム ) を同時に実行可能通信等により複数のプロセスが協調可能並行システムの構築並行システム通信 Proc2 プロセス ( プログラム