JP3635667B2 - Data flow graph verification device - Google Patents

Description

₂ を色とするトークンは同じ環境の値を運んでいると判定し、ノードを発火させる。これは、分岐ノードで分岐した２つの経路に対する検証を同時に行うとともに、各経路における検証で、その分岐ノードより前の経路断片での計算結果を共有できることを意味する。
【００１３】
次に、データフローグラフの検証方式について説明する。
【００１４】
まず、扱う構造について説明する。本検証装置により検出される、可到達性異常、伝播異常、全実行性異常、合流異常のいずれでもないプログラムは「良構造」であるという。以下の構造をもつプログラムは通常の実行時には正しく実行されるが、本検証法では合流異常として判定される。これらの構造は同じ機能をもつ良構造へ変換可能であるため問題はない。
【００１５】
図４（ａ）に示す分岐ノードを用いてサイクルを構成する繰り返し構造を考える。この構造は図４（ｂ）に変更可能である。このような指定繰り返し構造は関数の再起呼び出しに変換可能であるため、本検証系では、サイクルを構成しないプログラムだけを許し、図４（ａ）のようなサイクルを含む構造は合流異常があると判定する。
【００１６】
また、図５（ａ）に示す複数の経路が一つの実行経路を共有する構造は実行時にエラーを発生しない。しかし、この構造は図中の（ｂ）に示すような、より簡明な構造に変換可能である。このため、本検証系では、図５（ｃ）に例示するように、分岐ノードと合流ノードの対により分岐構造をネストしてできるプログラム構造だけを許し、図５（ａ）のようなネストしない構造は合流異常があると判定する。
【００１７】
次に、検出する異常について説明する。図１に異常があるプログラムの例を示す。図１において、白丸のノードは演算ノード、黒丸のノードは分配ノード、白丸にＳのノードは開始ノード、白丸にＥのノードは終了ノード、白丸にＳＷのノードは分岐ノード、逆三角形のノードは合流ノード、四角のノードは上述のノードにより形成される一つの経路を表す。また、ノードの左上の数字はノード番号を示す。以下に各異常について述べる。
【００１８】
まず、伝播異常は、開始ノードからトークンを出力しない終了ノード以外のノードに至る経路が存在するとき、伝播異常であるという。図１（ｇ）のノード４においては出力アークが存在しないためトークンを出力できない。
【００１９】
可到達性異常は、開始ノードから終了ノードまでトークンが伝播する経路が存在しないとき、可到達性異常であるという。例えば図１において、（ａ）のノード２、（ｄ）のノード６においてはトークンを出力できないため、また、（ｂ）のノード４、（ｃ）のノード３においては入力アーク上にトークンが揃わないため実行が停止し、終了ノードへトークンが到達しない。
【００２０】
全実行性異常は、開始ノードからトークンが到達する経路がないノードが存在するとき、全実行性異常であるという。例えば図１において、（ｂ）のノード２、（ｃ）のノード２は入力アークが存在しないため、発火する可能性はない。
【００２１】
合流異常は、分岐命令により分岐した経路をまとめること以外の目的で使用する合流ノードが存在する合流異常であるという。例えば図１において、（ｅ）のノード５では、合流ノードより先の経路を２つのトークンが伝播し、衝突することとなる。図１において、（ｆ）のノード２〜４の間は常にループ状態となり、先の経路上でトークンが衝突することとなる。
【００２２】
前述の経路断片識別子を値として持つトークンを検証実行に用いることにより、プログラムが良構造であるかを検出する。このために、発火規則を以下のように定める。
【００２３】
合流ノードの場合は、例えば、図６のような経路断片識別子の割り当てを表す木が与えられた場合には、値としてｃ₁ とｃ₂ もしくは、ｃ₃ とｃ₄ のよう兄弟関係にある経路断片識別子をもつトークンどうしが入力アーク上に揃った場合に発火する。
【００２４】
その他としては、等しい経路断片識別子をもつトークンが入力アーク上に揃った場合に発火する。
【００２５】
次に、検証のための実行法について説明する。ノードの実行状態を示すことにより、全実行性異常を検出する。このために、各ノードに対してフラグを付与する。このフラグを実行フラグと呼ぶ。実行フラグの値が１のときは、そのノードが実行されることを、０のときは実行されないことを表す。初期値は０である。
【００２６】
本検証装置は、データフローグラフ上の全てのノードに対して付与した実行フラグを０に初期化した後、以下に示す方式で処理を施す。
１．全ての入力アーク上にトークンが到達するまで待機させる。
２．入力アーク上にトークンが揃った後、前節で述べた発火規則に添ってノードの発火を行う。このとき、ノードの実行フラグを１にし、入力アーク上のトークンをノード内に取り込む。
３．ノード内のトークンの値をコピー（合流ノードの場合はトークンの値を親となる経路断片識別子を値とする）したトークンを出力アーク上に出力する。出力アークが存在しない場合は、トークンをノード内に取り込んだままとする。
【００２７】
それぞれのノードを上記の実行方式に従って発火させることにより、グラフ全体を非同期並列に実行する。
【００２８】
異常の検出条件について説明する。本検証装置により、検証対象とするプログラムを実行させ、実行中のノードがなくなった時点で検証のための実行を終了する。この際に、次の表１に示すことが言える。
【００２９】
【表１】

図７は、従来の検証装置の構成を示す。図中で、実線矢印は制御の流れを、点線矢印はデータの流れを表す。図中の各機能について説明する。
トークン到着監視機能：全ての入力アーク上にトークンが揃ったノードを検出し、発火規則を基に発火させる。ノードが発火した場合は、ノードの実行フラグを１にして制御をトークン入力機能に移す。
トークン入力機能：入力アーク上のトークンを、入力アークの順に並べてノード内に取り込む。
ノード分類機能：発火したノードを演算命令、分配命令、分岐命令、手続き呼び出し命令、手続き開始命令、手続き復帰命令、合流命令に分類し、そのノード種別をトークン出力機能に送る。
トークン出力機能Ａ：トークン出力機能Ａの詳細構成図を図８に示す。図中で、実線矢印は制御の流れを、点線矢印はデータの流れを表す。命令デコード機構は、ｌｉｎｅＡに流れてきたデータよりノード種別を知り、対応する出力機構へ制御を移行する。トークン消去機構はノード内に取り込んだトークンを消去する。各出力機構は命令の種類に応じて以下の様に動作する。なお、入力アーク上に到達したトークンとは、ノード内に取り込んだトークンのことを指す。
【００３０】
演算命令出力機構は、入力アーク上に到達したトークンの値をコピーしてトークンを生成し、出力アーク上に置く。
【００３１】
分配命令出力機構は、入力アーク上に到達したトークンの値をコピーして新たにトークンを生成し、全ての出力アーク上へ置く。
【００３２】
分岐命令出力機構は、第２入力アーク上に到達したトークンの値より得られる経路断片識別子の孫値を２つ求める。求めた２つの経路断片識別子を値とする２つのトークンを生成し、それぞれ出力アーク上へ置く。
【００３３】
手続き呼び出し命令出力機構は、第２入力アーク上のトークンをコピーし、手続き開始ノードの第１入力アーク上に置く。また、出力アークの名前を値としたトークンを生成する。第１入力アーク上のトークンの値として格納されている関数名から関数の手続き復帰ノードを求め、そのノードの第１入力アーク上に、生成したトークンを置く。
【００３４】
手続き開始命令出力機構は、入力アーク上のトークンのコピーを出力アーク上に置く。
【００３５】
手続き復帰命令出力機構は、第２入力アーク上の値を使用してトークン（結果の値）を生成する。第１入力アーク上のトークンの値として指定されたアークにトークン（戻り先）を置く。
【００３６】
合流命令出力機構は、各入力アーク上のトークンの値より得られる経路断片識別子に対し、共通の先祖となる値を求める。求めた経路断片識別子を値とするトークンを生成し、このトークンを出力アーク上へ置く。
【００３７】
図９に実行例を示す。図中で黒丸はトークン、白丸ノードは演算ノード、白丸に十字のノードは分配ノードを表す。また、斜線ノードは実行フラグの立ったノードを表す。以下に実行例の動作説明を示す。
１．開始ノードより経路断片識別子ｃ₁ なる値を持つトークンを出力する。関数呼び出しノードでは、値がｃ₁ であるトークンを手続き開始ノードの入力アーク上へ置く（図９（ｃ））。
２．関数の検証が終了し、手続き復帰ノードが発火した場合には、手続き復帰ノードの第１入力アークに置かれたトークンの値より復帰先アークを求め、求めたアーク上にトークンを置く（図９（ｄ））。
３．分岐ノードでは入力アーク上のトークンの値より得られる経路断片識別子
【外２】

