Effective ATS:
リーダー/ライター問題

一般に、動的なテストが難しい文脈において、ATS はより異彩を放っています。この記事では、並行プログラミングにおける古典的なリーダー/ライター問題の ATS における実装を紹介します。

この問題についての解説

リーダー/ライター問題はデータベースへのアクセスをモデルにしています。プロセスがデータベースからの読み出しをするためには、そのプロセスは読み出しアクセスが許可されなければなりません。プロセスがデーバベースへの書き込みをするためには、そのプロセスは書き込みアクセスが許可されなければなりません。読み出しアクセスと書き込みアクセスを同時に許可することはできません。複数の読み出しアクセスを同時に許可することはできますが、書き込みアクセスは一度に1つだけしか許可できません。

データベースアクセスを表わすインターフェイス

次のコードはデータベースにアクセスするための抽象インターフェイスです:

//
abstype DB = ptr
//
absview DBread_v
absview DBwrite_v
//
fun DBread (pf: !DBread_v | db: DB): void
fun DBwrite (pf: !DBwrite_v | db: DB): void
//

[DBread] を呼び出してデータベースから読み出すためには、(抽象) view [DBread_v] の証明が必要です。 [DBwrite] を呼び出してデータベースに書き込むためには、(抽象) view [DBwrite_v] の証明が必要です。

状態付きデータベース

なんらかの線形状態を共なうデータベースを表わすために、線形抽象型 [DBshell] を導入しましょう:

//
absvtype
DBshell (r: int, w: int) = ptr
//
vtypedef DBshell = [r,w:int] DBshell (r, w)
//

整数 r と w が与えられたとき型 [DBshell(r, w)] の値は、現時点で r 個の読み出しアクセスと w 個の書き込みアクセスを許可しているデータベースを内包した、状態付きデータベース (database-with-state) 見なせます。次の2つの証明関数は、パラメータ r と w に対するいくつかの強制を示しています:

//
praxi
lemma_DBshell_param
  {r,w:int} (!DBshell (r, w)): [0 <= r; 0 <= w; w <= 1] void
praxi
lemma_DBshell_param2
  {r,w:int} (!DBshell (r, w)): [r == 0 || (r > 0 && w == 0)] void
//

型 [DBshell(r, w)] が与えられたとき、証明関数 [lemma_DBshell_param] は r は自然数で w は 0 か 1 であることを示しています; 証明関数 [lemma_DBshell_param2] は、もし r が正の数であれば w は 0 でなければならないことを示しています。

状態付きデータベースに関するいくつかの関数を次に列挙します:

//
fun DBshell_dbget (x: !DBshell): DB
//
fun DBshell_nread {r,w:int} (x: !DBshell (r, w)): int (r)
fun DBshell_nwrite {r,w:int} (x: !DBshell (r, w)): int (w)
//

[DBshell_dbget] が、与えられた状態付きデータベースに関連したデータベースを返す意図を持っていることは明確です。 [DBshell_nread] と [DBshell_nwrite] に関しては、それぞれ r と w の値を獲得するために、型 [DBshell(r, w)] の状態付きデータベースに対して呼び出すことができます。

データベースアクセスのポリシーをエンコーディングする

データベースアクセスのポリシーは次に宣言された関数の型に形式的にエンコードされています:

//
fun DBshell_acquire_read
  {r:int} (x: !DBshell (r, 0) >> DBshell (r+1, 0)): (DBread_v | void)
fun DBshell_release_read
  {r,w:int} (pf: DBread_v | x: !DBshell (r, w) >> DBshell (r-1, w)): void
//
fun DBshell_acquire_write
  (x: !DBshell (0, 0) >> DBshell (0, 1)): (DBwrite_v | void)
fun DBshell_release_write
  {r,w:int} (pf: DBwrite_v | x: !DBshell (r, w) >> DBshell (r, w-1)): void
//

データベースから読み出すためには view [DBread_v] の証明が必要です。それを得るためには、現時点で書き込みアクセスを許可していない状態付きデータベースに対して [DBshell_acquire_read] を呼び出す必要があります。同様に、データベースへ書き込むためには view [DBwrite_v] の証明が必要です。それを得るためには、現時点で読み出しアクセスも書き込みアクセスも許可していない状態付きデータベースに対して [DBshell_acquire_write] を呼び出す必要があります。

共有された状態付きデータベース

共有された状態付きデータベースは、本質的に保護メカニズムで状態付きデータベースを包んだものです。共有された状態付きデータベースを表わす非線形の抽象型 [SDBshell] を導入してみましょう:

abstype SDBshell = ptr

予想できることですが、共有された状態付きデータベース内の状態付きデータベースを保護するために mutex を使います。次の2つの関数は、保護された状態付きデータベースを獲得/解放をするために呼び出されます:

