| 研究課題/領域番号 |
17500016
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
佐藤 周行 東京大学, 情報基盤センター, 准教授 (20225999)
|
|---|
| 研究分担者 |
SATO Hiroyuki The University of Tokyo, Information Technology Center, Associate Professor (20225999)
|
|---|
| 研究期間 (年度) |
2005 – 2007
|
| 研究課題ステータス |
完了 (2007年度)
|
| 配分額 *注記 |
3,740千円 (直接経費: 3,500千円、間接経費: 240千円)
2007年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2006年度: 1,300千円 (直接経費: 1,300千円)
2005年度: 1,400千円 (直接経費: 1,400千円)
|
|---|
| キーワード | 性能最適化 / コンパイラ / 分散環境 / セキュリティ / 形式化 / 分散スケジューリング / 検証 / 自律分散性 / 最適化 / 最適化コンパイラ / 型システム / Itanium2 / メモリモデル / XSLT |
|---|
| 研究概要 |
本研究の目的は検証付きコンパイラ(Verifying Compiler)をコンパイラ最適化に適用し、最適化の数理的な性質を明らかにし、適用の地平を拡大することにあった。検証付きコンパイラ(Verifying Compiler)は、もともとHoareの提唱したプログラムの正当性を併せて証明するコンパイラシステムとして21世紀の課題として提唱した概念である。本研究で目指すのは、コンパイラ最適化における上のような危機的状況に対応すべく最適化をその正しさの証明を込めて適用するコンパイラの構築であり、最適化検証つきコンパイラ(Optimization Verifying Compiler)と呼ぶべきものである。
本年度は特に、情報処理環境の急速な変化に対応し、Webを含む分散処理環境において「最適化」の知識がどのように抽出できるかの研究を行った。
具体的には、Folksonomyを対象にしてそこからプログラミングに有用なさまざまな概念を抽出することができた。抽出結果は直感的に正しいことを確認した。また分散環境における計算記述の形式化がセキュリティの記述と密接に関係することをあきらかにできた。具体的には、ワークフローの意味論の厳密な形式化をおこない、(形式化された)文書で表現する方法を提案した。
さらに、上と関係して具体的に最適性能のコードを探索するため、つまり「コンパイラ最適化を超えたパフォーマンスチューニング」について結果を得ることができた。具体的には数値計算に代表される性能を求める分野にプログラム変換の高階関数の理論を応用して、探索空間を広げることに成功した。
|
