Think Stitch
PRINCIPIA  最近の更新


プロセス CHAOSA によるプロセスの抽象化

プロセス CHAOSA を使ってプロセスを抽象化する方法についてご紹介します。 ここでご紹介する方法は The Theory and Practice of Concurrency の Chapter 12 Abstraction で説明されている方法です。

図のように2つのプロセス A, B と相互作用するプロセス P を考えます。 P-A 間, P-B 間で使用するイベントの集合をそれぞれ L, H とします。 L と H の間に共通するイベントはなく、P が使うイベントはこれですべてだとします。 つまりプロセス P のアルファベットが L ∪ H であるということです。

一般に A から見たときの P の動作は B の動作に依存するでしょう。 それでも様々に B 入れ替えたときに共通する P の振る舞いというものがあるでしょう。 これがどのようなものかということを考えます。 つまり B の部分を抽象化する、あるいは B に依存する部分を抽象化するという感じです。

このようなことを考える理由は2つあります。 1つは文字通り B に依存しない P の動作を大まかに把握したいことがあるからです。 もう1つは、B に依存しない P の動作を知り、それに対して A を設計することができれば、どのような B を持ってきてもシステムはうまく動くからです。 もちろんこれは極端な場合で、一般にはそのようなことはできませんけれども、ここで紹介する考え方を応用すると、ある範囲の B に対して適切に動作する A というものを考えることができるようになります。 B の特定の実装に依存するのではなく、規格あるいは仕様で定められた B の動作に対して設計を行うというのは重要なことでしょう。

Eager 抽象化

すぐに思いつく抽象化の方法は、H に属するイベントを隠蔽してしまうことです。 そうすれば P-A 間で使うイベント L だけが残るからです。 この抽象化の方法を eager 抽象化といいます。 eager という言葉は「しきりに〜したがっている」という意味です。 なぜこのような名前が付いているのかという理由については後で説明することにして、先に例を見ていただくことにします。

Eager 抽象化の例 その1

中間管理職的なプロセス P の典型的な例として、次のようなプロセスを考えます。

黒で示したイベント c0, c1, c2 は L に属し、水色で示したイベント a0, a1, a2 は H に属するとします。 上側の遷移は単純な指示の伝達です。A が P に c0 を指示したら、P は B に a0 で伝達します。 下側はもう少し複雑な例で、A が P に指示 c1 を出すと、P は B に a1 で伝達します。 これを受けて B は仕事をし、結果を a2 で P に送ります。P はこれを c2 で A に伝達します。

Eager 抽象化、すなわち隠蔽による抽象化は次のように行うことができます。

(define-process E-P
  (hide (list a0 a1 a2) P))

抽象化の結果、計算木は次のようになります。

A から見た P の振る舞いだけが残っています。これは期待通りでしょう。

Eager 抽象化の例 その2

次にもう少し複雑な例を見てみます。仕事の指示だけでなく、途中でキャンセルの指示ができるようなプロセスを考えます。 名前は Q としました。

太い遷移で示したパスがふつうに仕事をするパスです。 これに加えて、キャンセルができるようにしてあります。 (少し補足すると、プロセス Q の利用者であるプロセス A は、キャンセルをする場合 ack と cancel を両方待つというルールにしてあります。 それからキャンセルが間に合わず、B から結果が返ってきてしまった場合は、単に結果を捨てています。)

先ほどと同じように eager 抽象化を行うと次のようになります。

(define-process E-Q
  (hide (list i.req i.ack i.cancel) Q))

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

これを見ると、ちょっと困ったことになっています。 キャンセルを受け取る状態が tau 遷移混在形になっているので、自発的に tau 遷移してしまい、キャンセルが受け取られる可能性がほとんどありません。 これは一般的な振る舞いではないでしょう。

このような結果になってしまう原因は、H に属するイベントを隠蔽によって単純に tau に置き換えたことにあります。 実際のプロセス B は、H に属するイベントを発生させることもあるし、発生させないこともあります。 例えばプロセス B は i.req を拒否することもあるでしょうし、i.ack が発生するまでしばらく時間がかかることもあります。 これに対して tau は自発的に発生してしまうので、このような状況を正しく表していません。

