数理解析研究所講究録 1325 巻 2003 年 98-103

98
協調型言語に基づく並列プロセスのモデル検証
愛媛大学・理学部・数理科学科 大塚寛 (Hiroshi Ohtsuka)
Department of Mathematical Science,Faculty of Science, Ehime University

1

概要と背景

有限状態機械 (FSM) による\check \check \llcorner -6) 検証は、 仕様記述とその検証の基儲と . る, ここでは 般の並列プロセスではなく、 制限された協調型言語 [1] を用いた並列プロセスの検証、 具体的にはin, out, 操作を持つ各直列プロセスとタプル空間 [1] の間の通信を対象としたモデル検証 [3] あるいは適合性試験 [3] について検討する。 さらにこの手続きをなるべ . タプル空間側の主導で行うよ ’‘. 実験を試みたので、これについて報舌.f る当該研究者はある実験的なシステムにソフトウェア共同開発者として、 遠隔地からの実験/開発に参加しているが、 遠隔地であるゆえに実験やソフトウェアの共同開発時に不便さが生じる。
そこで実験の再現環境や共同開発者が担当するソフトウェアの仕様の API の再現環境としてタプル空間 [1] の変形された一種を利用し、 通常の手続き型言語にタプル空間ヘアクセスする基本的操作を加えた協調型言語 [1] による開発を行っている。 協調型言語におけるタプル空間はグローバルバッファとして働き、通信相手が特定される必要はなく、入出力時のデータの順序にも特に制限はない 8 しかしここでは、通信の相手がわかっておリデータの 1 頃序も保持されている通信を再現する環境として利用した。 そこでまず簡単にタプル空間を中心にシステムを概観する。
$\gamma*\cdot.$$-\wedge$$?.(i$$\langle$$v$

実験の再現環境として 実験データを取得/保持し、 タプル空間へのアクセスに従って、 取り入れた時間間隔で送出する。 同時に取り入れた時間間隔を超えてもアクセスがないデータの処理なども行う。実際には実験データを加工しタプル空間に送るプロセスを介して、実験装置からの直接的なデータだけでなく、 入カパラメータに従った実験データの生成も行っている。

API の再現環境として 通信相手のプロセスが仕様どおりに実装されているものとして、 APIを期待通りに再現させる。我々の開発するシステムは機能ごとにコンボーネントに分割され、 それらを実装した複数プロセスを並列動作させる形を取っている。 ここで各開発グループが担当するコンポーネントのソースを全員で共有することはせず、各コンポーネントの外部仕様 (API) にかかわる部分を正確に記述し、 それに従ってプロセス間の通信を実装するようにしている。 そこで他の共同開発者が担当するプロセスとの通信を仮想的にタプル空間との通信で代用している。
この場合も実験の再現環境と同じく時間制約を設けている。
なお以上の再現環境では、通信データなどの相手側のデータを取り寄せ、 それらをタプル空間に設定するという手順を踏むことで、 相手側プロセスとの仮想的な通信を再現している。
タプル空間のその他の機能

現在タプル空間内では呼出し手順の正しさなどをチェックしており、 単一プロセスの単体テスト時に利用している。我々が担当した単一プロセスは既知の数値計算アルゴリズムを通常の手続き型言語で実装しており、 タブル空間ヘアクセスする基本的操作は同期型のみを利用している。 この単一プロセスに対しては、仕様策定時には従来の表明による検証を、実装時にはタプル空間での上述のチェックをパスするものと仮定した通常の動作の下で単99
体テストを行った。
以上によりイベント駆動型プロセスの複数の並列動作を逐次型の複数の単一プロセスとタプル空間 (イベント駆動型) に分け、 単一プロセスに対して動作検証を行なったことになる。

2

協調型言語の軌跡モデル

今回の実験では上で述べたように相手側の通信データを取得し、 モデル検証および適合性試験時に利用しているが、 このデータはプロセスの軌跡とみなせる。 一方、 以前の研究 [5] で通信相手を特定しない非同期型通信 [4] を行うプロセス代数を提案し、 プロセスとタプル空間の組 (様相) によるラベル付き遷移システムで意味を与え、更に軌跡によるプロセスの等価性を考察 1f\check -。
これは今回の検証等の基礎となるので、 以下にその概略を述べる。

2.1

タプル空間の仕様

ここでの並列プロセス間の通信とは、以下の仕様をもつ特殊なバッファプロセスと見なせるタプル空間を媒介とした非同期型通信 [4] である。通信されるメッセージはラベルとデータ (を格納する領域) の組であるが、 今回の意味論を構築する際にはデータ部分は考慮しない。

out(v)

タプル空間が満杯でない限り、 タプル空間にメッセージin(v)

タプル空間に$\mathrm{v}$$\mathrm{v}$を追加できる。のラベルと一致するメッセージが存在すれば、 タプル空間からそれを取り出せる。
$\mathrm{r}\mathrm{d}(\mathrm{v})$

タプル空間に のラベルと一致するメッセージが存在すれば、 タプル空間からそれを読み込む。 タプル空間に変化はない。
$\mathrm{v}$

タプル空間への操作は全て排他的に行われ、 先着順に処理されるものとする [4]。 操作的意味論はタプル空間の変化に着目して構成する。 以下ではタプル空間をマルチセットと解釈する。

22

ブロセス代数

ラベルの集合$\Sigma$に対しアクションの集合 $A$ を以下で定義する。 ただし$A:=${out( )
$v$$|v\in\Sigma$$\tau\not\in\Sigma$である。

} $\cup\{in(v) |v\in\Sigma\}\cup\{rd(v)|v\in\Sigma\}\cup\{\tau\}$

以外のアクション {こ対し label(a) で のラベノレを表す。
構文は CCS のサブセットで、 並列プロセスがアクションプレフイツクス、 選択、 再帰プロセスの内部に現れないもののみを扱う (cf. Simple CCS)。

$\tau$$a$$a$

定義 2.1 (ブロセス表現) プロセス表現 $P$ を以下のように再帰的に定義する。 ただし a\in A。
並列ブロセス
単一プロセス$P$$::=$$S$$::=$$S|P||P$$x|0|a.S|S+S|\mu x.S$

プロセス表現 $P$ の自由変数、 自由変数への代入、 $P$ がガード的であること、 $P$ が閉じていること等は CCS と同じ意味である。

100
定義 22 (プロセス) $P$ に出現する再帰プロセス表現はすべてガード的であり、 なおかつ閉じたプロセス表現 $P$ をプロセスと呼び、 プロセス全体の集合を で表す。
$\mathcal{P}$

定義 23(様相) プロセス $P\in P$ とび、 様相全体の集合を で表す。の元から成るマルチセット $M$ の組く $P,$ $M>$ を様相と呼$\Sigma$$\mathrm{C}$

マルチセット $M$ に元$v$を追加する操作を $M+v$ で、 $M$ から元$v$を削除する操作を M-。で表す。

定義 2.4 ラベル付き遷移システムあるいは単に遷移システムとは、 4 項組く $S,$ so, $T,$ $arrow>$ であは遷移は初期状態、 はラベルの集合、は状態の集合、る。 ここで関係として定義される。 表記法として $(s, a, s’)$ \epsilon \rightarrow を $s-^{a}s’$ と書く。
$S$

$T$

$.\mathrm{s}.0\in S$

遷移関係 \rightarrow はその合成に拡張できる。 ラベル$arrow\subseteq\backslash S\cross T\cross S$$a_{1},$ $a_{2},$$\cdots,$$sarrow s’t$とするとき、 $s,$ $s’\in S$ に対しいった一連の遷移関係があることである。 このとき

$t=a_{1}a_{2}\cdots a_{n}\in T^{*}$

t4 尊出と呼ぶ。特に $n=0$ の場合$sarrow s\epsilon$

$t$

を$s$

$a_{n}\in T,$とは、$(n\geq 1)\}$

こ対しその系列をと$sarrow s_{1}a_{1}arrow s_{2}a_{2}\ldotsarrow s’a_{n}$の軌跡あるいはトレース、 $s’$ を$s$のとする。 また $D(s)=\{s’|\exists t\in T^{*}\mathrm{s}.\mathrm{t}. s-^{t}s’\}$ とおく。

様相に対する操作的意味を次の遷移関係から導出されるラベル付遷移システムで与える。
定義 2.5 様相く $P,$ $M>$ の遷移関係 \rightarrow を次の遷移規則で生成される最小の関係で定義する。

Tau

In

$<\tau.P,$ $M>arrow<P\tau,$ $M>$$\overline{in(v)}(v\inM)$$M>rightarrow<P,$$M-v>$$<in(v).P,$Outout(v)$<out(v).P,$ $M>arrow<P,$ $M+v>$$\mathrm{R}\mathrm{d}$$\overline{<rd(v).P,M>rdA^{(v}<P,M>}(v\in M)$

Sum$\mathrm{R}\mathrm{e}\mathrm{c}$

Comp

,

$\frac{<P,M>arrow<P’,M’>a}{<P+Q,M>arrow<Pa’,M>}$$M’>a$$<Q,$ $M>arrow<Q’,$$<P+Q,$ $M>arrow<Q’a,$ $M’>$,$\frac{<P\{\mu x.P/x\},M>arrow<P’,M’>a}{<\mu x.P,M>arrow<P,M’>a}$$<P,$ $M>arrow<P’a,$ $M’>$$<Q,$ $M>arrow<Q’a,$ $M’>$$<P||Q,$ $M>arrow a<P’||Q,$ $M’>$$<P||Q,$ $M>arrow a<P||Q’,$ $M’>$を初期状態とする遷移システム $<D(<P, \emptyset>),$ $<P,$$P$の軌跡の集合 traoe(<P,, $A,$ $arrow>$ であり、プロセス の軌跡の集合 trace(P) とは、 $<P,$
プロセス $P$ の意味とは、 様相 $<P,$$\emptyset>$$\emptyset>$.

$)=\{t|\exists s’\in \mathrm{C}\mathrm{s}.\mathrm{t}$$<P, \emptyset>arrow s’\}t$$\emptyset>$$\emptyset>$のことである。

定義 26(トレース等価) プロセス $P,$ $Q\in P$ がトレース等価であるとは、 trace(P)=traoe(Q)すなわち trace(<P,) $=trace(<Q, \emptyset>)$ であるときに言い $P\sim_{tr}Q$ と書く。
$\emptyset>$101 101
定理 27 トレース等価性に関して、 次の性質が成り立つ。 ただし a\in A。
$\mathit{1}$.

$\sim tr$は合同関係である。

2. $a.(P+Q)\sim_{tr}a.P+a.Q$
次に今回の検証に関係した並列プロセスの軌跡に関する性質を挙げる。
定理 28 $t\in tr\cdot ace(P||Q)$ でく $P||Q,$ $\emptyset>arrow t<R,$ $M>$ とすると

1.

に対して $|t’\uparrow in(v)|:.\cdot|t’\uparrow mt(v)|$(プレフィックス),
すなわち の中に現れる in(v) の個数は、 の中に現れる out(v) の個数を越えない。
$\forall v\in\Sigma$$\forall t\leq t$

$t’$

$t’$

2.

$\forall v\in\Sigma$[こ対して$\#(M, v)\leq|t\uparrow mt(v)|-|t\uparrow in(v)|$

特に $M$ の元の個数については$\# M\leq\sum_{v\in\Sigma}|t\uparrow \mathrm{o}ut(v)|-\sum_{v\in\Sigma}|t\uparrow in(v)|$

第 3 節ではデッドロックが起きないこと (deadlock-free) を対象とした安全性の検証の例を挙げている。今回の実験では 「バッファが空の状態でのバッファへの読み込み操作」すなわち 「タプルがないタプル空間へ in 操作」 が起きないことであり、 括弧部分を軌跡を用いて表すと$\sum_{v\in\Sigma}|t\uparrow mt(v)|<\sum_{v\in\Sigma}|t\uparrow in(v)|$すなわち $\# M=0$ の場合に上式が成り立たない場合を対象とすることになる。

3可達性解析

今回、 モデル検証を利用した安全性の検証として deadlock-free であることをシステムの設計時から検証し、単一プロセスとタプル空間との組み合わせでは定理 28 直後に述べた状態に絞り込み、 可達性解析時に対象とする FSM を生成するかわりに以下の方針で行なった。

1. 単一プロセス側では非決定的な動作を極力排してた上で軌跡を生成する。

2. タプル空間の動作をモデル化した状態空間の中で潜在的なデッドロツク状態に近づけることを優先して探索を進める。

3. 2. の方針により、 タプル空間に待たされているデータがない状態に進むために、 単一プロセス側の可能な軌跡から受信処理 (in(v)) を送信処理 $(mt(v))$ 上り優先して選ぶ。
なおもう一つの安全性である 「バッファあふれがないこと」 は時間制約に関わる事として今回の検証の対象とはしなかった。
以下では上の方法を、 デッドロックが起きる場合と起きない場合の例を用いて説明する。 いすれの場合も食事をする哲学者問題の 2 名 (phill, phi12) をモデル化したコード断片を挙げる。

102
デッドロックが起きる場合 右図の phill では Cl, C2 の順の順
序で in, out 操作を行うの{こ対し、 phi12 では C2,while (true) {while (true)
thinkin (C1);in (C2);
eat $()$ ;序で in, out 操作を行う。 それぞれの軌跡は以下の通り。

Cl$\dot{|}\mathrm{n}(\mathrm{C}\mathrm{l})\mathrm{i}\mathrm{n}(\mathrm{C}2)\mathrm{o}\mathrm{u}\mathrm{t}(\mathrm{C}\mathrm{l})\mathrm{o}\mathrm{u}\mathrm{t}(\mathrm{C}2)\mathrm{i}\mathrm{n}(\mathrm{C}\mathrm{l})\mathrm{i}\mathrm{n}(\mathrm{C}2)\cdots$$\mathrm{C}2$

in(C2)in(C1)out(C2)out(C1)in(C2)in(C1)$\mathrm{t}\mathrm{h}\mathrm{i}\mathrm{n}\mathrm{k}()$$()_{\mathrm{j}}$$\mathrm{C}1$

in (C2);in (C1);
eat $()$ ;out (C2);

out (C1) ;out (C2);$\cdots$$\}$$\{$;out (C1);$\}$

またタプル空間内ではラベル Cl, Cl に対応する長さ 1 のバッファが存在すると仮定する。

phill$\mathrm{p}\mathrm{h}\mathrm{i}\mathrm{l}2$

この場合通常の可達性解析時の FSM と同様であり、 状態数に変化はないので、 ポインタを持つ分だけ複雑になる。
while(true) {while(true)
デッドロックが起きな 1 合 右図の phill, phi12 では上のthink ;例の in ffl\epsilon の前に in(token) を、 out lWF の後に out(token)think ;in(token);in (token);
操作を行う。 それぞれの軌跡は以下の通りである。.
.
in(C2)
in(C2);
inin
Cl in(token)in(Cl)in(C2)out(C1)out(C2)out(token)$()$$\{$$()$$(\mathrm{C}1)_{*}$$j$$(\mathrm{C}1)_{j}$$\cdots$$\mathrm{C}2$in(token)in(C2)in(C1)out(C2)out(C1)out(token)

eat $()$ ;$\cdots$

またタプノレ空間内ではラベノレ token, Cl, Cl [こ対応する長さ 1 のバッファが存在すると仮定する。

}

eat $()$ ;out (C2);
out (C1);
out (C1) ;out (C2) ;out (token) ;out (token);

}

phill

phi12

例 32 タプル空間をモデル化した FSM は token, Cl, C2 各々の存在非存在に対応して 8 状態 (2状態同士の直積) の状態空間となる。 このとき我々の方法ではタプル空間の FSM の状態に対し遷移可能なアクションに対応する phiIl の軌跡へのポインタを持たせるのは上の例と同じだが、 その際状態空間中の遷移の起こり得ない状態を除くことにより、 5 状態に減らすことができる (次ページ図参照)。 この例での要点は、相手側コードが仕様を守って実装していると仮定した上で、token の in, out 操作が一番上とその直下の状態の間でしかなされないことである。
我々の方法を従来の FSM の並列合成による手法と比べると、・プロセス間の直接の通信ではなく、 タプル空間 (FSM) との通信に限った段階的なモデル検証/適合性試験

103.

FSM の状態空間の直積/最小化を経るのではなく、 軌跡の interleaving に当たる部分を前もって FSM に適用した特殊な FSM と軌跡によるモデル検証/適合性試験と捉えることができる。 FSM の遷移可能なアクションを軌跡に関係付ける
状況は、 失敗集合 [2] を構成する軌跡と拒絶集合を FSM 中に保持する状況と似ていると思われる。 また試験等価性 [4] に基づく手法と似ているが、 軌跡を探索のためのガイドとして利用する部分が異なると思われる。 しかしこれらの理論的根拠を確認するまでには至っていない。

なおこの手法により FSM の能力が上がるわけではなく、 実行効率もこの場合では数%でしかなかった。 しかし実装段階での通信時のエラーを解析するのに、 プロセスの軌跡が利用出来たのは都合が良かったとも言える。

4$\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{c}\mathrm{e}$of phill$\mathrm{F}\mathrm{S}\mathrm{M}$of bple Space

課題

今回の実験/開発では設計時に failur -divergence モデルを採用したが、 実装時のモデルにも採用したい。 また 「バッファあふれ」 についてはタイムアウト処理で対処したが、 実装時にはこれに関わる問題が頻繁に生じた。 これに対処するには、 時間オートマトンなどモデル中に時間制約を導入した上で検証/試験する必要がある。
なお協調型言語には非同期通信用の $inp$ 操作があるが、 そもそもプロセス間の非同期通信をタプル空間との通信に置き換えている事、 $inp$ 操作を使ったプログラミングは一般のプログラマにとって複雑である事などから、 $inp$ 操作を導入することには視野にいれていない。

参考文献[1] D. Gelernter, Generative Communication in Linda, ACM Transactions on ProgrammingLanguages and Systems, PP. 80-112, January 1985
[2] C. A. R. Hoare, Communicating Sequential Process, Prentice HaJl, 1985
[3] G. Holzmann, Design and Valdation of Computer Protocols. Prentice Hall, 1991

[4] R. De Nicola and R. Pugliese, Testing semantics of asynchronous distributed programs,Analysis and Verification of Multiple-Agent Languages. 5th LOMAPS Workshop. SelectedPapers, pp. 320-344, 1997
[5] 本多和正, 河原康雄, 森雅生, 大塚寛, 非同期型通信を用いた並列プロセスの意味論と並列言語への応用, 情報処理学会九州支部研究会報告, pP. 26-33, Mar. 1999