食事する哲学者の問題

パッケージ製品開発担当の大です。こんにちは。

先日、学生時代の恩師と久しぶりに食事する機会がありました。二人でワイングラスを傾けつつ、マルチコア時代のプログラミングに必要なものとは？みたいなお話を伺ってきました。その中で「食事する哲学者の問題（Dining Philosophers Problem）」の話が出てきました。

5人の哲学者が食事したり、考え事をしたりしている。かれらの前には、真ん中にスパゲッティの入った大きなボールが置かれた丸い食卓がある。その食卓には5枚の皿が置かれ、皿と皿の間にフォークが1本ずつ置かれている。
（中略）
スパゲッティをボールから取って自分の皿によそうには2本のフォークを必要とし、哲学者は一度に1本のフォークしかテーブルから取ることができない。（左右の手で同時に両側にある2本のフォークを取ることはできない、という意味。まずどちらかの側のフォークを取ってから、逆の側のフォークを取る。）哲学者同士は決して会話をしない。このため、5人が左のフォークを手にとって右のフォークが食卓に置かれるのを待つという危険なデッドロック状態が発生する可能性がある。

問題はどのように行動の規律を設定すれば（並行性アルゴリズム）、それぞれの哲学者が飢えずに済むか、すなわち食事と思索を永遠に続けられるか、である。

先生のお話は、「マルチスレッドのプログラムの潜在的な問題を見つけるのは難しいよね、そこでモデルの検査だよ！（PAT使おうぜ！）」という流れだったのですが、私はそれ以前にこの問題を知らなかったので、後日こっそりWikipediaを見ながら実装してみました。

デッドロックするパターン

まずは、Wikipediaの解説にある、デッドロックするパターンです。

• 左のフォークが得られるまで思索して待ち、フォークを取り上げる。
• 右のフォークが得られるまで思索して待ち、フォークを取り上げる。
• 食事する。
• 右のフォークを置く。
• 左のフォークを置く。
• 最初にもどって繰り返す。

Streamの練習がてら、Java8で書いてみました。

/**
 * デッドロックが発生する場合
 */
public class 食事する哲学者の問題 {
    static final int NUM = 5; // 哲学者の数 (=フォークの数)

    public static void main(String[] args) throws InterruptedException, ExecutionException {
        // ログの形式を「[<時:分:秒>] <ロガー名>番目の<呼び出し元> <メッセージ>」にしとく
        System.setProperty("java.util.logging.SimpleFormatter.format", "[%1$tT] %3$s番目の%2$s %5$s%n");

        List<フォーク> fs = Stream.generate(フォーク::new).limit(NUM).collect(Collectors.toList());

        new ForkJoinPool(NUM).submit(() -> {
            IntStream.range(0, NUM).parallel().forEach(i -> {
                フォーク 左 = fs.get(i);
                フォーク 右 = fs.get((i + 1) % NUM);
                Logger logger = Logger.getLogger(String.valueOf(i));
                try {
                    new 哲学者(左, 右, logger).食事();
                } catch (InterruptedException ex) {
                    logger.log(Level.SEVERE, null, ex);
                }
            });
        }).get();
    }
}

class フォーク {
    ReentrantLock lock = new ReentrantLock();

    void 使用する() {
        lock.lock();
    }

    void 解放する() {
        lock.unlock();
    }
}

class 哲学者 {
    static final int NUM_TURNS = 10; // 食事中のスパゲティを食べる回数
    static Random rand = new Random(System.currentTimeMillis());
    Logger logger;
    フォーク 左のフォーク;
    フォーク 右のフォーク;

    哲学者(フォーク 左, フォーク 右, Logger logger) {
        this.左のフォーク = 左;
        this.右のフォーク = 右;
        this.logger = logger;
    }

    void 食事() throws InterruptedException {
        logger.info("開始");
        for (int i = 0; i < NUM_TURNS; i++) {
            logger.log(Level.INFO, "{0}ターン目", i);
            左のフォークをとりあげる();
            右のフォークをとりあげる();
            スパゲティをボウルからよそって食べる();
            右のフォークを置く();
            左のフォークを置く();
        }
        logger.info("終了");
    }

    void 左のフォークをとりあげる() {
        long start = System.currentTimeMillis();
        左のフォーク.使用する();
        long end = System.currentTimeMillis();
        logger.log(Level.INFO, "思索した時間は{0}秒でした", ((end - start) / 1000.0));
    }

    void 右のフォークをとりあげる() {
        long start = System.currentTimeMillis();
        右のフォーク.使用する();
        long end = System.currentTimeMillis();
        logger.log(Level.INFO, "思索した時間は{0}秒でした", ((end - start) / 1000.0));
    }