路断片識別子を求める。次に求めた経路断片識別子をトークンの値として出力する（図９（ｅ））。
【００３８】
図９のように、全ての入力アーク上にトークンが揃った場合に、ノードに実行フラグを立てて、出力アーク上にトークンを置く。トークンが終了ノードに至った後（図９（ｆ）の時）、グラフ上に表１の検出条件を持つトークンやノードは存在しないため、異常のないプログラムと言える。
【００３９】
【発明が解決しようとする課題】
環境依存発火機能・環境依存分配機能を有するデータフロー計算機で実行されるプログラムに従来の検証装置を適用した場合、異常が検出されなくとも、ノードへの環境レベルの付け方によっては、ある実行環境レベルでは、可到達性異常、伝播異常、全実行性異常、合流異常が生じる場合がある。
【００４０】
例えば、図１０のように環境レベルを配したプログラムを考える。ここで、白丸のノードは演算ノードを表し、白丸に十字のノードは分配ノードを表す。各ノードの左側の数値はノード番号を表し、右側の数値は環境レベルを表す。実行環境レベル１，２のトークンを用いた場合には、図１０（ａ），（ｂ），（ｃ）のどのプログラムにおいても正常に動作する。しかし、実行環境レベル３のトークンが伝播する場合には、図１０（ａ）〜（ｃ）の各プログラムでそれぞれ以下に示す問題が発生する。
【００４１】
図１０（ａ）では、ノード１からノード１０まで、実行環境レベル３のトークンが伝播する経路がある。しかし、ノード６は環境レベルが３であるにもかかわらず、実行環境レベル３のトークンは到着しないため、実行は行われない。
【００４２】
図１０（ｂ）では、ノード１からノード１０まで、実行環境レベル３のトークンが伝播する経路は存在する。しかし、ノード４に到達した実行環境レベル３のトークンは、これより先のノードを実行できない。このため、このトークンはノード１０に到達しない。
【００４３】
図１０（ｃ）では、ノード７に到達した実行環境レベル３のトークンは、これより先のノードを実行できない。このため、トークンはノード１０に到達しない。
【００４４】
実行環境レベル別に実行を行った場合には、上述した誤りが発生する可能性がある。しかし、従来の検証装置による検証では、グラフの構造による可到達性異常と伝播異常と全実行性異常と合流異常を検出するだけであり、任意の環境レベルに対する可到達性異常と伝播異常と全実行性異常と合流異常の検出は行っていない。このため上述の誤りを検出できない。
【００４５】
また図１１にあるように、自関数の再帰呼び出しにより停止しない構造が考えられるが、従来の検証法ではこのような構造を検出できず、また、検証のための実行が停止しない。この異常を再帰異常と呼ぶ。
【００４６】
この問題を解決するために、与えられた実行環境レベルで実行されるべきノードが全て実行され、かつ、プログラムの開始ノードから終了ノードまでトークンが伝播することを、全ての実行環境レベルにおいて検出する必要がある。
【００４７】
本発明は、上記に鑑みてなされたもで、その目的とするところは、環境依存発火機能と環境依存分配機能を有するデータフロー計算機で実行される再帰関数を含むプログラムにおいて全ての実行環境レベルについて可到達性異常と伝播異常と全実行性異常と合流異常と、関数の再帰呼び出しによる再帰異常を検出するデータフローグラフ検証装置を提供することにある。
【００４８】
【課題を解決するための手段】
上記目的を達成するため、請求項１記載の発明は、環境レベルを付与したノードをアークで結合したデータフローグラフをプログラムとし、実行環境レベルを付与したトークンをアークを経由してノード上を伝播させ、環境依存発火機能と環境依存分配機能により発火制御するプログラム内のトークンの伝播上の正常性を検証するデータフローグラフ検証装置であって、トークンが伝播してきた経路上のノードに着目して、トークンがノードに入力できるかどうかの状態を示す入力状態を、当該トークンが伝播してきた経路上のノードに対するトークン伝播とエラー発生の状況に基づいて実行環境レベル毎に求める入力状態演算を行い、ノードが発火するかどうかの状態を示す到達状態を、入力状態および当該ノードの環境レベルに基づいて実行環境レベル毎に求める到達状態演算を行い、トークンが出力できるかどうかの状態を示す出力状態を、到達状態および出力アーク先ノードの環境レベルに基づいて実行環境レベル毎に求める出力状態演算を行う状態演算機能部を有することを特徴とする。
請求項２記載の発明は、請求項１記載の発明において、ノードが発火した際に、当該ノードへ入力するトークンに付与された関数の実行停止性に基づくと共に、前記ノードへ入力するトークンに呼び出し先関数が付与されている場合には当該呼び出し先関数の実行停止性にも基づいて、関数の相互呼び出しによる実行停止性を表す状態をノード種別に応じて求める有限再帰判別演算を行う有限再帰判別演算機能部を更に有することを特徴とする。
【００４９】
【作用】
本発明のデータフローグラフ検証装置では、トークンが伝播してきた経路上のノードに着目して、入力状態、到達状態、出力状態の各々をすべての入力アークの実行環境レベル毎の状態、入力状態とノードの環境レベル、到達状態と出力アーク先ノードの環境レベルの各々に基づいて実行環境レベル毎に状態演算し、呼び出し先関数の出力状態を引き継ぎ、関数内のノードを状態演算する。
【００５０】
【実施例】
以下、図面を用いて本発明の実施例を説明する。
【００５１】
なお、実施例を説明する前に、まず本発明のデータフローグラフ検証装置の基本概念について説明する。本検証装置は、任意の環境レベルに対する可到達性異常、伝播異常、全実行性異常、合流異常、再帰異常を検出するための手段１、および関数の再帰呼び出しによる停止しない状態を検出するための手段２を有する。
【００５２】
まず、手段１について説明し、その中の状態演算について説明する。
【００５３】
実行環境レベルは数値（ここでは自然数を用いる）で表す。数値が大きいほどレベルが高いことを意味する。ここで、ある実行環境レベルにおけるトークン伝播の状況を、その実行環境レベルの状態といい、その値を次の様に表す。
Ｔ：通常のプログラム実行時にトークンが伝播してくる可能性がある。
Ｎ：通常のプログラム実行時にトークンは伝播してこない。
Ｒ：通常のプログラム実行時に、発火出来ない。もしくは、トークンを出力出来ない状態が発生している。
Ｅ：通常のプログラム実行時に実行されない状態が発生している。
【００５４】
【外３】

ｓ₂ なる演算を次の様に定義する。
【００５５】
【数１】

また、レベルｌの実行環境レベルの状態を第ｌ要素とした、全ての実行環境レベルの状態を表す一次元ベクトルを状態ベクトルと呼ぶ。このとき状態ベクトルＳ₁ ＝（ｓ₁₁，ｓ₁₂，…，ｓ_1n），Ｓ₂ ＝（ｓ₂₁，ｓ₂₂，…，ｓ_2n）に対して、
【外４】

【数２】

ノードの第ｊ入力アーク上のトークンの値をＴ_j ＝（ｔ_j1，ｔ_j2，…，ｔ_jn）とする。このとき、Ｔ_j は状態ベクトルであり、ｔ_jkは実行環境レベルｋで、そのトークンが伝播してきた経路上のノードに対する、トークン伝播とエラー発生の状況を表している。次式により求まるＩ＝（ｉ₁ ，ｉ₂ ，…，ｉ_n ）を入力状態ベクトル、入力状態ベクトルを求める演算を入力状態演算と呼ぶ。入力状態ベクトルの第ｍ要素の値がＴのとき、実行環境レベルｍのトークンが、全ての環境入力アーク上に到達することを示す。
【００５６】
【数３】

【００５７】
Ｒ＝（ｒ₁ ，ｒ₂ ，…，ｒ_m ，…，ｒ_n ）を到達状態ベクトル、到達状態ベクトルを求める演算を、到達状態演算と呼ぶ。到達状態ベクトルの第ｍ要素の値がＴのとき、実行環境レベルｍのトークンで、ノードが発火することを示す。なお、ｔａｇはノードの環境レベルである。
【００５８】
【数４】

到達状態ベクトルをＲ＝（ｒ₁ ，ｒ₂ ，…，ｒ_m ，…，ｒ_n ）としたとき、第ｊ出力アークに対し、各要素が次式により求まるＯ_j ＝（ｏ_j1，ｏ_j2，…，ｏ_jm，…，ｏ_jn）を出力状態ベクトル、出力状態ベクトルを求める演算を、出力状態演算と呼ぶ。出力状態ベクトルの第ｍ要素の値がＴのとき、実行環境レベルｍのトークンを出力できることを示す。なお、ｔａｇ_out （ｊ）は第ｊ出力アーク先
【外５】

ある。
【００５９】
【数５】

