フォークを使い終わったら、それは "汚れた" フォークになり、汚れたフォークはトレイに置かなればなりません。 汚れたフォークを洗って、それらをテーブルに戻す掃除人がいます。
fun{a:vt0p} channel_insert (channel (a), a): void fun{a:vt0p} channel_takeout (chan: channel (a)): (a)もし [channel_insert] が満杯のチャネルに呼び出されたら、要素がチャネルから取り出されるまで呼び出し元はブロックします。 もし [channel_takeout] が空のチャネルに呼び出されたら、要素がチャネルに挿入されるまで呼び出し元はブロックします。
fun fork_changet (n: nphil): channel(fork)
このとき型 [nphil] は [natLt(5)] となるように (5未満の自然数となるように) 定義されています。
フォークを保管するチャネルは容量が 2 になるように設定されています。
(それぞれの中に) 大抵1つの要素を保管するチャネルの容量を 2 に設定する理由は、それらのチャネルが決して満杯にならないよう
(満杯になったチャネルによってブロックしてしまったと思われる呼び出し元を起こすためにシグナルを送る必要がないように)
保証するためです。
fun forktray_changet ((*void*)): channel(fork)
チャネルが決して満杯にならないように、このチャネルの容量は (5の代わりに) 6 を設定します
(全部で5つのフォークしかありません)。
implement phil_loop (n) = let // val () = phil_think (n) // val nl = phil_left (n) // = n val nr = phil_right (n) // = (n+1) % 5 // val ch_lfork = fork_changet (nl) val ch_rfork = fork_changet (nr) // val lf = channel_takeout (ch_lfork) val () = println! ("phil_loop(", n, ") picks left fork") // val () = randsleep (2) // sleep up to 2 seconds // val rf = channel_takeout (ch_rfork) val () = println! ("phil_loop(", n, ") picks right fork") // val () = phil_dine (n, lf, rf) // val ch_forktray = forktray_changet () val () = channel_insert (ch_forktray, lf) // left fork to dirty tray val () = channel_insert (ch_forktray, rf) // right fork to dirty tray // in phil_loop (n) end // end of [phil_loop][phil_loop] のコードを追うのは容易でしょう。
implement cleaner_loop () = let // val ch = forktray_changet () val f0 = channel_takeout (ch) // [f0] is dirty // val () = cleaner_wash (f0) // washes dirty [f0] val () = cleaner_return (f0) // puts back cleaned [f0] // in cleaner_loop () end // end of [cleaner_loop]関数 [cleaner_return] はまず与えられたフォークの番号を調べて、それからその番号を使ってそのフォークを保管するためのチャネルを見つけます。 その実際の実装は次のようになります:
implement
cleaner_return (f) =
{
val n = fork_get_num (f)
val ch = fork_changet (n)
val () = channel_insert (ch, f)
}
これで [cleaner_loop] のコードを追うのは容易でしょう。
DiningPhil2.sats DiningPhil2.dats DiningPhil2_fork.dats DiningPhil2_mylib.datsATS ソースコードをコンパイルして実行コードにする Makefile もあります。 しばらくシミュレーションを実行するとデッドロックが発生するはずです。