Effective ATS:
食事する哲学者の問題 その2

この記事では、ダイクストラによる有名な問題のわずかな変形の実装を紹介します。 この問題は単純ですが、線形型を使う説得力のある例です。

元の問題

5人の哲学者がテーブルの周りに座っています。 また5つのフォークが、それぞれのフォークが哲学者の左手と別の哲学者の右手の間に配置されるよう、テーブルの上に置かれています。 それぞれの哲学者は次の行動を繰り返します: 考えることと食事をすることです。 食事をするためには、哲学者はまず2つのフォークを獲得する必要があります: 1つは彼の左手にもう1つは彼の右手に持ちます。 食事が終わると、哲学者は獲得した2つのフォークをテーブルの上に置きます: 1つは彼の左手側にもう1つは彼の右手側に。

元の問題に対する変形

元の問題に次のようなひねりを加えます:

フォークを使い終わったら、それは "汚れた" フォークになり、汚れたフォークはトレイに置かなればなりません。 汚れたフォークを洗って、それらをテーブルに戻す掃除人がいます。

連絡するためのチャネル

チャネルは単なる容量固定の共有キューです。 次の2つの関数は与えられたチャネルに対して要素を挿入し、要素を取り出します:
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.dats
ATS ソースコードをコンパイルして実行コードにする Makefile もあります。 しばらくシミュレーションを実行するとデッドロックが発生するはずです。
この記事は Hongwei Xi によって書かれ、 Japan ATS User Group によって翻訳されています。