図１２に示す状態演算機能により、各実行環境レベルにおける可到達性異常、伝播異常、全実行性異常、合流異常、再帰異常を検出する。図中で実線矢印は制御の流れ、点線矢印はデータの流れを表す。データフローグラフの各ノードに対してＲフラグ、Ｅフラグと呼ぶ二つの一次元ベクトルを持たせる。これらのフラグの第ｍ要素は、実行環境レベルｍでの異常発生状況を表す。Ｒフラグの要素の値が１の時、その要素に対応する実行環境レベルで、そのノードが発火出来ないか、トークンを出力できないことを意味する。Ｅフラグの要素の値が１の時、その要素に対応する実行環境レベルでそのノードの入力アーク上にトークンが到達しないため、そのノードが実行されないことを意味する。
【００６０】
これらのフラグの要素の初期値は、０である。以下に、状態演算機能の各機構について述べる。
【００６１】
値読み取り機構は、ノード内に取り込まれたトークンより値を読み取り、その値をデータとして入力状態演算機構へ送る。
【００６２】
出力アーク判定機構は、出力アーク先にあるノードの環境レベルをデータとして、出力状態演算機構へ送る。
【００６３】
入力状態演算機構は、値読み取り機構よりトークンの値を受け取り、また、ｌｉｎｅＡよりノード種別を受け取り、入力状態演算を行う。演算結果をデータとして到達状態演算機構に送る。入力トークンの値にＲが含まれず、式（７）の結果にＲとなる要素がある場合には、その要素に対応するＲフラグの値を１とする。
【００６４】
到達状態演算機構は、入力状態演算機構より入力状態演算の結果を受け取り、到達状態演算を行う。演算結果をデータとして出力状態演算機構に送る。入力状態演算機構より受け取った値の要素がＥもしくはＮであり、演算によりＲが得られた要素がある場合には、その要素に対応するＲフラグの値を１とする。また、入力状態演算機構より受け取った値の要素がＮまたはＥであり、演算によりＥが得られた要素がある場合には、その要素に対応するＥフラグの値を１とする。
【００６５】
出力状態演算機構は、到達状態演算機構より到達状態演算の結果を受け取り、ｌｉｎｅＡよりノード種別を受け取り、また、出力アーク判定機構より出力アーク先にあるノードの環境レベルを受け取り出力状態演算を行う。演算結果をデータとして出力する。演算によりＲが得られた要素がある場合には、その要素に対応するＲフラグの値を１とする。
【００６６】
状態演算機能を有する実行経路検証系では、データフローグラフの全てのノードに対して以下に示す方式で処理を施すことにより検証のための実行を行う。
【００６７】
１．全ての入力アーク上にトークンが到達するまで待機させる。
２．入力アーク上にトークンが揃った後、従来技術と同じ発火規則に添ってノードの発火を行う。このとき、ノードの実行フラグを１にし、入力アーク上のトークンをノード内に取り込む。
３．状態演算機能は各機構を動作させる。
４．出力状態演算機構からの出力と、ノード内に取り込んだトークンの経路断片識別子と有限再帰判別ベクトルより新たにトークンを生成する。新たに生成したトークンを出力アーク上に出力する。ノード内のトークンを消去する。
【００６８】
次に、手段２について説明する。
【００６９】
有限再帰判別ベクトルは、関数の相互呼び出しによる実行停止性を表す論理値を要素として持つ一次元ベクトルであり、要素の値が１のとき呼び出しが停止することを表し、０のとき停止しないことを表す。なお、プログラムが使用している関数名とこの有限再帰判別ベクトルと実行経路検証系より得られた関数の状態ベクトルを対応付ける表を関数表と呼ぶ。
【００７０】
実行経路検証系で検証を行い、ノードが発火した際に、各ノードごとに以下に示す有限再帰判別演算を行う。
【００７１】
合流ノードに対しては、各トークンの値より得た有限再帰判別ベクトルの各要素について論理和を求める。
【００７２】
手続き呼び出しノードに対しては、各トークンの値として与えた有限再帰判別ベクトルの各要素について論理積を求める。さらに求めた有限再帰判別ベクトルと関数用の呼び出し先関数の有限再帰判別ベクトルの各要素について論理積を求める。
【００７３】
その他のノードに対しては、各要素について論理積を求める。
【００７４】
再帰関数検証系では、実行経路検証系が検証のための実行を行う際に以下のように動作する。
１．プログラムで使用している関数の中で検証を行う関数を求め、その検証対象関数名と検証対象関数の有限再帰判別ベクトルと全ての要素がＴの状態ベクトルを実行経路検証系に送る。
２．実行経路検証系の状態演算機能の実行後に、有限再帰判別演算を行う。 ３．実行経路検証系より関数に対する検証のための実行が終了した信号を受け取った際には、検証を行った関数の状態を調べ、関数表の中でその関数の項を更新する。プログラムに対する検証のための実行の終了判定を行い、終了しない場合は１に戻る。
【００７５】
上述したように、状態演算機能を有するデータ駆動実行型検証装置により、検証のための実行を行い、実行中のノードがなくなった時点で、もしくは終了判定機能により終了することを決定した時点で検証のための実行を終了する。このとき、トークンの位置と値、およびノードのフラグの値を調べることにより可到達異常、伝播異常、全実行異常、合流異常を知ることができ、また有限再帰判別ベクトルの値を調べることにより、関数の相互再帰呼び出しによる再帰異常を知ることができる。
【００７６】
次に、本発明の実施例について詳細に説明する。
【００７７】
なお、本実施例では、発火規則は次のように定める。関数復帰ノードでは、第２入力アーク上にトークンが到達した際に発火する。他のノードは従来技術と同様である。
【００７８】
図１３は、状態演算機能を有する本実施例の検証装置の構成を示すブロック図である。図１３において、実線の矢印は制御の流れを表し、点線の矢印はデータの流れを表す。
【００７９】
図１３に示す本検証装置は、再帰関数検証系１および実行経路検証系２を有する。再帰関数検証系１は、関数表作成機能部１１、検証関数更新機能部１２、関数表更新機能部１３、終了判定機能部１４、有限再帰判別演算機能部１５から構成されている。実行経路検証系２は、色付きトークン到達監視機能部２１、トークン入力機能部２２、ノード分類機能部２３、状態演算機能部２４、トークン出力機能Ｂ部２５、関数実行終了判定機能部２６から構成されている。
【００８０】
まず、再帰関数検証系１の各構成要素について説明する。
【００８１】
関数表作成機能部１１は、検証対象プログラムで使用する関数名と全ての要素の値が０の有限再帰判別ベクトルと全ての要素がＮである状態ベクトルとの対応を表す関数表を作成する。作成した関数表を記憶装置内の関数表および既関数表として登録する。また、記憶装置内の検証関数名を空にする。最後に検証関数更新機能部１２に制御を移行する。
【００８２】
検証関数更新機能部１２は、記憶装置より関数表と検証関数名を得る。次に検証関数名よりまだ検証していない関数を求め、その関数の全てのノードの実行フラグ、Ｒフラグ、Ｅフラグを初期化し、トークンを消去する。関数の開始ノード（もしくは、手続き開始ノードの入力アーク上）に対して、ノードに与えられた環境レベルのなかで最大の値と対応する要素までをＴとし、それ以上をＮとした状態ベクトルと要素の値が１の有限再帰判別ベクトル、そして経路断片識別子を値とするトークンを置き、関数名を検証関数名に登録する。全ての関数に対する検証が終了した場合は終了判定機能部１４に制御を移行する。
【００８３】
関数表更新機能部１３は、終了ノードにトークンが存在する関数について、そのトークンの値から得られる有限再帰判別ベクトルの値と状態ベクトルを、記憶装置内関数表の対応する関数の有限再帰判別ベクトルと状態ベクトルに代入する。検証関数更新機能部１２に制御を移行する。
【００８４】
終了判定機能部１４は、記憶装置内の関数表と既関数表とを比較し、等しい場合は検証のための実行を終了する。異なる場合は、記憶装置内の関数表を既関数表として記憶装置に登録し、記憶装置内の検証関数名を空にする。制御を検証関数更新機能部１２に移行する。
【００８５】
有限再帰判別演算機能部１５は、状態演算機能よりノード種別を受け取り有限再帰判別演算を行う。演算結果とノード種別をトークン出力機構に送り、制御をトークン出力機能Ｂ部２５に移す。
【００８６】
次に、実行経路検証系２の各構成要素について説明する。
【００８７】
トークン到達監視機能部２１、トークン入力機能部２２、ノード分類機能部２３は従来技術のものと同じであり、次の通りである。
【００８８】
トークン到達監視機能部２１は、全ての入力アーク上にトークンが揃ったノードを検出し、発火規則を基に発火させる。ノードが発火した場合は、ノードの実行フラグを１にして制御をトークン入力機能に移す。
【００８９】
トークン入力機能部２２は、入力アーク上のトークンを、入力アークの順に並べてノード内に取り込む。
【００９０】
ノード分類機能部２３は、発火したノードを演算命令、分配命令、分岐命令、手続き呼び出し命令、手続き開始命令、手続き復帰命令、合流命令に分類し、そのノード種別をトークン出力機能に送る。
【００９１】
状態演算機能部２４は、ノード分類機能部２３よりノード種別を受け取り状態演算を行う。演算結果とノード種別を有限再帰判別演算機能部１５に送り、制御を有限再帰判別演算機能部１５に移す。
【００９２】
トークン出力機能Ｂ部２５の詳細構成図を図１４に示す。図中で、実線矢印は制御の流れを、点線矢印はデータの流れを表す。命令デコード機構は、ｌｉｎｅＢに流れてきたデータにより、ノード種別を知る。次に、対応する出力機構に対して、ｌｉｎｅＡに流れてきた状態ベクトルと、ｌｉｎｅＣに流れてきた有限再帰判別ベクトルをデータとして対応する出力機構に送り、制御を移行する。トークン消去機構はノード内に取り込んだトークンを消去する。各出力機構は命令の種類に応じて以下の様に動作する。以降トークンとはノード内に取り込んだトークンのことを指す。
【００９３】
演算命令出力機構は、入力アーク上に到達したトークンの値の経路断片識別子と、命令デコード機構より受け取ったデータを値としてトークンを生成し、出力アーク上に置く。
【００９４】
分配命令出力機構は、トークンの値の経路断片識別子と命令デコード機構より受け取ったデータを値とするトークンを生成し、全ての出力アーク上へ置く。
【００９５】
分岐命令出力機構は、第２入力アークに到達したトークンの値の経路断片識別子に対する孫値を２つ求める。求めた２つの経路断片識別子と命令デコード機構より受け取ったデータを値とする２つのトークンを生成する。新たに生成したトークンをそれぞれの出力アーク上へ置く。
【００９６】
手続き呼び出し命令出力機構は、命令デコード機構より受け取ったデータの有限再帰判別ベクトルと、関数表より求めた呼び出し先関数の有限再帰判別ベクトルと、各要素ごとに論理積を求める。命令デコード機構より受け取ったデータの状態ベクトルと、呼び出し先関数の状態ベクトルを関数表より求めて、式（５）により新たな状態ベクトルを求める。命令デコード機構より受け取った状態ベクトルの要素にＲが含まれず、演算結果にＲの要素がある場合には、その要素に対応するＲフラグの値を１とする。最終的に得られた有限再帰判別ベクトルと状態ベクトル、第２入力アーク上に到達したトークンの値の経路断片識別子を値とするトークンを生成する。生成したトークンを出力アーク上に置く。
【００９７】
手続き開始命令出力機構は、トークンの値の経路断片識別子と命令デコード機構より受け取ったデータを値とするトークンを生成し、出力アーク上へ置く。
【００９８】
手続き復帰命令出力機構は、動作しない。
【００９９】
合流命令出力機構は、各トークンの値より得られる経路断片識別子に対し、共通の先祖となる値を求める。求めた経路断片識別子と命令デコード機構より受け取ったデータを値とするトークンを生成し、このトークンを出力アーク上へ置く。
【０１００】
関数実行終了判定機能部２６は、検証実行中の関数の終了ノードのみにトークンがある場合、関数表更新機能部１３に制御を移行する。それ以外の場合には色付きトークン到達監視機能部２１へ制御を移行する。
【０１０１】
次に、演算命令、分配命令、分岐命令、手続き呼び出し命令、合流命令の実行例を示す。以降で用いる図では、点線の白丸ノードは演算ノードもしくは各制御ノード、「●（（…），ａ，ｂ）」は状態ベクトル（…）と経路断片識別子ａと有限再帰判別ベクトルｂを値として持つトークン、右下側のベクトルは、Ｒフラグ、左下側のベクトルはＥフラグを表す。ノードの環境レベルを右上に示す。
【０１０２】
図１５に演算命令の処理例を示す。図中で白丸は演算ノードを表す。演算命令では以下のような処理を行う。
（１）トークンが、演算ノードの全ての入力アーク上に揃い、発火規則にも合致するため、演算ノードは発火する。
（２）入力状態演算、到達状態演算、出力状態演算を行う。出力状態演算で求めた到達状態ベクトルの第４要素がＲとなったので、Ｒフラグの第４要素の値を１にする。
（３）ノード内に取り込んだ各トークンの値の有限再帰判別ベクトルにより有限再帰判別演算を行い、有限再帰判別ベクトルの値を更新する。図の場合には有限再帰判別ベクトル（１１１１１）と出力状態ベクトルと経路断片識別子ｃ₁ を値とするトークンを出力アーク上に置く。
【０１０３】
図１６に分配命令の実行例を示す。図中で白丸に十字のノードは分配ノードを示す。分配命令では以下のような処理を行う。
（１）トークンが分配ノードの入力アーク上に到達し、発火規則にも合致するため、分配ノードは発火する。
（２）入力状態演算、到達状態演算、出力状態演算を行う。出力状態演算で求めた出力状態ベクトルの第４要素がＲとなったので、Ｒフラグの第４要素の値を１とする。
（３）ノード内に取り込んだ各トークンの値の有限再帰判別ベクトルにより有限再帰判別演算を行い、有限再帰判別ベクトルの値を更新する。図の場合には有限再帰判別ベクトル（１１１１１）と出力状態ベクトルと経路断片識別子ｃ₁ を値とするトークンを出力アーク上に置く。
【０１０４】
図１７に分岐命令の処理例を示す。図中で楕円型のノードは分岐ノードを示す。分岐命令では以下のように処理を行う。
（１）トークンが分岐ノードの入力アーク上に到達し、発火規則にも合致するため、分岐ノードは発火を行う。
（２）入力状態演算、到達状態演算、出力状態演算を行う。到達状態演算で求めた到達状態ベクトルの第５要素がＥとなったので、Ｅフラグの第５要素の値を１にする。また、出力状態演算の際に、求めた出力状態レベルの第３、第４要素がＲと求まったので、Ｒフラグの第３、第４要素の値を１にする。
（３）ノード内に取り込んだ各トークンの値の有限再帰判別ベクトルにより有限再帰判別演算を行い、有限再帰判別ベクトルの値を更新する。経路断片識別子ｃ₁ の孫値となる値（ｃ₁₁，ｃ₁₂）を求める。図の場合には、真側の出力アーク上に真側の出力状態ベクトルと有限再帰判別ベクトル（１１１１１）と経路断片識別子ｃ₁₁を、偽側の出力アーク上に偽側の出力状態ベクトルと有限再帰判別ベクトル（１１１１１）と経路断片識別子ｃ₁₂を値とするトークンを置く。
【０１０５】
図１８に手続き呼び出し命令の処理例を示す。図中で長方形型のノードは手続き呼び出しノードを示す。手続き呼び出し命令では以下のように処理を行う。
（１）トークンが手続き呼び出しノードの入力アーク上に到達し、発火規則にも合致するため、手続き呼び出しノードは発火する。
（２）入力状態演算、到達状態演算、出力状態演算を行う。入力状態演算で求めた入力状態ベクトルの第４要素が新たにＲとなったので、Ｒフラグの第４要素の値を１にする。求めた状態ベクトルと関数表より得た状態ベクトルとを式（５）で演算を行い、状態ベクトルを求める。
（３）ノード内に取り込んだ各トークンの値の有限再帰判別ベクトルにより有限再帰判別演算を行い、有限再帰判別ベクトルの値を更新する。図の場合には有限再帰判別ベクトル（００１１１）と経路断片識別子ｃ₁ と出力状態ベクトルを値とするトークンを出力アーク上に置く。
【０１０６】
図１９に合流命令の処理例を示す。図中で逆三角形のノードは合流ノードを示す。合流命令では以下のように処理を行う。
（１）トークンがノード３の入力アーク上に到達し、発火規則にも合致するため、ノード３は発火を行う。
（２）ノード３において、入力状態演算、到達状態演算、出力状態演算を行う。
（３）ノード内に取り込んだ各トークンの値の有限再帰判別ベクトルにより有限再帰判別演算を行い、有限再帰判別ベクトルの値を更新する。図の場合には有限再帰判別ベクトル（１１１１１）と経路断片識別子ｃ₁ と出力状態ベクトルを値とするトークンを出力アーク上に置く。
【０１０７】
図２０に実行例を示す。図中で白丸ノードは演算ノード、楕円のノードは分岐ノード、白丸に十字のノードは分配ノード、長方形のノードは関数呼び出しノードを表す。網掛けのノードは実行フラグの立ったノード、ノードの右上の数字は環境レベル、左下のベクトルはＥフラグを、右下のベクトルはＲフラグを表す（図では更新されたフラグのみ記す）。ノードに与えられた環境レベルの中で、最大となるものは３であるため、全ての要素が”Ｔ”である３要素の状態ベクトルと、”ｃ”なる経路断片識別子と全ての要素の値が１の有限再帰判別ベクトルを値として持つトークンを、開始ノードにおいて処理を始める。
【０１０８】
１．図２０（１）の関数呼び出しノードが発火する際に、入力アーク上には（（ＴＴＮ），ｃ，（１１１））なる値を持つトークンが伝播してくる。発火した後には、出力状態ベクトルは（ＴＴＮ）と求まる。関数表の呼び出し先関数ｆの項の状態ベクトル（ＮＮＮ）と求めた出力状態ベクトルとで式（５）の演算を行うと（ＲＲＮ）が求まる。新たに第１，２要素がＲと求まったのでＲベクトルの第１，２要素を１にする。また、入力トークンの有限再帰判別ベクトルの論理積により（１１１）が求まる。この有限再帰判別ベクトルと関数表の有限再帰判別ベクトルとの論理積により（０００）が求まる。従って、関数呼び出し命令の出力アーク上に（（ＲＲＮ），ｃ，（０００））なる値を持つトークンを出力する（図２０（１））。
２．図２０（２）の分岐ノードが発火する際に、入力アーク上にはそれぞれ（（ＲＲＴ），ｃ，（０００）），（（ＲＲＮ），ｃ，（０００））なる値を持つトークンが伝播してくる。発火した後には出力状態ベクトルは（ＲＲＲ）と求まる。新たに第３要素がＲと求まったのでＲベクトルの第３要素を１にする。有限
【外６】

