Think Stitch
PRINCIPIA  最近の更新


システムコールのモデル

いままでに何度か抽象化とその技の話をしてきました。 またミューテックスやセマフォを高い抽象度でモデル化して使ってきました。 抽象化の話はまだありますけど、ちょっと休憩させてもらって、逆に詳細なモデルを作ることを考えてみたいと思います。 題材は例によってミューテックスです。

ミューテックスについては過去に2レベルの抽象度でのモデルを示しました。 1つは SyncStitch ユーザガイドで紹介したもので、クライアントプロセスをイベントで区別するものでした。 もう1つはインターリーブによるサービスの共有で紹介したもので、クライアントプロセスを区別せず、インターリーブで共有して使うものでした。 これがもっとも抽象度の高いミューテックスモデルだと思います。

どちらのモデルもイベントによる同期型の相互作用を基にしたものであるという点では同じです。 一方、一般のオペレーティングシステムを見ると、CSP のような同期型の相互作用を基本としているものは少なく、ほとんどがシステムコールとか API と呼ばれる制御渡しを基本としたものを使っています。 そこで、このシステムコールを同期型の相互作用でモデル化することによって、ミューテックスを作ってみたいと思います。

アイデアは簡単で、システムコールの呼び出しとリターンを、それぞれイベント同期で表します。 プロセスは、呼び出しに対応するイベントで同期をしたら、そのままリターンに対応するイベントの発生を待つという約束にします。 実際にはリターンを待つ間にも並行して動作できるわけですけど、待つという約束によってシステムコールをシミュレートするわけです。 シーケンス図で表すと以下のようになります。

ふつうオペレーティングシステムはシステムコールを呼び出したプロセスを識別できると思いますが、ここではそれができないので、代わりにプロセスの方から ID を渡してもらうことにします。 つまり、システムコール呼び出しに対応するイベントでプロセスを区別するわけです。 これはユーザガイドに出てきたミューテックスと同じです。 違いは、ここではイベントの代わりにプロセス ID を引数とするチャネルを使うことです。 原理的には同じことになります。

マイクロカーネル方式のオペレーティングシステムで、メッセージによるプロセス間通信を相互作用の基礎としているものでは、ライブラリ関数の中でこれと同等の処理を行っているのかもしれません(ただの想像です。教えてください、知っている人)。

このように呼び出しとリターンを分けると、オペレーティングシステムがプロセスを待ち状態にするしくみをモデル化することができます。 例えば、2つのプロセスが連続してロックを要求した場合のシナリオは次のようになります。

オペレーティングシステムはプロセス B からのロック要求に対して、リターンに対応するイベントを発生させないことによって待ち状態を表現します。 これは実際のオペレーティングシステムの動作にかなり近いと思われます。

このモデルは、そのまま関数呼び出しのモデルとしても使えるように思われるかもしれません。 単純な場合はそのとおりなのですが、再帰や呼び返しがある場合はこのままでは表すことができません。 制御を渡しているわけではないので、関数呼び出しはどちらかというと逐次合成 seq を使ったプロセスの再利用の方が似ているように思います。

ロックを獲得するシステムコールでは待ち状態になる可能性がありますが、ロックを解放するシステムコールが待たされることはありません。 そこで、アンロックのシステムコールだけ、以前と同じようにイベント同期で表すという混成もありえます。 少しだけ抽象度を上げたということです。 少しだけ手を抜いたともいえます :P 。 こうするとモデルの状態数を少しだけ減らすことができますから、役に立つ場合もあるでしょう。 ただ後で見るように、実際に抽象化になっているのです。

では実際にモデルを作っていくことにしましょう。

イベント・チャネルと補助関数定義

クライアントプロセスの数を N とします。

(define N 3)
(define I (interval 0 N))
(define D (map list I))

各プロセスの、システムコールからのリターンを表すイベント p.id を定義します。 ここで id はプロセス ID 0, 1, ..., N-1 です。 これらは define-event-list を使ってまとめて定義します。

(define-event-list ps N "p")

同様に、各プロセスがロック中に行う仕事を表すイベント a.id, b.id を定義します。 イベントを2つ用意するのは、操作のアトミック性を確認するためです。 操作の開始イベント・完了イベントと考えることができます。

(define-event-list as N "a")
(define-event-list bs N "b")

ミューテックスのロック・アンロックを表すシステムコール用のチャネル lock, unlock と、イベント e-unlock を定義します。 アンロックもリターンを必要とするモデルではチャネル unlock を使います。 イベント同期でアンロックを表すモデルではイベント e-unlock を使います。

