関数型言語による Timed CSP 検証技法の提案 数理情報科学専攻 山川 武志

シングルコアからマルチコアへ シングルコアの問題 マルチコア（プロセッサ） 発熱、消費電力 クロックの限界 高速処理 低消費電力 CORE コンピュータの性能向上にあたって単一CPUのクロックを上げることで・・・ マルチコアでの並列処理に移行 CORE CORE February 5, 2010 Yamakawa Takeshi

並列処理の問題 複数の流れを考慮した設計が必要 デバック＆検証が困難 競合の危険性 デッドロック プロセスA プロセスB プロセスC 複数のプロセッサを協調させて処理させるときに難しさがあって February 5, 2010 Yamakawa Takeshi

形式手法(Formal method) システム開発の課題 システムが複雑になるにつれ、テスト工程が増大 潜在的なバグを持ったまま運用の可能性あり 要求 分析 設計 仕様 実装 テスト・ デバック 運用 保守 設計ミス発覚！ モデル 検証 February 5, 2010 Yamakawa Takeshi

形式手法(Formal method) システム開発の課題 システムが複雑になるにつれ、テスト工程が増大 潜在的なバグを持ったまま運用の可能性あり 要求 分析 設計 仕様 仕様書 自然言語 図、表 形式仕様記述 CSP,VDM B-Method Z記法 モデル 検証 形式手法 設計の工程で仕様記述言語を使用 設計の誤り、曖昧さを早い段階で除去 February 5, 2010 Yamakawa Takeshi

CSP(communicating sequential processes) プロセスはイベント、通信によって状態変化し、その動きは下記の代数演算子によって定義される。 PROC := SKIP (正常終了) | STOP (停止) | ch!v → PROC (output) | ch?x → PROC (input) | PROC ＼ {c} (hiding) | PROC [e1←e2] (renaming) | PROC ; PROC (sequential) | PROC △ PROC (interrupt) | PROC ＞ PROC (untimed timeout) | PROC □ PROC (external choice) | PROC П PROC (internal choice) | PROC ||| PROC (interleaving) | PROC [|c|] PROC (sharing) | PROC || PROC (parallel) | if b then PROC else PROC (boolean) P1 ch1 ch2 P2 P3 February 5, 2010 Yamakawa Takeshi

CSP(communicating sequential processes) プロセスはイベント、通信によって状態変化し、その動きは下記の代数演算子によって定義される。 P1 P2 = ch1!10 → P2’ P1 = (ch1?x → P1’) □ (ch2!3 → SKIP) P3 = ch2?x → if x=0 then SKIP else P3’ P1 || P2 || P3 10 ch1 ch2 P2 P3 Yamakawa Takeshi February 5, 2010

CSP(communicating sequential processes) プロセスはイベント、通信によって状態変化し、その動きは下記の代数演算子によって定義される。 P1’ P2 = ch1!10 → P2’ P1 = (ch1?x → P1’) □ (ch2!3 → SKIP) P3 = ch2?x → if x=0 then SKIP else P3’ P1 || P2 || P3 P1’ || P2’ || P3 10 ch1 ch2 P2’ P3 ch1.10 Yamakawa Takeshi February 5, 2010

プロセスのtrace＆failure CSPで記述したプロセスはtraceやfailureといった集合でとらえられる。 Traces(P) Failures(P) プロセスPのtrace trとその時点で 実行不可能なイベント集合Xの組(tr,X)の集合 P1’ 10 ch1 ch2 P2’ P3 Yamakawa Takeshi February 5, 2010

Verification&Refinement CSPで記述したモデルは仕様を満たしているかどうかを数学的にチェックできる trace refinement（安全性） SPEC P ⇔ Traces(SPEC) ⊇ Traces(P) SPEC P T P2 = ch1!10 → P2’ P1 = (ch1?x → P1’) □ (ch2!3 → SKIP) P3 = ch2?x → if x=0 then SKIP else P3’ P = P1 || P2 || P3 SPEC = ch1.v → ch2.v’ → SPEC P1 10 P2 P3 February 5, 2010 Yamakawa Takeshi

