【研究分野】ソフトウエア

【研究領域課題番号】22500023 (KAKENデータベースで見る）

【研究キーワード】

コンパイラ / 証明論 / 最適化 / プログラミング言語処理系

【研究成果の概要】

本研究では,プログラミング言語のコンパイルの過程に現れる種々の中間言語は,直感主義的論理学の証明システムとして表現でき,それらの言語間の変換は,証明変換として表現できるはずである,との基本的な洞察を基礎とし,関数型言語のコンパイル過程を自然演繹システムから,コード言語を表現するある種のシーケント計算系にいたる証明変換の合成として表現でき,その変換可能性を示すメタレベルの証明から,コンパイルアルゴリズムが抽出できることを示した.

【研究種目】基盤研究(C)

【研究期間】2010 - 2012

【配分額】3,770千円 (直接経費: 2,900千円、間接経費: 870千円)

【研究分野】ソフトウエア

【研究領域課題番号】22300007 (KAKENデータベースで見る）

【研究キーワード】

コンパイラ / コード最適化 / 時相論理 / 静的単一代入形式 / 網羅型データフロー 解析 / 要求駆動型データフロー解析 / キャッシュ効率化 / 大域値番号付け / 最適化 / COINS / スカラー置換 / 部分冗長性除去 / 部分無用コード除去 / キャッシュ最適化 / 時相論理理 / CTL

【研究成果の概要】

COINSコンパイラの低水準中間表現に対し,双方向時相論理であるCTL-FVを用いて最適化のパターンと変換を記述し,そこからモデル検査により,C言語の最適化器を生成した.一方,通常形式上の部分冗長除去(PRE)を静的単一代入形式上で行うように変換する汎用的な手法を開発した.また,PREおよびPREに似た部分無用コード除去法の効率化と効果の向上を行い,PREの応用として,同じ配列を参照するロード命令のキャッシュヒット率を向上させる手法を実現した.

【研究種目】基盤研究(B)

【研究期間】2010 - 2012

【配分額】18,070千円 (直接経費: 13,900千円、間接経費: 4,170千円)

【研究分野】ソフトウエア

【研究領域課題番号】19300006 (KAKENデータベースで見る）

【研究キーワード】

コンパイラ / 最適化器 / 検証 / 時相論理 / モデル検査 / 投機的部分冗長除去 / 無用コード / データフロー解析 / 部分無用コード除去 / 最適化 / SSA形式

【研究成果の概要】

時相論理を用いたコンパイラ最適化器の生成系を作成した.これにより,従来は実用にならないと思われていたものが手書きのものに近づいた.また,コンパイラの最適化器が正しいかどうかを,時相論理を用いて検証する方法を開発,実装した.これは,モデル検査によりバグを報告する.一方,プログラムの実行経路によって実行されない式を除去する部分冗長除去の最適化を,要求駆動の性質を用いて,ループ不変式のループ外移動を投機的に行えるように拡張した.本手法を実装し,評価した結果,従来法より効率的に高速なコードを生成できることを示した.

【研究種目】基盤研究(B)

【研究期間】2007 - 2009

【配分額】18,850千円 (直接経費: 14,500千円、間接経費: 4,350千円)

【研究分野】ソフトウエア

【研究領域課題番号】17500016 (KAKENデータベースで見る）

【研究キーワード】

性能最適化 / コンパイラ / 分散環境 / セキュリティ / 形式化 / 分散スケジューリング / 検証 / 自律分散性 / 最適化 / 最適化コンパイラ / 型システム / Itanium2 / メモリモデル / XSLT

【研究成果の概要】

本研究の目的は検証付きコンパイラ(Verifying Compiler)をコンパイラ最適化に適用し、最適化の数理的な性質を明らかにし、適用の地平を拡大することにあった。検証付きコンパイラ(Verifying Compiler)は、もともとHoareの提唱したプログラムの正当性を併せて証明するコンパイラシステムとして21世紀の課題として提唱した概念である。本研究で目指すのは、コンパイラ最適化における上のような危機的状況に対応すべく最適化をその正しさの証明を込めて適用するコンパイラの構築であり、最適化検証つきコンパイラ(Optimization Verifying Compiler)と呼ぶべきものである。
本年度は特に、情報処理環境の急速な変化に対応し、Webを含む分散処理環境において「最適化」の知識がどのように抽出できるかの研究を行った。
具体的には、Folksonomyを対象にしてそこからプログラミングに有用なさまざまな概念を抽出することができた。抽出結果は直感的に正しいことを確認した。また分散環境における計算記述の形式化がセキュリティの記述と密接に関係することをあきらかにできた。具体的には、ワークフローの意味論の厳密な形式化をおこない、(形式化された)文書で表現する方法を提案した。
さらに、上と関係して具体的に最適性能のコードを探索するため、つまり「コンパイラ最適化を超えたパフォーマンスチューニング」について結果を得ることができた。具体的には数値計算に代表される性能を求める分野にプログラム変換の高階関数の理論を応用して、探索空間を広げることに成功した。

【研究種目】基盤研究(C)

【研究期間】2005 - 2007

【配分額】3,740千円 (直接経費: 3,500千円、間接経費: 240千円)

【研究分野】ソフトウエア

【研究領域課題番号】16500016 (KAKENデータベースで見る）

【研究キーワード】

コンパイラ / 最適化 / 静的単一代入形式(SSA形式) / 検証 / モデル検査 / 時相論理

【研究成果の概要】

1.研究の背景
コンパイラの分野では,SSA形式(静的単一代入形式)などの新しい内部表現への対応,それを用いた最適化,書き下したコンパイラ部品の検証が切望されている.
2.SSA形式における逆変換の評価と最適化の新しい手法の開発
(i)SSA形式から通常形式への逆変換法は,Briggsらの方法とSreedharらの方法が知られている主な方法であるが,これまでそれらを比較した研究がなかった.我々は,この2つとBriggsらの方法の改良版を実装し,SPECベンチマークを用いた実験により比較し,Sreedharらの方法が現在の技術水準では実際上最良であることを示した.
(ii)SSA形式での最適化については種々提唱されているが,まだ不十分な点が多い.たとえば部分冗長除去やコード移動のアルゴリズムでは,SSA形式のφ関数を越えてのコードの移動が困難で,単純な例でも最適化できない例が知られている.本研究では,この問題点を解決し,値番号付けを含む部分冗長コード移動のアルゴリズムを開発,実装した.
3.コンパイラの最適化器の検証
(i)コンパイラの最適化器の検査法の一つとして,最適化前後で各変数の値をトレースとして出力し,その後にそれらを比較照合する,という方法により,各種最適化器の正しさを確認する方法を開発し,実装した.
(ii)時相論理による最適化の記述から自動的に最適化器を作成する研究を行った.実装上の工夫を行い,従来研究と比べ,最適化時間を実用的な時間内に収めることができたのが特長である.
(iii)既存の最適化器が満たすべき条件を時相論理により記述しておき,実際に最適化器を動かした後に,記述した条件が満たされているかどうかをモデル検査によりチェックする方法を開発し,実装,評価を行った.これにより,既存の手書きの最適化器の正しさを検証することができる.さらに未知のバグも発見できた.

【研究種目】基盤研究(C)

【研究期間】2004 - 2006

【配分額】3,500千円 (直接経費: 3,500千円)

【研究分野】ソフトウエア

【研究領域課題番号】16300009 (KAKENデータベースで見る）

【研究キーワード】

LMNtal / プログラミング言語 / グラフ書換え / 並行計算 / 言語処理系 / 最適化 / プログラム言語 / コンパイラ / 分散計算 / 多重集合書換え

【研究成果の概要】

LMNtal(elementalと発音)は,多重集合や並行処理やモビリティなどの概念を持つさまざまな計算モデルを簡明な形で統合することを目的として,研究代表者と研究分担者が提案したプログラミング言語モデルである.本研究は,階層グラフ書換え型の計算モデルとして確立しつつあったLMNtalを実用プログラミング言語に成長させるために必要な言語機能を設計し,実装技術を確立し,実際に処理系を構築して広く公開することを目標に推進した.
本研究によって得られた主要成果は以下の通りである.
(a)プログラミング言語としてのLMNtalの確立-階層グラフ書換えモデルに対して,基本データ型と基本演算,モジュールシステム,他言語インタフェースなどの導入方法を検討設計し,それらを用いて多様なライブラリの構築を行った.
(b)実装技法の確立と処理系の作成-LMNtal用中間言語へのコンパイラと,中間命令列を実行をつかさどる実行時処理系からなる処理系を構築した.特に,複数タスクを用いた非同期実行方式を設計・実装するとともに,逐次実行最適化機能や中間言語からJavaへのトランスレータも実装した.またグラフ自動整形機能をもつ実行可視化機能を設計・実装した.
(c)記述能力の検証-LMNtalの基本的記述能力の検証のために,π計算,Ambient計算,λ計算,CHR(Constraint Handling Rules)など,多様な計算モデルをLMNtalでエンコードして,開発した処理系上で動作確認を行った.
開発した処理系の規模は約5万行で,http://www.ueda.info.waseda.ac.jp/lmntal/から公開している.

【研究種目】基盤研究(B)

【研究期間】2004 - 2006

【配分額】8,300千円 (直接経費: 8,300千円)

【研究分野】計算機科学

【研究領域課題番号】13680399 (KAKENデータベースで見る）

【研究キーワード】

コンパイラ / 最適化 / SSA形式(静的単一代入形式) / 先端アーキテクチャ / コンパイラ・インフラストラクチャ / 命令レベル並列処理 / コード生成

【研究成果の概要】

1.コンパイラの分野では,技術移転の容易なコンパイラ・インフラストラクチャを利用した先端アーキテクチャ向けの最適化や,SSA(静的単一代入)形式などの新しい内部表現への対応が切望されている.本研究では, (1)コンパイラ・インフラストラクチャの積極的な利用
(2)スーパースカラやVLIWなど先端アーキテクチャ向けの最適化コード生成手法
(3)SSA形式などの新しい内部表現に対応した最適化の手法 を中心としたコンパイラの新しい手法を開発する.
2.平成13〜14年度に次のような成果を得た.
(1)科学技術振興調整費で作成されるコンパイラ・インフラストラクチャを利用して,SSA形式を用いた基本最適化部分を作成した.(研究発表の3,5,6).
(2)同上のコンパイラ・インフラストラクチャを利用して,SSA形式から通常形式への逆変換を行うアルゴリズムの比較を行った(研究発表の4).
(3)SSA形式を用いる進んだ最適化を行う手法を発表し(研究発表の7,8),これをコンパイラ・インフラストラクチャを利用して実現するための検討を行った.
(4)その他,上記の最適化やコード生成を行うための基礎となる,系統的デバッギングの研究(研究発表の1),プログラム特化の研究(研究発表の2),インタプリタ生成系の研究(研究発表の9)などを行った.

【研究種目】基盤研究(C)

【研究期間】2001 - 2002

【配分額】3,600千円 (直接経費: 3,600千円)

【研究分野】計算機科学

【研究領域課題番号】11680347 (KAKENデータベースで見る）

【研究キーワード】

コンパイラ / コード生成 / 命令レベル並列処理 / SSA形式(静的単一代入形式) / スーパースカラ / 最適化 / 中間コード

【研究成果の概要】

最近の計算機アーキテクチャでは,遅延命令や,複数機能ユニットによるスーパースカラ処理,パイプライン処理,内部並列処理などが行われている.これらは,コンパイラが目的コードを最適に配置することで,初めて目的コードを効率よく実行できるようなアーキテクチャであり,コンパイラの役割は益々重要になっている.
一方,コンパイラのバックエンド処理の新しい内部表現として,単一代入の変数を用いるSSA(Static Single Assignment)形式が提唱され,コンパイラのデータフロー解析や最適化変換が容易にできることで注目を浴びている.しかしSSA形式における最適化変換,およびその後のレジスタ割付けやコード生成フェーズとの接続法は十分解明されていない.
本研究では,これらの問題に対し,(1)最新アーキテクチャの特徴を生かした効率良いコードの生成手法,(2)SSA形式に対応した最適化やコード生成の手法,を中心としたコンパイラの新しい手法を開発することを目標とした.
本研究期間に,次のような成果を得た.
(1)分散プログラミング言語に対する異機種分散環境上での効率良いネイティブコードの生成の研究(雑誌論文の6)(2)スーパースカラマシンに対する,プロセッサ仕様記述を用いたコードスケジューラの研究(雑誌論文の4)(3)PDA(携帯情報端末)のような制約の強いプロセサにおける言語処理系の研究(雑誌論文の5)(4)SSA形式への変換法の研究(5)上記の最適化やコード生成を行うための基礎となる属性文法の研究(研究発表の2,3)や系統的デバッグ法の研究(雑誌論文の1)

【研究種目】基盤研究(C)

【研究期間】1999 - 2000

【配分額】3,600千円 (直接経費: 3,600千円)