並列プログラミング言語による Dining Philosophers Problem の検証 大井 謙 数理科学コース 4 年 福永研究室 2010 年 3 月 4 日 ( 木 ) 1.

Presentation on theme: "並列プログラミング言語による Dining Philosophers Problem の検証 大井 謙 数理科学コース 4 年 福永研究室 2010 年 3 月 4 日 ( 木 ) 1."— Presentation transcript:

1 並列プログラミング言語による Dining Philosophers Problem の検証 大井 謙 数理科学コース 4 年 福永研究室 2010 年 3 月 4 日 ( 木 ) 1

2 目次 1. 並列処理について 2. Dining Philosophers Problem 2.1. 問題の概要 2.2. 具体的な解法 2.2.1. Edsger W.Dijkstra による解法 2.2.2. Carel S.Scholten による解法 2.3. 解法についての検証 3. まとめ 2

3 1. 並列処理について 逐次処理と並列処理 – 逐次処理 : 1 つずつ処理を実行 – 並列処理 : 複数の処理を同時に実行 例 試し割りによる 1000 までの素数判 定 3 逐次処理並列処理 試し割り : 判定する数 を 3 ～ √n の整数で順 番に割る方法 n = 1 ~ 1000 n = 1 ~ 500n = 501 ~ 1000 素数 n を出 力 同時に判定 計算時間削減

4 2. Dining Philosophers Problem 2.1. 問題の概要 並列処理の同期問題を一般化した例 発端は 1971 年 Edsger W.Dijkstra の提示 Antony Hoare により一般化される – 互いに会話しない 5 人の哲学者達がいる – 空腹時に座り 自分の両隣のフォークを取る – 要求が満たされないと待ち続ける – 食事に必要なフォークは 2 本 – 片方ずつしか取れない ← ウィキペディア 「食事する哲学者の問 題」の 写真から引用 (http://ja.wikipedia.org/wi ki/ 食事する哲学者の問題 ) 5 台のコンピュータがある これらが 5 台のテープ装置に競合アクセスす る 同期 : 同時並行して動 く処理間で時系列的な 制御をすること 4

5 2. Dining Philosophers Problem 2.1. 問題の概要 哲学者達の振舞い フォークの振舞い 全体の振舞い –PHIL と FORK を並列処理 (5 つずつ 計 10) ← ウィキペディア 「食事する哲学者の問 題」の 写真から引用 (http://ja.wikipedia.org/wi ki/ 食事する哲学者の問題 ) 座る → 食べる → フォーク置く L → フォーク置く R → 立つ → PHIL = ( フォーク取る L → フォーク取る R → PHIL ) FORK = ( R 側 PHIL に取られる → L 側 PHIL に取られる → R 側 PHIL に置かれる → L 側 PHIL に置かれる → or FORK FORK ) 5

6 2. Dining Philosophers Problem 2.1. 問題の概要 何が問題なのか – 全員同時に腹が減ったとき 5 人が同時にフォークを取る その後 もう片方を取ろうとすると･･･ 誰の要求も満たされず 全員が永遠に待ち続け る ← ウィキペディア 「食事する哲学者の問 題」の 写真から引用 (http://ja.wikipedia.org/wi ki/ 食事する哲学者の問題 ) デッド ロック 6

7 2. Dining Philosophers Problem 2.2. 具体的な解法 デッドロックが起こる条件 5 人全員による満たされない要求が円になる 2 つの解法 – 哲学者の挙動を直接書き換える方法  Edsger W.Dijkstra による解 – 外部から哲学者の挙動に制限をかける方法  Carel S.Scholten による解 これを崩せば良 い！ 7

8 2. Dining Philosophers Problem 2.2. 具体的な解法 2.2.1. Edsger W.Dijkstra による解法 ( ※ ) 左利き：左 → 右 の順にフォークを取ると考える 哲学者達の振舞い 利き腕の違う哲学者を用意す る 座る → 食べる → フォーク置く L → フォーク置く R → 立つ → LPHIL = ( フォーク取る L → フォーク取る R → LPHIL ) 座る → 食べる → フォーク置く R → フォーク置く L → 立つ → RPHIL = ( フォーク取る R → フォーク取る L → RPHIL ) 8

9 2. Dining Philosophers Problem 2.2. 具体的な解法 2.2.1. Edsger W.Dijkstra による解法 ← ウィキペディア 「食事する哲学者の問 題」の 写真から引用 (http://ja.wikipedia.org/wi ki/ 食事する哲学者の問題 ) 右 左 左左 左 ステッ プ 01234 9

10 2. Dining Philosophers Problem 2.2. 具体的な解法 2.2.2. Carel S.Scholten による解法 ( ※ ) 召使いは 同時に 4 人以下の哲学者しか座らせない 召使いの振舞い 召使い (Footman) を 1 人 任用す る FOOT(0) = ( 座らせる → FOOT(1) ) FOOT( j ) = ( 座らせる → FOOT( j + 1 ) or 立たせる → FOOT( j - 1 ) ) FOOT(4) = ( 立たせる → FOOT(3) ) ( j ∈ {1, 2, 3} ) 10

11 2. Dining Philosophers Problem 2.2. 具体的な解法 2.2.2. Carel S.Scholten による解法 ← ウィキペディア 「食事する哲学者の問 題」の 写真から引用 (http://ja.wikipedia.org/wi ki/ 食事する哲学者の問題 ) ステッ プ 012 F 11

12 2. Dining Philosophers Problem 2.3. 解法についての検証 設計段階でミスがない事を保証できるか – 哲学者 1 人あたりの状態数は 6 通り – フォーク 1 本あたりの状態数は 3 通り – 哲学者は 5 人 フォークは 5 本 最悪状態数 = 6^5 * 3^5 = 約 190 万 検証ツールの重要性 例 CSP 記述の検証ツール（ PAT ） 手動では非常に困難！ CSP : 並行システムを 形式的に記述し、解析 するための言語 12

13 3. まとめ まとめ – 逐次処理と並列処理を対比した上 で並列処理に潜む問題点を確認 –Dining Philosophers Problem を 解決するための案を 2 つ提示・検 証 – 検証ツールの重要性について考察 13