なる経路断片識別子を求める。従って、出力アーク上に（（ＲＲＲ），ｃ₁ ，（０００）），（（ＲＲＲ），ｃ₂ ，（０００））なる値を持つトークンを出力する。
３．関数に対する検証のための実行が終了したあと、終了ノードのトークンの有限再帰判別ベクトルと状態ベクトルを関数表に代入する（図２０（３））。
４．未検証の関数に対して検証のための実行を行い、実行が終了したあと、終了ノードのトークンの有限再帰判別ベクトルと状態ベクトルを関数表に代入する（図２０（４）〜（５））。
５．全ての関数の実行が終了したあと、関数表が更新されているか確認し、更新されている場合は、再び検証のための実行を行う。
６．図２０（６）の関数呼び出しノードが発火する際に、入力アーク上には（（ＴＴＮ），ｃ，（１１１））なる値を持つトークンが伝播してくる。発火した後に、トークンの有限再帰判別ベクトルの論理積により（１１１）が求まる。この有限再帰判別ベクトルと関数表の有限再帰判別ベクトルとの論理積により（１１１）が求まる。出力状態ベクトルと関数表の状態ベクトルにより（ＴＴＮ）なる状態ベクトルが求まる。従ってトークンの値を（（ＴＴＮ），ｃ₁ ，（１１１））として出力する。
７．図２０（７）では、分岐ノードの入力状態演算の際にトークンの値の状態ベクトルの第３要素が新たにＲと求まったのでＲベクトルの第３要素を１にする。
８．関数に対する検証のための実行が終了したあと、終了ノードのトークンの有限再帰判別ベクトルを関数表の有限再帰判別ベクトルに代入する（図２０（８））。
９．全ての関数の実行が終了したあと、関数表が更新されているか確認し、更新されている場合は、再び検証のための実行を行う（図２０（１０））。
１０．関数表に変化がなくなった時点で検証のための実行を終える。この時に、後述の表２で述べる検出条件により、異常の存在を確かめる。
以上説明したように、状態演算機能を有するデータ駆動実行型検証装置により、検証対象とするプログラムグラフを実行する。再帰関数検証系の終了判定機能により終了判定がなされた時点で、もしくは、実行経路検証系で検証中に実行中のノードがなくなった時点で、検証のための実行を終了する。このとき、トークンの位置と値、および、ノードのフラグの値を調べることにより表２に示すように各異常の発生を検出できる。
【０１０９】
【表２】

