Think Stitch
PRINCIPIA  最近の更新


インターリーブによるサービスの共有

SyncStitch ユーザガイドで取り上げたミューテックスのモデルをもう1度見てみます。

ミューテックを表すプロセス MUTEX は、2つのプロセス P, Q それぞれに対して、ロック・アンロックのためのインターフェイスを用意していました。

プロセス P, Q はそれぞれ自分用に用意されたインターフェイスを使って、ロックを獲得し、仕事をして、仕事が終わったらアンロックします。 仕事を表すイベントが p1, p2 と2つになっているのは、アトミック性を確認するためでした。

並行合成は次のようになっていました。まず直接には相互作用を行なわない P と Q を空の同期リストで合成し、それからインターフェイスを指定して MUTEX と合成しました。

(define-process SYS
  (par (list lock.p unlock.p
             lock.q unlock.q)
    (par '() P Q)
    MUTEX))

計算木は次のとおりでした。復習はここまでです。

インターフェイスを改名で抽象化する

さて、何をするかというと、プロセス P, Q それぞれに用意されたインターフェイス用のイベントを、同じものにしてしまいましょう。 改名を使って抽象化するということです。 2つの抽象イベント lock, unlock を用意して、lock.p と lock.q をどちらも lock に、unlock.p と unlock.q をどちらも unlock に改名してしまいます。

(define-process SYSA
  (rename `((,lock.p . ,lock)
            (,unlock.p . ,unlock)
            (,lock.q . ,lock)
            (,unlock.q . ,unlock))
    SYS))

計算木は次のようになります。

見ての通り、ミューテックスは機能していて、ちゃんと排他制御が行われています。 このミューテックスは、誰がロックを獲得しているか気にしていないので、ここまで抽象化してしまっても問題ないのです。

もし、ロックの所有者がもう1度ロックをかけることを許すような仕様の場合には、これはできません。 現実のミューテックスにはそういうものがありますよね。 参照カウントを使って入れ子の呼び出しを管理してくれるミューテックスです。

抽象化されたモデルの場合は、誰がロック所有者なのかわかりませんし、再度ロックをかけてきたプロセスが誰かもわかりませんから、入れ子の呼び出しはできません。 それでも、複数のクライアントがいて、誰がサービスを受けているかを気にしなくてよい場合は、最初からこの抽象度でモデル化してもよいということです。

インターリーブによるミューテックスのモデル

最初からクライアントを区別しないミューテックスを作ってみます。 このモデル化のかなめはインターリーブです。 いままでのモデルと違って、クライアントプロセス P と Q はサービスを受けるために同じイベントを発生させます。 これらが同期することはもちろん意図していません。 したがって P と Q はインターリーブさせます。 このインターリーブが、この抽象度でのモデル化を可能にしているということです。

以下の接続図のように、インターリーブを使った結合とサービスの共有は、いわばインターリーブを OR 条件のように使ったようなものです。 (一般に、接続線の間に弧を描いたら AND の意味でしょうけど、ここではどうしても線を引きたかったんです。ごめんなさい)

ミューテックス MUTEX

ミューテックスを表すプロセス MUTEX は次のようになります。 誰がロックしているのか、関知しません。

クライアントプロセス

各クライアントプロセスは、共有インターフェイスを使ってロック・アンロックを行います。

並行合成

システムは次のように並行合成します。

(define-process SYS
  (par (list lock unlock)
    (par '() P Q)
    MUTEX))

いままでと変わりはないのですが、インターリーブを使ってサービスを共有する場合には順序が大切です。

  1. まず先に、サービスを共有するすべてのクライアントプロセスをインターリーブで並行合成します。
  2. 次に、サービスを提供するプロセスと、インターフェイスを指定して並行合成します。

もしこの順序を守らず、先にクライアントの一部とサービスプロセスを合成してしまうと、あとから合成するクライアントが別のクライアントと同期してしまうことになります。 これに対して、インターフェイスがクライアントごとに用意されている場合は、それだけを指定して任意の順序で合成することができます。 (しかし、たいていは同期リストの指定が面倒になります。)

システムの計算木は次のようになります。 先に抽象化したものと同じものが得られました。

インターリーブによるセマフォのモデル

もう1つ例をご紹介します。インターリーブを使い、クライアントを区別しない抽象度でセマフォを作ってみます。

最高3個のプロセスが同時に使用できるリソースがあるとして、セマフォで制御することを考えます。 クライアントプロセスは5個あるとしましょう。

セマフォのインターフェイスイベントを wait と signal とします。 wait は使用許可(P 命令)、signal は使用終了通知(V 命令)を表します。

クライアントプロセスの個数を M = 5 個とし、そのうち最高 N = 3 個のプロセスが同時に処理を行えるとします。 各クライアントプロセスには番号で ID を振ります。 各クライアントプロセスの仕事をイベント p.0, p.1, ... で表します。 これらは define-event-list で一度に定義できます。 詳細はリファレンスマニュアルを見てください。

(define-event wait)
(define-event signal)

(define M 5)
(define N 3)

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

セマフォ SEM

セマフォプロセスは次のようになります。 セマフォは通過できる残りのプロセス数を表すカウンタ c を持っています。 初期値は N です。 カウンタが 0 でない間は使用許可(通過許可) wait を出します。 signal を受けたらカウンタの値を戻しておきます。

セマフォの計算木は次のようになります。 スタックとそっくりです。

クライアントプロセス

クライアントプロセスには番号 k で ID を振ります。 各プロセスは、まず wait でリソースの使用許可を取り、許可が取れたら仕事をします。 仕事は ID k に対応するイベント p.k で表します。 define-event-list で定義された ps はイベントのリストなので、list-ref を使って k 番目のイベントを発生させます。 仕事が終わったら signal を出して終了報告します。

(define-process (P k)
  (! wait
     (! (list-ref ps k)
        (! signal (P k)))))

並行合成

並行合成によってシステムを構築します。 手順に従い、まずクライアントをインターリーブで合成します。 次に、インターフェイスを同期リストに指定してセマフォと合成します。

(define-process SYS
  (par (list wait signal)
    (SEMAPHORE N)
    (xpar k (interval 0 M) '()
        (P k))))

クライアントの数 M が変更しやすいように、ここでは限量子 xpar を使いました。

(xpar k (interval 0 M) '() (P k))

xpar の構文は次のとおりです。

(xpar var range synclist process)

変数 varrange で表されたリストの各要素を値にとるときのプロセス process を並行合成します。 synclist は同期リストです。 結果、上の式は次のものと同じになります。

(par '() (P 0) (P 1) (P 2) (P 3) (P 4))

探査

システムの計算木の一部を示しました。 最初5個のプロセスはどれにも仕事を開始する権利があります。 どれが選ばれるかは非決定的で、セマフォも制御できません。 クライアントを区別しないのですから当たり前ですけど。

3個以内であれば、任意のプロセスが同時に仕事を行うことができます。 3個のプロセスが wait を発行すると、そのうちのどれかが仕事を終えるまで wait は受理されなくなります(図の選択されている状態です)。 仕事を行う順序も、signal が発行される順序も任意(インターリーブ)になります。 (図ではわかりやすく仕事と signal を分けていますが、実際にはこれらもインターリーブになります。)

2013/08/20
© 2013,2014,2015 PRINCIPIA Limited