Think Stitch
PRINCIPIA  最近の更新


アルファベット指定による並行合成

本日 SyncStitch version 1.1.0 をリリースしました。 今回のリリースではアルファベット指定による並行合成の演算子 apar と、その限量子バージョンである xapar をサポートしました。 そこで、アルファベット指定による並行合成について説明したいと思います。

ユーザガイドで、アルファベットというのはモデルの中で使用するすべてのイベントの集合ですと説明しました。 これを記号 Σ で表すのでした。 実は CSP でアルファベットを考える流儀には2つあるんです。 1つはユーザガイドで説明した考え方で、モデル全体で使うイベントの集合 Σ をアルファベットと呼ぶ流儀です。 もう1つは Hoare 先生オリジナルの文献である Communicating Sequential Processes で使われている流儀で、それぞれのプロセスが固有のアルファベットを持つと考えます。つまり、プロセスが発生させる可能性のあるイベントの集合を、そのプロセスのアルファベットというのです。 こちらの流儀では、プロセス P のアルファベットを α(P) と表します。 (α はギリシャ文字のアルファです。ご使用の環境/ブラウザによっては、A の小文字と区別がつかないかもしれません。)

それぞれの流儀で、CSP 理論の細かいところが所々違うので、文献を読むときにはどちらの流儀で書かれているのか気をつけた方がよいです。 Hoare 先生の流儀では、もともと SyncStitch が持っていた並行合成と、今回追加されたアルファベット指定による並行合成の区別はないのです。 以上で、文献を読む人のための前置きをおしまいにして、本題に戻ります。

アルファベットによる並行合成は、英語では Alphabetized parallel といいます。 「アルファベットによる並行合成」という日本語は私が勝手にそう呼んでいるだけなので、他の文献では違う呼び方になっているかもしれません(ごめんなさい)。 アルファベットによる並行合成に対して、いままでの並行合成はインターフェイス指定による並行合成(英語では Interface parallel)といいます。 どちらも指定されたプロセスを並行合成するという点では同じです。 違いは同期するイベントの指定方法です。

インターフェイス指定による並行合成では、指定されたプロセス間で同期するイベントおよびチャネルを、同期リストという形で指定しました。 これに対して、アルファベット指定による並行合成では、各プロセスが使うイベントとチャネルのリストを個別に指定します。

アルファベット指定による並行合成は、CSP の記号で次のように書きます。

P と Q が並行合成されるプロセスです。A はプロセス P が使うイベントとチャネルの集合、B は Q が使う集合です。 これを SyncStitch では次のように書きます。

(apar A P B Q)

これがどのようプロセスを表しているのかを順に説明します。 まず、SyncStitch で採用している流儀(Hoare 先生の流儀ではない方)での、プロセスのアルファベットについて説明します。

プロセスのアルファベット

アルファベット指定による並行合成で各プロセスに対して指定する、プロセスが使うイベントとチャネルのリストのことをプロセスのアルファベットといいます。 同じ言葉がいろいろ違うものを意味するので、ややこしくて申し訳ないです。

プロセスを定義すると、必然的にそのプロセスが発生しうるイベントは決まりますよね。 例えば次のプロセスを考えます。

(define-process P
  (alt (! a STOP) (! b (! c STOP))))

このプロセスはイベント a, b, c を発生する可能性があります。 Hoare 流でいえば α(P) = {a, b, c} です(細かいことをいうといろいろあるんですが)。 アルファベット指定による並行合成では、これとは別にイベントとチャネルのリストを指定するんです。

アルファベット指定による並行合成で、プロセス P のアルファベット A が指定されると、P は A に含まれているイベントとチャネルだけを発生することができます。 もしそれ以外のものを発生させる機会があったとしても、発生させることはできません。 制限されてしまうのです。

プロセス P の定義からわかる、発生させる可能性のあるイベントの集合を X すると、アルファベット指定による並行合成の元で発生させることのできるイベントは X と A の共通部分、下図のオレンジ色の部分に含まれるイベント・チャネルだけになります。 X からはみ出している部分(A ∖ X)はもともと記述にないので、発生しません。 A でカバーされていない X の部分(X ∖ A)は、制限されて発生させられない部分です。

これがアルファベット指定による並行合成の基本の1つです。

同期・非同期の区別 - プロセスが2個の場合

まずプロセスが2つの場合について説明します。

(apar A P B Q)

このとき、A と B の関係は一般的に次の図のようになります。

このとき、A と B に共通する部分(図のオレンジ色の部分)については、P と Q は同期しなければなりません。 つまりそこに含まれるイベントは、両方が発生しうるときだけ発生します。 これに対して、A だけに含まれるイベント(図の緑色の部分)は、プロセス P が単独で発生させることができます。 B についても同様です。 これがアルファベット指定による並行合成のルールです。 おおまかにいうと、次の等式が成り立つということです(ほんと、細かいことはいろいろあるのですが)。

