Think Stitch
PRINCIPIA  最近の更新


非同期通信で同期型通信を実現する

同期型の相互作用で非同期の相互作用を表すことは簡単です。間にキューを入れればよいだけですから。 逆に、非同期の相互作用がプリミティブとして与えられている場合に、同期型の相互作用を実現できるのかどうか以前から気になっていました。 一般論を展開するというようなことは手に余りますので、ささやかな例で考えてみたいと思います。 プロトコルを専門にされている方からは笑われてしまうようなことかもしれませんが、よろしかったらお付き合いください。 誤りや、もっとよい方法があるとご教示いただければ幸いです。

非同期通信のモデル

非同期通信をキューで表すことにします。CSP で記述するのでキューはプロセスになります。 実際には非同期通信プリミティブを提供するオペレーティングシステムであったり、プログラミング言語要素であったり、あるいは物理的な通信路であったりします。 本質的なことは、文字通り送信と受信とが同期しておらず遅延があることと、キューの出口を除いて中をのぞき見たり操作したりすることはできないということです。そういう制限の元で問題を考えることにします。

プロセスの構成を図示すると以下のようになります。CSP の同期型通信で非同期通信を表し、その上で同期型通信を表すというちょっとややこしいことになりますけど :P

同期相互作用のためのプロトコル

同期通信を実現するためのプロトコルを考えて見ます。 1対1通信の場合は1組のメッセージ交換でできそうです。 本来であれば双方向通信なので対称性がありますけど、ここでは対称性を壊した解を考えます。 プロセス P が主導権を持っていて、プロセス Q は受身だとします。

プロセス P が同期したいと思ったときには、同期要求メッセージ RSY を送ります。 プロセス Q はこれを受けた後、同期できる場合には同期応答 ASY を返します。

逆にプロセス Q が先に同期したいと思ったときには、プロセス P が同期要求 RSY を送ってくるのを待ちます。 送られてきたら同期応答 ASY を返します。つまり同じプロトコルです。

"イベントの選択"がある場合にはもう少し工夫が必要になります。例えば以下の図のようにプロセス P がプロセス Q, R と相互作用する場合を考えます。どちらの通信路においてもプロセス P が主導権を持っているとします。

プロセス P が Q, R いずれかとの同期を選択する場合は、双方に対して同期要求 RSY を送ることになります。

これに対してプロセス Q が先に同期応答 ASY を返してきた場合、プロセス R に出した同期要求をキャンセルしなければなりません。 そこでキャンセル用のメッセージ CAN を用意することにします。

同期要求をキャンセルできるようにすると、逆に同期が確定する時点が曖昧になってしまいます。そこで同期が確定したことを表すメッセージ SYE も用意します。

まず同期が成立するシーケンスは次のようになります。

キャンセルの場合には同期確定 SYE の代わりにキャンセル要求 CAN を送ります。

上のシーケンスでは同期応答 ASY が間にありますけれども、これは必然ではありません。実際、キャンセル要求と同期応答は交錯することがあります。

仕様

まずはじめに仕様を考えます。何を持って正しいとするかという問題については次のように考えました。

以下の図のように3つのプロセスがあってそれぞれ通信路で接続されているとします。

各プロセスは次の中から任意に1つを選んで実行するとします。

  1. 左側にあるプロセスとだけ同期する。
  2. 右側にあるプロセスとだけ同期する。
  3. 2つのプロセスとの同期を選択する。

(デッドロックがありますけど、それも仕様のうちです :P)

各プロセスがどの選択肢を選んだのかを表すイベント e.p.k と、同期後に発生させるイベント w.k.i.j を用意します。 ここで p はプロセスの種別(P = 0, Q = 1, R = 2)、k は上の選択肢(0 オリジンに変えて 0, 1, 2)、i は選択かどうか(非選択 = 0, 選択 = 1)、j は左右の区別(左=0, 右=1)です。 後者は同期した2つのプロセスがそれぞれ発生させることになります。

例えばプロセス P が同期選択を選び、プロセス Q は P との同期を選んだ場合、以下のようなトレースがありえます。

e.0.2         ; P select
e.1.1         ; Q right
c0            ; sync
w.1.0.1       ; Q
w.0.1.0       ; P

