Think Stitch
PRINCIPIA  最近の更新


プロセス CHAOSA

今回は CHAOSA というプロセスをご紹介します。 言葉で説明すると、指定されたイベントを任意に発生させる可能性があるプロセスのうちで、もっとも非決定的で発散していないプロセスです。 比較でいうとプロセス RUNA はもっとも決定的なプロセスということになります。 なぜなら A に含まれるイベントをどれも拒否しないからです。 逆にいえば CHAOSA は A に含まれるどのイベントも発生させる可能性があるのに、どれも拒否します。 イベントの集合 A 全体を指定したとしても拒否するということです。

プロセス RUNA のときと同じように、わかりやすくするために、まず A がイベントだけを含んでチャネルを含まない場合の CHAOSA 定義をします。

(define-process (CHAOS A)
  (ndc
    STOP
    (xalt e A (! e (CHAOS A)))))

比較のために、RUNA の定義も再掲します。

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

最初の部分でプロセス STOP との非決定的選択が入っている点が異なります。 計算木は次のようになります。

デッドロック状態に至る非決定的な分岐があるので、すべてのイベントを拒否するわけです。

プロセス CHAOSA と RUNA はどちらも指定されたイベントを発生させることができるので、トレースによる比較では区別することができません。 しかし拒否を含めて正当性を比較すると、CHAOSA の方がより非決定的であることがわかります。

プロセス CHAOSA をトレースモードで観てみると、次のようにすべてのイベント集合を拒否することが分かります。 極小受理が空集合だけということは、指定されたイベントの集合 A の任意の部分集合を拒否するということです。 これには A 自身も含まれます。

もっとも非決定的なプロセスというと、次のようなプロセスを想像するかもしれません。

しかしこのプロセスはイベントの集合 A 全体を拒否しません。 トレースモードで観てみると次のようになります。

極小受理集合が {{a}, {b}, {c}} ですから、極大拒否集合は {{b, c}, {c, a}, {a, b}} となります。 したがって、このプロセスの拒否は次のようになります。

{{}, {a}, {b}, {c}, {a, b}, {b, c}, {c, a}}

つまり A = {a, b, c} 以外はすべて拒否するということです。 この1点において、CHAOSA の方が非決定的だということです。 実はこのプロセスにも DFA という名前がついています。

拒否の復習ついでに、もう1つ例として以下のプロセス P を見てみます。

極大拒否集合は {{a}, {b}, {c}} になりますから、このプロセス P の拒否は次のようになります。

{{}, {a}, {b}, {c}}

これはプロセス DFA の拒否集合の部分集合ですから、P の方がより決定的であるということになります。 実際に検査をすると、次のようになります。

つまり、非決定的な方から並べるとつぎのような順序になっているということです。

プロセス RUNA を検査プロセスとして各プロセスと並行合成してみると、CHAOSA だけがデッドロックを持っていることがわかります。

(define-process S_CHAOS
  (par A (CHAOS A) (RUN A)))

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

プロセス RUNA のときと同じようにチャネル関連の関数を使うと、プロセスパラメータ A にチャネルを含むリストを指定することのできるプロセス CHAOSA を定義することができます。

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

(define-process (CHAOSx B)
  (ndc
    STOP
    (xalt e B (! e (CHAOSx B)))))

トレースと拒否による比較でもっとも"大きい"プロセスは?

プロセス RUNA のところで、プロセス STOP がトレース比較の元でどのようなプロセスに対しても正当性条件を満たしてしまうという話をしました。 同じように、拒否を含めた正当性比較でもそのようなプロセスがあります。 正当性関係を大小関係のように考えて、右辺にあるプロセスの方が"大きい"と表現することにすると、もっとも大きいプロセスということになります。 それはイベントを発生させる可能性を持たず、起動したら直ちに発散するプロセス DIV です。 プロセス DIV は、補助的なイベント x を使って次のように定義することができます。

(define-process DIV
  (hide (list x) DIV0))

(define-process DIV0
  (! x DIV0))

プロセス DIV は発散していて、かつイベントを一切発生させないので(SyncStitch の流儀では)拒否を持ちません。 したがってプロセス STOP よりもさらに"大きい"プロセスということになります。

補足

Hoare 先生の教科書では CHAOS という名前のプロセスはここで説明したものとは異なるプロセスを表しているので注意が必要です。 そこでは CHAOS が任意のイベントを発生させることができて、もっとも非決定的で、かつ発散しているプロセスとして定義されています。 ここでは、以前にも紹介した Roscoe 先生の The Theory and Practice of Concurrency での流儀にしたがって CHAOSA と発散するプロセスを分けています。

Roscoe 先生の本では発散するプロセスを表すのに小文字で太文字の div が使われています。 しかし小文字の div は Scheme の割り算の関数名と衝突してしまうので、ここでは大文字で表しました。

発散するプロセスの拒否について、SyncStitch がどのような定義を採用しているかについては SyncStitch ユーザガイドを見てください。

完全のために説明抜きでもう1つ補足させてください。 SyncStitch ではサポートしていませんが、CSP の意味論にはもう1つ、よく使われるものとして失敗発散モデルというものがあります。 それに基づいた正当性比較では、また少し違った"大小関係"が現れます。 興味のある方は Roscoe 先生の本を見てください。

2013/10/12
© 2013,2014,2015 PRINCIPIA Limited