適応的並列計算を支援する プロトコルの設計と正当性の証明 電子情報工学科 近山・田浦研究室 関谷岳史 背景 • 長時間を要する分散計算 – CPU/ネットワーク負荷の変化 – 利用可能資源の増減 • 資源の効率的な利用のためには、計算 中にプロセスを参加・脱退させたい 適応的並列計算の必要性 適応的並列計算 • 正しく記述・実装するのが 困難 – プロセスの脱退によるメッ セージの喪失が起き得る （図） – 同時に複数のプロセスが脱 退する場合はさらに複雑 • 実用的には単純なモデル・ 接続のトポロジーで実装 – 複数プロセスの脱退であれ ば、中央サーバが調停して 脱退を順次行うなど 本研究の目的 • 「安全な」脱退を支援するプロトコルの設 計 – 任意のトポロジー – 任意の時点で脱退を希望可能 – メッセージが喪失・複製することがない • そのプロトコルのフォーマルな証明 • 動作確認・性能評価のための実装 発表の流れ • • • • • 関連研究 問題設定 提案するプロトコル 実装と評価 まとめ 関連研究 適応に対するアプローチ 1. 単純なモデルでメッセージが通信路にない瞬間に脱 退するもの – – クライアント・サーバモデル(Ninf [Sato et al. 1997]など) バリア同期をとって脱退 ([松原 et al. 2003]など) メッセージの喪失を許容するもの 2. – – → 分散Cilk [Robert et al.1997] P2P通信システム (Tapestry [Ben et al. 2000]など) それらに対して本研究では – – – 非同期メッセージパッシングシステム 接続トポロジーを制限しない・各プロセスが自律的に脱退で きる 故障がない限りメッセージを失うことがない 問題設定 • 仮定 – 通信路はFIFO・故障なし・双方向リンク – プロセスは脱退を完了する前までは任意の時点で メッセージを生産し、送信する – プロセスは脱退を完了する前までは受け取ったメッ セージを消費または転送する – 参加プロセス間のトポロジーが変化しない – 脱退を希望していないプロセスの集合がなすグラフ は連結 • プロトコルの満たすべきこと – メッセージが喪失・複製しない – 脱退を希望したプロセスは有限ステップで脱退を完 了できる 提案プロトコルの概要 • 安全に脱退するには – 脱退直前のプロセス宛に通信路中をメッセージが飛 行していない – 脱退後のプロセス中にメッセージが取り残されない • プロトコルの基本方針 – プロトコルメッセージ＋ポート（通信チャネルの端点） の状態変化 – 脱退を希望するプロセス宛にメッセージが来ないよ うにする – メッセージが取り残されないよう、転送できる隣接プ ロセスを見つける プロトコルの流れ n p ACK NMS n p NMS n n h h h n ACK ACK n p NMS n : normal h : half close p : parent c : child l : closed • ポートの状態はnormal で初期化 • 脱退を希望するとまわ りにNMS (send no more)を送り、ポートの 状態をhalf_closeにす る • NMSを受け取るとポー トの状態をparentにして ACKを返す プロトコルの流れ pl ACK ACK p ACK pl h h cl hl p ACK ACK pl ACK n : normal h : half close p : parent c : child l : closed • ひとつACKを受け取る と、ポートの状態をchild にして、他のチャネルに ACKを送り、ポートの状 態をparentにする • parentのポートにACK を受け取るとポートの状 態をclosedにする • 残ったプロセスにACK を送り状態をclosedに する 提案プロトコルによる脱退の例(1) 開始前 提案プロトコルによる脱退の例(2) 1プロセス以外が脱退を開始 脱退したい 脱退したい 脱退したい 脱退したい 脱退したい 脱退したい 脱退したい 脱退したい 脱退したい 脱退したい 提案プロトコルによる脱退の例(3) NMSを隣接プロセスに送信 提案プロトコルによる脱退の例(4) 脱退しないプロセスはACKを返す 提案プロトコルによる脱退の例(5) ACKを受信したら他のプロセスにACK送信 提案プロトコルによる脱退の例(6) 木構造の葉のほうから順に脱退 プロトコルの記述 Event user send: ∃p ∈ P (p.state = normal or half close or child) ⇒ m := new message p.send(DATA(m)) Event want to leave: leave = 0 and ∀p ∈ P ( p.state = normal or closed) ⇒ leave := 1 forall p ∈ P such that p.state = normal: p.send(NMS) p.state := half close Event user receive: received(DATA(m)) from p ⇒ if leave = 0: deliver DATA(m) to user else: add DATA(m) to M Event forwarding: M is not empty and ∃p ∈ P (p.state = normal or half close or child) ⇒ pop DATA(m) from M p.send(DATA(m)) Event receive NMS: received(NMS) from p ⇒ if p.state = normal: p.send(ACK) p.state := parent Event receive ACK: received(ACK) from p ⇒ if p.state = half close: p.state := child forall q ∈ P such that q.state = half close: q.send(ACK) q.state := parent else if p.state = parent: p.state := closed Event finish leaving: M is empty and ∃p ∈ P (p.state = child (others are closed)) ⇒ p.send(ACK) p.state := closed 正当性の証明の概要 • メッセージが喪失しない(Safety) – アルゴリズムを追っていくことで証明 • 希望したプロセスはいつか脱退できる (Progress) – 不変条件(A),(B)が成り立つことを証明 – チャネルの状態変化がいずれ進行し、完了 することを示す 不変条件 F parent->childの有 向エッジの集合 D parent->half_close の有向エッジの集 合 n n p NMS c h c p p c ACK pp ACK ACK 不変条件 A) Fはforestをなす B) F+Dはdagをなす n : normal h : half close p : parent c : child p c p h h ACK h 実装と動作確認・性能評価 • TCPを用いた通信ライブラリとして実装 • 動作の様子のデモ – 実験環境:情報理工istbsクラスタ – ノード数190中128ノードが脱退 – 実験結果のログをjava Appletを用いて表示 脱退に要する時間の評価 0.8 0.7 • 実験環境 順次脱退プロトコル 0.5 time(sec) – istbsクラスタ – 190ノード×2プロセス – プロセス数分のメッセージ が転送され続ける – 同時に複数ノード脱退 0.6 0.4 0.3 0.2 提案プロトコル 0.1 0 0 20 40 60 80 脱退したノード数 • 順次脱退プロトコルとの比較実験 – 順次脱退プロトコルでは線形に時間が増加 – 提案プロトコルでは比較的増加がゆるやか 100 120 140 まとめと課題 • 安全な脱退を支援するプロトコルの設計・ 正当性の証明 – 任意のトポロジー・任意のプロセスが脱退す るモデル – ほぼ自律的な脱退が可能 • 今後の課題 – プロセスの参加に対応 – ルーティング
© Copyright 2024 ExpyDoc
