氏名: 鈴木 晃 (m953420)
論文題目: 命令レベル並列プロセッサに対するコンパイラの
SCCS動作式による仕様記述とその検証技法
論文概要
本論文では、R.Milnerにより提案されているSCCS(Synchronous CCS)を用い、
プログラムの仕様記述と、命令レベル並列プロセッサ
の仕様記述から実行可能な命令系列を導出するコンパイラの仕様記述手法
を提案する。
さらに、この仕様記述に対して構文的な操作を行なうことにより効率的に検証
する技法を提案する。
命令レベル並列プロセッサは複数のALUとレジスタをもつ。
このようなプロセッサをターゲットとするコンパイラには、ALUとレジスタ
をできるだけ並列に使って高速にプログラムを実行するコード生成機構が
要求される。しかし、並列性を伴う場合、命令の実行が
非決定的になり、実現レベルでの検証やテストは非常に複雑になる。
従って、コンパイラ開発の際には、抽象的なレベルで仕様記述し、テスト・
検証することが有効であると考えられる。
本論文では、並列に実行されるプログラムの各命令を並行プロセス、ALUとレジ
スタを共有資源としてモデル化することで、実行中のプログラムを細部が
抽象化された並行システムとしてとらえてコンパイラの仕様記述を与える。
この仕様記述の枠組として R.Milner の SCCS を用いる。
SCCSは、同時に発生する動作は、すべて同期するという原理に基づい
た並行システム記述の体系である。このSCCSの
原理をプロセッサ内のシステムクロックと解釈すれば、ハードウェ
アと命令の仕様記述を自然に行うことができる。
本手法では、コンパイラにより生成されるコードは、仕様記述から生成される
複数のコードの1つである。このことに基づき、コンパイラのコード
生成をモデル化する。
このモデル化に基づいてSCCS記述を与え、検証ツール
Concurrency Workbenchを用いて、実行可能なコードを生成する。
さらに、得られた SCCS記述に対する検証技法を提案する。
本論文で得られるSCCS記述を検証するときには、並列合成演算子が多数
出現するため、LTS(ラベル付き遷移システム)モデルの非決定性が大きくなり、
LTSモデルを構成する際に状態遷移数が爆発する。このため、検証には多くのメモリ
を必要とする。しかし本仕様記述では、非決定的な状態遷移のほとんどが
制限演算子により削除され無駄になる。この点に注目し、SCCS動作式を
あらかじめ構文的に変換して状態遷移数を抑える手法を与え、
この変換がSCCSの強等価性に対して
健全であることを示す。
目次に戻る