    void スパゲティをボウルからよそって食べる() throws InterruptedException {
        logger.info("");
        Thread.sleep(1000 + rand.nextInt(1000)); // 適当な時間経過
    }

    void 左のフォークを置く() {
        左のフォーク.解放する();
        logger.info("");
    }

    void 右のフォークを置く() {
        右のフォーク.解放する();
        logger.info("");
    }
}

実行してみると、こんな感じであっけなくデッドロックが発生してプログラムが停止しました。

[15:52:05] 1番目の哲学者 食事 開始
[15:52:05] 1番目の哲学者 食事 0ターン目
[15:52:05] 4番目の哲学者 食事 開始
[15:52:05] 4番目の哲学者 食事 0ターン目
[15:52:05] 4番目の哲学者 左のフォークをとりあげる 思索した時間は0秒でした
[15:52:05] 4番目の哲学者 右のフォークをとりあげる 思索した時間は0秒でした
[15:52:05] 4番目の哲学者 スパゲティをボウルからよそって食べる
[15:52:05] 3番目の哲学者 食事 開始
[15:52:05] 3番目の哲学者 食事 0ターン目
[15:52:05] 3番目の哲学者 左のフォークをとりあげる 思索した時間は0秒でした
[15:52:05] 0番目の哲学者 食事 開始
[15:52:05] 0番目の哲学者 食事 0ターン目
[15:52:05] 2番目の哲学者 食事 開始
[15:52:05] 2番目の哲学者 食事 0ターン目
[15:52:05] 2番目の哲学者 左のフォークをとりあげる 思索した時間は0秒でした
[15:52:05] 1番目の哲学者 左のフォークをとりあげる 思索した時間は0秒でした
[15:52:07] 4番目の哲学者 右のフォークを置く
[15:52:07] 4番目の哲学者 左のフォークを置く
[15:52:07] 4番目の哲学者 食事 1ターン目
[15:52:07] 0番目の哲学者 左のフォークをとりあげる 思索した時間は1.833秒でした
[15:52:07] 3番目の哲学者 右のフォークをとりあげる 思索した時間は1.834秒でした
[15:52:07] 3番目の哲学者 スパゲティをボウルからよそって食べる

（中略）

[15:52:30] 2番目の哲学者 右のフォークをとりあげる 思索した時間は3.795秒でした
[15:52:30] 4番目の哲学者 左のフォークをとりあげる 思索した時間は1.411秒でした
[15:52:30] 2番目の哲学者 スパゲティをボウルからよそって食べる
[15:52:30] 3番目の哲学者 食事 4ターン目
[15:52:31] 2番目の哲学者 右のフォークを置く
[15:52:31] 3番目の哲学者 左のフォークをとりあげる 思索した時間は1.925秒でした
[15:52:31] 1番目の哲学者 右のフォークをとりあげる 思索した時間は4.624秒でした
[15:52:31] 2番目の哲学者 左のフォークを置く
[15:52:31] 2番目の哲学者 食事 4ターン目
[15:52:31] 1番目の哲学者 スパゲティをボウルからよそって食べる
[15:52:33] 1番目の哲学者 右のフォークを置く
[15:52:33] 2番目の哲学者 左のフォークをとりあげる 思索した時間は1.552秒でした
[15:52:33] 0番目の哲学者 右のフォークをとりあげる 思索した時間は4.892秒でした
[15:52:33] 0番目の哲学者 スパゲティをボウルからよそって食べる
[15:52:33] 1番目の哲学者 左のフォークを置く
[15:52:33] 1番目の哲学者 食事 4ターン目
[15:52:34] 0番目の哲学者 右のフォークを置く
[15:52:34] 0番目の哲学者 左のフォークを置く
[15:52:34] 0番目の哲学者 食事 4ターン目
[15:52:34] 4番目の哲学者 右のフォークをとりあげる 思索した時間は4.904秒でした
[15:52:34] 1番目の哲学者 左のフォークをとりあげる 思索した時間は1.423秒でした
[15:52:34] 4番目の哲学者 スパゲティをボウルからよそって食べる
[15:52:36] 4番目の哲学者 右のフォークを置く
[15:52:36] 0番目の哲学者 左のフォークをとりあげる 思索した時間は1.301秒でした
[15:52:36] 3番目の哲学者 右のフォークをとりあげる 思索した時間は4.28秒でした
[15:52:36] 3番目の哲学者 スパゲティをボウルからよそって食べる
[15:52:36] 4番目の哲学者 左のフォークを置く
[15:52:36] 4番目の哲学者 食事 5ターン目
[15:52:37] 3番目の哲学者 右のフォークを置く
[15:52:37] 3番目の哲学者 左のフォークを置く
[15:52:37] 3番目の哲学者 食事 5ターン目
[15:52:37] 3番目の哲学者 左のフォークをとりあげる 思索した時間は0秒でした
[15:52:37] 4番目の哲学者 左のフォークをとりあげる 思索した時間は1.661秒でした

