食事する哲学者の問題 - TLA+メモ@ウィキ

食事する哲学者の問題

食事する哲学者の問題は、並行性や同期の問題を理解するための古典的な問題でエドガー・ダイクストラによって1965年に提唱された。

問題の設定は次のとおり

5人の哲学者が円形のテーブルを囲んで座っています。彼らの前にはスパゲティの皿があり、哲学者たちの間にはフォークが5本あります。哲学者は次の2つの活動を繰り返します：思索と食事。しかし、食事をするためには、彼の左右のフォークの両方を使う必要があります。

この問題は、すべての哲学者が同時に食事を始めようとすると、各哲学者が左右のフォークを1本ずつしか持てず、食事を始めるためには2本必要なため、デッドロック（行き詰まり）が発生する可能性があることを示す。

モデル

------------------------ MODULE Dining_Philosophers ------------------------
 
EXTENDS Integers, Sequences, TLC
 
(*--algorithm sample {
 (* グローバル変数宣言 *)
 (* フォークの初期状態は置かれた状態 *)
variables forks = [i \in 1..5 |-> "down"];
 
(* プロセス *)
process (philosopher \in 1..5)
(* selfは自身のプロセス番号を示す特別な変数*)
variables left = self, right = (self % 5) + 1;
{
    Thinking:
        skip;
    (* 左のフォークを持つ *)
    PickUpLeft:
        await forks[left] = "down";
        forks[left] := "up";
    (* 右のフォークを持つ *)
    PickUpRight:
        await forks[right] = "down";
        forks[right] := "up";
    Eating:
        skip;
    (* 右、左の順でフォークを置く *)
    PutDownRight:
        forks[right] := "down";
    PutDownLeft:
        forks[left] := "down";
        (* 初期に戻る *)
        goto Thinking;
};
 
}*)
\* BEGIN TRANSLATION
VARIABLES forks, pc, left, right
 
vars == << forks, pc, left, right >>
 
ProcSet == (1..5)
 
Init == (* Global variables *)
        /\ forks = [i \in 1..5 |-> "down"]
        (* Process philosopher *)
        /\ left = [self \in 1..5 |-> self]
        /\ right = [self \in 1..5 |-> (self % 5) + 1]
        /\ pc = [self \in ProcSet |-> "Thinking"]
 
Thinking(self) == /\ pc[self] = "Thinking"
                  /\ TRUE
                  /\ pc' = [pc EXCEPT ![self] = "PickUpLeft"]
                  /\ UNCHANGED << forks, left, right >>
 
PickUpLeft(self) == /\ pc[self] = "PickUpLeft"
                    /\ forks[left[self]] = "down"
                    /\ forks' = [forks EXCEPT ![left[self]] = "up"]
                    /\ pc' = [pc EXCEPT ![self] = "PickUpRight"]
                    /\ UNCHANGED << left, right >>
 
PickUpRight(self) == /\ pc[self] = "PickUpRight"
                     /\ forks[right[self]] = "down"
                     /\ forks' = [forks EXCEPT ![right[self]] = "up"]
                     /\ pc' = [pc EXCEPT ![self] = "Eating"]
                     /\ UNCHANGED << left, right >>
 
Eating(self) == /\ pc[self] = "Eating"
                /\ TRUE
                /\ pc' = [pc EXCEPT ![self] = "PutDownRight"]
                /\ UNCHANGED << forks, left, right >>
 
PutDownRight(self) == /\ pc[self] = "PutDownRight"
                      /\ forks' = [forks EXCEPT ![right[self]] = "down"]
                      /\ pc' = [pc EXCEPT ![self] = "PutDownLeft"]
                      /\ UNCHANGED << left, right >>
 
PutDownLeft(self) == /\ pc[self] = "PutDownLeft"
                     /\ forks' = [forks EXCEPT ![left[self]] = "down"]
                     /\ pc' = [pc EXCEPT ![self] = "Thinking"]
                     /\ UNCHANGED << left, right >>
 
philosopher(self) == Thinking(self) \/ PickUpLeft(self)
                        \/ PickUpRight(self) \/ Eating(self)
                        \/ PutDownRight(self) \/ PutDownLeft(self)
 
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars
 
Next == (\E self \in 1..5: philosopher(self))
           \/ Terminating
 
Spec == Init /\ [][Next]_vars
 
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
 
\* END TRANSLATION
 

解説

このコードは、問題の基本的なモデルでデッドロック（全哲学者が同時にフォークを拾おうとして行き詰まる状態）やリソースの競合（隣接する哲学者が同じフォークを必要とする状態）などの問題を解決する対策は含まれていない。このモデルをモデルチェッカで検査するとデッドロックが検出される。