ツールの必要性 利便性や人為的なミスを防ぐためには検証ツールの利用が望ましい。 Design Verification Implementation ✔ OK × failure 利便性や人為的なミスを防ぐためには検証ツールの利用が望ましい。 現在、CSPを拡張した理論であるTimed CSPに関するツールがない。 Timed CSP検証用ツールの開発へ Yamakawa Takeshi February 5, 2010

TIMED CSP TIMED CSPは時間に関する代数演算子をCSPに加え、さらに理論を拡張したものである。 時間を考慮した動作が表現可能であり、各プロセスはイベント、通信、時間によって状態変化する。 3 time PROC := SKIP (正常終了) | STOP (停止) | ch!v → PROC (output) | ch?x → PROC (input) | PROC ＼ {c} (hiding) | PROC [e1←e2] (renaming) | PROC ; PROC (sequential) | PROC △ PROC (interrupt) | PROC ＞ PROC (untimed timeout) | PROC □ PROC (external choice) | PROC П PROC (internal choice) | PROC ||| PROC (interleaving) | PROC [|c|] PROC (sharing) | PROC || PROC (parallel) | if b then PROC else PROC (boolean) P1 WAIT d wait process c@u → P(u) timed event prefix c → P timed prefix P ► Q timeout P △d Q timed interrupt P2 P3 d d Yamakawa Takeshi February 5, 2010

TIMED CSP TIMED CSPは時間に関する代数演算子をCSPに加え、さらに理論を拡張したものである。 時間を考慮した動作が表現可能であり、各プロセスはイベント、通信、時間によって状態変化する。 PROC := SKIP (正常終了) | STOP (停止) | ch!v → PROC (output) | ch?x → PROC (input) | PROC ＼ {c} (hiding) | PROC [e1←e2] (renaming) | PROC ; PROC (sequential) | PROC △ PROC (interrupt) | PROC ＞ PROC (untimed timeout) | PROC □ PROC (external choice) | PROC П PROC (internal choice) | PROC ||| PROC (interleaving) | PROC [|c|] PROC (sharing) | PROC || PROC (parallel) | if b then PROC else PROC (boolean) 5 time P1’ WAIT d wait process c@u → P(u) timed event prefix c → P timed prefix P ► Q timeout P △d Q timed interrupt P2 P3 d d February 5, 2010 Yamakawa Takeshi

TIMED CSP TIMED CSPは時間に関する代数演算子をCSPに加え、さらに理論を拡張したものである。 時間を考慮した動作が表現可能であり、各プロセスはイベント、通信、時間によって状態変化する。 PROC := SKIP (正常終了) | STOP (停止) | ch!v → PROC (output) | ch?x → PROC (input) | PROC ＼ {c} (hiding) | PROC [e1←e2] (renaming) | PROC ; PROC (sequential) | PROC △ PROC (interrupt) | PROC ＞ PROC (untimed timeout) | PROC □ PROC (external choice) | PROC П PROC (internal choice) | PROC ||| PROC (interleaving) | PROC [|c|] PROC (sharing) | PROC || PROC (parallel) | if b then PROC else PROC (boolean) 5 time P1’ WAIT d wait process c@u → P(u) timed event prefix c → P timed prefix P ► Q timeout P △d Q timed interrupt P2 P3’ d d February 5, 2010 Yamakawa Takeshi

Timed CSP Explorerの開発 ツールの開発には関数型言語MLを用いた。 P: event∪time → process P ch.10 P’ P(ch.10) ≡ P’ プロセスはイベントを引数にとりプロセス（関数）を返す関数としてとらえる。 Yamakawa Takeshi February 5, 2010

