LTSA(3) 哲学者問題
LTSAの紹介３回目ということで、食事をする哲学者の問題を扱いたいと思います。
食事をする哲学者の問題は、並行システムが語られる際によく使われる例題となります。哲学者の問題をざっと説明します。
スパゲティが置かれたテーブルに、５人の哲学者が座っています。哲学者の横にはそれぞれフォークが置いてあります。
哲学者は、いつもは考え事をしているのですが、時々思いついたようにフォークを両手に取り、スパゲティを食べます。
哲学者は、横にある二つのフォークを使ってスパゲティを食べます。ですので、食事中の哲学者の隣に座る二人の哲学者は、すでにフォークを利用されているため、スパゲティを食べたくても食べられません。
それでも、食事中の哲学者がスパゲティを食べ終わり、フォークを元の場所に置けば、二人ともまた食べられるようになります。
さてここで、一つの制約を設けます。哲学者は１ステップにつき一つのフォークしか手に取ることができないものとします。
ですので、哲学者が食事を取るためには、２ステップ必要ということです。
このような制約があるとき、いかなる時でも常に哲学者が食事を取り続けることができるようにするためには、どのようにすればよいかというのが、哲学者の問題となります。
さて、まずは哲学者についてモデリングを行います。
哲学者は、
- 考える
- 右のフォークを取る
- 左のフォークを取る
- 食べる
- 左のフォークを置く
- 右のフォークを置く
を繰り返すものとします。
RIGHT#GET、LEFT#GET、LEFT#PUT、RIGHT#PUTはそれぞれ、右のフォークを取る、左のフォークを取る、左のフォークを置く、右のフォークを置くということを表現するものとします。
これを、LTSAで表現すると、次のようになります。
P = (thinking -> right.get -> left.get -> eat -> left.put -> right.put -> P).
次に、フォークをモデリングします。これは、特に違和感はないと思います。
これを、LTSAで表現すると、次のようになります。
F = (get -> put -> F).
さてここで、哲学者が二人の場合について、考えてみましょう。
単純に上記の簡単なモデルを足し合わせると、次のようになります。しかし、これでは問題が発生します。
P1 = (thinking -> right.get -> left.get -> eat -> left.put -> right.put -> P1). P2 = (thinking -> right.get -> left.get -> eat -> left.put -> right.put -> P2). F1 = (get -> put -> F1). F2 = (get -> put -> F2).
LTSAでは、同じラベルは同期で実行されます。ですので、P1とP2のthinkingは同時に実行され、right.getもまた同時に実行されます。
今回は、P1とP2のフォークの取得は、同期されるものではありません。ですので、異なるラベルを設定する必要があります。
そこで、P1とP2のラベルについて、それぞれp1とp2をヘッダとして付与します。
P1 = (p1.thinking -> p1.right.get -> p1.left.get -> p1.eat -> p1.left.put -> p1.right.put -> P1). P2 = (p2.thinking -> p2.right.get -> p2.left.get -> p2.eat -> p2.left.put -> p2.right.put -> P2). F1 = (get -> put -> F1). F2 = (get -> put -> F2).
次に、哲学者のフォークの取得アクションと、フォークのイベントを同期させる必要があります。
現在は、F1、F2ともに同期されていません。同期させるために名前を哲学者のp1.right.getなどと同じラベルにする必要があります。
また、フォークはそれぞれ、哲学者１からでも取得できる必要があり、哲学者２からでも取得できる必要があります。
ですので、F1は、P1.right.getと、P2.left.get（哲学者は向かい合わせ）のいずれでもイベントを同期できる必要があります。
また、P1.right.getの後は、P1.right.put、P2.left.getの後は、P2.left.putが呼び出されるようにする必要があります。
LTSAでは、ラベルによる分岐を次のように表現できます。
Branch = ( cond1 -> proc1 -> Branch
| cond2 -> proc2 -> Branch).
このように記述すると、Branchというプロセスは、cond1もしくはcond2のいずれのラベルでも遷移することができます。この記述法を利用すると、先ほどのフォークは次のように記述できます。
F1 = ( p1.right.get -> p1.right.put -> F1
| p2.left.get -> p2.left.get -> F1).
さて、これらを組み合わせると、下記のようになります。
P1 = (p1.thinking -> p1.right.get -> p1.left.get -> p1.eat -> p1.left.put -> p1.right.put -> P1). P2 = (p2.thinking -> p2.right.get -> p2.left.get -> p2.eat -> p2.left.put -> p2.right.put -> P2). F1 = (p1.right.get -> p1.right.put -> F1 | p2.left.get -> p2.left.put -> F1). F2 = (p1.left.get -> p1.left.put -> F2 | p2.right.get -> p2.right.put -> F2).
コンパイルすると、次のような出力が得られます。文面をよく見ると、「DEADLOCK」という単語が出てきています。
Compiled: P1 Compiled: F2 Compiled: F1 Compiled: P2 Composition: DEFAULT = P1 || F2 || F1 || P2 State Space: 6 * 3 * 3 * 6 = 2 ** 10 Composing... potential DEADLOCK −− States: 23 Transitions: 38 Memory used: 5140K Composed in 47ms DEFAULT minimising.. Minimised States: 23 in 15ms
ここで、よく見てみましょう。なんと、下図の赤枠の状態から先の状態が見つかりません。
この状態に遷移するラベルシーケンスを調べてみましょう。調べるためには、ボタン「Check Safety」をクリックします。
すると、次のような出力が得られます。
これは、デッドロックに至るためのラベルシーケンスになります。このシーケンスでは、哲学者１が右のフォークを取り、哲学者２もまた右手のフォークを取ったということになります。
Trace to DEADLOCK: p1.thinking p1.right.get p2.thinking p2.right.get
５人の場合だと、次のようなケースにあたります。
みな全員、右手のフォークを取得し、左手のフォークを取得しようとして誰も取れずに固まってしまった状態です。
このように、LTSAを用いると、簡単にデッドロックが発生するかを確認できます。
さて、デッドロックを解消するにはどうしたらいいでしょうか。
最も簡単な方法は、奇数番目の席に座る哲学者は右手から、偶数番目の席に座る哲学者は左手からフォークを取ることです。
一番上の席を１番目の席とし、時計まわりに２，３，４，５とします。
ここで、１が右手、２が左手、３が右手、４が左手、５が右手という順番に取ろうとすると、次のようになります。
３番目と５番目は、大変残念なことに、フォークを取ることに失敗しています。でも代わりに、１と２と４は、まだ食事をとるチャンスは残されています。
このように、少なくとも先ほどのデッドロックは回避できているかのように見えます。では実際に、先ほどの二人でのモデルを利用して回避できていることを確認してみましょう。
さきほどのLTSA記述について、P2のフォークの取得順序(leftとright)を入れ替えた記述になります。
P1 = (p1.thinking -> p1.right.get -> p1.left.get -> p1.eat -> p1.left.put -> p1.right.put -> P1). P2 = (p2.thinking -> p2.left.get -> p2.right.get -> p2.eat -> p2.right.put -> p2.left.put -> P2). F1 = (p1.right.get -> p1.right.put -> F1 | p2.left.get -> p2.left.put -> F1). F2 = (p1.left.get -> p1.left.put -> F2 | p2.right.get -> p2.right.put -> F2).
無事に、下記のような出力が得られます。
Compiled: P1 Compiled: F2 Compiled: F1 Compiled: P2 Composition: DEFAULT = P1 || F2 || F1 || P2 State Space: 6 * 3 * 3 * 6 = 2 ** 10 Composing... −− States: 20 Transitions: 32 Memory used: 15880K Composed in 16ms DEFAULT minimising.. Minimised States: 20 in 0ms
この場合、たしかにデッドロックが発生していないことがわかりました。
さて、これを５人の場合に拡張してみましょう。
P1 = (p1.thinking -> p1.right.get -> p1.left.get -> p1.eat -> p1.left.put -> p1.right.put -> P1). P2 = (p2.thinking -> p2.left.get -> p2.right.get -> p2.eat -> p2.right.put -> p2.left.put -> P2). P3 = (p3.thinking -> p3.right.get -> p3.left.get -> p3.eat -> p3.left.put -> p3.right.put -> P3). P4 = (p4.thinking -> p4.left.get -> p4.right.get -> p4.eat -> p4.right.put -> p4.left.put -> P4). P5 = (p5.thinking -> p5.right.get -> p5.left.get -> p5.eat -> p5.left.put -> p5.right.put -> P5). F1 = (p1.right.get -> p1.right.put -> F1 | p5.left.get -> p5.left.put -> F1). F2 = (p1.left.get -> p1.left.put -> F2 | p2.right.get -> p2.right.put -> F2). F3 = (p3.right.get -> p3.right.put -> F3 | p2.left.get -> p2.left.put -> F3). F4 = (p3.left.get -> p3.left.put -> F4 | p4.right.get -> p4.right.put -> F4). F5 = (p5.right.get -> p5.right.put -> F5 | p4.left.get -> p4.left.put -> F5).
たぶん、これで大丈夫だと思いますｗ
コンパイルすると、次のような結果が得られます。
Compiled: P1 Compiled: F5 Compiled: F4 Compiled: F3 Compiled: F2 Compiled: F1 Compiled: P5 Compiled: P4 Compiled: P3 Compiled: P2 Composition: DEFAULT = P1 || F5 || F4 || F3 || F2 || F1 || P5 || P4 || P3 || P2 State Space: 6 * 3 * 3 * 3 * 3 * 3 * 6 * 6 * 6 * 6 = 2 ** 25 Composing... −− States: 1856 Transitions: 7408 Memory used: 6187K Composed in 85ms DEFAULT minimising.... Minimised States: 1856 in 222ms
あと、画像は表示できません。LTSA的な限界です。
デッドロックが発生していないので、問題なさそうです。
さて、上記のLTSA記述、本当に正しいかどうかが良く分からないですよね。余談ですが、形式的検証技術の最大の欠点は、テストできないコードが多すぎて、そのコードが機能的に妥当かどうかの判断が難しいところなんです。やっぱり、プログラムとして動作させてみて、しかも形式的に検証できるというのが最強だと思うんですよ。
さて、そんな話はともかく、今回むりくり５人に拡張しましたが、次回は、もっとスマートな方法で拡張したいと思います。
直感的に正しい記述かどうかを判断できるような方法で書き変えたいと思います。