fun SDBshell_acquire (sx: SDBshell): DBshell
fun SDBshell_release (sx: SDBshell, x: DBshell): void

ここで次に宣言された関数の実装を見てみましょう:

//
fun SDBshell_acquire_read (sx: SDBshell): (DBread_v | void)
fun SDBshell_release_read (pf: DBread_v | sx: SDBshell): void
//
fun SDBshell_acquire_write (sx: SDBshell): (DBwrite_v | void) 
fun SDBshell_release_write (pf: DBwrite_v | sx: SDBshell): void
//

これらは並行プログラミングにおいて (競合状態を引き起こさずに) データベースアクセスを安全にサポートするために呼び出されます。

共有された状態付きデータベース内には条件変数もあります。もしプロセスが読み出そうとした時にそのデータベースが別のプロセスに書き込みアクセスを許可していたなら、次の関数 [SDBshell_wait_read] がその条件変数を待ち合わせるプロセスによって呼び出されます:

//
extern
fun SDBshell_wait_read
  {r:int}
(
  sx: SDBshell, x: !DBshell (r, 1) >> DBshell
) : void // end of [SDBshell_wait_read]
//

同様に、もしプロセスが書き込もうとした時にそのデータベースが別のプロセスに読み出しアクセスか書き込みアクセスを許可していたなら、次の関数 [SDBshell_wait_write] がその条件変数を待ち合わせるプロセスによって呼び出されます:

extern
fun SDBshell_wait_write
  {r,w:int | r+w >= 1}
(
  sx: SDBshell, x: !DBshell (r, w) >> DBshell
) : void // end of [SDBshell_wait_write]

条件変数を待ち合わせているプロセスを起こすために、次の関数 [SDBshell_signal] を使うことができます:

//
extern fun SDBshell_signal (sx: SDBshell): void
//

さらに、[SDBshell_acquire_read] と [SDBshell_acquire_write] の実装を容易にするために、次のように2つの補助関数を宣言します:

extern
fun SDBshell_acquire_read2
  (sx: SDBshell, x: !DBshell >> _): (DBread_v | void)
extern
fun SDBshell_acquire_write2
  (sx: SDBshell, x: !DBshell >> _): (DBwrite_v | void)

次のコードは [SDBshell_acquire_read] を実装しています:

implement
SDBshell_acquire_read
  (sx) = (pf | ()) where
{
  val x = SDBshell_acquire (sx)
  val (pf | ()) = SDBshell_acquire_read2 (sx, x)
  val () = SDBshell_release (sx, x)
}

implement
SDBshell_acquire_read2
  (sx, x) = let
//
prval () =
  lemma_DBshell_param (x)
//
val w = DBshell_nwrite (x)
//
in
//
if w = 0
  then DBshell_acquire_read (x)
  else let
    val () = SDBshell_wait_read (sx, x) in SDBshell_acquire_read2 (sx, x)
  end // end of [else]
//
end // end of [SDBshell_acquire_read2]

次のコードは [SDBshell_release_read] を実装しています:

implement
SDBshell_release_read
  (pf | sx) = () where
{
  val x = SDBshell_acquire (sx)
  val () = DBshell_release_read (pf | x)
  val r = DBshell_nread (x)
  val () =
    if r = 0
      then SDBshell_signal (sx)
    // end of [if]
  val () = SDBshell_release (sx, x)
}

次のコードは [SDBshell_acquire_write] を実装しています:

implement
SDBshell_acquire_write
  (sx) = (pf | ()) where
{
  val x = SDBshell_acquire (sx)
  val (pf | ()) = SDBshell_acquire_write2 (sx, x)
  val () = SDBshell_release (sx, x)
}

implement
SDBshell_acquire_write2
  (sx, x) = let
//
prval () =
  lemma_DBshell_param (x)
prval () =
  lemma_DBshell_param2 (x)
//
val r = DBshell_nread (x)
//
in
//
if r = 0
  then let
    val w = DBshell_nwrite (x)
  in
    if w = 0
      then DBshell_acquire_write (x)
      else let
        val () = SDBshell_wait_write (sx, x)
      in
        SDBshell_acquire_write2 (sx, x)
      end // end of [else]
    // end of [if]
  end // end of [then]
  else let
    val () = SDBshell_wait_write (sx, x) in SDBshell_acquire_write2 (sx, x)
  end // end of [else]
//
end // end of [SDBshell_acquire_write2]

次のコードは [SDBshell_release_write] を実装しています:

implement
SDBshell_release_write
  (pf | sx) = () where
{
  val x = SDBshell_acquire (sx)
  val () = DBshell_release_write (pf | x)
  val () = SDBshell_signal (sx)
  val () = SDBshell_release (sx, x)
}

残りの実装について

この記事のコード全体は次のファイルから入手できます:

DB_read_write.sats
DB_read_write.dats

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