2006 Fiscal Year Annual Research Report
| Project/Area Number |
18700028
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
中田 明夫 大阪大学, 大学院情報科学研究科, 助教授 (60295839)
|
|---|
| Keywords | 組込みソフトウェア / 実時間制約 / パイプラインプロセッサ / モデル検査 / 実行時間解析 / パラメトリック解析 |
|---|
| Research Abstract |
命令キャッシュを持つパイプラインプロセッサ上で実行される任意の機械語プログラムが、指定した実時間制約を満たすための、プロセッサの動作周波数およびプログラム中の各ループの実行回数に関する条件式を自動導出する手法を提案した。提案手法は、入力として、機械語プログラムコード、プロセッサアーキテクチャ情報、および、プログラムの各部分の実行時間の間に成立すべき実時間制約をとる。機械語プログラムとしては、命令語としてロード、ストア、算術論理演算およびジャンプ命令を含み、任意の制御構造をとるプログラムを仮定する。プロセッサアーキテクチャ情報としては、命令フェッチ、実行などのパイプラインステージ構成情報、各命令語のステージ実行順、および、命令キャッシュのキャッシュブロックサイズと連想方式(n-wayセットアソシアティブなど)を指定可能である。実時間制約としては、与えられたプログラム全体を制御構造において入口と出口をそれぞれ一つのみ持つコードブロックに分割し、各ブロックの最良または最悪実行時間の間に成立する条件を、定数およびパラメータ変数を含む線形不等式の論理結合で指定することにより与える。例えば、ブロックB1,B2に対して「T(B1)<T(B2)+x+1」(B1の最悪実行時間はB2の最良実行時間にx+1より常に小さい)などといった実時間制約を指定可能である。提案手法では、まず、プログラムおよびプロセッサアーキテクチャ情報から、プログラムの実時間的な振舞いを表現するパラメータ付時間オートマトンモデルMを構成する。得られるモデルはプロセッサ動作周波数f、および、プログラム中の各ループiの実行回数kiをパラメータとして持つ。モデルの構成においては、まず、プログラムの条件分岐をすべて非決定分岐とみなし制御構造のみに着目する。そして、パイプライン処理による並列動作を考慮し、かつ、命令キャッシュによる実行時間の変化を制御構造とキャッシュアーキテクチャ情報から静的に解析することによりモデルを構成する。次に、プログラムコードおよび実時間制約式から、実時間制約式を満たさないようなプログラム実行系列の集合を受理するパラメータ付時間オートマトンモデルPを構成する。最後に、モデルMとモデルPの積オートマトンの受理系列集合が空であるための各パラメータに関する条件式を、既存のパラメトリックモデル検査手法に帰着することにより導出する。提案手法をライントレースカー制御プログラムやMotionJPEGデコーダに適用し、実用的な計算時間で実時間制約を満たすためのプロセッサ動作周波数およびループ回数の許容範囲を導出できることを示した。
|
Research Products
(1 results)
