■プロセスの並列化構成

1.並列化構成の定義

2.並列化プロセスの例

3. 諸定理

練習問題3-1

参考資料・リンク集

前章で与えたプロセス定義とプロセス木表現に関する定義に基づき、プロセスの並列化構成について説明する。
並列化オペレータ || のための、木合成の手順を与える。次に、並列化に関する諸定理を列挙する。

この章で学習する内容は以下の3つである。

1. 並列化構成の定義（Definition of Parallel Composition）
2. 並列化プロセスの例（Parallel Process Examples）
3. 諸定理（Laws and Propositions）

練習問題3-1

●並列化構成の定義（Definition of Parallel Composition）

1.1 定義
1.2 並列化構成の手順の例

1.1 定義

T1,T2 を、定義 Def-2.2a に基づいたプロセス木とする。

プロセス木 T1,T2 の、action集合 L による同期を行うことを、並列化構成という。

並列化の記法として、T1 |[L]| T2　と書く。

同期に用いるaction集合 L は、Lは空でない、かつ、プロセス木 T1 かつ T2 に現れるラベル Act(T1) または Act(T2) の元でなければならない。つまり、

L = { L' : non-empty labelset s.t. L' ⊆ Act(T1)∩Act(T2) }.

並列化構成 T1 |[L]| T2 の木操作の定義は、以下の通り。

