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

3つの最も際だった ATS の機能は、依存型、線形型、ローカライズ可能なテンプレートです。 この記事では、ダイクストラによる有名な問題である5人の食事する哲学者の問題の実装を紹介しようと思います。 この問題は単純ですが、線形型を使う説得力のある例です。

この問題についての解説

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

リソースを表わす線形型

はじめに、次のような型定義を導入しましょう: 
typedef phil = int
哲学者を表わす型として [int] の代わりに [phil] を使う唯一の目的は、後続のコードをより簡単に表現するためです。

この問題で描写されているフォークは共有リソースです。 次にフォークを表わす線形抽象型を導入しましょう: 

absvt@ype fork = int
この宣言は [fork] はサイズが [int] のサイズに等しいような抽象 viewtype (つまり線形抽象型) であることを意味しています。 [fork] と [int] が同じサイズであるという情報は、型検査が終わって抽象型が具象型で置き換えられるまでは有効ではないことに注意してください。

哲学者が彼の左のフォークを獲得/解放するために、次の関数を呼び出すことができます: 

fun phil_acquire_lfork (n: phil): fork
fun phil_release_lfork (n: phil, f: fork): void
哲学者が彼の右のフォークを獲得/解放するために、次の関数を呼び出すことができます: 
fun phil_acquire_rfork (n: phil): fork
fun phil_release_rfork (n: phil, f: fork): void
フォークは共有リソースなので、フォークの獲得/解放を表わすこれらの関数は一般になんらかのロックメカニズムを必要とします。 フォークが獲得されたら、それを使った後には解放されるべきです。 フォークに線形型を割り当てることで、フォークの経過を追いかけてそれらが適切に扱われていることを保証するために、ATS の型システムを信頼することができます。

ループとして実装された哲学者

この問題の説明に従って、哲学者をシミュレートする次のようなループを実装してみましょう: 
extern
fun phil_loop (n: phil): void
implement
phil_loop (n) = let
  val () = phil_think (n)
  val ((*void*)) = phil_dine (n)
in
  phil_loop (n)
end // end of [phil_loop]
リソースが不要な関数 [phil_think] は次のように実装できます: 
extern
fun phil_think (n: phil): void
implement
phil_think (n) =
(
  randsleep (10) // for sleeping up to 10 secs
)
リソースの獲得と解放を必要とする関数 [phil_dine] は次のように実装できます: 
extern
fun phil_dine (n: phil): void
implement
phil_dine (n) = let
//
  val lf = phil_acquire_lfork (n)
  val () = randsleep (1) // for sleeping up to 1 secs
  val rf = phil_acquire_rfork (n)
//
  val () = randsleep (3) // for sleeping up to 3 secs
//
  val () = phil_release_lfork (n, lf)
  val () = phil_release_rfork (n, rf)
//
in
  // nothing
end // end of [phil_dine]
[lf] と [rf] 両方には線形型 [fork] が割り当てられているので、それらは線形値であることに注意してください。 あらゆる線形値はなんらかの方法で消費もしくは返されなればならないので、呼び出し [phil_release_lfork] (もしくは [phil_release_rfork]) を削除すると型検査でたやすく検出可能な型エラーを引き起こします。 これはリソースを表現する値に線形型を割り当てる大きな利点です。

残りの実装について

もし [phil_loop] を5つのスレッドで動作させるなら、5つのフォークを保護するために (それぞれ1つずつ) 5つの mutex を用いることができます。 また5つのフォークを保護するために1つの mutex を使うこともでき、するとビジーウェイトを回避するためにいくつかの条件変数を導入することになります。 代わりに、ここでの実装は [phil_loop] を (システムコール [fork] によって生成された) 5つのプロセスの上で動作させています。 そしてそれらのプロセスで共有している5つのフォークを格納するメモリを確保するために [mmap] を呼び出します。 フォークを保護するためにファイルシステム下層を用いたロックを生成し、ビジーウェイトを回避するためにランダムな長さのスリープを挿入しています。 この実装のスタイルは主にデモを目的として選択されています。 興味のある読者には、mutex とおそらく条件変数を用いてスレッドに基づいた実装を作ってみることをおすすめします。

テスト

与えられた実装でのそれぞれの哲学者は、はじめに左のフォークを次に右のフォークを取ることに注意してください。 彼ら全員が左手にフォークを持った場合、デッドロックが発生します。 このようなデッドロックを回避する単純な方法は、(5人の中で) 1人の哲学者がまず右のフォークを次に左のフォークを取ることです。

5人の食事する哲学者の問題は、デッドロックとデッドロックの回避に対する学習の導入になりました。 与えられた実装を実行すると、数分の内にデッドロックが発生するのを目にするでしょう。 デッドロックしたプロセスを全て削除するために、どうか [kill] コマンドを使ってください。

この記事は Hongwei Xi によって書かれ、 Japan ATS User Group によって翻訳されています。