この抽象化が eager 抽象化と呼ばれるのはこのためです。 H に属するイベントが「発生したがっている」というわけです。 もし H に属するイベントが、提示すると必ず発生するイベント、つまりシグナルイベントであれば、 tau への置き換えは適切なものになります。 例えば B が表示装置で、H に属するイベントが出力イベントであるような場合です。 つまり eager 抽象化というのはシグナルイベントを抽象化するときに適切な抽象化であるということです。 (シグナルイベントについては SyncStitch ユーザガイドを見てください。)

Lazy 抽象化

ではシグナルイベントでない場合はどのようにしたらよいでしょうか。 先ほどもいいましたように、一般にプロセス B は H に属するイベントを発生させることもあるし、発生させないこともあります。 そのうちもっとも一般的な状況というのは、H に属するイベントの発生がもっとも非決定的な場合です。 つまり CHAOSH の場合です。

そこで B を CHAOSH で置き換えて P と並行合成を行い、しかるのちに H を隠蔽することを考えます。 少し乱暴ですが直感的ないい方をすると、B としてもっとも「やんちゃな」プロセスを選んで並行合成したときに、A からどのように見えるかを考えればいいわけです。

これを式で書くと次のようになります。

(hide H (par H P (CHAOS H)))

あるいは hpar を使って次のように書くこともできます。

(hpar H P (CHAOS H))

CSP の記号で書くと次のようになります。

\[ (P\,\ \underset{H}{||}\ \textit{CHAOS}_H) \setminus H \]

この抽象化の方法を lazy 抽象化といいます。 lazy とは「怠惰な」という意味です。イベントを発生させたりさせなかったりするという意味合いなのでしょう。

Lazy 抽象化の例

先ほどのプロセス Q を lazy 抽象化してみます。定義は次のようになります。

(define-process L-Q
  (let ((H (list i.req i.ack i.cancel)))
    (hpar H
      Q
      (CHAOS H))))

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

CHAOS に非決定性があるために、抽象化したプロセスにも非決定性が現れます。 H に属するイベントが発生しない方が選ばれたとしても、L に属するイベントの遷移があればデッドロックにはなりません。 しかし状態 Q4 のように H に属するイベントの遷移しかない状態では、デッドロックの可能性があります。 これは図で X とマークした状態です。

計算木が複雑なので、トレースモードで見てみることにします。

抽象化のおかげで、req に対して ack または cancel が発生するという全体像が一見してわかります。 状態3は状態 0 と遷移および極小受理集合が同じなので、同じ状態です。 これに対して状態 2 はすべてのイベント集合を拒否するので状態 0 とは異なる状態です。 cancel の後にはデッドロックに至るパスがあるからです。 状態 1 には極小受理が2つあります。これより ack だけ、あるいは cancel だけ待つのではいけないことがわかります。 両者の集合 {ack, cancel} は拒否ではないので、両方提示すれば必ずどちらかは同期することがわかります。 (ちなみに状態 Q3 から状態 Q に cancel の遷移を追加すれば、cancel は拒否しなくなります。)

混成抽象化

プロセス B が発生するイベント H のうち、一部がシグナルイベントである場合は、eager 抽象化と lazy 抽象化を組み合わせることで適切な抽象化を行うことができます。 これを混成抽象化(mixed abstraction)といいます。

H の部分だけでなく、システム全体で使用するシグナルイベントの集合を S とします。 すると混成抽象化は次のように表すことができます。

\[ (P\,\ \underset{H \setminus S}{||}\ \textit{CHAOS}_{H \setminus S}) \setminus H \]

上の記号の定義は元本に合わせました。 SyncStitch の場合は、H の要素のうちでシグナルイベントではないイベントのリスト N を持つ方が便利です。 この場合、式は次のようになります。

(hide H (par N P (CHAOS N)))

抽象度の調整

Lazy 抽象化ではプロセス B が最も非決定的である場合を考えました。 時には B の動作についてもう少し知識がある場合もあるでしょう。 それをプロセスで表して B と置き換えてみることができます。 置き換えるプロセスを変えることで、抽象度を調整していることになります。 これは特徴プロセスと似た考え方ですね。

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