Think Stitch
PRINCIPIA  最近の更新


メモプロセス

逐次合成 seq によってプロセスを再利用する方法には1つ欠点があります。それは呼び出されるプロセスが呼び出し元のプロセスに値を渡す方法がないという点です。下請けプロセスが結果を返す方法がないということです。

例えば、チャネル rch からデータを受信して返すことを仕事とするプロセス SUB を考えます。プロセス SUB は受信したデータを呼び出し元のプロセス P に返したいのですが・・・

(define-process P
  (seq
    SUB
    ???))

(define-process SUB
  (? rch (x) ???))

プロセス SUB は受信したデータ x をどのように呼び出し元に渡せばよいのかわかりません。同じく、呼び出し元プロセス P もどのように受け取ればよいのかわかりません。この問題はメモプロセスというプロセスを使うと解決できます。

メモプロセスは、その名の通り、受け取ったデータを覚えておいて、後で返してくれるプロセスです。

メモプロセスを使う場合の典型的な構造は次のようになります。

はじめに、主プロセスはサブプロセスを呼び出します。これは逐次実行 seq によります。もしサブプロセスにデータを渡す必要があるときには、プロセスパラメータを使うことができます。(図ではこれを点線で示してあります。)

サブプロセスは仕事をした結果として主プロセスに渡したいデータを、チャネル mwr を通じてメモプロセスに渡します。その後で SKIP によって終了します。すると制御は主プロセスに戻ります。

メモプロセスは主従プロセスとは並行して走ります。主プロセスはサブプロセスの結果をメモプロセスから受け取ることができます。

モデリング

プロセス MEMO

メモプロセスは受け取ったデータを保持するためのプロセスパラメータ m を持ちます。メモプロセスはデータの読み出しも書き込みもいつでもできるようにします。データの読み出しはチャネル mrd を通じて行います。クライアントから見て、読み出しは受信なので、メモプロセスから見ると送信になります。書き込みはチャネル mwr を通じて行います。受け取ったデータでプロセスパラメータを更新します。

(define-process (MEMO m)
  (alt
    (! mrd (m) (MEMO m))
    (? mwr (x) (MEMO x)) ))

メモプロセスの計算木はつぎのようになります。

プロセス SUB

プロセス SUB の仕事は、チャネル rch からデータを受信して、それを呼び出し元に返すことです。これを実現するために、SUB は受信したデータをメモプロセスに渡します。その後、主プロセスに制御を戻すために SKIP で終了します。

(define-process SUB
  (? rch (x)
     (! mwr (x)
        SKIP)))

主プロセス P

主プロセス P ははじめに seq を使ってプロセス SUB を呼び出します。プロセス SUB が仕事を終えると制御が戻ります。このとき結果データがメモプロセスにあるので、これをチャネル mrd を通じて引き取ります。この例では、データを受け取れたことを確認するために、チャネル ch への出力を加えてあります。

(define-process P
  (seq
    SUB
    (? mrd (x)
       (! ch (x) STOP))))

システムプロセス SYSTEM

最後にシステム全体の動作を表すプロセス SYSTEM を並行合成によって定義します。プロセス SYSTEM は主プロセス P とメモプロセス MEMO の合成です。プロセス SUB は主プロセス P から呼び出されるので、並行合成には参加しません。

(define-process SYSTEM
  (par (list mrd mwr)
    P
    (MEMO 0)))

シミュレーション

システムの動作の一部を計算木で見てみます。例えば値 1 を受信した遷移を見ていくと、確かに主プロセスが値 1 を受け取ったことを確認できます。


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