【０１１０】
【発明の効果】
以上説明したように、本発明によれば、状態演算機能を有するデータ駆動実行型検証装置により検証のための実行を行い、実行中のノードがなくなった時点で、または終了判定機能により終了することを決定した時点で検証のための実行を終了し、この時トークンの位置と値、およびノードのフラグの値を調べることにより可到達異常、伝播異常、全実行異常、合流異常を検出することができ、また有限再帰判別ベクトルの値を調べることにより関数の相互再帰呼び出しによる再帰異常を検出することができる。
【図面の簡単な説明】
【図１】異常のあるプログラムの例および検出できる異常の例を示す図である。
【図２】色付きトークンによる実行例を示す図である。
【図３】分岐ノードで色を与える際の問題点を示す説明図である。
【図４】扱う構造（繰り返しの表現）を示す図である。
【図５】扱う構造（分岐と合流）を示す図である。
【図６】経路断片識別子の例を示す図である。
【図７】従来の色付きトークンによるデータ駆動実行型検証装置の構成を示すブロック図である。
【図８】図７の検証装置に使用されているトークン出力機能Ａの詳細な構成を示すブロック図である。
【図９】従来のデータ駆動実行による検証例を示す図である。
【図１０】不完全な実行を行うグラフの例を示す図である。
【図１１】自関数の再帰呼出状態を示す図である。
【図１２】状態演算機能を示す図である。
【図１３】本発明の一実施例に係わる状態演算機能を有する検証装置の構成を示すブロック図である。
【図１４】図１３の検証装置に使用されているトークン出力機能Ｂ部の構成を示すブロック図である。
【図１５】演算命令の処理例を示す図である。
【図１６】分配命令の処理例を示す図である。
【図１７】分岐命令の処理例を示す図である。
【図１８】手続き呼び出し命令の処理例を示す図である。
【図１９】合流命令の処理例を示す図である。
【図２０】状態演算機能を用いた検証例を示す図である。
【符号の説明】
１ 再帰関数検証系
２ 実行経路検証系
１１ 関数表作成機能部
１２ 検証関数更新機能部
１３ 関数表更新機能部
１４ 終了判定機能部
１５ 有限再帰判別演算機能部
２１ 色付きトークン到達監視機能部
２２ トークン入力機能部
２３ ノード分類機能部
２４ 状態演算機能部
２５ トークン出力機能Ｂ部
２６ 関数実行終了判定機能部[0001]
[Industrial application fields]
The present invention relates to a data flow graph verification apparatus for a program executed by a data flow computer having an environment dependent firing function and an environment dependent distribution function.
[0002]
[Prior art]
First, an outline of the operation of the data flow computer that executes the target program in the verification apparatus will be described.
[0003]
In this data flow computer, a data flow graph composed of nodes assigned numerical data (referred to as environment level) is used as a program, and a token provided with numerical data (referred to as execution environment level) is used.
[0004]
Let N be the set of nodes. The environment level of the node n (nεN) is represented as tag (n). tag the environment level of the node connected to the tip of the nth i-th input arc_in(N, i), tag the environmental level of the node connected to the tip of the jth output arc of n_out(N, j). The execution environment level l is given to the token. At this time, l<tag_inAn arc extending from a node having an environment level satisfying (n, i) to n is called an n environment input arc.<tag_outAn arc stretched to a node having an environment level that satisfies (n, j) is called an environment output arc.
[0005]
The environment-dependent firing function is a function that causes a node to wait until all tokens are arranged on all environment input arcs, and fires a node after tokens are arranged on these arcs. The environment-dependent distribution function is a function that outputs a token giving an execution environment level on all environment output arcs.
[0006]
With the above function, when execution of a program is started with a certain execution environment level l assigned to a token, the token is propagated only between nodes having an environment level of 1 or higher, and only nodes having an environment level of 1 or higher are transmitted. Can be executed.
[0007]
Next, a colored token model using a path identifier will be described.
[0008]
By introducing the concept of colored tokens in a data flow execution device, it is possible to prevent interaction between tokens having different colors. Thereby, one graph can be executed simultaneously in a plurality of colors (environments).
[0009]
First, the basic model of the colored token will be described. FIG. 2 shows an execution example. In the figure, “● (K, a)” represents a token of value K color a. In FIG. 2B, since the tokens having the same color are not arranged on all the input arcs, the node is not ignited. In FIG. 2C, since the tokens having the same color i are aligned on all the input arcs, the node is ignited. When firing is performed in this way, the data flow graph can be shared by a plurality of execution environments by color.
[0010]
When performing verification, if all of a plurality of paths are divided into cases and verified one by one, the number of executions required increases as the number of branch instructions increases. For this reason, in order to complete the verification by executing one graph once, the branch instruction outputs tokens with different colors for all output arcs. At this time, a problem occurs in the case of a program having a structure as shown in FIG. On the arc indicated by a bold line in the figure, a branch node (a node having an SW character in an ellipse) gives a new color, and a token having a different color propagates, so that it cannot be ignited.
[0011]
In order to solve the above problem, for each branch path of a branch instruction (an instruction given to a branch node), a path fragment identifier (Kuniaki Naoi, Naohisa Takahashi: Inteable Path detection method using Presburger arithmetic, Intelligent Software Engineering) Study Group 1992, 11) Id_pfIs granted. This series <Id_pf1, Id_pf2, ..., Id_pfj> Is called a path identifier. By using the path identifier as the token color, tokens on a plurality of paths can be identified. The branch node that is the control node creates a path identifier by adding a different path fragment identifier depending on the branch direction to the color (path identifier) of the input token, and outputs this to the output arc as the token color.
[0012]
Where two colors c₁= <Id_p11, Id_p12, ..., Id_p1j>, C₂= <Id_p21, Id_p22, ..., Id_p2k> At this time, i = 1, 2,..., J (j<k), Id_p1i= Id_p2iC₁C₂Ancestors (c₂C₁
[Outside 1]

₂It is determined that tokens with the color carry the same environment value, and the node is fired. This means that the two paths branched at the branch node can be verified at the same time, and the results of the path fragments before the branch node can be shared by the verification in each path.
[0013]
Next, a data flow graph verification method will be described.
[0014]
First, the structure handled will be described. A program detected by the verification device that is not any of reachability abnormality, propagation abnormality, total execution abnormality, or merging abnormality is said to be “good structure”. A program having the following structure is executed correctly during normal execution, but is judged as a merging abnormality in this verification method. Since these structures can be converted to good structures having the same function, there is no problem.
[0015]
Consider a repetitive structure that constitutes a cycle using the branch nodes shown in FIG. This structure can be changed to FIG. Since such a designated repeated structure can be converted into a function re-call, this verification system allows only programs that do not constitute a cycle, and a structure including a cycle as shown in FIG. judge.
[0016]
In addition, the structure in which a plurality of paths shown in FIG. 5A share one execution path does not generate an error during execution. However, this structure can be converted into a simpler structure as shown in FIG. For this reason, in this verification system, as illustrated in FIG. 5C, only a program structure in which a branch structure is nested by a pair of a branch node and a merging node is allowed and not nested as shown in FIG. 5A. The structure is determined to have a merging abnormality.
[0017]
Next, the detected abnormality will be described. FIG. 1 shows an example of an abnormal program. In FIG. 1, a white circle node is an operation node, a black circle node is a distribution node, a white circle S node is a start node, a white circle E node is an end node, a white circle SW node is a branch node, and an inverted triangle node is A merge node and a square node represent one path formed by the nodes described above. The number at the upper left of the node indicates the node number. Each abnormality is described below.
[0018]
First, a propagation abnormality is a propagation abnormality when there is a path from a start node to a node other than an end node that does not output a token. In node 4 in FIG. 1 (g), the token cannot be output because there is no output arc.
[0019]
A reachability abnormality is said to be a reachability abnormality when there is no path through which a token propagates from the start node to the end node. For example, in FIG. 1, since the tokens cannot be output at the node 2 of (a) and the node 6 of (d), the tokens are arranged on the input arc at the node 4 of (b) and the node 3 of (c). Execution stops and the token does not reach the end node.
[0020]
An all-execution error is an all-execution error when there is a node that does not have a path for a token to reach from the start node. For example, in FIG. 1, node 2 in (b) and node 2 in (c) have no possibility of firing because there is no input arc.
[0021]
The merging abnormality is said to be a merging abnormality in which there are merging nodes that are used for purposes other than collecting paths branched by a branch instruction. For example, in FIG. 1, in the node 5 of (e), two tokens propagate along the path ahead of the joining node and collide. In FIG. 1, the node 2 to 4 in (f) is always in a loop state, and tokens collide on the previous path.
[0022]
By using the token having the above-mentioned path fragment identifier as a value for execution of verification, it is detected whether the program has a good structure. For this purpose, the firing rules are defined as follows.
[0023]
In the case of a merging node, for example, when a tree representing allocation of path fragment identifiers as shown in FIG.₁And c₂Or c_ThreeAnd c_FourFired when tokens having sibling path fragment identifiers are aligned on the input arc.
[0024]
Otherwise, it fires when tokens with equal path fragment identifiers are aligned on the input arc.
[0025]
Next, an execution method for verification will be described. By indicating the execution state of the node, all execution abnormality is detected. For this purpose, a flag is assigned to each node. This flag is called an execution flag. When the value of the execution flag is 1, it means that the node is executed, and when it is 0, it means that the node is not executed. The initial value is 0.
[0026]
The verification apparatus initializes execution flags assigned to all nodes on the data flow graph to 0, and then performs processing in the following manner.
1. Wait until tokens arrive on all input arcs.
2. After the tokens are aligned on the input arc, the node is ignited according to the firing rules described in the previous section. At this time, the execution flag of the node is set to 1, and the token on the input arc is taken into the node.
3. A token obtained by copying the value of the token in the node (in the case of a joining node, the token value is the parent path fragment identifier) is output on the output arc. If there is no output arc, leave the token in the node.
[0027]
By firing each node according to the above execution method, the entire graph is executed in asynchronous parallel.
[0028]
An abnormality detection condition will be described. The verification apparatus causes the verification target program to be executed, and the verification execution is terminated when there is no node being executed. At this time, the following Table 1 can be said.
[0029]
[Table 1]

FIG. 7 shows the configuration of a conventional verification apparatus. In the figure, solid arrows indicate the flow of control, and dotted arrows indicate the flow of data. Each function in the figure will be described.
Token arrival monitoring function: Detects nodes with tokens on all input arcs and fires them based on firing rules. If the node fires, the execution flag of the node is set to 1 and control is transferred to the token input function.
Token input function: The tokens on the input arc are arranged in the order of the input arc and taken into the node.
Node classification function: The fired node is classified into an operation instruction, a distribution instruction, a branch instruction, a procedure call instruction, a procedure start instruction, a procedure return instruction, and a merge instruction, and the node type is sent to the token output function.
Token output function A: A detailed configuration diagram of the token output function A is shown in FIG. In the figure, solid arrows indicate the flow of control, and dotted arrows indicate the flow of data. The instruction decoding mechanism knows the node type from the data flowing to line A, and shifts control to the corresponding output mechanism. The token erasure mechanism erases the token captured in the node. Each output mechanism operates as follows according to the type of instruction. Note that the token that has reached the input arc refers to a token that has been captured in the node.
[0030]
The operation instruction output mechanism generates a token by copying the value of the token that has reached the input arc, and places the token on the output arc.
[0031]
The distribution command output mechanism creates a new token by copying the value of the token that has arrived on the input arc, and places it on all the output arcs.
[0032]
The branch instruction output mechanism obtains two grandchild values of the path fragment identifier obtained from the value of the token reached on the second input arc. Two tokens whose values are the obtained two path fragment identifiers are generated and placed on the output arc, respectively.
[0033]
The procedure call instruction output mechanism copies the token on the second input arc and places it on the first input arc of the procedure start node. In addition, a token having a value corresponding to the name of the output arc is generated. A procedure return node of the function is obtained from the function name stored as the token value on the first input arc, and the generated token is placed on the first input arc of the node.
[0034]
The procedure start instruction output mechanism places a copy of the token on the input arc on the output arc.
[0035]
The procedure return instruction output mechanism uses the value on the second input arc to generate a token (result value). Place the token (return destination) in the arc specified as the value of the token on the first input arc.
[0036]
The merge command output mechanism obtains a common ancestor value for the path fragment identifier obtained from the token value on each input arc. A token whose value is the obtained path fragment identifier is generated, and this token is placed on the output arc.
[0037]
FIG. 9 shows an execution example. In the figure, a black circle represents a token, a white circle node represents an operation node, and a white circle and cross node represent a distribution node. A hatched node represents a node with an execution flag. The following describes the operation of the execution example.
1. Path fragment identifier c from the start node₁A token with the value In a function call node, the value is c₁Is placed on the input arc of the procedure start node (FIG. 9C).
2. When the function verification ends and the procedure return node fires, the return destination arc is obtained from the value of the token placed in the first input arc of the procedure return node, and the token is placed on the obtained arc (FIG. 9). (D)).
3. For branch nodes, the path fragment identifier obtained from the token value on the input arc
[Outside 2]