(apar A P B Q) = (par (A ∩ B) P Q)

実際の例を見てみます。

(define-process P0
  (apar
    (list a b)
    (alt (! a SKIP) (! b SKIP) (! b1 SKIP))
    (list a c)
    (alt (! a SKIP) (! c SKIP) (! c1 SKIP))))

1番目のプロセスはアルファベットで指定されたイベント a, b だけを発生させることができます。 制限の効果を見るために、これ以外に b1 を発生させるようにしておきました。 2番目のプロセスは a と c です。 a は共通しているので、同期しなければなりません。これに対して b, c はそれぞれが独立して発生させることができます。 計算木は次のようになります。

 
 
 

a は同期していること、b, c はそれぞれが発生させていること、b1, c1 は発生しないことが確認できます。 終了に関しては par と同様です(実はこれが apar を par で置き換えられない理由なのですが・・・細かいことはいろいろあるのです)。

プロセスを3個以上並行合成する場合

アルファベット指定による並行合成がインターフェイス指定の並行合成で表せるのであれば、単なる糖衣構文ということになります。 (実際にはイベント発生に制限がかかる部分があるので、糖衣構文ではないのですが、それを除くと書き換えは可能です。) しかしプロセスが3つ以上あるときにはとても便利なのです。 なぜかというと、それぞれが自分のしゃべるイベントだけを指定すればいいので、どれが同期するか、とか、どの順序で合成するか、とか考えなくても済むからです。 (もちろんまったく考えなくてよいわけではありませんが。)

apar は3つ以上のプロセスを指定することができます。 一般的な構文は次のとおりです。

(apar A1 P1 A2 P2 A3 P3 ...)

このようにアルファベットとプロセス式を交互に何個も並べることができます。

プロセスが3個以上ある場合、同期の規則は次のようになります。 これは2個の場合も(当然)含んでいます。

  • イベント e がどの Ak にも含まれていなければ、発生しない。
  • イベント e が Ak だけに含まれていて、他のアルファベットに含まれていないければ、プロセス Pk は単独でイベント e を発生させることができる。
  • イベント e が2個以上のアルファベットに含まれている場合には、対応するプロセスすべてが同期しなければならない。すなわち、対応するすべてのプロセスが発生しうるときだけ発生する。

プロセスが3個ある場合について、もっと具体的に見てみます。

(apar A P B Q C R)

アルファベットを A, B, C とします。 これらの一般的な関係は下図のようになります。

  • 緑色の部分 A ∖ (B ∪ C) に含まれるイベントについては、プロセス P が単独で発生させることができます。
  • 水色の部分 (A ∩ B) ∖ C に含まれるイベントについては、プロセス P と Q だけが同期します。
  • オレンジ色の部分 A ∩ B ∩ C に含まれるイベントについては、プロセス P, Q, R すべてが同期します。
  • 対称的な他の領域についても同様です。

具体的な例を見てみます。 少しでもわかりやすくなるようにイベント名を工夫しました。 例えば、プロセス P だけが発生させるイベントを a, プロセス P と Q だけが同期するイベントを ab とする、等です。

(define-process P1
  (apar
    (list a ab ca abc)
    (alt (! a SKIP) (! a1 SKIP)
         (! ab SKIP) (! ca SKIP) (! abc SKIP))
    (list b bc ab abc)
    (alt (! b SKIP) (! b1 SKIP)
         (! bc SKIP) (! ab SKIP) (! abc SKIP))
    (list c ca bc abc)
    (alt (! c SKIP) (! c1 SKIP)
         (! ca SKIP) (! bc SKIP) (! abc SKIP)) ))

計算木は次のようになります。 (一部省略)(クリックすると拡大)

アルファベット指定による並行合成の限量子版 xapar

アルファベットを指定して、可変個数のプロセスを並行合成する場合には xapar を使うことができます。 構文は次のとおりです。

(xapar var range A P)

引数 var, range の意味は他の限量子と同じです。 range を評価した結果であるリストの要素1つ1つを変数 var が取るときの、プロセス P を並行合成します。 A はアルファベットです。 インターフェイス指定による並行合成 xpar と異なり、アルファベット A は変数 var のスコープ内にあります。 つまりアルファベット A の中で変数 var を参照することができます。 プロセスごとにアルファベットを指定するわけですから、これは当然ですね。

CSP の教科書に出てくる例では、アルファベット指定による並行合成がよく使われています。 いままでインターフェイス指定に書き換えていた方には面倒をおかけしました。

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