To construct the tree T= T1|[L]|T2 apply the following rules (1)--(4)
wherever applicable.
　
Now, let <v1,v2> be a node of T already constructed, and
let <r1,r2> be the root of T, where rj is the root of Tj (j=1,2).
　
(1) if x is a label not in L (including i) and v1[x>v1' in T1,
    then add a node <v1,v2>[x><v1',v2> to T.
　
(2) same as (1) with respect to T2.
　
(3) if y is a label in L, v1[y>v1' is in T1 and v2[y>v2' is in T2,
    then add a node <v1,v2>[y><v1',v2'> to T.
　
(4) assume now that none of the above rules (1)--(3) are applicable 
    any more to the node v=<v1,v2> already constructed. Then, we have
　
    v is an X- node(leaf) of T
    iff
    both v1 and v2 are X-nodes of T1 and T2 respectively;
    otherwise v is a STOP-node of T.

並列化構成後のプロセス木 T = T(P) = T1|[L]|T2 であるとき、並列プロセス P の teminating $ は 木のX-node、stop は 木の STOP-node に対応する。

プロセス P1,P2 の並列化構成後のプロセスPについて、T(P) = T(P1)|[L]|T(P2)であるとき、プロセス P = P1|[L]|P2 と書く。

特に、同期ラベル集合 L が、L = Act(T1)∩Act(T2) である場合、これは Full-Synchronization となり、[L]を略して P1||P2 のように書く。木との関係で、以下は明らか。

P = P1||P2 iff T(P)=T(P1)||T(P2).

他方、同期ラベル集合 を 空 とした場合、これは interleaving となり、[]のかわりに、 P1 ||| P2 のように書く。

1.2 並列化構成の手順の例

プロセス P1,P2が以下の定義であるとする。

Process P1 := a;c;$
Process P2 := b;c;$

これのプロセス木 T1=T(P1),T2=T(P2)は、定義 Def-2.2a に基づいて以下の通り。

Process Tree T1 : r1 [a> vt1 [c> X1
Process Tree T2 : r2 [b> vt2 [c> X2

ここで、Act(T1)={a,c}, Act(T2)={b,c}である。
この2つのプロセス木の同期ラベル c による並列プロセス T = T1 |[c]| T2 を、上記の定義 Def-3.1 に従って構成してみよう。

まず、{c} ∈ L⊆ Act(T1)∩Act(T2) かつ空でない　ので、同期化ラベルとしての条件を満たしている。<v1,v2>=<r1,r2>が T の root node として構成されているとする。

次に、手順(1)--(4)を執り行う。

(1) label 'a' is a label not in L and v1 [a> vt1 in T1,
    then add a node <v1,v2> [a> <vt1,v2> to T. Next,
    label 'b' is a label not in L and v2 [b> vt2 in T2,
    then add a node <vt1,v2> [b> <vt1,vt2> to T.
　
(2) label 'b' is a label not in L and v2 [b> vt2 in T2,
    then add a node <v1,v2> [b> <v1,vt2> to T. Next,
    label 'a' is a label not in L and v1 [a> vt1 in T1,
    then add a node <v1,vt2> [a> <vt1,vt2> to T.
　
(3) label 'c' is a label in L, vt1 [c> X1 is in T1
                           and vt2 [c> X2 is in T2,
    then add a node <vt1,vt2> [c> <X1,X2> to T.
　
(4) after step(3), we do not have any more to the node
    v=<v1,v2> already constructed,
    because vt_terminate = <X1,X2> is an X- node(leaf) of T
    iff both X1 and X2 are X-nodes of T1 and T2 respectively.

    Tree T has a terminating <X1,X2>, no STOP-node
    (i.e. T is deadlock-free )

以上の操作により、並列プロセス T = T1 |[c]| T2 を得る。

Process Tree T : r(T)=<r1,r2>=<v1,v2>, 
                 <v1,v2> [a> <vt1,v2> [b> <vt1,vt2>
                 <v1,v2> [b> <v1,vt2> [a> <vt1,vt2>
                 <vt1,vt2> [c> <X1,X2>.

ここで、Act(T)={a,b,c} である。
判りやすくするために、各々のラベルをrenamingしても良い。例えば以下。

r := <v1,v2>
va := <vt1,v2>
vb := <v1,vt2>
vab := <vt1,vt2>
X := <X1,X2>

結局、P = P1|[c]|P2 = a;c;$ |[c]| b;c;$ = a;b;c;$ [] b;a;c;$ である。
（ P = (a;b;$ [] b;a;$)>>(c;$) と見ることもできる ）

図3.1 プロセスP1,P2の並列構成　P = P1 |[c]| P2

●並列化プロセスの例（Parallel Process Examples）

いくつかの代表的なプロセスの並列化構成の例を見てみる。

strongly equivalentであることを、記号 "=" で書く。
observational equivalentであることを、記号 "==" で書く。

例3-1：

Process P1 := a;i;i;b;$
Process P2 := i;a;i;b;$
　
P =  P1 || P2
  =  a;i;i;b;$ || i;a;i;b;$
  == a;b;$

例3-2：

Process P1 := a;b;$
Process P2 := a;b;a;$
　
P = P1 || P2 
  = a;b;$ || a;b;a;$ 
  = a;b;stop

例3-3：

Process P1 := a;b;$
Process P2 := a;b;$ [ ] b;a;$
　
P = P1 || P2
  = a;b;$ || (a;b;$ [ ] b;a;$)
  = a;b;$

例3-4：

Process P1 := a;(b;d;$ [ ] c;$)
Process P2 := a;(b;c;$ [ ] d;$)
　
P = P1 || P2
  = (a;(b;d;$ [ ] c;$)) || (a;(b;c;$ [ ] d;$))
  = a;b;stop

●諸定理（Laws and Propositions）

3.1 並列化操作 || に関する定理
3.2 recursive process *[]に関する補題

3.1 並列化操作 || に関する定理

Law 3.1：

Law 3.1:  the labels of T do not contain internal action 'i'
          implies T||T = T.

Law 3.1a：

Law 3.1a: the labels of T contain internal action 'i'
          implies T||T == T. (obs. equiv.)

例3-5：

Process P1 := a;i;b;$ であるとき、P1 || P1 == P1 である。
なお、P = P1 || P1 = a;i;i;b;$ となる。（定義 Def.3-1 を確認せよ）

Law 3.2：

Law 3.2:  T1||T2 = T2||T1

Law 3.3：

Law 3.3:  c;T1 || c;T2 = c;(T1||T2),
          if c is not an internal action i.

Law 3.4：

Law 3.4:  a;T1 || c;T2 = a;(T1 || c;T2),
          if a≠c and a is not in Act(T2) and c in Act(T1).

Law 3.5：

Law 3.5:  a;T1 || b;T2 = a;(T1||b;T2) [ ] b;(a;T1 ||T2),
          if a is not in Act(T2) and b is not in Act(T1).

3.2 recursive process *[]に関する補題

Prop. 3.1：

Prop. 3.1: *[a;c] || *[b;c] = *[a;b;c [ ] b;a;c]

Prop. 3.2：

Prop. 3.2: *[c;a] || *[b;c] = b;c;(*[a;c] || *[b;c])

Prop. 3.3：

Prop. 3.3: *[a;c] || *[c;b] = a;c;*[a;b;c [ ] b;a;c]

練習問題3-1

[1] プロセス P1,P2が以下であるとする。

Process P1 := *[coin,accept,dispence]
Process P2 := *[dispence,refill]

P = P1 |[dispence]| P2 を構成せよ。
これは、何の動作を表す並列プロセスであったか？
（BLAの並列プロセスに関する記述性の高さを確認せよ）

[2] 簡単なプロトコル SPROTの例について、諸定義と補題を用いて、以下を示せ。

PSEND = *[PUT;msg;ack]
PREC = *[msg;GET;ack]

SPROT = PSEND || PREC = *[PUT;msg;GET;ack].

[3] 例3-1〜例3-4について、定義 Def.3-1 の手順に従って P を構成し、確認せよ。

[4] 例3-5 P1 := a;i;b;$ であるとき、P = P1 || P1 = a;i;i;b;$ となることを、定義 Def.3-1 の手順に従って P を構成し、確認せよ。

[5] 3.1 並列化操作 || に関する定理 の Law 3.1〜3.5 を、これまでに取り上げた諸定義・定理を用いて示せ。

[6] 3.2 recursive process *[]に関する補題 の Prop.3.1〜3.3を示せ。

wasaki@cs.shinshu-u.ac.jp
Copyright(c) Katsumi Wasaki. All rights reserved.