Think Stitch
PRINCIPIA  最近の更新


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

システムコールのモデルでは、システムコールのシミュレーションを使って8個のミューテックスモデルを作りました。 (そのうち2つは準備体操で、システムコールのモデルとしてふさわしくないので、実質6個です。) 今回はその中でどれがよいかという話をしようと思います。

公平性と飢餓状態(スタベーション starvation)

SyncStitch ユーザガイドの中で、公平性についてほんのさわりだけ紹介しました。 状態遷移モデルで遷移が公平であるとは、その遷移が起こりうる機会が繰り返し発生するならば、いつかは必ず発生するということです。 日常的な意味では、公平とは何か2つ以上のものを比較して使う言葉ですけど、ここでの専門用語としての公平さは、意味を極力純化した結果として1つの遷移の性質を表すものになってします。

しかし実際には2つ以上の遷移がある場合が問題になります。 例えばある状態 S から2つの遷移 a, b が出ていて、プロセスが状態 S に何度も繰り返しやってくるとします。 しかも a も b も発生できる状況にある、つまり対向のプロセスもイベントを提示しているとします。 このとき、いつかはかならず a が発生するならば a の遷移は公平であるということになります。

ところが公平性というのは対称的な比較の問題ではないので、遷移 a は公平だけれども遷移 b は公平ではないということも起こりえます。 実際、いつでも遷移 a が選ばれるとすると、a は定義により公平ですけど、b は公平ではないということになります。

CSP のイベント選択に公平性はないので、上の例でいうと遷移 a も b もどちらも公平ではありません。 したがって永久に a だけが発生するかもしれないし、永久に b だけが発生するかもしれません。 この2つの極端な状況は、可能性として排除されないのです。

すると遷移 a を待っている対向のプロセスは、遷移 a が発生する可能性があるにも関わらず永久に待たされるということがあり得ます。 このような状況を飢餓状態あるいはスタベーション(starvation)といいます。

例えば複数のプロセスがロックを取り合う場合、何回チャレンジしてもロックが取れないプロセスが出てしまう可能性があります。 このように可能性としてはリソースを獲得するチャンスがあるにも関わらず永久に獲れないので、リソースに飢えている、つまり飢餓状態というわけです。 リソーススタベーション(資源飢餓)といういい方もあるようです。

公平なミューテックス

繰り返すと CSP の遷移に公平性はないので、複数のプロセスが同時にシステムコールの呼び出しイベント lock.k を提示してロックを取り合うとき、どれもいつかは必ず発生するとはいえません。 同じように、インターリーブで共有する抽象的なミューテックスのモデルでも、すべてのプロセスが lock を提示する場合、どのプロセスもいつかはロックを獲得できるとはいえません。 後者の場合、これ以上の仕掛けがミューテックスにないので、この抽象度で公平性を議論することはできません。

しかしシステムコールをシミュレートして作ったモデルでは、もう少し精密な議論をすることができます。 ふつうオペレーティングシステムのスケジューリングにはある程度の公平性があるので、あるプロセスがまったくコードを実行できないということはありません(ここでは優先順位はないとしておきます)。 したがって、どのプロセスも lock システムコールを呼び出そうとすればいつかは呼び出しに到達すると考えていいでしょう。 イベントの言葉でいい直せば、プロセスが lock.k を提示していればいつかは発生すると仮定するわけです。

すると問題は、lock.k が発生したらいつかはロックが獲得できるのかどうかということです。 これがここで問題にしたいミューテックスそのものの公平性の問題です。 あるミューテックスの実装では、プロセスが lock システムコールで待ちに入ったら、必ず有限の時間内にそのプロセスにロックを割り当ててくれます。 一方で永久に待ち状態に置かれたままで、ロックをもらえないような実装もあります。 前者を公平なミューテックスと呼ぶことにします。後者は不公平ですね(というのは聞いたことがありませんが)。

公平なミューテックスの条件をもう1度整理しましょう。 ロックが獲得できたとは、ロックシステムコールから返ってきたということですから、リターンに対応するイベント p.k が発生することだと考えることができます。 したがって公平なミューテックスの条件は次のとおりです。

ロックシステムコールの呼び出しイベント lock.k が発生したら、必ず有限のステップでリターンイベント p.k が発生する。