Find the road segment identifier. Next, the obtained path fragment identifier is output as a token value (FIG. 9E).
[0038]
As shown in FIG. 9, when tokens are arranged on all input arcs, an execution flag is set on a node and tokens are placed on output arcs. After the token reaches the end node (FIG. 9 (f)), the token or node having the detection conditions shown in Table 1 does not exist on the graph.
[0039]
[Problems to be solved by the invention]
When a conventional verification device is applied to a program executed on a dataflow computer having an environment-dependent firing function and environment-dependent distribution function, even if no abnormality is detected, depending on how the environment level is assigned to the node, a certain execution environment level Then, reachability abnormality, propagation abnormality, total feasibility abnormality, and merging abnormality may occur.
[0040]
For example, consider a program with environmental levels as shown in FIG. Here, a white circle node represents an operation node, and a white circle-cross node represents a distribution node. The numerical value on the left side of each node represents the node number, and the numerical value on the right side represents the environmental level. When tokens at execution environment levels 1 and 2 are used, the program operates normally in any of the programs shown in FIGS. 10 (a), 10 (b), and 10 (c). However, when an execution environment level 3 token is propagated, the following problems occur in the programs shown in FIGS.
[0041]
In FIG. 10A, there is a path through which a token of execution environment level 3 propagates from node 1 to node 10. However, even though the environment level is 3, the node 6 is not executed because the token of the execution environment level 3 does not arrive.
[0042]
In FIG. 10B, there is a path through which the execution environment level 3 token propagates from the node 1 to the node 10. However, the token of the execution environment level 3 that has reached the node 4 cannot execute the node beyond this. For this reason, this token does not reach the node 10.
[0043]
In FIG. 10C, the token of the execution environment level 3 that has reached the node 7 cannot execute the node beyond this. For this reason, the token does not reach the node 10.
[0044]
When the execution is performed for each execution environment level, the above-described error may occur. However, the verification by the conventional verification device only detects the reachability abnormality, propagation abnormality, total execution abnormality, and merge abnormality due to the structure of the graph. No feasibility abnormality or merge abnormality is detected. For this reason, the above-mentioned error cannot be detected.
[0045]
Further, as shown in FIG. 11, a structure that does not stop by recursive calling of its own function is conceivable. However, the conventional verification method cannot detect such a structure, and execution for verification does not stop. This abnormality is called a recursive abnormality.
[0046]
To solve this problem, it is detected at all execution environment levels that all nodes that should be executed at a given execution environment level are executed and a token is propagated from the start node to the end node of the program. There is a need.
[0047]
The present invention has been made in view of the above, and the object of the present invention is for all execution environment levels in a program including a recursive function executed by a data flow computer having an environment-dependent firing function and an environment-dependent distribution function. It is an object of the present invention to provide a data flow graph verification device that detects a reachability abnormality, a propagation abnormality, a total execution abnormality, a merging abnormality, and a recursive abnormality due to a recursive function call.
[0048]
[Means for Solving the Problems]
  In order to achieve the above object, according to the first aspect of the present invention, a data flow graph in which nodes having environment levels are connected by arcs is used as a program, and tokens having execution environment levels are propagated on the nodes via arcs. This is a data flow graph verification device that verifies the normality of token propagation in a program that is controlled by the environment-dependent firing function and environment-dependent distribution function. , The input state indicating whether or not the token can be input to the node is calculated for each execution environment level based on the status of the token propagation and error occurrence to the node on the path through which the token has propagated, Based on the input state and the environment level of the node, the arrival state indicating whether the node will fire The arrival state calculation required for each execution environment level is performed, and the output state that indicates whether the token can be output is calculated for each execution environment level based on the arrival state and the environment level of the output arc destination node. It has a state calculation function part.
  The invention according to claim 2 is the invention according to claim 1, wherein when a node is ignited, the call is made to the token input to the node and based on the stoppage of the function given to the token input to the node. A finite recursive discriminant that performs a finite recursive discriminant operation that determines the state indicating the execution stoppage by the mutual call of the function according to the node type based on the execution stoppage of the callee function when the destination function is given It further has a calculation function part.
[0049]
[Action]
In the data flow graph verification device of the present invention, focusing on the nodes on the path through which the token has propagated, each of the input state, the arrival state, and the output state is defined as the state and input state for each input arc execution environment level. State calculation is performed for each execution environment level based on the environment level of the node, the arrival state, and the environment level of the output arc destination node, the output state of the call destination function is taken over, and the state of the nodes in the function is calculated.
[0050]
【Example】
Embodiments of the present invention will be described below with reference to the drawings.
[0051]
Before describing the embodiments, first, the basic concept of the data flow graph verification apparatus of the present invention will be described. The verification apparatus detects means 1 for detecting a reachability abnormality, propagation abnormality, total execution abnormality, merge abnormality, recursive abnormality for an arbitrary environmental level, and a state in which a function does not stop due to a recursive function call. Means 2 are included.
[0052]
First, the means 1 will be described, and the state calculation therein will be described.
[0053]
The execution environment level is represented by a numerical value (a natural number is used here). The larger the value, the higher the level. Here, the state of token propagation at a certain execution environment level is called the state of the execution environment level, and its value is expressed as follows.
T: A token may be propagated during normal program execution.
N: The token is not propagated during normal program execution.
R: Cannot fire during normal program execution. Or, a state where the token cannot be output has occurred.
E: A state that is not executed during normal program execution has occurred.
[0054]
[Outside 3]

s₂The operation is defined as follows.
[0055]
[Expression 1]

Also, a one-dimensional vector representing all execution environment level states with the state of the execution environment level of level 1 as the l-th element is called a state vector. At this time, the state vector S₁= (S₁₁, S₁₂, ..., s_1n), S₂= (S_{twenty one}, S_{twenty two}, ..., s_2n)
[Outside 4]

[Expression 2]

The token value on the jth input arc of the node is T_j= (T_j1, T_j2, ..., t_jn). At this time, T_jIs a state vector, t_jkIndicates the status of token propagation and error occurrence for a node on the path through which the token has propagated at the execution environment level k. I = (i₁, I₂, ..., i_n) Is called an input state vector, and an operation for obtaining the input state vector is called an input state operation. When the value of the m-th element of the input state vector is T, it indicates that the token of execution environment level m reaches on all environment input arcs.
[0056]
[Equation 3]

[0057]
R = (r₁, R₂, ..., r_m, ..., r_n) Is an arrival state vector, and an operation for obtaining an arrival state vector is called an arrival state operation. When the value of the m-th element of the arrival state vector is T, it indicates that the node is fired with the token of the execution environment level m. Note that tag is the environmental level of the node.
[0058]
[Expression 4]

Let the arrival state vector be R = (r₁, R₂, ..., r_m, ..., r_n), Each element is obtained by the following equation for the j-th output arc._j= (O_j1, O_j2, ..., o_jm, ..., o_jn) Is an output state vector, and an operation for obtaining an output state vector is called an output state operation. When the value of the m-th element of the output state vector is T, it indicates that a token of execution environment level m can be output. Tag_out(J) is the jth output arc destination
[Outside 5]

is there.
[0059]
[Equation 5]

