Think Stitch
PRINCIPIA  最近の更新


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

"システムコールのモデル" で作ったミューテックスのうち、待っているプロセスをキュー(FIFO)で管理するものが公平であることを "公平なミューテックス(スタベーション問題)" で確認しました。 でも実際にミューテックスを作るというような機会は、オペレーティングシステムでも作らない限りないでしょう。 オペレーティングシステムを作る機会なんてそうそうないですよね。 昔はリアルタイム OS を作る機会は結構あったようですけど。

応用上重要なのは、オペレーティングシステムが提供している同期のしくみを組み合わせて、公平なミューテックスを作ることでしょう。 その一例として、公平ではないセマフォを使って公平なミューテックスを作ることにします。 この例は、前に "セマフォによるバリア(ランデブ)" のところで紹介した本 "The Little Book of Semaphores" から借りました。

不公平なセマフォ

セマフォのプロセスは次のようにモデル化できます。いままでとほぼ同じパターンです。

(define-process (SEM initial-count)
  (SEMX initial-count '()))

(define-process (SEMX c cs)
  (alt
    (? wait (r) (not (memq r cs))
       (if (= c 0)
           (SEMX 0 (cons r cs))       ; (1)
           (! r (SEMX (- c 1) cs))))  ; (2)
    (? signal (r) (not (memq r cs))
       (! r
          (if (null? cs)
              (if (= c M)
                  STOP
                  (SEMX (+ c 1) cs))  ; (3)
              (xndc q cs              ; (4)
                (! q
                   (SEMX 0 (remq1 q cs)))))))))

インターフェイス用のチャネルは wait と signal にしました。 引数はプロセス ID で、前にやったようにリターンイベントをプロセス ID として使う方法を選択しました。

セマフォプロセスは2つのプロセスパラメータを持っています。 1つはセマフォのカウンタ c, もう1つは待ちプロセスのリスト cs です。 プロセスの入り口 SEM は、カウンタの初期値を指定できるように、プロセスパラメータ initial-count を持っています(珍しく説明的な名前)。

まず wait が呼ばれた場合、カウンタが 0 ならば呼び出しプロセスを待たせます (1)。 不公平なので、待ちリスト cs のどこに追加しても同じですから、いちばん簡単な先頭に追加します。 カウンタが正の場合は、カウンタをデクリメントしてリターンさせます (2)。

次は signal です。 待っているプロセスがない場合は、カウンタをインクリメントするだけです (3)。 ただし、モデルを有限にするために、カウンタが最大値 M に達しているときに signal が呼ばれたらデッドロックするようにしておきます。 このあたりは、仕様も含め、いろいろ選択の余地がありますけど、ここでは簡単なものを選んでおきます。 待っているプロセスがいる場合は、そのうちの1つを非決定的に選んで解放します。 つまり不公平です (4)。

不公平であることの確認

"公平なミューテックス(スタベーション問題)" と同じ方法で、上のセマフォが不公平であることをおおまかに確認しておきます。 前も見たとおり公平であることははっきりさせることができる場合がありますけど、公平でないことははっきりいえないので、おおまかな確認です。

初期値を1としたセマフォはミューテックスの(近似的な)代用になるので、このことを利用して前の検査を流用します。 クライアントプロセス P のインスタンスを複数用意して並行に走らせます。それぞれ排他的に仕事を行う必要があるとします。

クライアントプロセス P

クライアントプロセスは前のものと同じです。 ロックして仕事 a.id, b.id を実行し、アンロックします。 仕事を表すイベント a.id, b.id を指定するために、リターンイベント p の他に数によるプロセス ID も状態変数で持つことにします。 どちらかに統一してもいいんですけどね。

システムプロセス SYS

クライアントプロセス P のインスタンスを N 個作ってセマフォと並行合成します。 セマフォの初期値は1です。

(define-process SYS
  (par (cons* wait signal ps)
    (xpar k (interval 0 N) '()
      (P k (list-ref ps k)))
    (SEM 1)))

安全性の確認

セマフォをミューテックスとして使っているので、排他制御が正しく行われているかどうか、安全性のチェックもすることにします。 安全性の仕様 SAFETY と、これと比較するために内部イベントを隠蔽したシステムプロセス HSYS を用意します。

安全性の仕様 SAFETY

(define-process SAFETY
  (xalt k (interval 0 N)
    (! (list-ref as k)
        (! (list-ref bs k)
           SAFETY))))

内部イベントを隠蔽したシステムプロセス HSYS

(define-process HSYS
  (hide (cons* wait signal ps)
    SYS))

安全性検査の結果

結果は次のとおり確認できました。

不公平の確認

続いて不公平の確認をします。

公平であることを確認する仕様

仕様は前と同じです。 wait.0 が発生したあと、L ステップ以内にリターンイベント p.0 が発生するかどうかを追跡します。 制限ステップ数 L をプロセスパラメータにしました。いろいろ代えて試せるようにするためです。 こうすると再コンパイルが必要ないので、キャッシュが効いて効率よく検査できます。

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

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

公平性の検査結果

結果は次のようになります。L= 10000 でもロックが獲得できない場合があるので、モデルの作りからみても公平性はないとみてよいでしょう。 繰り返しますが、公平でないとはっきりしたわけではありません。 しかし、もう少し小さな L でパスを調べるとわかりますが、プロセスが少なくとも3つあると、そのうちのひとりが永久に仲間はずれにされる場合があることがわかりますので、公平性はありません。

HSYS をトレースモードで観る

最後の検査項目は、HSYS をトレースモードで観るためのものです。計算木は次のようになります。

確かに排他制御がなされています。状態 4, 5, 6 は 0 と同じ状態です。遷移を見るとわかります。

以上で不公平なセマフォの準備は終わりです。

公平なミューテックスのモデル

"The Little Book of Semaphores" のセクション 4.3.1 から、公平なミューテックスのコードを引用します。 コードの説明は本を見てください :P 。

1 room1 = room2 = 0
2 mutex = Semaphore(1)
3 t1 = Semaphore(1)
4 t2 = Semaphore(0)
1 mutex.wait()
2   room1 += 1
3 mutex.signal()
4
5 t1.wait()
6   room2 += 1
7   mutex.wait()
8   room1 -= 1
9
10   if room1 == 0:
11     mutex.signal()
12     t2.signal()
13   else:
14     mutex.signal()
15     t1.signal()
16
17 t2.wait()
18   room2 -= 1
19
20   # critical section
21
22   if room2 == 0:
23     t1.signal()
24   else:
25     t2.signal()

2つの共有変数 room1, room2 と3つのセマフォ mutex, t1, t2 を用意しています。 mutex もセマフォです。先と同じようにミューテックスの代わりに使っています。 (セマフォの本なので。本のとおりにすることにします。)

セマフォは用意したので、あと共有変数と上のプロセスを用意します。

共有変数 VAR

共有変数を表すプロセス VAR を定義します。

(define-process (VAR v)
  (alt
    (! rd (v) (VAR v))
    (? wr (x) (VAR x))))

クライアントプロセス P

本のコードと対応がつけやすいように、平たいインデントでプロセス式を書きました。 ちょっと気持ち悪いかもしませんが。

(define-process (P id p)
  (! mutex.wait (p)
  (! p
  (? room1.rd (x)
  (! room1.wr ((+ x 1))
  (! mutex.signal (p)
  (! p

  (! t1.wait (p)
  (! p
     (? room2.rd (x)
     (! room2.wr ((+ x 1))
     (! mutex.wait (p)
     (! p
     (? room1.rd (x)
     (! room1.wr ((- x 1))
     (if (= x 1)
         (! mutex.signal (p)
            (! p
               (! t2.signal (p)
                  (! p (P1 id p)))))
         (! mutex.signal (p)
            (! p
               (! t1.signal (p)
                  (! p (P1 id p))))))
)))))))))))))))

(define-process (P1 id p)
  (! t2.wait (p)
  (! p
     (? room2.rd (x)
     (! room2.wr ((- x 1))
     ;; critical section
     (! (list-ref as id)
     (! (list-ref bs id)

     (if (= x 1)
         (! t1.signal (p)
            (! p (P id p)))
         (! t2.signal (p)
            (! p (P id p))))
)))))))

元のコードの10行目では room1 を参照しているので、if 文の分岐双方に mutex.signal があります。 if 文の前にまとめてしまうと、別のプロセスが room1 を更新してしまうかもしれないからです。 この点、プロセス式の方ではプロセスローカルな変数 x に値を引き取っているので、mutex.signal を後で2つ書く必要はないのですが、混乱を避けるために元のコードと同じにしてあります。

システムプロセス SYS

以上のプロセスを並行合成して、システムプロセスを作ります。 共有変数を2つ、セマフォを3つ、改名を使って作ります。

(define-process SYS
  (par (cons* mutex.wait mutex.signal
              t1.wait t1.signal
              t2.wait t2.signal
              room1.rd room1.wr
              room2.rd room2.wr
              ps)
    (xpar k (interval 0 N) '()
      (P k (list-ref ps k)))
    (par '()
      (rename `((,wait . ,mutex.wait)
                (,signal . ,mutex.signal))
        (SEM 1))
      (rename `((,wait . ,t1.wait)
                (,signal . ,t1.signal))
        (SEM 1))
      (rename `((,wait . ,t2.wait)
                (,signal . ,t2.signal))
        (SEM 0))
      (rename `((,rd . ,room1.rd)
                (,wr . ,room1.wr))
        (VAR 0))
      (rename `((,rd . ,room2.rd)
                (,wr . ,room2.wr))
        (VAR 0)))))

内部イベントを隠蔽したシステムプロセス HSYS

確かにミューテックスになっていることを確認するために、安全性の検査をします。 そのために内部イベントを隠蔽したシステムプロセス HSYS を用意します。

(define-process HSYS
  (hide (cons* mutex.wait mutex.signal
               t1.wait t1.signal
               t2.wait t2.signal
               room1.rd room1.wr
               room2.rd room2.wr
               ps)
    SYS))

公平性の仕様

トリガとして mutex.wait(p.0) を使います。これが発生したら、L ステップ以内にイベント a.0 が発生すればよいとします。

(define-process (SPEC L)
  (ndc
    (! mutex.wait ((car ps)) (SPEC-HUNT L L))
    (xndc u (remq ($ mutex.wait (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 = 3 の場合、検査の結果は以下のようになりました。 安全性の条件、公平性の条件ともに成り立つことが確認できました。 プロセス HSYS の計算木は、上で見たものとまったく同じになります。

残念ながら、N = 4 とすると、状態数が多すぎて SyncStitch の能力を超えてしまいます。 コードの作りからいって、少なくとも N = 7 くらいまでは検査したいところです。 詳細は本を見ていただくとわかりますが、プロセスが3つの部屋に分けられるので、クリティカルセクションを除く残り2つの部屋で3つのプロセスが競合するとすると合計7個になります。 次回はモデルを抽象化することによって状態数を減らし、N = 7 の場合を検査することに挑戦したいと思います。

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