e も w も発生順序は任意です。加えてプロセス R の発生させる e が混じることがあります。

この振る舞いを非同期通信上の同期通信で実現した場合、c0 の部分はより複雑なプロトコルに置き換わることになりますが、e と w だけを含むトレースは一致するはずです。 そこでここでは、同期のためのプロトコルで使用するイベントを隠蔽したときにトレース集合が一致するという必要条件を仕様と考えることにします。

仕様モデル

では具体的に仕様モデルを作ることにします。上記の動作を何回か繰り返すことにします。繰り返しの回数を N とします。 最初は N = 1 としておきます。いつものように簡単な方から調べるのはよい戦略です。

(define N 1)

イベント定義

仕様は同期型通信で作ります。そのためのチャネルを用意します。 チャネルにしたのは値を渡すためではなく、単にイベントの集合として使うためです。

(define-channel c (k) '((0) (1) (2)))

次に、各プロセスの選択を表すイベントを定義します。

(define-channel e (k j) (combinations '((0 1 2) (0 1 2))))

イベントの最後は同期後に発生させるイベント w です。動作を繰り返すことにしたので、パラメータをもう1つ追加して何番目の同期によるものかがわかるようにします。

(define-channel w (p t c n)
  (combinations `((0 1 2) (0 1) (0 1) ,(interval 1 (+ N 1)))))

プロセス定義

各プロセスは以下のように共通に定義できます。

(define-process (P k n)
  (if (= n 0)
      STOP
      (alt
        (! e (k 0)
           (! c (k)
              (! w (k 0 0 n)
                 (P k (- n 1)))))
        (! e (k 1)
           (! c ((mod (+ k 2) 3))
              (! w (k 0 1 n)
                 (P k (- n 1)))))
        (! e (k 2)
           (alt
             (! c (k)
                (! w (k 1 0 n)
                   (P k (- n 1))))
             (! c ((mod (+ k 2) 3))
                (! w (k 1 1 n)
                   (P k (- n 1)))))))))

プロセスパラメータ k はプロセスの番号(0, 1, 2)、n は動作を繰り返す回数です。 見ての通り、3つの選択肢の中から任意に1つを選び、対応するイベント e を発生させたあと同期します。 同期したら、選択と同期先に対応するイベント w を発生させます。

仕様システムプロセス定義

プロセス P を3つ合成してシステムプロセスを作ります。 アルファベット指定による並行合成演算子の限量子版を xapar を使いました。 それぞれが発生させるイベントを指定します。

(define-process RSYS
  (xapar k '(0 1 2)
    (cons* ($ e k 0) ($ e k 1) ($ e k 2)
           ($ c k) ($ c (mod (+ k 2) 3))
           (map (lambda (x) (apply $ w k x))
                (combinations
                 `((0 1) (0 1) ,(interval 1 (+ N 1))))))
    (P k N)))

最後に通信で使うチャネル c を隠蔽して仕様が完成します。

(define-process HRSYS
  (hide (list c) RSYS))

非同期通信による同期通信モデル

次に設計モデルを作ります。

イベント・チャネル定義

キューの長さを表すパラメータを定義しておきます。

(define QL 2)

キューに格納できるメッセージ、いいかえるとキューの入出力チャネルの定義域を決めます。 通信の主導権を握っているプロセスから受身のプロセスに向かう方向を"下り"、逆の方向を"上り"と定義します。 各メッセージはシンボルで表します。下りのメッセージは同期要求 RSY, 同期確定 SYE, そしてキャンセル CAN です。 上りは同期応答 ASY だけです。