The state calculation function shown in FIG. 12 detects reachability abnormality, propagation abnormality, total execution abnormality, merge abnormality, and recursion abnormality at each execution environment level. In the figure, solid arrows indicate control flow, and dotted arrows indicate data flow. Each node of the data flow graph has two one-dimensional vectors called R flag and E flag. The m-th element of these flags represents an abnormality occurrence state at the execution environment level m. When the value of the element of the R flag is 1, it means that the node cannot fire or cannot output a token at the execution environment level corresponding to the element. When the value of the element of the E flag is 1, it means that the node is not executed because the token does not reach the input arc of the node at the execution environment level corresponding to the element.
[0060]
The initial values of these flag elements are zero. Hereinafter, each mechanism of the state calculation function will be described.
[0061]
The value reading mechanism reads a value from the token fetched in the node, and sends the value as data to the input state calculation mechanism.
[0062]
The output arc determination mechanism sends the environmental level of the node at the output arc destination as data to the output state calculation mechanism.
[0063]
The input state calculation mechanism receives a token value from the value reading mechanism and receives a node type from line A, and performs an input state calculation. The calculation result is sent as data to the arrival state calculation mechanism. If R is not included in the value of the input token and there is an element that becomes R in the result of Expression (7), the value of the R flag corresponding to that element is set to 1.
[0064]
The arrival state calculation mechanism receives an input state calculation result from the input state calculation mechanism and performs an arrival state calculation. The calculation result is sent as data to the output state calculation mechanism. If the element of the value received from the input state calculation mechanism is E or N and there is an element for which R is obtained by the calculation, the value of the R flag corresponding to that element is set to 1. If the element of the value received from the input state calculation mechanism is N or E, and there is an element for which E is obtained by the calculation, the value of the E flag corresponding to that element is set to 1.
[0065]
The output state calculation mechanism receives the result of the arrival state calculation from the arrival state calculation mechanism, receives the node type from line A, and receives the environmental level of the node at the output arc destination from the output arc determination mechanism, and performs the output state calculation. The calculation result is output as data. If there is an element for which R is obtained by the calculation, the value of the R flag corresponding to that element is set to 1.
[0066]
In an execution path verification system having a state calculation function, execution is performed for verification by performing processing in the following manner on all nodes of the data flow graph.
[0067]
1. Wait until tokens arrive on all input arcs.
2. After tokens are aligned on the input arc, the node is ignited according to the same firing rules as in the prior art. At this time, the execution flag of the node is set to 1, and the token on the input arc is taken into the node.
3. The state calculation function operates each mechanism.
4). A new token is generated from the output from the output state calculation mechanism, the path fragment identifier of the token fetched in the node, and the finite recursive discrimination vector. The newly generated token is output on the output arc. Erase the token in the node.
[0068]
Next, the means 2 will be described.
[0069]
The finite recursive discriminant vector is a one-dimensional vector having a logical value representing the execution stoppage property due to the mutual call of functions as an element. When the element value is 1, the call is stopped, and when it is 0, the call is not stopped. Represent. A table that associates the function name used by the program, the finite recursive discriminant vector, and the state vector of the function obtained from the execution path verification system is called a function table.
[0070]
Verification is performed by the execution path verification system, and when a node is ignited, the following finite recursive discrimination operation is performed for each node.
[0071]
For the merge node, a logical sum is obtained for each element of the finite recursive discrimination vector obtained from the value of each token.
[0072]
For the procedure call node, a logical product is obtained for each element of the finite recursive discrimination vector given as the value of each token. Further, a logical product is obtained for each element of the obtained finite recursive discriminant vector and the finite recursive discriminant vector of the function call destination function.
[0073]
For other nodes, the logical product is obtained for each element.
[0074]
The recursive function verification system operates as follows when the execution path verification system performs execution for verification.
1. A function to be verified is obtained from the functions used in the program, and the verification target function name, the finite recursive discriminant vector of the verification target function, and the state vector of all elements are sent to the execution path verification system.
2. After execution of the state calculation function of the execution path verification system, a finite recursive discrimination calculation is performed. 3. When the execution path verification system receives a signal indicating that the execution for verification of the function has been completed, the state of the verified function is checked, and the function term is updated in the function table. An execution end determination for verifying the program is performed. If the execution is not ended, the process returns to 1.
[0075]
As described above, the data-driven execution verification device having the state calculation function performs the verification, and the verification is performed when there is no node being executed, or when the termination determination function determines that the termination is performed. End execution for. At this time, it is possible to know the reachability abnormality, propagation abnormality, total execution abnormality, merging abnormality by examining the token position and value, and the flag value of the node, and by examining the value of the finite recursive discrimination vector, Recursion anomalies due to mutual recursive calls to functions can be known.
[0076]
Next, examples of the present invention will be described in detail.
[0077]
In the present embodiment, the firing rules are determined as follows. The function return node fires when a token arrives on the second input arc. Other nodes are the same as in the prior art.
[0078]
FIG. 13 is a block diagram showing the configuration of the verification apparatus of this embodiment having a state calculation function. In FIG. 13, a solid arrow indicates a control flow, and a dotted arrow indicates a data flow.
[0079]
The verification apparatus shown in FIG. 13 has a recursive function verification system 1 and an execution path verification system 2. The recursive function verification system 1 includes a function table creation function unit 11, a verification function update function unit 12, a function table update function unit 13, an end determination function unit 14, and a finite recursive discrimination calculation function unit 15. The execution path verification system 2 includes a colored token arrival monitoring function unit 21, a token input function unit 22, a node classification function unit 23, a state calculation function unit 24, a token output function B unit 25, and a function execution end determination function unit 26. ing.
[0080]
First, each component of the recursive function verification system 1 will be described.
[0081]
The function table creation function unit 11 creates a function table representing the correspondence between the function name used in the verification target program, the finite recursive discrimination vector in which all element values are 0, and the state vector in which all elements are N. The created function table is registered as a function table and an existing function table in the storage device. Also, the verification function name in the storage device is emptied. Finally, control is transferred to the verification function update function unit 12.
[0082]
The verification function update function unit 12 obtains a function table and a verification function name from the storage device. Next, a function that has not yet been verified is obtained from the verification function name, the execution flag, R flag, and E flag of all nodes of the function are initialized, and the token is erased. For a function start node (or on the input arc of a procedure start node), T is the element corresponding to the maximum value among the environment levels given to the node, and N is a state vector with more than that. A finite recursive discriminant vector whose element value is 1 and a token whose value is a path fragment identifier are placed, and the function name is registered in the verification function name. When verification for all functions is completed, control is transferred to the termination determination function unit 14.
[0083]
The function table update function unit 13 uses the value of the finite recursion discriminant vector and the state vector obtained from the token value for the function having the token at the end node, and the finite recursion discriminant vector of the corresponding function in the function table in the storage device. And assign to the state vector. Control is transferred to the verification function update function unit 12.
[0084]
The end determination function unit 14 compares the function table in the storage device with the existing function table, and ends the execution for verification if they are equal. If they are different, the function table in the storage device is registered in the storage device as an existing function table, and the verification function name in the storage device is made empty. Control is transferred to the verification function update function unit 12.
[0085]
The finite recursive discrimination calculation function unit 15 receives the node type from the state calculation function and performs a finite recursive discrimination calculation. The calculation result and the node type are sent to the token output mechanism, and control is transferred to the token output function B unit 25.
[0086]
Next, each component of the execution path verification system 2 will be described.
[0087]
The token arrival monitoring function unit 21, the token input function unit 22, and the node classification function unit 23 are the same as those in the prior art, and are as follows.
[0088]
The token arrival monitoring function unit 21 detects a node in which tokens are arranged on all input arcs, and ignites them based on the firing rules. If the node fires, the execution flag of the node is set to 1 and control is transferred to the token input function.
[0089]
The token input function part 22 arranges the tokens on the input arc in the order of the input arcs and takes them into the node.
[0090]
The node classification function unit 23 classifies the fired node into an operation instruction, a distribution instruction, a branch instruction, a procedure call instruction, a procedure start instruction, a procedure return instruction, and a merge instruction, and sends the node type to the token output function.
[0091]
The state calculation function unit 24 receives the node type from the node classification function unit 23 and performs state calculation. The calculation result and the node type are sent to the finite recursive discrimination calculation function unit 15, and control is transferred to the finite recursion discrimination calculation function unit 15.
[0092]
A detailed configuration diagram of the token output function B unit 25 is shown in FIG. In the figure, solid arrows indicate the flow of control, and dotted arrows indicate the flow of data. The instruction decoding mechanism knows the node type based on the data flowing to lineB. Next, to the corresponding output mechanism, the state vector flowing to line A and the finite recursive discrimination vector flowing to line C are sent as data to the corresponding output mechanism, and control is transferred. The token erasure mechanism erases the token captured in the node. Each output mechanism operates as follows according to the type of instruction. Hereinafter, the token refers to a token taken into the node.
[0093]
The arithmetic instruction output mechanism generates a token by using the path fragment identifier of the token value reached on the input arc and the data received from the instruction decoding mechanism as values, and places the token on the output arc.
[0094]
The distribution instruction output mechanism generates tokens whose values are the path value identifier of the token value and the data received from the instruction decoding mechanism, and places them on all output arcs.
[0095]
The branch instruction output mechanism obtains two grandchild values for the path fragment identifier of the token value that has reached the second input arc. Two tokens are generated with the two path fragment identifiers obtained and the data received from the instruction decoding mechanism as values. Place the newly created token on each output arc.
[0096]
The procedure call instruction output mechanism obtains a logical product for each element of the finite recursion discriminant vector of the data received from the instruction decode mechanism, the finite recursion discriminant vector of the callee function obtained from the function table. The state vector of the data received from the instruction decoding mechanism and the state vector of the callee function are obtained from the function table, and a new state vector is obtained from equation (5). If R is not included in the element of the state vector received from the instruction decoding mechanism and there is an R element in the operation result, the value of the R flag corresponding to that element is set to 1. A token is generated whose value is the path fragment identifier of the finally obtained finite recursive discrimination vector and state vector, and the token value reached on the second input arc. Place the generated token on the output arc.
[0097]
The procedure start instruction output mechanism generates a token whose value is the path fragment identifier of the token value and the data received from the instruction decode mechanism, and places it on the output arc.
[0098]
The procedure return instruction output mechanism does not operate.
[0099]
The merge command output mechanism obtains a common ancestor value for the path fragment identifier obtained from the value of each token. A token whose value is the obtained path fragment identifier and data received from the instruction decoding mechanism is generated, and this token is placed on the output arc.
[0100]
The function execution end determination function unit 26 transfers control to the function table update function unit 13 when there is a token only in the end node of the function being verified. In other cases, control is transferred to the colored token arrival monitoring function unit 21.
[0101]
Next, execution examples of an operation instruction, a distribution instruction, a branch instruction, a procedure call instruction, and a merge instruction are shown. In the diagrams used in the following, dotted white circle nodes are operation nodes or control nodes, and “● ((..., A, b)” is a state vector (...), A path fragment identifier a, and a finite recursive discrimination vector b. The token held, the lower right vector represents the R flag, and the lower left vector represents the E flag. The environmental level of the node is shown in the upper right.
[0102]
FIG. 15 shows a processing example of the operation instruction. In the figure, white circles represent operation nodes. The arithmetic instruction performs the following processing.
(1) Since the tokens are aligned on all the input arcs of the computation node and match the firing rules, the computation node fires.
(2) Input state calculation, arrival state calculation, and output state calculation are performed. Since the fourth element of the arrival state vector obtained by the output state calculation is R, the value of the fourth element of the R flag is set to 1.
(3) A finite recursive discriminant operation is performed using the finite recursive discriminant vector of each token value fetched in the node, and the value of the finite recursive discriminant vector is updated. In the case of the figure, a finite recursive discrimination vector (11111), an output state vector, and a path fragment identifier c₁Place a token with value on the output arc.
[0103]
FIG. 16 shows an execution example of the distribution instruction. In the figure, white circles indicate cross nodes. The distribution instruction performs the following processing.
(1) The distribution node fires because the token arrives on the input arc of the distribution node and matches the firing rules.
(2) Input state calculation, arrival state calculation, and output state calculation are performed. Since the fourth element of the output state vector obtained by the output state calculation is R, the value of the fourth element of the R flag is set to 1.
(3) A finite recursive discriminant operation is performed using the finite recursive discriminant vector of each token value fetched in the node, and the value of the finite recursive discriminant vector is updated. In the case of the figure, a finite recursive discrimination vector (11111), an output state vector, and a path fragment identifier c₁Place a token with value on the output arc.
[0104]
FIG. 17 shows an example of branch instruction processing. In the figure, elliptical nodes indicate branch nodes. The branch instruction performs the following processing.
(1) Since the token reaches the input arc of the branch node and matches the firing rule, the branch node fires.
(2) Input state calculation, arrival state calculation, and output state calculation are performed. Since the fifth element of the arrival state vector obtained by the arrival state calculation is E, the value of the fifth element of the E flag is set to 1. In addition, since the third and fourth elements of the obtained output state level are obtained as R during the output state calculation, the values of the third and fourth elements of the R flag are set to 1.
(3) A finite recursive discriminant operation is performed using the finite recursive discriminant vector of each token value fetched in the node, and the value of the finite recursive discriminant vector is updated. Route fragment identifier c₁A value (c₁₁, C₁₂) In the case of the figure, the true output state vector, the finite recursive discriminant vector (11111), and the path fragment identifier c on the true output arc.₁₁On the false output arc, the false output state vector, the finite recursive discriminant vector (11111), and the path fragment identifier c.₁₂Put a token whose value is.
[0105]
FIG. 18 shows a processing example of the procedure call instruction. In the figure, rectangular nodes indicate procedure call nodes. The procedure call instruction performs the following processing.
(1) Since the token arrives on the input arc of the procedure call node and matches the firing rule, the procedure call node fires.
(2) Input state calculation, arrival state calculation, and output state calculation are performed. Since the fourth element of the input state vector obtained by the input state calculation is newly R, the value of the fourth element of the R flag is set to 1. The obtained state vector and the state vector obtained from the function table are calculated by equation (5) to obtain the state vector.
(3) A finite recursive discriminant operation is performed using the finite recursive discriminant vector of each token value fetched in the node, and the value of the finite recursive discriminant vector is updated. In the case of the figure, a finite recursive discrimination vector (00111) and a path fragment identifier c₁And put a token whose value is the output state vector on the output arc.
[0106]
FIG. 19 shows a processing example of the merge instruction. In the figure, the inverted triangle nodes indicate the merge nodes. The merge instruction performs the following processing.
(1) Since the token arrives on the input arc of node 3 and matches the firing rule, node 3 fires.
(2) At node 3, input state calculation, arrival state calculation, and output state calculation are performed.
(3) A finite recursive discriminant operation is performed using the finite recursive discriminant vector of each token value fetched in the node, and the value of the finite recursive discriminant vector is updated. In the case of the figure, the finite recursive discrimination vector (11111) and the path fragment identifier c₁And put a token whose value is the output state vector on the output arc.
[0107]
FIG. 20 shows an execution example. In the figure, white circle nodes represent operation nodes, ellipse nodes represent branch nodes, white circle cross nodes represent distribution nodes, and rectangular nodes represent function call nodes. A shaded node indicates a node with an execution flag, an upper right number indicates an environment level, a lower left vector indicates an E flag, and a lower right vector indicates an R flag (only updated flags are shown in the figure). Among the environment levels given to the node, the maximum is 3, so that a three-element state vector in which all elements are “T”, a path fragment identifier of “c”, and values of all elements Starts processing a token having a finite recursive discrimination vector of 1 as a value at the start node.
[0108]
1. When the function call node in FIG. 20 (1) fires, a token having a value of ((TTN), c, (111)) propagates on the input arc. After firing, the output state vector is determined as (TTN). (RRN) is obtained by performing the calculation of Expression (5) with the state vector (NNN) of the term of the callee function f in the function table and the obtained output state vector. Since the first and second elements are newly determined as R, the first and second elements of the R vector are set to 1. Further, (111) is obtained by the logical product of the finite recursive discrimination vector of the input token. (000) is obtained by the logical product of this finite recursive discriminant vector and the finite recursive discriminant vector of the function table. Therefore, a token having a value of ((RRN), c, (000)) is output on the output arc of the function call instruction (FIG. 20 (1)).
2. When the branch node in FIG. 20 (2) fires, tokens having values of ((RRT), c, (000)) and ((RRN), c, (000)) propagate on the input arc, respectively. Come on. After firing, the output state vector is determined as (RRR). Since the third element is newly determined as R, the third element of the R vector is set to 1. Finite
[Outside 6]

Is obtained. Therefore, ((RRR), c on the output arc₁, (000)), ((RRR), c₂, (000)) is output.
3. After execution for verification of the function is completed, the finite recursive discriminant vector and the state vector of the token of the end node are substituted into the function table (FIG. 20 (3)).
4). Execution for verification is performed on the unverified function, and after the execution is completed, the finite recursive discriminant vector and the state vector of the token of the end node are substituted into the function table (FIGS. 20 (4) to (5)). .
5). After all functions have been executed, it is checked whether the function table has been updated. If it has been updated, execution for verification is performed again.
6). When the function call node in FIG. 20 (6) fires, a token having a value of ((TTN), c, (111)) propagates on the input arc. After firing, (111) is obtained by the logical product of the finite recursive discriminant vectors of tokens. (111) is obtained by the logical product of this finite recursive discriminant vector and the finite recursive discriminant vector of the function table. A state vector (TTN) is obtained from the output state vector and the state vector of the function table. Therefore, the token value is ((TTN), c₁, (111)).
7). In FIG. 20 (7), since the third element of the state vector of the token value is newly determined as R during the calculation of the input state of the branch node, the third element of the R vector is set to 1.
8). After execution for verification of the function is completed, the finite recursive discriminant vector of the token of the end node is substituted into the finite recursive discriminant vector of the function table (FIG. 20 (8)).
9. After the execution of all functions is completed, it is checked whether the function table has been updated. If it has been updated, execution for verification is performed again (FIG. 20 (10)).
10. When the function table no longer changes, execution for verification is finished. At this time, the presence of an abnormality is confirmed based on detection conditions described in Table 2 to be described later.
As described above, the program graph to be verified is executed by the data driven execution type verification apparatus having the state calculation function. When the end determination is made by the end determination function of the recursive function verification system, or when there is no node being executed during verification in the execution path verification system, the execution for verification ends. At this time, occurrence of each abnormality can be detected as shown in Table 2 by examining the token position and value and the value of the node flag.
[0109]
[Table 2]