ここでステップといっているのは、なんらかのイベントが発生することです。 プロセスがデッドロックする場合を除いて、常になんらかのイベントが発生しますから、その発生を1単位として時間を計測すると考えます。 つまり有限のステップとは、有限のイベント発生回数後に、という意味です。

ミューテックスの公平さを表す仕様

次の問題は、上で整理したミューテックスの公平さを表す仕様をどのようにモデル化するかという問題です。 これには SyncStitch ユーザガイドで紹介した特徴プロセスの考え方を使います。 特徴プロセスとは、プロセスが持つ性質を表すプロセスのことをいうのでした。 この特徴プロセスと対象のプロセスを正当性検査で比較すると、対象のプロセスがその性質を持っているかどうかわかるのでした。

したがってここでは、ミューテックスの公平性を表す特徴プロセスを作ればいいわけです。 この特徴プロセスは次のように考えることができます。 ここではプロセス ID 0 のプロセスに注目することにします。 プロセスは対称なので、どのプロセスを選んでも同じことです。 戦略を述べると、lock.0 が発生してから決められた時間制限内にリターンイベント p.0 が必ず発生するというプロセスにすることです。

  1. まずはじめは lock.0 以外のイベントは何が何度発生してもよい。
  2. もし lock.0 が発生したら、時間の上限 L をセットして次の監視プロセスに移行する。
  3. 監視プロセスではリターンイベント p.0 が発生するかどうかを監視する。もし発生したら初期状態に戻る。
  4. リターンイベント p.0 以外のイベントが発生した場合は時間の上限をデクリメントして監視を続ける。
  5. 上限が 0 になった場合は p.0 が発生しなければいけないとする。

特徴プロセスの定義は次のようになります。

(define L 30)

(define-process SPEC
  (ndc
    (! lock (0) (SPEC-HUNT L))
    (xndc u (remq ($ lock 0) Events)
      (! u SPEC))))

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

定数 L は時間の上限です。 「どのイベントが起こってもよい。しかしどれかは起こらなければならない」という条件を表すには拒否が必要なので、検査はトレースだけではなく、トレースと拒否による正当性検査になります。 したがって非決定的選択 ndc, xndc を使う必要があります。そうでなければ、「すべて発生できなければならない」という意味になってしまうからです。 厳密には、初期状態では停止する場合が含まれていてもよいはずですが、システムがデッドロックしないことは検査済みなので、簡単のため外してあります。 (これに対してリターン待ちではデッドロックできません。公平ではなくなるからです。)

ロックシステムコールの呼び出しイベント lock.0 が発生したら、監視プロセス SPEC-HUNT に移行します。 プロセスパラメータ n は残り時間で、上限 L で初期化します。 残り時間 n が 0 でないときは、監視プロセス SPEC-HUNT も決定的選択を使って任意のイベントを発生可能とします。 もしここでリターンイベント p.0 が発生したら、初期状態 SPEC に戻ります。 残り時間 n が 0 のときには、必ず p.0 が発生しなければなりません。

説明が遅れましたが、モデルの中で定義されているすべてのイベントは、リストとして Events に入っています。 つまりアルファベット Σ のリスト版です。 したがって、lock.0 以外のイベントは (remq ($ lock 0) Events) と表すことができます。 チャネルイベントは eq? での同一性が保証されているので、remq が使えます。

公平性の検査

では公平さの検査しましょう。 もし上限 L が小さければ、たとえ公平であったとしてもロック獲得前にタイムアウトになり、違反と見なされてしまうでしょう。 そうならないように十分大きな L を見積もってみます。

プロセスが N 個あるとして、あるプロセスがまずロックを獲得し、その状態で残り N-1 個のプロセスが待ち状態に入る場合がワーストケースです。 プロセス 0 は最後に lock.0 を発行したとします。 それぞれのプロセスがリターンイベント p.k, 仕事 a.k, b.k, アンロック unlock.k, そしてリターンイベント p.k を実行しますから、 5(N - 1) ステップ程度の待ちが発生するはずです。 したがって例えば N = 3 とすると、10 あたりが境界になります。

気がついた人もいると思いますが、実はこれは甘い(あれ?どっちだ?)見積もりです。 なぜかというと、一度ロックを解放したプロセスが再び割り込んでくるかもしれないからです。 それでもいつかは必ず p.0 が発生するならば公平性はあるわけです。 そうすると原理的には上限を設定することができないということになります。

