Think Stitch
PRINCIPIA  最近の更新


不公平なセマフォで作る公平なミューテックス 2

前回は不公平なセマフォをシステムコールのシミュレート方式で作り、その上で公平なミューテックスを作りました。 システムコールのシミュレートは詳細度が高いので、どうしても状態数が多くなってしまいます。 結果として N = 3 の場合までしか検査することができませんでした。 今回は抽象度を上げることで、より大きな N に対して検査できるようにします。 抽象化の戦略は次のとおりです。

プロセス定義

修正した各プロセスを順にお見せします。

セマフォ

イベントで同期するだけのタイプにします。 これをインターリーブによって共有します。

(define-process (SEM c)
  (alt
    (if (= c 0)
        STOP
        (! wait (SEM (- c 1))))
    (if (= c M)
        STOP
        (! signal (SEM (+ c 1))))))

共有変数

インターフェイスを読み書き rd, wr からアトミックな inc, dec に変えます。 あと、デクリメント dec の後 0 になったかどうかの判定が必要なので、ユーザガイドのリーダ・ライタ問題で使ったテクニックを使います。 dec の他に dec0 を用意し、デクリメントの結果が 0 の場合は dec0 とだけ、0 でない場合は dec とだけ同期するようにします。 クライアントプロセスは両方提示します。 どちらと同期したかによって 0 になったかどうかを判断できます。

(define-process (VAR v)
  (alt
    (! inc (VAR (+ v 1)))
    (if (= v 1)
        (! dec0 (VAR 0))
        (! dec (VAR (- v 1))))))

クライアントプロセス P

セマフォ、共有変数の修正に合わせて、クライアントプロセスも修正します。 イベント b はコメントアウトしてあります。 安全性の検査を行うときにはコメントを外してください。

(define-process (P id)
  (! (list-ref ps id)      ; (*)
  (! t1.wait
     (! room2.inc
     (alt
       (! room1.dec0
          (! t2.signal
             (P1 id)))
       (! room1.dec
          (! t1.signal
             (P1 id))) )))))

(define-process (P1 id)
  (! t2.wait
     (alt
       (! room2.dec0
          ;; critical section
          (! (list-ref as id)
;         (! (list-ref bs id)
          (! t1.signal (P id))))
;         )
       (! room2.dec
          ;; critical section
          (! (list-ref as id)
;         (! (list-ref bs id)
          (! t2.signal (P id))))
;         )
       )))

ここでひとつ問題があります。 前のモデルでは mutex.wait(p.0) をトリガに使っていました。 すなわち、もし mutex.wait(p.0) が発生したら、必ず有限ステップ以内に a.0 が発生するということを検査しました。 しかし今回の修正で mutex を取り除いてしまったので、トリガになるものがありません。 他のインターフェイスもみな、インターリーブによる共有方式になったので、プロセス 0 だけを識別することができません。 そこで、room1.inc を各プロセスごとに用意して使い分けることにします。 これが (*) の部分です。

システムプロセス

システムプロセスは次のようになります。 まず mutex 用のセマフォを取り除きました。 それから、room1.inc の代わりに、p.0, p.1, p.2, ... を使います。 これは1対多の改名になります。

(define-process SYS
  (par (cons* t1.wait t1.signal
              t2.wait t2.signal
              room1.inc room1.dec room1.dec0
              room2.inc room2.dec room2.dec0
              ps)
    (xpar k (interval 0 N) '()
      (P k))
    (par '()
      (rename `((,wait . ,t1.wait)
                (,signal . ,t1.signal))
        (SEM 1))
      (rename `((,wait . ,t2.wait)
                (,signal . ,t2.signal))
        (SEM 0))
      (rename `(,@(map (lambda (p) (cons inc p)) ps)
                (,dec . ,room1.dec)
                (,dec0 . ,room1.dec0))
        (VAR 0))
      (rename `((,inc . ,room2.inc)
                (,dec . ,room2.dec)
                (,dec0 . ,room2.dec0))
        (VAR 0)))))

公平性の仕様

公平性の仕様では、トリガを p.0, すなわち (car ps) にします。

(define-process (SPEC L)
  (ndc
    (! (car ps) (SPEC-HUNT L L))
    (xndc u (remq (car ps) Events)
      (! u (SPEC L)))))

(define-process (SPEC-HUNT n L)
  (if (= n 0)
      (! (car as) (SPEC L))
      (ndc
        (! (car as) (SPEC L))
        (xndc u (remq (car as) Events)
          (! u (SPEC-HUNT (- n 1) L))))))

検査

このモデルであれば N = 7 まで検査をすることができます。 結果は以下のとおり、安全性、公平性ともに持っていることがわかります。

N と状態数の対応は次のとおりでした。 (この表はイベント b を外した場合の状態数です。)

N状態数
250
3217
4856
53,179
611,346
739,393

グラフにすると次のようになります。

状態数を対数にすると次のようになります。

これからわかるように、状態数は N に対してほぼ指数関数的に増加しています。 したがって、ある程度以上はどうしても検査が不可能になります。 検査できる範囲が、現実に使う範囲、あるいは性質がほぼ出尽くしたであろうと思われる範囲をカバーできればよいのですが、そうでない場合はあまり意味がないということになります。

N = 7 は微妙な境界線だと思いますけど、今回はここまでにしておきます。

補足

ここまでやると、元のコードと性質が違ってしまうのではないかという懸念があるでしょう。 それは確かにあると思います。 この話を始めるとまた長くなるので、簡単に結論だけいうと、結果として欲しいのは公平なミューテックスなので、最終的なミューテックスのモデルが、安全性と公平性を持っていればいいと考えることにします。

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