(57)【要約】【課題】パラメトリック実行時間解析装置及び解析方法を提供する。【解決手段】実時間性を持つソフトウェア部品は、実行時間がプロセッサなどの実行環境に依存するため、異なる環境への再利用は一般に困難である。従来方法は有限オートマトンに基づいており、再帰呼び出しがあるプログラムは扱えなかった。本発明は、パラメトリック実行時間解析を用いて、プログラムの実行時間を個々の処理の実行時間と繰り返し回数とのパラメータを用いた式の形で求めることにより、異なる実行環境においても実時間制約を満たすためのパラメータの最適化を、数理計画法を用いて行うものであり、一般化Parikhの定理に基づき、再帰を含むプログラムを扱うことを可能にしたものである。【選択図】図１
2013171352.tif 000002
【特許請求の範囲】
【請求項１】
マーカー注釈された対象プログラムソースコードを入力する入力手段、
プログラム処理品質パラメータの指定を注釈として持つ高級言語プログラムから、アセンブラプログラムを生成するコンパイラ手段、
該コンパイラ手段にて生成されたアセンブラプログラムから、その制御フローを表現する文脈自由文法を生成する文脈自由文法生成手段、
前記文脈自由文法生成手段にて生成された文脈自由文法から、語の順序が可換とみなした場合に等価となる正規表現を求める正規表現生成手段、
該正規表現生成手段にて得られた正規表現から、プログラムの最悪実行時間を表わし、一般にパラメータ変数を含む式を導出するパラメトリック実行時間解析手段、
該パラメトリック実行時間解析手段にて得られたパラメータ付最悪実行時間と時間制約から、時間制約を満たすためのパラメータに関する制約条件を導き、その制約の下で、与えられた目的関数を最適化するパラメータ群の最適値の組を導出するパラメータ最適化手段、
を含むことを特徴とするパラメトリック実行時間解析装置。
【請求項２】
マーカー注釈された対象プログラムソースコードを入力するステップ、
プログラム処理品質パラメータの指定を注釈として持つ高級言語プログラムから、アセンブラプログラムを生成するステップ、
該コンパイラ手段にて生成されたアセンブラプログラムから、その制御フローを表現する文脈自由文法を生成するステップ、
前記文脈自由文法生成手段にて生成された文脈自由文法から、語の順序が可換とみなした場合に等価となる正規表現を求めるステップ、
該正規表現生成手段にて得られた正規表現から、プログラムの最悪実行時間を表わし、一般にパラメータ変数を含む式を導出するステップ、
該パラメトリック実行時間解析手段にて得られたパラメータ付最悪実行時間と時間制約から、時間制約を満たすためのパラメータに関する制約条件を導き、その制約の下で、与えられた目的関数を最適化するパラメータ群の最適値の組を導出するステップ、
を含むことを特徴とするパラメトリック実行時間解析方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、パラメトリック実行時間解析装置及び解析方法に関する。
【背景技術】
【０００２】
近年、組込みソフトウェアの高機能化・高性能化が進んでいる一方で、市場競争により、限られた開発期間で、実時間制約の充足と低コスト化、低消費電力化を達成するソフトウェア開発手法が求められている。
【０００３】
そのような大規模化する実時間ソフトウェアの開発期間短縮のためには、通常のソフトウェアと同様にソフトウェア部品の再利用が有効であると考えられる。しかし、特に実時間性を持つソフトウェア部品に関しては、実行時間がプロセッサなどの実行環境に依存するため、異なる環境への再利用は一般に困難である（非特許文献１）。
【０００４】
例えば、実時間動画圧縮ソフトウェアや暗号処理ソフトウェアなどにおいては、圧縮率、解像度、暗号強度など、それを変更することによってソフトウェアの機能を損なわず、処理の品質のみに影響する設計パラメータが存在している。それらのパラメータの多くはプログラムの特定箇所の繰り返し回数と関連している。それらのパラメータ、およびCPUの動作周波数の最小限の調整により、新しい動作環境でプログラムが実時間制約を満たし、かつ低消費電力で実行できるようにする最適設計支援方法が望まれる。
【０００５】
ソフトウェアの実時間制約の保証のために、従来、プログラムの最悪実行時間(Worst Case Execution Time: WCET）解析方法（非特許文献２、３）が研究されてきた。これらの既存のWCET解析方法を実時間ソフトウェアの再利用に用いる場合、次のような問題が生じる。
・プロセッサ、バス、メモリなどのハードウェアや (システムコールを利用しているソフトウェアの場合)OSなどの実行環境を指定しなければ正確な実行時間の見積もりが困難である。
・解析の結果、実時間制約を満たさないと判明した場合、その制約を満たすように修正を行う一般的な指針がない。
・再利用対象のソフトウェアを最適に実行できる動作環境の仕様決定に用いたい場合には、実行環境を変えながら試行錯誤で解析するしかない。
【０００６】
これらの問題を解決するために、パラメトリックプログラム実行時間解析方法（非特許文献４）が提案された。この文献４は、単一CPU単一タスクの実行環境で動作する実時間ソフトウェアを対象とし、実時間プログラムのソースコード、実行環境の情報及びプログラムの実行時間に関する実時間制約が与えられたときに、一般にプログラム及び実行環境のパラメータに関する多項式の形で、実時間制約を満たして、解析対象のプログラムの最悪実行時間の見積もりを自動導出するというものである。ここで、プログラムのパラメータとは、プログラムの指定した個所の繰り返し回数であるとし、実行環境のパラメータとしては、CPUの動作周波数および各命令後の実行に要する主要クロック数の上限および下限であるとする。
【０００７】
従来のWCET解析方法などでは、実行環境パラメータを具体的に与える必要があり、それらの最適値は試行錯誤で探す必要があった。しかしこの方法では、実時間制約を満たすための最適なパラメータの条件を選択することが可能となる。
【０００８】
非特許文献４に記載の方法では、プログラムの制御構造を有限オートマトンの形で抽出し、正規表現に変換することによりプログラムの繰り返し構造を導出し、プログラムの実行時間をループ回数の関数として導出している。しかし、再帰呼び出しを含むプログラムのクラスは有限オートマトンで表現可能なプログラムのクラスより大きいことが知られており（非特許文献７）、一般に再帰呼び出しがあるプログラムは扱えないという問題があった。
【０００９】
一方、非特許文献５では、正規表現の代数的モデルであるKleene代数において連接演算（積）を可換とした代数（可換Kleene代数）を用いて、任意の文脈自由言語に対してその語の終端記号の順序を入れ替えても等価とみなした語集合が正規表現で表現可能であることが示されており（一般化Parikhの定理）、その正規表現を求めるアルゴリズムが提案されている。任意の再帰を含むプログラムは文脈自由文法で表現可能であり、プログラムの実行時間は（キャッシュやパイプライン実行などによる微妙な影響を無視すれば）個々の単位動作の実行時間の合計のみに依存し、その実行順には依存しないため、文献５の結果を援用することにより、任意の再帰を含むプログラムの繰り返し構造を表現する正規表現を導出することができる。
【先行技術文献】
【非特許文献】
【００１０】
【非特許文献１】N. G. Leveson and K. A. Weiss: “Making embedded software reuse practical and safe”, Proc. of the 12th ACM SIGSOFT Int. Symp. on Foundations of Software Engineering (FSE 2004) ,pp.171-178, 2004.
【非特許文献２】P. Puschner and A. Burns: “A review of worst-case execution-time analysis”, The Int. Journal of Time-Critical Computing Systems, 18, pp.115-128, 2000.
【非特許文献３】J. Engblom, A. Ermedahl, M. Sjodin, J. Gustafsson and H. Hansson: “Worst-case execution-time analysis for embedded real-time systems”, Int. Journal of Software Tools for Technology Transfer, 4, pp.437-455, 2003.
【非特許文献４】河井敏宏,中田明夫：「実時間ソフトウェア再利用のためのパラメトリック実行時間解析の一手法」,信学技報SS,Vol.107,No.505,pp.97-102, 2008.
【非特許文献５】W. Hopkins and C. Kozen: “Parikh's theorem in Commutative Kleene Algebra”, Proc. of the 14th IEEE Symp. on Logic In Computer Science (LICS 1999), pp.394-401, 1999.
【非特許文献６】ARM Ltd.: “ARM7TDMI Technical Reference Manual”, Revision r4p1,    http://infocenter.arm.com/ help/topic/com.arm.doc.ddi0210c/, 2004.
【非特許文献７】都倉信樹:「オートマトンと形式言語」, pp. 47-128,昭晃堂, 2002.
【非特許文献８】P. Puschner and C. Koza: “Calculating the maximum, execution time of real-time programs”, Real-Time Systems, Vol. 1, No. 2, pp. 159176, 1989.
【発明の概要】
【発明が解決しようとする課題】
【００１１】
本発明は、前述のような事情にかんがみてなされたものであり、可換Kleene代数における一般化Parikhの定理に基づいた、再帰を含むプログラムに対するパラメトリック実行時間解析装置及び解析方法を提供するものである。
【００１２】
本発明に係る解析方法は、以下の順序で実行される。
1．プログラムソースから、プログラムの各文の実行順の可能性を示す文脈自由文法を生成する。
2．得られた文脈自由文法を、各文の実行回数が等しくなるような正規表現に変換する。
3．得られた正規表現から、プログラムの実行時間をパラメータに関する式で導出する。
また、本発明では、解析対象のプログラムソースから得られた文脈自由文法を入力とし、その文脈自由文法を正規表現に変換して、最悪実行時間を出力する解析装置を提供する。この装置を用いていくつかのプログラムを対象にパラメータ付き最悪実行時間を導出し、提案方法の有効性を実証する。
【課題を解決するための手段】
【００１３】
請求項1に係るパラメトリック実行時間解析装置は、マーカー注釈された対象プログラムソースコードを入力する入力手段、プログラム処理品質パラメータの指定を注釈として持つ高級言語プログラムから、アセンブラプログラムを生成するコンパイラ手段、該コンパイラ手段にて生成されたアセンブラプログラムから、その制御フローを表現する文脈自由文法を生成する文脈自由文法生成手段、前記文脈自由文法生成手段にて生成された文脈自由文法から、語の順序が可換とみなした場合に等価となる正規表現を求める正規表現生成手段、該正規表現生成手段にて得られた正規表現から、プログラムの最悪実行時間を表わし、一般にパラメータ変数を含む式を導出するパラメトリック実行時間解析手段、該パラメトリック実行時間解析手段にて得られたパラメータ付最悪実行時間と時間制約から、時間制約を満たすためのパラメータに関する制約条件を導き、その制約の下で、与えられた目的関数を最適化するパラメータ群の最適値の組を導出するパラメータ最適化手段、を含むものである。
【００１４】
請求項２に係るパラメトリック実行時間解析方法は、マーカー注釈された対象プログラムソースコードを入力するステップ、プログラム処理品質パラメータの指定を注釈として持つ高級言語プログラムから、アセンブラプログラムを生成するステップ、該コンパイラ手段にて生成されたアセンブラプログラムから、その制御フローを表現する文脈自由文法を生成するステップ、前記文脈自由文法生成手段にて生成された文脈自由文法から、語の順序が可換とみなした場合に等価となる正規表現を求めるステップ、該正規表現生成手段にて得られた正規表現から、プログラムの最悪実行時間を表わし、一般にパラメータ変数を含む式を導出するステップ、該パラメトリック実行時間解析手段にて得られたパラメータ付最悪実行時間と時間制約から、時間制約を満たすためのパラメータに関する制約条件を導き、その制約の下で、与えられた目的関数を最適化するパラメータ群の最適値の組を導出するステップ、を含むものである。
【発明の効果】
【００１５】
本発明によれば、パラメータ付き最悪実行時間が正しく導出され、導出時間も極めて短時間とすることができる。
【図面の簡単な説明】
【００１６】
【図１】本発明に係るパラメトリック実行時間解析装置の構成を示すブロック図である。
【図２】本発明に係るパラメトリック実行時間解析方法の動作を説明するためのフローチャートである。
【図３】C言語でのプログラム例(fact.c)を示す図である。
【図４】パラメトリック実行時間解析を説明するためのフローチャートである。
【図５】本発明に係るパラメトリック実行時間解析装置を説明するための概略フローチャートである。
【図６】コンパイル後のアセンブラコードの命令語数と導出時間の関係を示すグラフである。
【発明を実施するための形態】
【００１７】
図１において、１は、マーカー注釈された対象プログラムソースコードを入力する入力手段、２は、入力手段１にて入力されたプログラムソースコードをコンパイルし、アセンブラコードを得るコンパイラ生成手段、３は、このアセンブラコードの制御フローを解析し、文脈自由文法に変換する制御フロー解析手段、４は、文脈自由文法から、一般化Parikhの定理を用いて正規表現に変換する正規表現変換手段、５は、正規表現と、各命令語の実行時間の情報より、パラメータ付き最悪実行時間を導出するパラメトリック実行時間解析手段、６は、パラメータ付き最悪実行時間、時間制約、目的関数から、数理計画問題ソルバよりパラメータの最適値を求めるパラメータ最適化手段、７は、得られた最適値のデータを出力する出力手段である。これらは、コンピュータにより構成される。
【００１８】
図２に示すように、本実施形態にかかる解析方法は以下のステップよりなる。
ステップS1：マーカー注釈された対象プログラムソースコードを入力する。
【００１９】
ステップS2：入力手段１にて入力されたプログラムソースコードをコンパイルし、アセンブラコードを得る。すなわち、既存のコンパイラを用いて、プログラム処理品質パラメータの指定を注釈として持つ高級言語プログラムから、アセンブラプログラムを生成するのである。ここでプログラム言語はインラインアセンブラ構文をサポートしたコンパイラが利用可能な任意のものでよい。プログラム処理品質パラメータとは、プログラム中のループの繰り返し回数パラメータのことであり、プログラムの具体的な機能に応じて画像処理の解像度や暗号処理の暗号強度などに対応する。プログラム処理品質パラメータの指定は、インラインアセンブラ構文を用いて、プログラムの特定箇所にマーカーという注釈記述を行うことで指定する。マーカーとは、プログラムの指定箇所の実行回数が指定したパラメータ変数（又は定数）の値となることの指定である。
【００２０】
ステップS3：アセンブラコードの制御フローを解析し、文脈自由文法に変換する。
これは次の順序で行なわれる。
・アセンブラプログラムの先頭からi番目の命令に対して、非終端記号Siを対応付ける。
・アセンブラコードの具体的な各命令語aに対して、終端記号aを対応付ける。
・アセンブラプログラム内に現れる各マーカーm(X) (Xは指定されたパラメータ変数)に対して、終端記号m(X)を対応付ける。
・先頭からi番目の命令語が分岐命令以外の通常の命令語aであったならば、生成規則Si->aSi+1を対応付ける。
・先頭からi番目の命令語がマーカーm(X)であったならば、生成規則Si->m(X)Si+1を対応付ける。
・先頭からi番目の命令語が無条件分岐命令bであり、分岐先が先頭からj番目の命令語ならば、生成規則Si->bSjを対応付ける。
・先頭からi番目の命令語が条件分岐命令cであり、条件成立時の分岐先が先頭からj番目の命令語ならば、生成規則Si->cSj | cSi+1を対応付ける。
・先頭からi番目の命令語が無条件コール命令dであり、分岐先が先頭からj番目の命令語ならば、生成規則Si->dSjSi+1を対応付ける。
・先頭からi番目の命令語が条件コール命令eであり、条件成立時の分岐先が先頭からj番目の命令語ならば、生成規則Si->eSjSi+1|eSi+1を対応付ける。
【００２１】
ステップS4：文脈自由文法から、一般化Parikhの定理を用いて正規表現に変換する。
この際、求めた正規表現が(α・m(X)・β)^* の形の部分式をもつとき、これらの部分式をそれぞれ (α・β)^X に置換する。（Xは任意のパラメータ変数名）
・この置換は、マーカーm(X)を含むもっとも内側の部分式から行う。
・任意の(E)^*の形の部分式は高々１つのマーカーしか含まないと仮定する。
・そのようなプログラム、すなわち、繰り返しループ中に高々１つのマーカーが指定されたプログラムのみを対象とする。
【００２２】
ステップS5：正規表現と、各命令語の実行時間の情報より、パラメータ付き最悪実行時間を導出する。ここで、各命令語の実行時間は、プロセッサパラメータ等の式で与えられている。
【００２３】
ステップS6：パラメータ付き最悪実行時間、時間制約、目的関数から、数理計画問題ソルバよりパラメータの最適値を求める。すなわち、得られたパラメータ付最悪実行時間と時間制約から、時間制約を満たすためのパラメータに関する制約条件を導き、その制約の下で、与えられた目的関数を最適化するパラメータ群の最適値の組を導出するのである。
ステップS7：得られた最適値のデータを出力する。
【００２４】
本発明で扱うパラメトリック実行時間解析とは、入力としてプログラムの総実行時間を個々の手続き文の実行時間及びプログラムの再帰回数やループ文の繰り返し回数に関する式の形で出力するものである。C言語での再帰を含むプログラム例を図３に示す。
【００２５】
図３に示すように、プログラムソースコードの各関数、またはループ文の内部に対して、明示的に対応付けするために、プログラムの設計者が手動でインラインアセンブラ構文を用いて“marker=X”(Xはパラメータ変数名、または定数)という文字列を、コンパイル後のアセンブラコードの対応する箇所に埋め込まれるように挿入する。この文字列をマーカーと呼ぶ。マーカーに指定したパラメータ変数(もしくは定数)Xのことを以下、マーカー変数と呼ぶ。マーカーの位置のコードの繰り返し回数がマーカー変数に対応付けられているものとする。
【００２６】
入力となる解析対象のプログラムとは、図３に示すような、再帰が書ける任意の手続き型プログラムで、繰り返し回数の最大値が有限であるようなプログラムとする。
【００２７】
実行環境情報
プログラムの各文の実行時間は、CPU速度など、実行環境に依存する。そこで、本発明では解析対象のプログラムを構成する各文（単位動作）の最悪実行時間があらかじめ与えられているとする。 本発明では、特に現実のプログラムコードを対象とし、コンパイラの最適化オプションに依存しない実行時間の見積もりを得るため、プログラムソースをコンパイルした後のアセンブラコード（ネイティブコード）を解析対象とし、プロセッサの動作周波数f、および、各命令語の最悪実行サイクル数wj (j=1,…,p) (pは命令語の総数)をパラメータ変数、もしくは定数で与えるものとする。以下、fやwjなどのパラメータを実行環境パラメータと呼ぶ。例えば、 ARM社の組込み用32ビットRISCプロセッサARM7TDMI（非特許文献６）の各命令語の実行サイクル数(一部)は、表２に示す通りである。
【表１】
2013171352.tif 000003
【００２８】
I：内部データ処理サイクル数(レジスタ間転送のみ)
S：逐次メモリアクセスサイクル数
N：非逐次メモリアクセスサイクル数
n：転送メモリワード数
m：乗数のワード幅（単位：バイト）
【００２９】
パラメトリック実行時間解析
パラメトリック実行時間解析とは、前述した方法でマーカー変数（又は定数）xi (i=1,…,k) (kはマーカーの総数)によって注釈付けられたプログラムソースコードと、そのプログラムソースコードの実行環境情報、すなわち、プロセッサ動作周波数fおよび各命令語の最悪実行サイクル数wj (j=1,…,p)が与えられたときに、パラメータ付き最悪実行時間を表す式を導出することである。ここで、パラメータ付き最悪実行時間とは、入力となるプログラムを、実行環境情報で指定した実行環境で、マーカー位置の繰り返し回数が指定した回数となるように実行したときの実行時間の最悪値の見積もりを、各マーカー変数xi、実行環境パラメータf、wjの関数の形で求めたものである。
【００３０】
例えば、ARMプロセッサの例では、各命令語の最悪実行サイクル数wjはパラメータS,N,Iの関数となるので、パラメータ付き最悪実行時間は、例えば(4S + (2N + I)×X)/f (Xは繰り返し回数パラメータ)のように表現される。このパラメトリック実行時間解析の概要を図２に示す。
【００３１】
解析方法の流れ
本発明方法の説明として、まず、プログラムと文脈自由文法の対応について説明する。次に、文脈自由文法から正規表現への変換手法を説明し、最後に正規表現から実行時間を導出する方法を説明する。
【００３２】
文脈自由文法の生成
文脈自由文法（非特許文献７）は、左辺が一つの非終端記号で、右辺が終端記号と非終端記号からなる長さ0以上の系列であるような生成規則の集合、および開始記号の指定（非終端記号から一つ選択）からなるものである。文脈自由文法の詳細な定義は省略する。 終端記号の集合をΣとする。左辺が等しい２つの生成規則A → w、 A → w’をA → w |w’と略記する。3つ以上の場合も同様とする。また、特に断りのない限り、生成規則において英小文字および数字は終端記号、英大文字で始まる記号列は非終端記号を表すものとする。
【００３３】
解析対象となるプログラムソースコードから、文脈自由文法を生成する際、次のような方針で変換する。
・生成する語が、プログラムにおける文の実行順の任意の可能性を表すように変換する。
・プログラムの逐次実行は「語の連接」に対応させる。
・if文などの分岐は「｜」に対応させる。
・関数定義は、関数に対応する非終端記号を導入し、生成規則の左辺にその非終端記号、右辺に関数の本体を表す語を記述することで表現する。
・関数呼び出しは、関数を非終端記号に対応させ、当該関数を呼び出している位置にその非終端記号を記述することで表現する。
・繰り返し文やジャンプ命令などは、等価な関数呼び出しに変換する。
例えば図３に示すプログラムの関数Factを非終端記号Fとし、3行目のif文をa、4行目をb、7行目をcという実行環境情報から得られたパラメータ変数、または定数とし、上記の方針に従って変換すると、次式で表される。
【数１】
2013171352.tif 000004
【００３４】
正規表現への変換
正規表現（非特許文献７）は、以下の（a）〜（f）の規則で定義されるもの全体である。
（a）記号ε、φは正規表現である。
（b）a∈Σであるとき、aは正規表現である。
（c）EとFが正規表現ならば、(E +F)も正規表現である。
（d）EとFが正規表現ならば、(E・F)も正規表現である。
（e）Eが正規表現ならば(E)*も正規表現である。
（f）（a）〜（e）までで定義されるもののみが正規表現である。
【００３５】
正規表現の意味は、Σ上の語集合への対応関係により定義される。正規表現E、Fに対応する語集合を[E]、[F]とすると、[ε]= {ε}、 [φ]=φ、 [E+F]=[E]∪[F]、 [E・F]=[E]・[F] (右辺の「・」は語集合の連接演算)、 [(E)*]=[E]*と定義される。正規表現E・Fは、「・」を省略してEFと書いても同じ意味であるとする。
【００３６】
文脈自由文法で生成される言語で正規表現では表せないものが存在することが知られている（非特許文献７）。 従って、一般には任意の文脈自由言語に対してそれを表現する正規表現を求めることはできない。しかし、語の各記号の順序を入れ替えた語を等価とみなした場合、文脈自由文法が表す言語と等価な言語を表現する正規表現を求めることができる。 例えば「aaabbb」と「ababab」は異なる語である。しかし、「a」と「b」がそれぞれ単一で実行時間を表すとすると、2つの語が表す実行時間は、どちらも「ab」の三つ分で等しいとみなせる。一般に文脈自由言語{anbn|n>0}は正規言語ではないが、記号の順序を入れ替えても等価とみなすことにより、等価な正規表現(ab)*を得ることができる。
【００３７】
そのような文脈自由文法から正規表現への変換は、可換Kleene代数における一般化Parikhの定理（非特許文献５）を用いることで行える。（可換）Kleene代数は、φを0（加法単位元）、εを1（乗法単位元）、 +を加法(‘+’)、・を乗法(‘・’)、 *を*に対応させることで正規表現を代数で表現したものであり、形式的には以下のように定義される（非特許文献５）。
【００３８】
定義1
Kleene代数とは7つ組(Σ,S,+,・,*,0,1)で、任意のp、q ∈ Σ∪Sに対して加法('+')に関してべき等（すなわち、p + p = p）であり、加法('+')および乗法('・')に関して半環('+'に関して逆元のない環)を成し、以下の公理を満たすものと定義する。
【数２】
2013171352.tif 000005
【００３９】
ただし、「≦」は以下のように定義する。
【数３】
2013171352.tif 000006
【００４０】
可換Kleene代数とは、乗法「・」が可換であるようなKleene代数であると定義する。
【００４１】
例として、図３のプログラムから生成した文脈自由文法(1)を文献５に記載の方法に基づいて正規表現に変換する手順を示す。まず、文法の各生成規則から可換Kleene代数の不等式へと変換する。可換Kleene代数の不等式への変換を下記に示す。
【００４２】
・各非終端記号を変数(x、y、zなど)に変換。
・「｜」は和(+)に、連接は積(・)に変換。
・各終端記号はそのまま定数として扱う。
・ループ（for文など）は、( )*に変換する(*は繰り返し回数とする)。
・空語(ε)は定数1に、空集合(φ)は定数0に変換。
・生成規則（左辺）→（右辺）を不等式（右辺）≦（左辺）に変換。
【００４３】
これに従って数式１を変換すると、以下のようになる。
【数４】
2013171352.tif 000007
【００４４】
次に得られた可換Kleene代数上の連立不等式系の最小解を求める。この最小解は可換Kleene代数において元の文脈自由文法が生成する言語と等価となる（非特許文献５）。この最小解を可換Kleene代数における一般化Parikhの定理に基づいて導出する。この定理は以下のように述べられる。
【００４５】
定理1（一般化Parikhの定理（非特許文献５））
可換Kleene代数の不等式f(x)≦xの最小解はf’(f(0))*・f(0)で表せる。ただし、f(x)を可換Kleene代数上のxに関する任意の多項式とし、f’(x)は以下を満たすf(x)の変形操作(fの「微分」と呼ばれる)とする。
【数５】
2013171352.tif 000008
【００４６】
定理1を用いて数式４の最小解を求めると、
【数６】
2013171352.tif 000009
【００４７】
となり、これが図３のプログラムと各文の実行回数が等しくなるような正規表現となる。
【００４８】
最悪実行時間の導出
最悪実行時間は正規表現から導出する。正規表現Eに対応する最悪実行時間をET(E)とすると、 ET(0) = ∞(停止しないプログラムに対応)、 ET(1) = 0、 ET(E・F) = ET(E)+ET(F)、 ET(E+F) = max(ET(E)、 ET(F))、 ET(E*) = ET(E)×m(E) (ただし、m(E)は正規表現E中で*演算子のスコープ外に現れるマーカー変数)という規則に従って導出する。 マーカー変数は、入れ子になっている場合を除き、一つの繰り返し中にマーカーの指定はただ一つしか存在しないと仮定している。
【００４９】
例えば図３に示す関数Factの呼び出し回数を表すマーカー変数をNとし、式６の正規表現から実行時間を求めると、以下のようになる。
【数７】
2013171352.tif 000010
【００５０】
解析方法の概要
以下本発明に係る解析方法では、解析対象の再帰を含むプログラムソースコードから得られた文脈自由文法を入力とし、可換Kleene代数の方程式の解を求めて、パラメータ付き最悪実行時間を表す式が出力される。図３に解析対象の最悪実行時間を表す式を導出する解析方法の概要を示す。
【００５１】
入力形式
本発明方法では、次のような文脈自由文法Gを入力とする.実行環境情報は前述したARM7TDMIプロセッサの情報を用いる（他の実行環境にも容易に対応可能である）。Gは非終端記号をSi (iは先頭からi番目の命令語に対応)とした文脈自由文法Si → ｗの集合である。ただし、wは可換Kleene代数の記法で次のように記述されるものとする。 例えば、図３の文脈自由文法(1)を入力とすると、次式となる。
【数８】
2013171352.tif 000011
【００５２】
実際には、解析対象プログラムをコンパイルした後のアセンブラコードの各命令語について次のような生成規則を対応させる.ただし本方法は、アセンブラコードから変換した文法のみならず、ユーザが任意に入力した文脈自由文法を処理可能である。
【００５３】
まず各命令語に対して終端記号を対応付ける。次に、解析対象プログラムの i番目の命令語が分岐以外の通常の命令語aならば、生成規則Si → a・Si+1に対応させる. 特にaがマーカーm(X) (Xはマーカー変数名)であっても同様に、生成規則Si → m(X)・Si+1に対応させる.i番目の命令語が無条件分岐bならば生成規則Si → b・Sｊ(jは分岐先の命令語の番号)、条件分岐cならばSi → c・Sｊ+ c・Si+1、無条件コール命令dならばSi → d・Sj・Si+1と変換する（条件コール命令なども同様に変換可能）。最後に、開始記号はS1とする.このように得られた文脈自由文法を入力とし、二分木のデータ構造に変換する。この変換部分の実装は、構文規則に基づいてパーサ(ソースコードの構文解析を行うコンパイラの一部分)を生成するyacc (Yet Another Compiler-Compiler)、および、字句解析を行うlex  (Lexical analyser generator)を用いて行った。
【００５４】
最悪実行時間を表す式の導出
非特許文献６により、文脈自由文法の生成規則x→f(x)に対応する可換Kleene代数の不等式f(x)≦xの最小解は、次式で求められることが知られている。
【数９】
2013171352.tif 000012
【００５５】
例えば、式８の生成規則に式９を適用すると、S1を表す正規表現を以下のように求めることができる。
【数１０】
2013171352.tif 000013
【００５６】
本発明方法では、この求めた解により、一般にプログラム及び実行環境のパラメータ付き最悪実行時間の見積もりを導出する。この解を導出する操作を以下に示す。
1．f(x)の変数xに0を代入し、f(0)を求める。
2．f(x)を変数xで微分し、f’(x)を求める。
3．f’(x)の変数xにf(0)を代入し、f’(f(0))を求める。
微分を求める操作については定理1に基づいて行う。なお、複数の変数を含む式が入力となる場合は、そのうち１つの変数に着目し、その他の変数を定数とみなして定理１を適用することにより変数を１つずつ消去する。例えば、
【数１１】
2013171352.tif 000014
【００５７】
このような場合は、変数S2に着目し、変数S1を定数とみなして定理１を適用し解を求めると、次のような解が得られる。
【数１２】
2013171352.tif 000015
【００５８】
このS2の解である式１２の右辺には変数S2が現れることはなく、また、変数S2を持つ他の不等式に代入すれば、入力内容全体からS2という変数を消去できる。例えば、式１２にはまだS1という変数が残っているが、式１２に式１０を代入すれば、次のような解を得ることができる。
【数１３】
2013171352.tif 000016
【００５９】
このような手順により、相互再帰など任意の再帰構造を持つプログラムに対して解を得ることができる。
【００６０】
分割統治法による効率化
複雑な式になると計算量が増えてしまい、ツールを用いる環境によっては導出が困難になる可能性がある。そこで、本発明では基本ブロック毎にパラメータ付き最悪実行時間を表す式を導出し、その後に導出したすべての式を統括する分割統治法で導出の簡単化を図っている。
【００６１】
ここで基本ブロックとは、コンピュータにおいて一つの入り口と一つの出口を持ち、内部に分岐を含まないプログラムソースコードを指す。基本ブロックの終了は、他のプログラムソースコードへのジャンプ命令である。以下に、この基本ブロック毎に分割してパラメータ付き最悪事項時間を表す式を導出する手順を以下に述べる。
【００６２】
1.入力を可換Kleene代数の形式に変換する。
2.変換された入力を基本ブロック毎に分割する。
3.基本ブロック毎にパラメータ付き最悪実行時間を表す式を導出する。
4.各基本ブロックを単位動作とみなした文脈自由文法を構成し、各基本ブロックの最悪実行時間を未定パラメータとしたパラメトリック最悪実行時間の式を導出する。
5.4.で求めた式に3.で求めた各基本ブロックの最悪実行時間を表す式を代入し、簡約化する。
5.で簡約化が終わると、パラメータ付き最悪実行時間の式がmax{e1、…、em}という形で得られる。ただし、mは実行時間が最悪になり得るプログラムの実行経路の総数である。これらの式e1、…、emをパラメトリック最悪実行時間の候補と呼ぶ。
【実施例】
【００６３】
実験
実験目的及び方法
図３で示した再帰を含む例題fact.c(命令語数39)及び非特許文献８で用いられたカメラで撮影して得られた画像から重心を計算する画像処理プログラムcamera_example.c(命令語数164)を対象とし、適用実験を行った。
【００６４】
実験環境は、CPU：Intel Core2 Duo 2.53GHz、OS：Windows XP Professional、メモリ：1.98GBである。この下で、camera_example.cとfact.cのパラメータ付き最悪実行時間を導出し、結果の正しさを評価する。また、camera_example.cのサイズの異なるいくつかのコード断片について導出することにより、プログラムサイズに対する導出時間の変化を評価した。
【００６５】
実験結果
fact.cでは再帰呼び出しの繰り返し回数を示すマーカー変数Nの1次式で、パラメータ付き最悪実行時間が正しく導出され、導出時間は0.2秒かからなかった。camera_example.cでは画像処理の繰り返し回数を示す縦画素数と横画素数のマーカー変数の2次式で、パラメータ付き最悪実行時間が正しく導出され、導出時間は1.5秒かからなかった。よって、解析の導出時間は小規模のプログラムに対しては十分高速であるといえる。
【００６６】
次に、camera_example.cのコンパイル後のコードについて、先頭からn語まで(n = 66、88、118、141、152、164)のコード断片について解析を行い、導出時間の変化を評価した。その結果を図４に示す。図に示す66語〜130語までの解析結果では最悪実行時間の候補が2つ導出でき、141語〜164語の解析結果では候補が4つ導出できた。図４より、最悪実行時間の候補数が導出時間に差をつけたといえる。また、候補が2つの時と4つの時では、それぞれ導出時間がほぼ一定であるため、導出時間は最悪実行時間の候補数に関係するといえる。
【産業上の利用可能性】
【００６７】
本発明は、高機能化、高性能化が進んでいる組込みソフトウェアの分野において、実時間制約の充足と低コスト化、低消費電力化を達成するソフトウェア開発に適用して有用である。
【符号の説明】
【００６８】
１      入力手段
２      コンパイラ生成手段
３      制御フロー解析手段
４      正規表現変換手段
５      パラメトリック実行時間解析手段
６      パラメータ最適化手段
７      出力手段  
【図１】
2013171352.tif 000017
【図２】
2013171352.tif 000018
【図３】
2013171352.tif 000019
【図４】
2013171352.tif 000020
【図５】
2013171352.tif 000021
【図６】
2013171352.tif 000022