[0110]
【The invention's effect】
As described above, according to the present invention, execution for verification is performed by the data driven execution type verification apparatus having the state calculation function, and the process is terminated when there is no node being executed or by the end determination function. The execution for verification is terminated at the time of determination, and at this time, the reachability error, propagation error, total execution error, and merge error can be detected by examining the token position and value and the value of the node flag. In addition, by examining the value of the finite recursive discriminant vector, it is possible to detect recursive anomalies due to mutual recursive calls of functions.
[Brief description of the drawings]
FIG. 1 is a diagram illustrating an example of a program having an abnormality and an example of an abnormality that can be detected.
FIG. 2 is a diagram illustrating an execution example using colored tokens.
FIG. 3 is an explanatory diagram showing a problem when a color is given at a branch node.
FIG. 4 is a diagram illustrating a structure to be handled (repetition expression).
FIG. 5 is a diagram showing a structure to be handled (branching and merging).
FIG. 6 is a diagram illustrating an example of a route fragment identifier.
FIG. 7 is a block diagram showing a configuration of a conventional data driven execution type verification apparatus using colored tokens.
8 is a block diagram showing a detailed configuration of a token output function A used in the verification apparatus of FIG.
FIG. 9 is a diagram showing a verification example by conventional data driving execution.
FIG. 10 is a diagram illustrating an example of a graph that performs incomplete execution;
FIG. 11 is a diagram showing a recursive call state of the own function.
FIG. 12 is a diagram illustrating a state calculation function.
FIG. 13 is a block diagram showing a configuration of a verification apparatus having a state calculation function according to an embodiment of the present invention.
14 is a block diagram showing a configuration of a token output function B unit used in the verification apparatus of FIG. 13;
FIG. 15 is a diagram illustrating a processing example of an arithmetic instruction.
FIG. 16 is a diagram illustrating a processing example of a distribution command.
FIG. 17 is a diagram illustrating a processing example of a branch instruction.
FIG. 18 is a diagram illustrating a processing example of a procedure call instruction.
FIG. 19 is a diagram illustrating a processing example of a merge instruction.
FIG. 20 is a diagram illustrating a verification example using a state calculation function.
[Explanation of symbols]
1 Recursive function verification system
2 Execution path verification system
11 Function table creation function
12 Verification function update function part
13 Function table update function
14 End determination function part
15 Finite recursive discrimination function
21 Colored token arrival monitoring function
22 Token input function part
23 Node classification function
24 State calculation function part
25 Token output function part B
26 Function execution end judgment function part

Claims (2)

A data flow graph in which nodes with environment levels are connected by arcs is used as a program, and tokens with execution environment levels are propagated on the nodes via arcs, and firing control is performed by the environment-dependent firing function and environment-dependent distribution function. A data flow graph verification device for verifying the normality of token propagation in a program,
Paying attention to the node on the path that the token has propagated,
Perform an input state calculation for each execution environment level based on token propagation to the node on the path that the token has propagated and the status of error occurrence, indicating the state of whether the token can be input to the node,
Perform arrival state calculation for each execution environment level, based on the input state and the environment level of the node, the arrival state indicating whether or not the node is ignited,
Data having a state calculation function unit for performing an output state calculation for each execution environment level based on an arrival state and an environment level of an output arc destination node as an output state indicating whether or not a token can be output Flow graph verification device. When a node fires, it is based on the execution stoppage of the function assigned to the token input to the node, and if the call destination function is assigned to the token input to the node, the call destination function is executed. The finite recursive discriminant calculation function part which performs the finite recursive discriminant calculation which calculates | requires the state showing the execution stop property by the mutual call of a function according to a node classification based on stop property further Data flow graph verification device.

Images