(define DD '((RSY) (SYE) (CAN)))
(define DU '((ASY)))

各キューの入出力チャネルを定義します。以下の図を参照してください。

(define-channel qdi0 (m) DD)
(define-channel qdo0 (m) DD)
(define-channel qui0 (m) DU)
(define-channel quo0 (m) DU)

(define-channel qdi1 (m) DD)
(define-channel qdo1 (m) DD)
(define-channel qui1 (m) DU)
(define-channel quo1 (m) DU)

(define-channel qdi2 (m) DD)
(define-channel qdo2 (m) DD)
(define-channel qui2 (m) DU)
(define-channel quo2 (m) DU)

キュープロセス

キューを用意します。入出力チャネルをプロセスパラメータで総称化してあります。

(define-process (QUE in out q)
  (alt
    (if (null? q)
        STOP
        (! out ((car q)) (QUE in out (cdr q))))
    (if (= (length q) QL)
        STOP
        (? in (m) (QUE in out (append q (list m)))))))

プロセス P

プロセス P は2つの通信路どちらについても主導権を持っています。したがって同期をする場合は自ら同期要求 RSY を送信します。

(クリックで拡大)

選択の場合のシーケンスは以下のようになっています。キャンセルと同期確定の順序は任意ですが、ここではこのようにしました。

状態 P12 で選択を行っています。念のために補足しておくと、ここでは2つのキューの出口を監視しているということです。先に受信割り込みが発生した方を選ぶと考えてもよいですし、交互にポーリングを行って、先に受信した方を選ぶと考えてもかまいません。

プロセス R

プロセス R はどちらの通信路も受身になります。この場合、同期要求 RSY をいつでも監視していて、状態として持っておくという選択肢もあります。ここではそのつどキューを見にいくことにします。このモデルの抽象度ではあまり違いはないと思います。

(クリックで拡大)

同期応答 ASY を送ったら同期確定 SYE またはキャンセル CAN を待ちます。キャンセルの場合は同期要求 RSY 待ちから再試行します。

例えば状態 R3 に加えて R2 でもキャンセルを待つこともできます。そうすると無駄な同期応答 ASY の送信を避けることができる可能性が高まりますけど、質的な振る舞いとしては変化ないと思います。気になる人は調べてみてください。

プロセス Q

プロセス Q は上下線混在です。

(クリックで拡大)

選択の場合、ここでは無条件にまず同期要求 RSY を出してしまうことにしました。先にもう1つの通信路からの同期要求 RSY を確認する方法もあります。こちらについてはあとで調べることにします。

状態 Q14 ではまだキャンセル CAN される可能性があるので、通信路1へのキャンセル送信は同期確定後になります。

システムプロセス

プロセス P, Q, R と6個のキューを並行合成してシステムプロセスを作ります。

(define-process SYS
  (apar
    (cons* qdi0 quo0 qdi2 quo2
           ($ e 0 0) ($ e 0 1) ($ e 0 2)
           (map (lambda (x) (apply $ w 0 x)) wdom))
    (P0 N)
    (cons* qui0 qdo0 qdi1 quo1
           ($ e 1 0) ($ e 1 1) ($ e 1 2)
           (map (lambda (x) (apply $ w 1 x)) wdom))
    (Q0 N)
    (cons* qui1 qdo1 qui2 qdo2
           ($ e 2 0) ($ e 2 1) ($ e 2 2)
           (map (lambda (x) (apply $ w 2 x)) wdom))
    (R0 N)
    (list qdi0 qdo0) (QUE qdi0 qdo0 '())
    (list qui0 quo0) (QUE qui0 quo0 '())
    (list qdi1 qdo1) (QUE qdi1 qdo1 '())
    (list qui1 quo1) (QUE qui1 quo1 '())
    (list qdi2 qdo2) (QUE qdi2 qdo2 '())
    (list qui2 quo2) (QUE qui2 quo2 '())))

仕様と比較するために、非同期通信で使うイベント、つまりキューの入出力チャネルを隠蔽します。

(define-process HSYS
  (hide (list qdi0 qdo0 qui0 quo0
              qdi1 qdo1 qui1 quo1
              qdi2 qdo2 qui2 quo2)
    SYS))

検査

まず繰り返し回数を N = 1 として検査します。以下の通り、2つのトレース集合は一致します。ここまではうまくいっているようです。

続いて N = 2 としてみます。するとトレース違反が見つかります。

プロセスエクスプローラを開くと、以下のようになっています。

(クリックで拡大)

トレースを見ると、通信路 c0 と c1 上で同期が可能な状態で w.0.0.0.1 が発生していますから c0 の方が同期したことがわかります。したがって次に発生すべきイベントは、仕様どおり w.1.1.1.2 です。これに対して設計モデルはプロセス Q が w.1.1.0.2 を発生するといっているので何かがおかしいことになります。

パスをさかのぼっていくと、何が悪いのかわかります。下の環境ウィンドウを見るとわかるように、プロセス Q は状態 Q10 にいるのに、なぜかキューには同期応答 ASY がすでに入っています。結果として、プロセス P はこのあと発行する同期要求 RSY に応答があったと勘違いして同期を確立してしまいます。 したがって、設計モデルが発行している w.0.0.0.1 は実は間違いによるもので、仕様と異なり、設計モデルは Q-R 間で同期していたのでした。

(クリックで拡大)

このようになった原因は、1回目の同期の際にキャンセルされた P-Q 間同期の同期応答 ASY が残っていたからです。これは典型的なキャンセル問題ということになります。

設計モデルの修正:シーケンサの導入

これを解決するにはキャンセルされた同期要求に対応する同期応答を捨てることです。 しかしキューの中を覗いたり操作したりすることはできませんから、受信した際に捨てるということになります。 ところがメッセージを見ただけでは捨てるべきものかどうか判断することができません。これに対処する定石の1つは、メッセージに識別子をつけることです。いわゆるシーケンサです。

まず同期要求メッセージを拡張して識別子がつけられるようにします。メッセージを (RSY id) とします。 id は主導権を握っている側が要求のたびに異なる値を指定します。ここでは同期の繰り返し回数を指定することにします。

同様に同期応答も (ASY id) と拡張します。受け取る側は同期要求 (RSY id) で指定された id と同じ識別子をつけて同期応答 (ASY id) を発行します。こうすると過去にキャンセルされた同期要求に対応する同期応答には異なる識別子がついていますから、判別して捨てることができるわけです。

(クリックで拡大)

受信側では受け取ったメッセージを状態変数に保存しておき、同期応答を発行するときにそこから識別子を取り出して付加します。

(クリックで拡大)

検査2

N = 2, QL = 2 として検査を行うと、トレース違反が見つかります。

プロセスエクスプローラを開くと以下のようになります。

(クリックで拡大)

発生できるはずのイベント w.0.1.1.1 および w.2.0.0.1 が遷移リストにありません。 それもそのはずで、プロセス P はまだ状態 P10 にいて、同期要求 RSY を発行していません。

なぜこんなことになるかというと、環境ウィンドウを見るとわかります。 プロセス Q が前回の同期要求とキャンセルを引き取っていないので、キューがあふれているからです。 実際、キューの大きさを QL = 4 とすると検査をパスします。

応答優先への設計変更

キューがあふれるのを避けるために、できるだけキューを先に調べるようにしてみます。

まずプロセス Q の場合は、同期要求 RSY の送信と受信を同時に待つようにします。キューがあふれていると送信はブロックしますが、こうしておけば受信はできます。実際のコードでも送信可能通知やポーリングによって同様の効果を得ることができるでしょう。

(クリックで拡大)

プロセス P については、固定された順序での同期要求発行をやめて、キューの空いている方から送信することにします。 さらに1つ同期要求を送信したら、もう1つの要求発行と同期応答を同時に待つようにします。

(クリックで拡大)

以上の変更を加えると、キューの長さが QL = 1 でも仕様を満たすことができます。

まとめ

ここで用意した仕様の範囲では、という条件付きではありますが、非同期通信で同期通信を実現するには、シーケンサを持つ同期要求、同じくシーケンサを持つ同期応答、そして同期確立とキャンセルからなるプロトコルを使えばよいということがわかりました。

CSP を基礎として開発されたプロセッサ Transputer は、プロセッサ間通信のために4つのシリアルリンクを持っていたそうです。具体的にどのような設計になっていたのかは知りません。ただ、マルチプロセッサのシステムでプロセッサ間通信を行う場合はおそらく非同期通信になるのではないかと想像していました。そうすると CSP(Transputer の場合は occam でしたが) で記述したモデルを物理的なプロセッサに配置する場合、物理的な非同期リンク上でどのように CSP の同期型通信を実現するかということが問題になると思っていました。そのためのささやかな検討をしてみたということでした。

2014/02/09

© 2013,2014,2015 PRINCIPIA Limited