Think Stitch
PRINCIPIA  最近の更新


スケジューラ

並行プロセスの理論は CSP の他にもいろいろあります。 CSP と並んで有名なものの1つに π 計算 (π-calculus)というものがあります。 記号 π は円周率のパイですが、円周率とは関係ありません。 (このページをご覧になっている環境によっては π がちょっと見にくいかも知れません。)

π 計算の理論は Robin Milner さんによって作られました。 Milner さんは関数型プログラミング言語や定理証明の分野でも業績があるそうです。 残念なことに、数年前に亡くなられたそうです。

Milner さんの著作 Communicating and Mobile Systems: the π-calculus に、スケジューリングに関する面白い問題があります。 書かれている文章の感じからすると、実際にどこかであった話に基づいているようです。しかも何年も見つからなかったバグのようです。 当然のことながら本の中では π 計算を使ってモデル化・分析されているのですが、ここではこれを SyncStitch を使って分析してみたいと思います。

問題はこうです。 ある仕事を繰り返し実行する N 個のプロセス P0, P1, ...,PN-1 があるとします。 各プロセスが仕事を行う期間は重複してもかまいませんが、仕事を開始する順序は番号順でなければならないとします。 プロセス P0 から初めて P1, P2 と順に仕事を開始します。 PN-1 の後は P0 に戻ります。 これを繰り返します。 仕事を完了する順序に制約はありません。 しかし1つの仕事を完了してからでなければ、次の仕事を開始することはできません。 スケジューラの目的は、このようにプロセスを制御することです。

仕事の開始と完了を開始イベントと完了イベントで表します。 プロセス Pk の開始イベント、完了イベントをそれぞれ a.k, b.k とします。 例えば N = 3 の場合、具体的なイベントは a.0, b.0, a.1, b.1, a.2, b.2 となります。

ユーザガイドで取り上げたリーダ・ライタ問題と異なり、開始イベントと完了イベントは単にプロセスが行う仕事の開始と完了を表しているだけではありません。 この2つのイベントは、スケジューラがプロセスを制御するために使う相互作用のためのイベントです。 開始イベント a.k はプロセス Pk が仕事を開始してもよいというスケジューラからの許可を表します。 プロセス側から見れば仕事の開始要求ということになります。 完了イベント b.k は、プロセスがスケジューラへ仕事の完了を通知するイベントです。 スケジューラは各イベント a.k, b.k を提示するかどうかでプロセスを制御するわけです。

開始イベントと完了イベントを使うと、スケジューラが実現すべき条件を次のように表すことができます。

  • 開始イベントは a.0 からはじめて番号順に発生しなければなりません。最後のプロセスまでいったら先頭に戻ります。つまり循環的に実行します。
  • 各プロセスは、次の仕事を開始する前に、必ず前の仕事を完了させなければなりません。つまり、対応する a.k と b.k は交互に発生しなければなりません。
  • 上の2つの条件で禁止されていないイベントは、いつでも発生できるようにしなければなりません。

仕様のモデル化

仕様を表すプロセス SPEC を定義します。

イベント定義

define-event-list を使って、N 個の開始イベントと完了イベントを定義します。 ここでは N = 4 とします。

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

変数 as, bs の値はそれぞれ次のようなイベントのリストになります。

as = (a.0 a.1 a.2 a.3)
bs = (b.0 b.1 b.2 b.3)