しかし幸いなことに、これは「公平だけれども検査で確認できない場合がある」といっているだけです。 検査で公平であることが確認されれば、公平であることが保証されます。 (逆だったら困りますよね。)

では L = 30 として検査をします。 おっとその前に、システムプロセスの定義を修正して隠蔽を外しておきます。 lock.0 や p.0 だけでなく、すべてのイベントをカウントするためです。

(define-process (SYS MUTEX unlock-type)
  (par
      (if (eq? unlock-type 'event)
          (cons* lock e-unlock ps)
          (cons* lock unlock ps))
    (xpar k I '() (P k unlock-type))
    MUTEX))

検査の結果は次のとおりです。

ここでは MUTEX0 と MUTEX1 も入れておきました。 これらが公平なのは自明です。lock.0 のあとは p.0 しか発生させないのですから。

この段階で公平であるといえるのは MUTEX5 だけです。 これは待ちに入るプロセスを ms の末尾に追加するバージョンでした。 つまり待ち行列(FIFO, First-In First-Out)になっているバージョンです。 これは納得のいく結果でしょう。

(define-process MUTEX5
  (MUTEX5D #f '()))

(define-process (MUTEX5D m ms)
  (alt
    (? lock (k) (not (memv k ms))
       (if (eqv? k m)
           STOP
           (if m
               (MUTEX5D m (append ms (list k)))   ; (*)
               (! (list-ref ps k)
                  (MUTEX5D k ms)))))
    (? unlock (k) (not (memv k ms))
       (if (and m (eqv? k m))
           (if (null? ms)
               (! (list-ref ps k)
                  (MUTEX5D #f '()))
               (ndc
                 (! (list-ref ps k)
                    (! (list-ref ps (car ms))
                       (MUTEX5D (car ms) (cdr ms))))
                 (! (list-ref ps (car ms))
                    (! (list-ref ps k)
                       (MUTEX5D (car ms) (cdr ms))))))
           STOP))))

それ以外のプロセスについては、上での議論の通り、この結果からは公平であるかどうかはわかりません。 例として MUTEX2 のパスを見てみると次のようになっています。

これを見ると、プロセス 0 が待っている間にプロセス 1 と 2 が交互にロックを持っていってしまうので、タイムアウトまでロックがもらえない様子がわかります。 作りからいって、これを避けるしくみはありませんから、MUTEX2 には公平性を持っていません。 他のミューテックスでも同様になります。

ちなみに MUTEX5 は L = 10 まで検査をパスします。 L = 9 とすると、以下のように違反になります。 これは見積もりのとおりでした。たまたまかな。

以上より、結論としては MUTEX5 の実装がよいということになりました。

補足

上限を設定しなければいけないところが、ちょっとこの検査の弱点です。 しかも違反があった場合は、公平であるかどうかわかりません。 それでも、検査をパスした場合でも公平でないときがあるというよりはずっとよいでしょう。 (論理学を勉強した人は、健全性とか完全性とかいう言葉を知っているでしょう。) あと、数学的に厳密にいうと、いつかは必ず発生するということと、上限を設定することができるというのは違うわけです。

これらの欠点を持たない手法もあります。 興味のある人のために名前だけ出しておくと、時間論理(あるいは時相論理)というものを使う方法です。 時間論理とは、おおまかにいうと、命題論理に、時間に関するオペレータを加えた論理です。 これを使うと、公平性の条件、すなわち lock.0 が発生したら、いつかは必ず p.0 が発生するという条件をずばりそのまま表すことができます。 しかも時間論理をサポートしたツールでは、上限など設定しなくても完全な検査をすることができます。 完全といったのは、公平かどうかを検査で必ず判別できるという意味です。 さらに、ツールによっては遷移の公平さを選択することができるものがあります。 興味がある人は、例えば Spin model checker や NuSMV を調べてみてください。

ミューテックスのモデルをもっと工夫すると、待ち行列への割り込みがあるのに公平性もあるようなものを作ることができます。 それが目的というよりは、プロセスに優先順位をつけつつ公平性も保つにはどうしたらいいかという問題に興味があります。 原則として、待ち行列からプロセスを選ぶ際には優先順位に基づいた選択をするとします。 すると、優先順位の低いプロセスは飢える可能性があります。 そこで割り当ての回数を数えて、それに基づいて割り当てを制限したり、優先順位を調整したりする戦略が考えられます。 挑戦してみてはいかがでしょうか :P 。

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