（強制終了）

ログ中のハイライトしている部分が、各哲学者の最後の行動です。全員が左のフォークを持ち、右のフォークが空くのを待ちながら思索し続けるデッドロック状態になっています。

NetBeansのプロファイラで見てみるとこんな感じになりました。

ワーカーのスレッドの紫の部分がスパゲティを食べているところ（実際にはスリープ）で、茶色い部分がフォークをとりあげられるようになるまで思索している部分です（スレッドの番号=哲学者の番号ではないので注意）。

実際には、このプログラムは停止せずに最後まで（このプログラムでは各哲学者がスパゲティを10回食べると食事が終わる）行く場合もあります。停止する場合もバラバラで、開始直後に終了することもあれば、半分以上過ぎてから停止することもあります。そこらへんが「潜在的な問題を見つけることの難しさ」なんだと思います。

ウェイターを配する解法 (Arbitrator solution)

解法のひとつめは、セマフォを使用します。

比較的単純な解法は、食卓にウェイターを配置することでなされる。哲学者らはフォークを手に取る際に必ずウェイターの許可を取ることとする。ウェイターはどのフォークが使われているかを把握しているので、デッドロックを防ぐよう調停することができる。4本のフォークが使用中のとき、最後のフォークを哲学者が要求した場合、ウェイターが許可するのを待つ必要があり、使用中のフォークが解放されるまで許可は与えられない。哲学者が常に右のフォークより先に左のフォークをとる（あるいは逆）よう決めておけば、話は単純化される。ウェイターはセマフォと呼ばれるダイクストラが1965年に導入した概念のように振る舞う。

ハイライトされているところが、デッドロックするパターンのコードに追加／変更された部分です。

/**
 * ウェイターを配置する解法
 */
public class 食事する哲学者の問題 {
    static final int NUM = 5; // 哲学者の数 (=フォークの数)

    public static void main(String[] args) throws InterruptedException, ExecutionException {
        // ログの形式を「[<時:分:秒>] <ロガー名>番目の<呼び出し元> <メッセージ>」にしとく
        System.setProperty("java.util.logging.SimpleFormatter.format", "[%1$tT] %3$s番目の%2$s %5$s%n");

        List<フォーク> fs = Stream.generate(フォーク::new).limit(NUM).collect(Collectors.toList());

        Semaphore ウェイター = new Semaphore(NUM);

        new ForkJoinPool(NUM).submit(() -> {
            IntStream.range(0, NUM).parallel().forEach(i -> {
                フォーク 左 = fs.get(i);
                フォーク 右 = fs.get((i + 1) % NUM);
                Logger logger = Logger.getLogger(String.valueOf(i));
                try {
                    new 哲学者(左, 右, ウェイター, logger).食事();
                } catch (InterruptedException ex) {
                    logger.log(Level.SEVERE, null, ex);
                }
            });
        }).get();
    }
}

class フォーク {
    ReentrantLock lock = new ReentrantLock();

    void 使用する() {
        lock.lock();
    }

    void 解放する() {
        lock.unlock();
    }
}

class 哲学者 {
    static final int NUM_TURNS = 10; // 食事中のスパゲティを食べる回数
    static Random rand = new Random(System.currentTimeMillis());
    Logger logger;
    フォーク 左のフォーク;
    フォーク 右のフォーク;
    Semaphore ウェイター;

    哲学者(フォーク 左, フォーク 右, Semaphore ウェイター, Logger logger) {
        this.左のフォーク = 左;
        this.右のフォーク = 右;
        this.ウェイター = ウェイター;
        this.logger = logger;
    }

    void 食事() throws InterruptedException {
        logger.info("開始");
        for (int i = 0; i < NUM_TURNS; i++) {
            logger.log(Level.INFO, "{0}ターン目", i);
            ウェイターにフォークを使って良いか尋ねる();
            左のフォークをとりあげる();
            右のフォークをとりあげる();
            スパゲティをボウルからよそって食べる();
            右のフォークを置く();
            左のフォークを置く();
            ウェイターにフォークを使い終わったことを告げる();
        }
        logger.info("終了");
    }