Timed CSP Explorer構成 コード生成部 CSP検証部 CSP記述を解析し、実行用ML記述を 出力する。 channel in,out:Int P = in?x -> out!fact(x) -> P fact(x) = if x>1 then x*fact(x-1) else 1 ML記述 channel in,out:Int fun P = prefix( input(in,x), prefix( output(out,fact(x)), Recur(P) ) fact(x) = if x>1 then x*fact(x-1) else 1 CSP検証部 February 5, 2010 Yamakawa Takeshi

コード生成部 コンパイラの字句解析、構文解析技術を用いてプロセスの構造を木構造でとらえる。 木を行きがけ順（根→左→右）で探索しながら目的のMLコードを出す。 TEST = out!10 → ( (a → P || b → Q) △t1 c →t2 R ) test = prefix(out.10, tinterrupt( parallel( prefix(a,P), prefix(b,Q) ), Time t1, tprefix(c, Time t2, R ) ) February 5, 2010 Yamakawa Takeshi

CSP検証部 生成部により出力された関数はCSPプロセスの実装になっている。 プロセスに対応した関数にイベントを与えることで、プロセスの振る舞いを検査することができる。 TEST = out!10 → ( (a → P || b → Q) △t1 c →t2 R ) test = prefix(out.10, tinterrupt( parallel( prefix(a,P), prefix(b,Q) ), Time t1, tprefix(c, Time t2, R ) ) February 5, 2010 Yamakawa Takeshi

例 Fischer’s algorithm 相互排他アルゴリズム 共有変数によりenterできるプロセスを唯一に制御 Qi = req.i → read?x → if x≠0 then SKIP else ( write!i → enter.i → exit.i → SKIP ) V(value) = read!value → V(value) [] write?i → V(i) FISCHER = (|||n∈3Qn) || V(0) SPEC = [] n∈3 enter.i → exit.i → SKIP SPEC FISCHER enter.1 enter.2 enter.3 exit.1 exit.2 exit.3 req.1 req.2 req.3 Q1 Q2 Q3 write read write read write read Shared variable V 2 Yamakawa Takeshi February 5, 2010

例 Fischer’s algorithm 相互排他アルゴリズム 共有変数によりenterできるプロセスを唯一に制御 Qi = req.i → read?x → if x≠0 then SKIP else ( write!i → enter.i → exit.i → SKIP V(value) = read!value → V(value) [] write?i → V(i) FISCHER = (|||n∈3Qn) || V(0) SPEC = [] n∈3 enter.i → exit.i → SKIP SPEC FISCHER enter.1 enter.2 enter.3 exit.1 exit.2 exit.3 req.1 req.2 req.3 Q1 Q2 Q3 write read write read write read Yamakawa Takeshi February 5, 2010

例 Fischer’s algorithm 相互排他アルゴリズム 共有変数によりenterできるプロセスを唯一に制御 Qi = req.i → read?x → if x≠0 then SKIP else ( write!i →ε read?y → if y≠i then SKIP else enter.i → exit.i → write!0 → SKIP ) ►δ STOP V(value) = read!value → V(value) [] write?i → V(i) FISCHER = (|||n∈3Qn) || V(0) SPEC = [] n∈3 enter.i → exit.i → SKIP SPEC FISCHER enter.1 enter.2 enter.3 exit.1 exit.2 exit.3 req.1 req.2 req.3 Q1 Q2 Q3 1 1 write read write read write read 1 2 February 5, 2010 Yamakawa Takeshi

まとめ 研究結果 関数型言語の利点をいかすことでCSPのプロセスを簡潔に実装できることを示したうえで、Timed CSPプロセスの実装を行った。 自動検証ツールTimed CSP Explorerを試作しそれを用いて排他制御アルゴリズムの検証を行った。 今後 リアルタイムシステムの設計、検証に応用していく。 大規模システムに耐えうる状態圧縮のアルゴリズムの考案とその実装を行う。 Yamakawa Takeshi February 5, 2010