Think Stitch
PRINCIPIA  最近の更新


自動リセットイベントオブジェクト

Microsoft Windows の Win32 API が提供している同期オブジェクトの1つ、イベントオブジェクトをモデル化します。 イベントオブジェクトには2つの種類、手動リセットと自動リセットがあります。 ここでは自動リセットのイベントオブジェクトをモデル化します。 検査の舞台は条件変数と同じものを使います。

状況設定

条件変数はミューテックスと分離すると正しく機能しないことがわかりました。 では、ミューテックスを分離した条件変数の代わりに自動リセットイベントを使ったらどうなるのか、ということを調べてみたいと思います。

自動リセットイベントのモデル

条件変数の検査で作ったプロセスを流用するために、イベントオブジェクトのインターフェイスで使うチャネル名を条件変数と同じ wait, signal とします。 wait は WaitForSingleObject, signal は SetEvent に対応します。

イベントオブジェクトのプロセスを EVENTOBJ とします。 2つのプロセスパラメータ s と ps を用意します。 s はシグナル状態を表す論理変数です。 イベントオブジェクトは待っているプロセスがいないときに SetEvent された場合、シグナル状態を維持するので、この変数が必要です。 ps は待っているプロセスのリターンイベントのリストです。

モデルは次のようになります。

(define-process (EVENTOBJ s ps)
  (alt
    (? wait (r) (not (memq r ps))
       (if s                            ; (1)
           (! r (EVENTOBJ #f '()))      ; (2)
           (EVENTOBJ #f (cons r ps))))  ; (3)
    (? signal (r) (not (memq r ps))
       (! r                             ; (4)
          (if (null? ps)                ; (5)
              (EVENTOBJ #t '())         ; (6)
              (! (car ps)               ; (7)
                 (EVENTOBJ #f (cdr ps))))))
    (! terminate SKIP)))                ; (8)

まず wait を見てみます。 もしイベントオブジェクトがシグナル状態だったら (1) そのままリターンさせます。 イベントオブジェクトは非シグナル状態になります (2)。 非シグナル状態だった場合は待ちリストに加えます (3)。 ここでは先頭に追加しました。 イベントオブジェクトは FIFO ではないからです。 MSDN の説明を引用しておきます。

"An event object whose state remains signaled until a single waiting thread is released, at which time the system automatically sets the state to nonsignaled. If no threads are waiting, the event object's state remains signaled. If more than one thread is waiting, a waiting thread is selected. Do not assume a first-in, first-out (FIFO) order. External events such as kernel-mode APCs can change the wait order."

http://msdn.microsoft.com/en-us/library/windows/desktop/ms682655(v=vs.85).aspx/html

次は signal です。 まず呼び出したプロセスは返してしまいます (4)。 次に待っているプロセスがいるかどうかを調べます (5)。 もし待ってるプロセスがいない場合はシグナル状態にするだけです。 すでにシグナル状態であった場合は何も変わらないことになります。 この点についても MSDN に明記されています。

"Setting an event that is already set has no effect."

http://msdn.microsoft.com/en-us/library/windows/desktop/ms686211(v=vs.85).aspx/html

待っているプロセスがいた場合は、先頭のものを解放します (7)。

最後に、終了のためのしかけを入れておきます (8)。

他のプロセス

他のプロセスを再掲しておきます。

P

Qx

MUTEX

(define-process (MUTEX m ms)
  (alt
    (? lock (r) (not (memq r ms))
       (if (eq? r m)
           STOP
           (if m
               (MUTEX m (append ms (list r)))
               (! r (MUTEX r ms)))))
    (? unlock (r) (not (memq r ms))
       (if (and m (eqv? r m))
           (! r
              (if (null? ms)
                  (MUTEX #f '())
                  (! (car ms)
                     (MUTEX (car ms) (cdr ms)))))
           STOP))
    (! terminate SKIP)))

MEM

(define-process (MEM m)
  (alt
    (! rd (m) (MEM m))
    (? wr (x) (MEM x))
    (! terminate SKIP)))

SYS3

CV を EVENTOBJ と入れ替えます。

(define-process SYS3
  (par (cons* lock unlock
              wait signal
              rd wr
              terminate p qs)
    (seq
      (par '()
        (P (- N 1))
        (if (null? (cdr qs))
            (Qx (car qs))
            (xpar q qs '() (Qx q))))
      (! terminate SKIP))
    (par (list terminate)
      (MEM 0)
      (MUTEX #f '())
      (EVENTOBJ #f '()))))

検査

孤独な条件変数の場合、N = 1 でもデッドロックしました。 しかし自動リセットイベントオブジェクトに置き換えると、デッドロックは発生しません。

しかし N = 2 とするとデッドロックします。

状況は以下の通りです。プロセス P と Q1 は終了していますが、 Q0 は待ちリストに残っていて状態 Q8 にいます。

パスを追うと概略は次のとおりです

  • A. Q1 が共有変数の値 0 を読んで待ちに入ろうとしています。アンロックをしたところまでで、まだ待ち状態ではありません。
  • B. ここで Q0 に切り替わり、同じく 0 を読んでアンロックしたところまでです。
  • C. P が動いて変数をインクリメントし、イベントオブジェクトをシグナル状態にします。待っているプロセスはないからです。
  • D. さらにそのままもう1度インクリメント、signal を呼びます。待っているプロセスはなく、すでにシグナル状態なので、これは状態を変えません。
  • E. Q1 が wait を呼び出し待ちに入ろうとしましたが、イベントオブジェクトはシグナル状態なのですぐに解放されます。イベントオブジェクトは非シグナル状態になります。
  • F. Q0 が待ち状態になります。
  • G. Q1 が変数をデクリメントして終了します。

さらに P も2回インクリメントしたので終了します。プロセス Q0 を起こす人はいません。

問題は2回目の signal が空振りになることです。今回はやさしかったですね。

Windows NT の頃は同期オブジェクトの種類が少なくて困っていた人もいるでしょう。 その後プロセス間だと SignalObjectAndWait, スレッドに関しては pthread に対応するものが追加されたので、だいぶ楽になりました。 もっとも Windows XP をサポートしなければならない場合、後者は使えません (T_T)。

2013/09/07
© 2013,2014,2015 PRINCIPIA Limited