    void 左のフォークをとりあげる() {
        long start = System.currentTimeMillis();
        左のフォーク.使用する();
        long end = System.currentTimeMillis();
        logger.log(Level.INFO, "思索した時間は{0}秒でした", ((end - start) / 1000.0));
    }

    void 右のフォークをとりあげる() {
        long start = System.currentTimeMillis();
        右のフォーク.使用する();
        long end = System.currentTimeMillis();
        logger.log(Level.INFO, "思索した時間は{0}秒でした", ((end - start) / 1000.0));
    }

    void スパゲティをボウルからよそって食べる() throws InterruptedException {
        logger.info("");
        Thread.sleep(1000 + rand.nextInt(1000)); // 適当な時間経過
    }

    void 左のフォークを置く() {
        左のフォーク.解放する();
        logger.info("");
    }

    void 右のフォークを置く() {
        右のフォーク.解放する();
        logger.info("");
    }

    void ウェイターにフォークを使って良いか尋ねる() throws InterruptedException {
        ウェイター.acquire(2);
        logger.info("");
    }

    void ウェイターにフォークを使い終わったことを告げる() {
        ウェイター.release(2);
        logger.info("");
    }
}

ログ出力は省略します。プロファイラではこんな感じになりました。

デッドロックするパターンに比べて、効率良く同時に二人づつ食事できているように見えます。

リソース階層を使用する方法 (Resource hierarchy solution)

解法のふたつめは、リソース階層を使用します。

もう1つの単純な解法は、リソース（この場合はフォーク）に半順序を割り当てる方法で、リソースの要求順序は常にリソースの順序の通りに行い、リソース解放はその逆の順序に行う。そして、順序的に無関係なリソースをあるユニットが同時に使うことはないとする。リソース（フォーク）に1から5までの番号を付与し、動作ユニット（哲学者）は常に番号の若い方のフォークを先にとり、それから番号の大きい方のフォークをとる。個々の哲学者がとるフォークの番号は決まっている。そして、フォークを置く場合は番号の大きい方を先に置き、それから番号の若い方のフォークを置く。この場合、5人の哲学者のうち4人が同時に番号の若い方のフォークをとると、番号の一番大きいフォークだけが残ることになり、5番目の哲学者はフォークをとることができない。さらに、その番号が一番大きいフォークをとれる哲学者は1人しかいないため、その哲学者だけが両方のフォークを持って食事できる。彼が食事を終えてフォークを置くとき、まず番号の大きい方から置き、続いて番号の若い方のフォークを置くので、後者のフォークを待っていた哲学者がそのフォークをとって食事を始められるようになる。
この解法はダイクストラが最初に提案したものの1つである。

ハイライトされているところが、デッドロックするパターンのコードに追加／変更された部分です。

/**
 * リソース階層による解法
 */
public class 食事する哲学者の問題 {
    static final int NUM = 5; // 哲学者の数 (=フォークの数)

    public static void main(String[] args) throws InterruptedException, ExecutionException {
        // ログの形式を「[<時:分:秒>] <ロガー名>番目の<呼び出し元> <メッセージ>」にしとく
        System.setProperty("java.util.logging.SimpleFormatter.format", "[%1$tT] %3$s番目の%2$s %5$s%n");

        List<フォーク> fs = Stream.generate(フォーク::new).limit(NUM).collect(Collectors.toList());

        new ForkJoinPool(NUM).submit(() -> {
            IntStream.range(0, NUM).parallel().forEach(i -> {
                フォーク 左 = fs.get(i);
                フォーク 右 = fs.get((i + 1) % NUM);
                Logger logger = Logger.getLogger(String.valueOf(i));
                フォークを使う順番 順番 = i < (i + 1) % NUM ? フォークを使う順番.左から右 : フォークを使う順番.右から左;
                try {
                    new 哲学者(左, 右, 順番, logger).食事();
                } catch (InterruptedException ex) {
                    logger.log(Level.SEVERE, null, ex);
                }
            });
        }).get();
    }
}

enum フォークを使う順番 {

    左から右, 右から左
}

class フォーク {
    ReentrantLock lock = new ReentrantLock();

    void 使用する() {
        lock.lock();
    }

    void 解放する() {
        lock.unlock();
    }
}

class 哲学者 {
    static final int NUM_TURNS = 10; // 食事中のスパゲティを食べる回数
    static Random rand = new Random(System.currentTimeMillis());
    Logger logger;
    フォーク 左のフォーク;
    フォーク 右のフォーク;
    フォークを使う順番 順番;

    哲学者(フォーク 左, フォーク 右, フォークを使う順番 順番, Logger logger) {
        this.左のフォーク = 左;
        this.右のフォーク = 右;
        this.順番 = 順番;
        this.logger = logger;
    }