(環境ウィンドウ等でのイベントオブジェクトの実際の表示は #<event:a.0:6> のようになります。)

個々のイベントの指定を簡潔に行うために、次の関数を用意しておきます。 これを使うと、k 番目の開始イベントと完了イベントはそれぞれ (a k), (b k) と表すことができます。

(define (a k) (list-ref as k))
(define (b k) (list-ref bs k))

プロセス S

仕様を表すプロセス SPEC の補助として、パラメータを持つプロセス S を定義します。 プロセス SPEC にパラメータを持たせると、初期状態や検査式など、参照する各所で初期値を指定しなければならなくなるからです。

プロセス S には2つのパラメータ k, ws を用意します。

  • k は次に仕事を開始するプロセスの番号です。
  • ws は仕事を実行しているプロセスの番号のリストです。

スケジューラの戦略は次のとおりです。

  • k 番目のプロセスだけが開始イベント a.k を発生できるようにします。ただし前の仕事を実行中の場合は、完了するまで待たなければなりません。
  • 仕事を実行中のプロセスはどれでも完了できるようにします。より具体的には ws に含まれているすべての番号 j について、完了イベント b.j を発生できるようにします。完了は k 番目のプロセスが実行中の場合であっても可能です。逆に実行中でないプロセスが完了イベントを発生させることは許しません。

k 番目のプロセスが仕事を実行中かどうかは、k が ws に含まれているかどうかでわかります。 実行中でなければ次の仕事を開始することができるので、イベント (a k) を提示します。 (a k) が発生したら、k を ws に加え、k をインクリメントします。 k が N - 1 だった場合には 0 に戻します。

仕事を実行中のプロセスはどれでも完了できるようにするには、ws に含まれているプロセス番号 i に対応する完了イベント (b i) をすべて提示します。 ws がリストなので、限量子 xalt を使います。 もし番号 j のイベント b.j が発生した場合には、j をリスト ws から取り除きます。

(define-process (S k ws)
  (alt
    (if (member k ws)
        STOP
        (! (a k) (S (mod (+ k 1) N) (cons k ws))))
    (xalt j ws
      (! (b j) (S k (remove j ws))))))

プロセス SPEC

プロセス S を使ってプロセス SPEC を定義します。 仕事は P0 から開始するので、パラメータ k の初期値は 0 です。 初期状態で実行中のプロセスはないので、パラメータ ws の初期値は空リスト () です。

(define-process SPEC (S 0 '()))

スケジューラの設計

仕事をする N 個のプロセスを制御するスケジューラを、リング状に接続した N 個のコンポーネントプロセスで構成します。 ちょっとかっこいいですね。 各コンポーネントプロセスを A0, A1, ..., AN-1 とします。 各コンポーネント Ak が仕事をするプロセス Pk に対応していて、Pk が行う仕事の開始と完了を制御します。

コンポーネントはすべて同じ構造であるとします。 仕事をするプロセスを制御するためのチャネル a, b と、仕事を開始する権利を受け渡しするためのチャネル c, d を用意します。 実際には a, b, c, d はイベントですが、接続するという感じを強調するためにチャネルと呼ぶことにします。

プロセス A の状態を2種類に分けます。 対応するプロセスが仕事を開始できる状態とできない状態です。 これを「開始する権利をもっている」という考え方で区別します。 権利を持つプロセス A は開始イベント a を発生させた後、チャネル c を使って次のプロセスに権利を渡します。 同時に権利を持っていない状態に遷移します。 チャネル c は次のプロセスのチャネル d につなげておきます。 チャネル d から権利を受け取った次のプロセスは、権利を持った状態に遷移します。 これをリング状につなげることによって、仕事を開始する順番を守ることができます。 スケジューラの初期状態では、プロセス A0 だけが権利を持っている状態で、残りはすべて持っていない状態とします。 プロセス A の動きから、リング上には権利を持ったプロセスが常に1つだけあることがわかります。

イベント定義

権利を受け渡しするためのイベント c.k を定義します。 a.k, b.k と同じように、個々のイベントを参照するための関数を用意しておきます。

(define-event-list cs N "c")

(define (c k) (list-ref cs k))

プロセス A

プロセス A を次のように定義します。

  • 状態 C と B は遷移 a と b の間にあるので仕事中の状態、状態 A と D は仕事をしていない状態です。
  • 状態 A と C は遷移 d と c の間にあるので仕事を開始する権利を持っている状態、状態 B と D は権利を持っていない状態です。状態 C は仕事を開始した後ですが、まだ権利を渡していないので、権利を持っている状態です。

状態 A と D は並行合成のときに参照するので、スコープをグローバルにします。

プロセス A の各状態には5つの状態変数 a, b, c, d と k を持たせます。 これは本当の変数ではなく、再利用のためのパラメータです。 状態変数 a, b, c, d には並行合成のときに具体的なイベントを指定します。 k にはプロセスの番号を入れます。 これは分析のときに見やすくするためで、動作には関係しません。ちょっとした工夫です。

プロセス SYS

プロセス A を N 個並行合成して、スケジューラの実装を表すプロセス SYS を作ります。 ここでは N = 4 とします。 プロセス P0 に対応するプロセス A0 の初期状態は、仕事を開始する権利を持っていて、かつ仕事をしていない状態 A とします。 後はすべて権利を持っておらず仕事中でもない状態 D を初期状態とします。 状態変数 a, b, c, d には接続図にあるとおりにイベントを指定します。 プロセス Ak の状態変数 d には、1つ前のプロセス Ak-1 の c を指定します。 A0 には AN-1 の c を指定します。

(define-process SYS
  (hpar cs
    (par '()
      (A 0 (a 0) (b 0) (c 0) (c 3))
      (D 2 (a 2) (b 2) (c 2) (c 1)))
    (par '()
      (D 1 (a 1) (b 1) (c 1) (c 0))
      (D 3 (a 3) (b 3) (c 3) (c 2)))))

偶数番目のプロセスと奇数番目のプロセス分けて並行合成を行うと、同期リストの指定が簡単になります。

検査

シンプルで見通しのよい設計に思われます。 これのどこに問題があるというのでしょう。 早速、設計したスケジューラが仕様を満たしているかどうか検査してみます。

デッドロックと発散の検査

まずデッドロックと発散がないことを確認します。検査を行うと、仕様、実装ともにデッドロックも発散もないことがわかります。

正当性検査

正当性検査を行うと拒否違反が見つかります。

拒否違反の分析

SPEC, SYS それぞれの計算木は次のとおりです。

仕様 SPEC の遷移リストウィンドウを見ると、仕様が発生させることのできるイベントは b.0, b.1, b.2, b.3 の4つであることがわかります。 仕事をする4つのプロセスがすべて仕事中なので、いずれもが完了できるからです。

環境ウィンドウでパラメータの値を見ると、仕様プロセスの状態が詳しくわかります。 パラメータ ws の値が (3 2 1 0) なので、すべてのプロセスが仕事中です。 パラメータ k の値が 0 なので、次に仕事を開始することができるのはプロセス P0 であることがわかります。 しかし ws に 0 が含まれているので、開始イベント a.0 は発生できません。

仕様 SPEC の極小受理 (b.0 b.1 b.2 b.3) だけです。 一方、SYS の遷移リストウィンドウを見ると、発生できるイベントは b.0, b.1, b.2 の3つであることがわかります。 この3つは仕様の遷移リストにもあるので、トレース違反はありません。 しかし、この3つのイベントからなる集合は仕様の極小受理を含んでいません。 b.3 がないからです。 したがって拒否違反があることになります。

SYS のプロセス木を見ると、3つのプロセスが状態 B、残りの1つが状態 C にいることがわかります。 最後に仕事を開始したプロセス A3 が権利を渡そうとしているのに、次のプロセス A0 は自分の仕事が終わるまで受け取らないので、結果として A3 が完了イベントを提示することができなくなっています。

これからわかることは、権利を持っていないときにはいつでも権利を受け取れるようにしておかなければならないということです。 具体的には状態 B でもイベント d を待たなければならないということです。

修正と確認

この点を修正したプロセス A を示します。 イベント d を先に受け取れるようにするということは、イベント b と d を任意の順序で発生できるようにするということです。

再度検査を実行すると、仕様を満たしていることが確認できます。

仕様と実装の一致

仕様 SPEC と実装 SYS を交換して比較検査を行うと、この2つは同じプロセスであることがわかります。

実は仕様 SPEC は非決定性を持っていないので、SPEC ⊑ SYS であれば SPEC = SYS となります。 仕様はトレースにあるイベントを拒否しないので、実装も拒否できず、同じイベントの遷移を持たざるを得ないからです。 仕様の意味から考えても、非決定性がないということは選択の余地がないということで、仕様の通りそのままに実装しなければならないということです。

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