Think Stitch
PRINCIPIA  最近の更新


プロセス RUNA

CSP の教科書には、いくつか名前のついたプロセスが出てきます。 そのうちの1つ RUNA を紹介したいと思います。

言葉で直観的に説明すると、プロセス RUNA は指定されたイベントを任意に発生させるプロセスです。 わかりやすく定義すると次のようになります。

(define-process (RUN A)
  (xalt e A
    (! e (RUN A))))

ここでプロセスパラメータ A はイベントのリストです。 指定されたイベントのリスト A に含まれる任意のイベントを発生させるプロセスというわけです。

例えばイベント a, b, c が定義されていて、(list a b c) を A に指定すると、RUNA の計算木は次のようになります。

パラメータ A にすべてのイベントのリスト、つまりアルファベットを指定すると、どんなイベントでも発生できるプロセスになります。 アルファベットは数学の記号では Σ で、これはふつう集合を表します。 SyncStitch では Events という擬似変数を使うことができます。こちらは集合ではなくイベントのリストです。 残念ながら擬似変数はプロセス定義の中でしか使うことができないので、プロセスの初期状態の指定では使うことができません。 そこで次のように補助的なプロセスを定義します。

(define-process RUN-ALL (RUN Events))

イベントとチャネルが次のように定義されているとします。

(define-event a)
(define-event b)
(define-event c)

(define-channel ch (x) '((0) (1)))

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

たとえば次のチャネル定義を加えると...

(define-channel ch2 (x y) '((0 0) (0 1) (1 0)))

プロセス定義を修正しなくても、自動的に遷移が追加されます。

チャネルが指定できるようにする

プロセス RUNA を実際に使うときには、イベントだけでなくチャネルを指定できた方が便利です。 これを実現する方法はいくつかありますが、ここでは関数 channel-events を使うことにします。 関数 channel-events はアルファベット Events と同じくプロセス定義の中だけで使うことができる関数で、チャネルを与えると、そのチャネルに属するすべてのチャネルイベントをリストにして返してくれます。 順序は不定です。 これを使うとプロセス RUNA を次のように定義することができます。

(define-process (RUN A)
  (let ((es (filter event? A))
        (cs (filter channel? A)))
    (let ((chevs
           (append-map channel-events cs)))
      (RUNx (append es chevs)))))

(define-process (RUNx B)
  (xalt e B
    (! e (RUNx B))))

まず与えられたリスト A をイベントとチャネルに分類します。 次に、各チャネルについて、関数 channel-events を使ってチャネルイベントのリストを取得し、それらを連結します。 最後に分離しておいたイベントのリストを連結すれば、すべてイベントに変換できたことになります。

例えばパラメータ A に (list a b ch) を指定すると、次のようになります。

イベントに変換した後のパラメータ B の値は次のとおりです。

プロセス RUNA とトレース比較

セマフォによるバリア(ランデブ) のところで、トーレスによる比較も精度の荒い正当性検査と考えることができるという話をしました。 (trace Q P) という検査は次のような正当性関係だと考えることができます。 区別のために文字 T をつけてあります。トレースによる比較という意味です。

定義は次のとおりでした。

プロセスを指定する順序が逆であることに注意してください。 これの意味するところは、実装 Q が実行できることは、仕様 P がやってもよいということの中に入っていなければならないということでした。 言い換えれば、仕様がやってよしという以外のことをしてはいけないということです。 これを安全性というのでした。

この点から考えると、アルファベットを指定したプロセス RUNΣ はすべてのイベントを発生することができますから、もっとも一般的なプロセスであるということができます。 つまりプロセス RUNΣ を仕様と見なすと、どんなプロセス P もこれを満たすということです。

トーレス比較の場合は、プロセスを区別する精度が荒いせいで、どんなプロセスを仕様として与えられても満たしてしまうプロセスが存在しました。 それはプロセス STOP です。

プロセス STOP は何もイベントを発生させませんから、悪いことが起こるはずがありません。 これはコードを書かなければバグは起こらないということに対応しています :P

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