Think Stitch
PRINCIPIA  最近の更新


公平なミューテックス(スタベーション問題)2

活性(liveness)の検査で説明した方法をシステムコール形式のミューテックスに適用してみます。 問題は、公平なものはどれかということです。

仕様プロセス Q

最終的にイベント a.0 が発生すればよいので、仕様プロセス Q は次のようになります。

(define-process Q
  (! (car as) STOP))

テストハーネス XSYS

テスト用のハーネスでは、システムプロセス SYS と制約プロセス R を並行合成した後、a.0 以外のイベントを隠蔽します。 (アンロックがイベントであるタイプへの対応は省略しました。)

(define-process (XSYS MUTEX)
  (hide (remq (car as) Events)
    (par Events
      R
      (SYS MUTEX 'channel))))

制約プロセス R

制約プロセスは、トリガの選別とイベント a.0 が発生した後の動作の切捨てを行います。 トリガについてはひと工夫必要です。 最初に lock(0) が発生したらロックが獲得できるのは当然です。 問題になるのは、先に誰かがロックを持っている状態で lock(0) を実行し、待ちリストに加えられたときです。 待ちに入る順序は、プロセスを並べた順列の数だけあるので、これを非決定性を使ってすべて調べることにします。

(define-process R
  (xndc k (interval 0 N)
    (! lock (k)
       (! (list-ref ps k)
          (R0 (remv k (interval 0 N)))))))

(define-process (R0 ks)
  (if (null? ks)
      (R1 (remq (car as) Events))
      (xndc k ks
        (! lock (k) (R0 (remv k ks))))))

(define-process (R1 A)
  (alt
    (! (car as) STOP)
    (xalt e A (! e (R1 A)))))

まず先頭のプロセスを非決定的に選んでロックシステムコールを呼び出します。 これはすぐにリターンするはずなので、対応するリターンイベントを待ちます。

残ったプロセスのリストを ks とします。要素はプロセス ID です。 ここからさらに非決定的にプロセスを選び、順にロックシステムコールを呼び出します。 ロックを獲得した先頭のプロセスはまだ動いていない(動かしていない)ので、すべてのプロセスが待ちに入ります。

すべてのプロセスが待ちに入ったら、イベント a.0 の監視モードになります。 a.0 以外のすべてのイベントを無視し、a.0 が発生したら停止します。

検査結果

検査結果は次のとおりです。 待ち行列を使っている MUTEX5 が公平であることが、この方法でも再度確認できました。

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