(define-channel lock (k) D)
(define-channel unlock (k) D)
(define-event e-unlock)

最後に、リストから指定された要素を1つだけ取り除く関数 remv1 を用意しておきます。

(define (remv1 x xs)
  (cond ((null? xs) '())
        ((eqv? x (car xs)) (cdr xs))
        (else
         (cons (car xs) (remv1 x (cdr xs))))))

安全性の仕様

まず仕様を定義します(正しい順序)。 ミューテックスが排他性・アトミック性を保証してくれることを確認するので、安全性の仕様です。 各プロセスの a.id, b.id は、この順序で連続して実行され、入り混じることがあってはなりません。 そこで仕様は次のようになります。

(define-process SAFETY
  (xalt k I
    (! (list-ref as k)
       (! (list-ref bs k)
          SAFETY))))

計算木は次のとおりです。

クライアントプロセス

クライアントプロセスを以下のように定義します。 プロセス ID は抽象状態で定義して継承してあります。 これに加えて、unlock-type という状態変数を用意してあります。 ミューテックスのアンロックシステムコールでリターンを待つか、あるいはイベント同期で済ませるかを区別するための変数です。 変数 unlock-type の値がシンボル event の場合はイベント e-unlock を使います。 変数 unlock-type の値がシンボル channel の場合はチャネル unlock を使い、リターンを待ちます。 まとめてしまったので、ちょっと見にくくなってしまったかもしれません。 (図では省略してありますが、実際のガードは (eq? unlock-type 'event) 等です。)

  1. チャネル lock を使ってオペレーティングシステムにロックを要求します。これがロックシステムコールの呼び出しに対応します。
  2. イベント p.id を待ちます。システムコールからのリターンに対応します。
  3. ロックが獲得できたら、イベント a.id, b.id を順に発生させます。
  4. unlock または e-unlock を使ってロックを解放(ミューテックスをアンロック)します。
  5. チャネル unlock を使う場合はリターンをイベント p.id で待ちます。

システムプロセス

これからいろいろなミューテックスのモデルを紹介するので、先にシステムプロセスを定義しておきます。 システムプロセスも unlock-type をパラメータで指定できるようにしておきます。 これは使用するミューテックスのタイプに応じて指定します。 クライアントプロセスに渡すと同時に、同期リストに unlock を含めるのか e-unlock を含めるのか、どちらかを選択します。(両方いれちゃってもいいんですけどね。)

まずクライアントプロセスをインターリーブで並行合成してからミューテックスと合成します。 ミューテックスはインターリーブによる共有ではありませんが、インターフェイスにチャネルを使っているので、この順序で合成する方がずっと簡単です。

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

ご覧のとおり、システムプロセスはプロセスパラメータに MUTEX というものを持っています。 これは使用するミューテックスプロセスをパラメータ化しているのです。 実はこんなことができるんですね。他の人には内緒にしてください。 これによってミューテックスごとにシステムプロセスを定義したり、変更したりしなくても済みます。 これはコンポーネントの交換と正当性でコンテキスト C[P] と書いたものと同じです。SYS[MUTEX] というわけです。

ミューテックス MUTEX0

ではミューテックスを作っていきましょう。 最初のモデルでは、ロックシステムコールを呼び出したプロセスに対応するリターン、さらにアンロックとリターンを順番に発生させるだけのものです。 これは実質ユーザガイドに出ているものと同じです。

(define-process MUTEX0
  (? lock (k)
     (! (list-ref ps k)
        (! unlock (k)
           (! (list-ref ps k)
              MUTEX0)))))

どれか1つのプロセスがロックを獲得すると、他のプロセスはシステムコールを呼ぶことすらできないので、荒いモデルとなっています。

ミューテックス MUTEX1

MUTEX0 のアンロックをイベントに代えたモデルです。 以前に作ったものの中間の抽象度になります。

(define-process MUTEX1
  (? lock (k)
     (! (list-ref ps k)
        (! e-unlock
           MUTEX1))))

ミューテックス MUTEX2

以上は準備体操です。 ここからオペレーティングシステムのカーネルっぽい仕事をしましょう。ちょっと楽しいです(少なくとも私は)。

ミューテックスプロセスに2つのプロセスパラメータ m と ms を用意します。 パラメータ m はロックを獲得しているプロセスの ID を表します。 誰もロックしていない場合は #f です。 パラメータ ms は、ロック中にロックを要求したプロセスの ID を入れておくリストを表します。 つまりおおまかにいうと待ち行列ということです。 ms が空でないのは m が #f でない場合だけです。 つまり不変条件(プロセス不変条件 :P )は次のとおりです。

m = #f --> ms = ()

先に定義を見ていただきましょう。解説はそのあとで。

(define-process MUTEX2
  (MUTEX2A #f '()))

(define-process (MUTEX2A m ms)
  (alt
    (? lock (k) (not (memv k ms))
       (if (eqv? k m)                            ; (1)
           STOP
           (if m                                 ; (2)
               (MUTEX2A m (cons k ms))           ; (3)
               (! (list-ref ps k)                ; (4)
                  (MUTEX2A k ms)))))             ; (5)
    (? unlock (k) (not (memv k ms))
       (if (and m (eqv? k m))                    ; (6)
           (if (null? ms)                        ; (7)
               (! (list-ref ps k)                ; (8)
                  (MUTEX2A #f '()))              ; (9)
               (! (list-ref ps k)                ; (10)
                  (! (list-ref ps (car ms))      ; (11)
                     (MUTEX2A (car ms) (cdr ms))))) ; (12)
           STOP))))

まず基本方針として、何か正しくないことが起こった場合は STOP を使ってデッドロックさせるようにします。 こうすればデッドロック検査で見つけることができるからです。 (プログラムを書くときに assert などを使ってできるだけ早く問題が発覚するようにするのはよい習慣だといわれていますよね。あれと同じです。)

まずロックから見ます。もしロックを要求したプロセスが、すでにロックを所有するプロセスであった場合 (1) は停止することにします。 つまり再帰的なロックは許可しないということです。これはモデルを単純にするためだけの理由です。

次に、ロックされているかどうかをチェックします(2)。 すでにロックされている場合は、呼び出したプロセスを ms に加えます(3) 。 それ以外には何もしません。つまり呼び出したプロセスのリターンイベント p.k は発生しないので、待ち状態に入ります。 ロックされていない場合は、プロセスをリターンさせ(4)、ロックの所有者として記録します(5)。

続いてアンロックを見ます。 アンロックが実行できるのは、ロックされていて、かつ呼び出したプロセスが所有者である場合だけです(6)。 それ以外の場合は停止させます。

もし待っているプロセス ms が空ならば(7)、呼び出しプロセスをリターンさせ(8)、ロックを解放します(9)。

もし待っているプロセスがある場合は、まず呼び出したプロセスをリターンさせ(10)、次にリスト ms の先頭にあるプロセスにロックを渡します。 そのために先頭のプロセスをリターンさせ(11)、所有者として記録します(12)。 選ばれたプロセスは ms から取り除いておきます(12)。

さて、うずうずしている方もいるのではないかと思います (^^)。 気になるポイントが3つありますね。 1つ目はリスト ms にプロセス追加する位置、2つ目は同じことですが ms からどのプロセスを選ぶか、そして3つ目は unlock を呼び出したプロセスと選ばれたプロセスをリターンさせる順序です。 これは後でやりますので、ちょっと待ってください。

先に1つ補足をしておきます。lock, unlock それぞれにガードをつけてあります。 これはモデルを有限にするためのもので、ミューテックスの振る舞いに関係するものではありません。 クライアントプロセスがルールを守っていれば、待ち状態にあるプロセスがロックを要求することはないわけですけど、検査プログラムはそんなルールを知りませんからどんどん要求を出してしまうからです。 それを抑制するためのガードです。 システムプロセスの一部として使っている場合にはルールが守られるので必要ないのですが、ミューテックス単独で検査をする場合に備えて入れてあります。

ミューテックス MUTEX3

先に進む前に、MUTEX2 のアンロックをイベントに代えたバージョンも示しておきます。

(define-process MUTEX3
  (MUTEX3B #f '()))

(define-process (MUTEX3B m ms)
  (alt
    (? lock (k) (and (not (eqv? k m)) (not (memv k ms)))
       (if m
           (MUTEX3B m (cons k ms))
           (! (list-ref ps k)
              (MUTEX3B k ms))))
    (! e-unlock
       (if m                                      ; (1)
           (if (null? ms)
               (MUTEX3B #f '())
               (! (list-ref ps (car ms))          ; (2)
                  (MUTEX3B (car ms) (cdr ms))))
           STOP))))

抽象度を上げたために表現できなくなった点が2点あります。

このようにモデルを記述する抽象度によって表現できるものが変わるということがよくわかると思います。

ミューテックス MUTEX4

MUTEX2 に対して、ロック解放者と獲得者をリターンさせる順序を非決定的にしてみました。

(define-process MUTEX4
  (MUTEX4C #f '()))

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

実システムでは、応用によってどちらが優先されるか変わるので、一概にどちらがよいとはいえないでしょう。 プロセスに優先順位をつけられるオペレーティングでは、優先順位で解決する方がいいこともあるでしょう。

ミューテックス MUTEX5

今度はリスト ms に加える位置を、先頭から末尾に変えてみました。 これは真の意味での待ち行列になっています。 つまり、待ちに入った順序と同じ順序で次のロックが与えられるということです。

(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))))

ミューテックス MUTEX6

今度は待ちリスト ms からプロセスを選ぶ戦略を変えてみます。 もっとも一般性があるのは、プロセスを非決定的に選ぶことでしょう。 この場合、追加の位置はまったく問題ではなくなります。 (待っているプロセスが1つの場合、非決定性はありません。この場合も xndc を使っていますけど ^^;)

(define-process MUTEX6
  (MUTEX6E #f '()))

(define-process (MUTEX6E m ms)
  (alt
    (? lock (k) (not (memv k ms))
       (if (eqv? k m)
           STOP
           (if m
               (MUTEX6E m (cons k ms))
               (! (list-ref ps k)
                  (MUTEX6E k ms)))))
    (? unlock (k) (not (memv k ms))
       (if (and m (eqv? k m))
           (if (null? ms)
               (! (list-ref ps k)
                  (MUTEX6E #f '()))
               (ndc
                 (! (list-ref ps k)
                    (xndc j ms                     ; (*)
                      (! (list-ref ps j)
                         (MUTEX6E j (remv1 j ms)))))
                 (xndc j ms                        ; (*)
                   (! (list-ref ps j)
                      (! (list-ref ps k)
                         (MUTEX6E j (remv1 j ms)))))))
           STOP))))

ミューテックス MUTEX7

さらに一般化することができます。 いままでのモデルでは、システムコールを呼び出したプロセスがリターンする場合、リターンイベントの発生待ちのときには他のプロセスはシステムコールを発行することができませんでした。 これを可能にすることもできます。

リターン待ちをしているプロセスの ID を記録するプロセスパラメータ rs を用意します。 いままで即座にリターンしていた部分では、イベントを発生させる代わりに rs への登録を行います (1, 2)。

(define-process MUTEX7
  (MUTEX7F #f '() '()))

(define-process (MUTEX7F m ms rs)
  (alt
    (? lock (k) (and (not (memv k ms)) (not (memv k rs)))
       (if (eqv? k m)
           STOP
           (if m
               (MUTEX7F m (cons k ms) rs)
               (MUTEX7F k ms (cons k rs)))))   ; (1)
    (? unlock (k) (and (not (memv k ms)) (not (memv k rs)))
       (if (and m (eqv? k m))
           (if (null? ms)
               (MUTEX7F #f '() (cons k rs))
               (xndc j ms
                 (MUTEX7F j (remv1 j ms) (cons* k j rs))))  ; (2)
           STOP))
    (if (null? rs)  ; (3)
        STOP
        (xndc j rs  ; (4)
          (! (list-ref ps j)
             (MUTEX7F m ms (remv1 j rs)))))))

そして、システムコールの処理と並行して、リターン待ちプロセスがある場合は任意に(非決定的に)選んでリターンできるようにします (3, 4)。

尚、モデルを有限にするためのガードに rs も加えてあります。

以上、いくつかのモデルを見てきました。 ちょっと調子に乗りすぎた感じもありますけど、詳細なモデルではいろいろな選択ができることがわかると思います。 まだ可能性が残っていますしね :P 。

検査

では検査をしてみましょう。結果は次のとおりです。 いくつかのミューテックスについては、正当性関係も調べてみました。

すべてのミューテックスが安全性検査をパスしていることがわかります。

ミューテックス間の正当性検査をみると、MUTEX6 の一般性がわかります。 MUTEX7 はより一般的と思いましたが、MUTEX6 との違いが出ています。 それぞれの計算木は次のとおりです。

MUTEX7 ではリターンを待たずに次のプロセスのシステムコールを受け付けるので、当然といえば当然でした。

安全性検査なので、ほんとに a, b が発生しているのかどうか気になるかもしれません。 仕様をちょっと変えると、正当性検査で確認することができます。(つまり、ご自分でどうぞということです ^^;)

一番重要な質問は「結局どれがいいの?」ということでしょう。 それについてはいずれまた、ということで :P 。

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