    void 食事() throws InterruptedException {
        logger.info("開始");
        for (int i = 0; i < NUM_TURNS; i++) {
            logger.log(Level.INFO, "{0}ターン目", i);
            if (this.順番 == フォークを使う順番.左から右) {
                左のフォークをとりあげる();
                右のフォークをとりあげる();
                スパゲティをボウルからよそって食べる();
                右のフォークを置く();
                左のフォークを置く();
            } else {
                右のフォークをとりあげる();
                左のフォークをとりあげる();
                スパゲティをボウルからよそって食べる();
                左のフォークを置く();
                右のフォークを置く();
            }
        }
        logger.info("終了");
    }

    void 左のフォークをとりあげる() {
        long start = System.currentTimeMillis();
        左のフォーク.使用する();
        long end = System.currentTimeMillis();
        logger.log(Level.INFO, "思索した時間は{0}秒でした", ((end - start) / 1000.0));
    }

    void 右のフォークをとりあげる() {
        long start = System.currentTimeMillis();
        右のフォーク.使用する();
        long end = System.currentTimeMillis();
        logger.log(Level.INFO, "思索した時間は{0}秒でした", ((end - start) / 1000.0));
    }

    void スパゲティをボウルからよそって食べる() throws InterruptedException {
        logger.info("");
        Thread.sleep(1000 + rand.nextInt(1000)); // 適当な時間経過
    }

    void 左のフォークを置く() {
        左のフォーク.解放する();
        logger.info("");
    }

    void 右のフォークを置く() {
        右のフォーク.解放する();
        logger.info("");
    }
}

ログ出力は省略します。プロファイラの出力はこんな感になりました。

セマフォを使うパターンに比べて、バランスが悪い気がしますね。

まとめ

Wikipediaに載ってるほかの２つの解法（「モニタを使った解法」と「Chandy/Misraの解法」）はまだ未着手ですが、ひとまずここまで。デッドロックの他にもうひとつ発生し得る問題「リソーススタベーション」も考慮できてません。いずれこれらも考えてみたいと思います。

冒頭で出てきたモデル検査ツールのPATでは、この問題をこんな風に記述するそうです。さっぱりわかりませんが、左下のほうに

assert DiningPhilosophers() deadlock free;

と、「デッドロックするかどうか」を検査しているのがわかります。実際にデモを動かして見せてもらうと、とり得るすべての状態をグラフ化して「デッドロックするよ！」と教えてくれて感心しました。

一般のプログラミング言語でも、FindBugsなどの静的解析ツールみたいな感じで手軽にこういう検査ができるようになると便利ですね。

おまけ

今回はJava 8のStream APIを使用し、parallel()を呼び出すことで手軽に並列化を実現しました。また、Java 7から導入されたForkJoinPoolで並列性レベルを明示的に指定しています。どちらも使用しない場合にどうなるか、ちょっとやってみましょう。

        //new ForkJoinPool(NUM).submit(() -> {
            IntStream.range(0, NUM).forEach(i -> {
                フォーク 左 = fs.get(i);
                フォーク 右 = fs.get((i + 1) % NUM);
                Logger logger = Logger.getLogger(String.valueOf(i));
                try {
                    new 哲学者(左, 右, ウェイター, logger).食事();
                } catch (InterruptedException ex) {
                    logger.log(Level.SEVERE, null, ex);
                }
            });
        //}).get();

ひとりの哲学者が食事し、終わったら次の哲学者が…、と順番に食事をしました。当然デッドロックは発生しませんが待ち時間もないので、思索もせず食べっぱなしですね（笑）

こんどはparallel()のみ指定して、並列性レベルは指定しないでやってみます。

        //new ForkJoinPool(NUM).submit(() -> {
            IntStream.range(0, NUM).parallel().forEach(i -> {
                フォーク 左 = fs.get(i);
                フォーク 右 = fs.get((i + 1) % NUM);
                Logger logger = Logger.getLogger(String.valueOf(i));
                try {
                    new 哲学者(左, 右, ウェイター, logger).食事();
                } catch (InterruptedException ex) {
                    logger.log(Level.SEVERE, null, ex);
                }
            });
        //}).get();

並行して4人が食べたあと、最後に1人が食事をしました。ワーカーは3つで、１人はmainスレッドを使っているみたいですね。ForkJoinPoolのAPIドキュメントによると、デフォルトの並列性レベルはプロセッサ数と同じなのだそうです。Intel Core i5、コア4つのマシンで動作させたので、こういう結果になったのですね。なるほど。