Think Stitch
PRINCIPIA  最近の更新


プロセスの動的生成 2

引き続き、プロセスの動的生成に関するモデリングの技をご紹介します。

親プロセスの継続

並行合成 par で子プロセスを生成した場合、親プロセスは待ち状態に入り、すべての子プロセスが終了すると、親プロセスも終了しました。しかし、すべての子プロセスが終了した後で、親プロセスが仕事をしたいことがあります。並行合成 par と逐次合成 seq を組み合わせるとこれを実現することができます。

プロセス P はイベント c を受けたら2つの子プロセスを生成します。このとき、並行合成 par と、子プロセスの終了後に親プロセスが実行したいプロセスを、逐次合成 seq で連結しておきます。こうしておくと、すべての子プロセスが終了したときに、次のプロセスへ移行するからです。

(define-process P
  (! c
     (seq
       (par '()
         (! a1 SKIP)
         (! a2 SKIP))
       (! b SKIP))))

計算木は次のようになります。状態 A は2つの子プロセスが終了した状態です。ここから par が終了し、結果として seq 内での移行が起こって状態 B になります。

もし状態 A で持っている情報を状態 B に受け渡ししたい場合には、メモプロセスを使うことができます。

親子プロセス再び

子プロセス Q を生成して、完了待ちをする親プロセスの例をもう1度考えます。今回は、子プロセスの生成を2度行うことにします。

(define-process P
  (! c
     (par (list b)
       Q                           ; 1回目起動
       (! b                        ; 完了待ち
          (! c
             (par (list b)
               Q                   ; 2回目起動
               (! b SKIP)))))))    ; 完了したら親も終了

(define-process Q
  (! a (! b SKIP)))

このプロセスにはデッドロックがあります。なぜかわかりますでしょうか。

プロセスエクスプローラで見てみると次のようになっています。

選択されている状態は、2個目のプロセス Q のインスタンスが完了通知 b を出そうとしているところです。しかし状態は緑色ですから、遷移はありません。親プロセスは受け取りの準備ができています。なぜこの状態で b が発生できないか、わかりますでしょうか。

2つある par ノードはどちらもイベント b を同期リストに持つので、すでに終了してしまった1個目のプロセス Q のインスタンスもイベント b を発生させないと、イベントは発生できないのです。つまり3つのプロセスが同期しなければならなくなっています。このように CSP の同期は2つのプロセスだけでなく、3つ以上のプロセスの間でも同期することができるのですが、ここではそれが問題を起こしてしまいました。

解決案 1

これを解決する1つの方法は、子プロセスのインスタンスごとに異なる完了通知イベントを使うことです。ここでは b1, b2 とします。完了イベントが異なるので、子プロセスの定義も分けることになります。

(define-process P
  (! c
     (par (list b1)
       Q1
       (! b1
          (! c
             (par (list b2)
               Q2
               (! b2 SKIP)))))))

(define-process Q1
  (! a (! b1 SKIP)))

(define-process Q2
  (! a (! b2 SKIP)))

今度はデッドロックしません。

2個目のインスタンスも終了できるようになっています。

解決案 2

2つの子プロセスが同時に実行されるのであれば、完了通知イベントを分けることは必然です。しかし、この例のように順番に実行する場合にはやや無駄な感じがします。順番実行するのですから、逐次合成を使えば問題を解決できます。

2つのインスタンス実行を逐次合成 seq で連結します。こうすると、1つの完了通知イベントを使いまわすことができます。

(define-process P
  (seq
    (! c
       (par (list b)
         Q
         (! b SKIP)))
    (! c
       (par (list b)
         Q
         (! b SKIP)))))

(define-process Q
  (! a (! b SKIP)))
2013/08/03
© 2013,2014,2015 PRINCIPIA Limited