• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Generation and verification of compiler optimizers using temporal logic and high-level SSA form optimization considering aliases

Research Project

Project/Area Number 19300006
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Research Field Software
Research InstitutionTokyo Institute of Technology

Principal Investigator

SASSA Masataka  Tokyo Institute of Technology, 大学院・情報理工学研究科, 教授 (20016182)

Co-Investigator(Kenkyū-buntansha) TAKIMOTO Munehiro  東京理科大学, 理工学部, 講師 (00318205)
Project Period (FY) 2007 – 2009
Project Status Completed (Fiscal Year 2009)
Budget Amount *help
¥18,850,000 (Direct Cost: ¥14,500,000、Indirect Cost: ¥4,350,000)
Fiscal Year 2009: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2008: ¥6,240,000 (Direct Cost: ¥4,800,000、Indirect Cost: ¥1,440,000)
Fiscal Year 2007: ¥8,060,000 (Direct Cost: ¥6,200,000、Indirect Cost: ¥1,860,000)
Keywordsコンパイラ / 最適化器 / 検証 / 時相論理 / モデル検査 / 投機的部分冗長除去 / 無用コード / データフロー解析 / 部分無用コード除去 / 最適化 / SSA形式
Research Abstract

We made a generator of compiler optimizers using temporal logic. This showed the efficiency of the generated optimizer, that was previously considered unpractical, approaches the hand-made one. We also developed and implemented a method that verifies the correctness of compiler optimizers using temporal logic. The system reports bugs by model checking. On the other hand, we extended the partial redundancy elimination, which can remove expressions executed on only some paths, for speculatively hoisting expressions out of loops using a demand-driven property. We conducted experiments to evaluate our method, so that we showed that it is less costly and generates more efficient code than previous works.

Report

(4 results)
  • 2009 Annual Research Report   Final Research Report ( PDF )
  • 2008 Annual Research Report
  • 2007 Annual Research Report
  • Research Products

    (36 results)

All 2009 2008 2007 Other

All Journal Article (21 results) (of which Peer Reviewed: 21 results) Presentation (9 results) Book (2 results) Remarks (4 results)

  • [Journal Article] 質問伝播に基づく投機的部分冗長除去2009

    • Author(s)
      滝本宗宏
    • Journal Title

      情報処理学会論文誌プログラミング Vol.2,No.5

      Pages: 15-27

    • NAID

      110007970926

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] 自動的等価性差分の抽出によるSSAコンパイラ最適化器の生成するコードの正しさの検証2009

    • Author(s)
      Fang Ling, 佐々政孝
    • Journal Title

      情報処理学会論文誌プログラミング Vol.2,No.4

      Pages: 33-52

    • NAID

      110007970918

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] Comparison and evaluation of backtranslation algorithms for static single assignment forms, Computer Languages2009

    • Author(s)
      Sassa, M., Ito, Y., Kohama, M.
    • Journal Title

      Systems & Structures 2

      Pages: 173-195

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] Comparison and evaluation of back-translation algorithms for static single assignment forms2009

    • Author(s)
      Sassa, M., Ito, Y., Kohama, M.
    • Journal Title

      Computer Languages, Systems & Structures 35,2

      Pages: 173-195

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 自動的等価性差分の抽出によるSSAコンパイラ最適化器の生成するコードの正しさの検証2009

    • Author(s)
      Fang Ling, 佐々政孝
    • Journal Title

      情報処理学会論文誌 プログラミング 2,4

      Pages: 33-52

    • NAID

      110007970918

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 質問伝播に基づく投機的部分冗長除去2009

    • Author(s)
      滝本宗宏
    • Journal Title

      情報処理学会論文誌 プログラミング 2,5

      Pages: 15-27

    • NAID

      110007970926

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Verification of Compiler Optimization Using Temporal Logic by Checking Value Equality Difference2009

    • Author(s)
      Fang, L., Sassa, M.
    • Journal Title

      Eighth International Workshop on Compiler Optimization meets Compiler Verification(COCV 2009) 8(CD-ROM)

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 要求駆動型部分無用コード除去2008

    • Author(s)
      滝本宗宏
    • Journal Title

      組込みシステムシンポジウム 2008

      Pages: 107-114

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] 時相論理を用いたコンパイラ最適化器の実行の正しさの検査, (推薦論文・PPL2007)2008

    • Author(s)
      佐原聡一郎, 佐々政孝
    • Journal Title

      コンピュータソフトウェア Vol.25,No.1

      Pages: 151-166

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] 静的単一代入形式を用いた最適化2008

    • Author(s)
      滝本宗宏, 佐々政孝
    • Journal Title

      コンピュータソフトウェア Vol.25,No.1

      Pages: 30-46

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] 静的単一代入形式を用いた最適化2008

    • Author(s)
      佐々政孝, 滝本宗宏
    • Journal Title

      コンピュータソフトウェア Vol.25,No.1

      Pages: 19-29

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] COINSコンパイラ・インフラストラクチャの開発2008

    • Author(s)
      中田育男, 渡邊坦, 佐々政孝, 森公一郎, 阿部正佳
    • Journal Title

      コンピュータソフトウェア Vol.25,No.1

      Pages: 2-18

    • NAID

      110006572495

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] 静的単一代入形式上で通常形式部分冗長除去を実現する汎用的手法2008

    • Author(s)
      今橋孝典, 伊藤陽, 佐々政孝
    • Journal Title

      情報処理学会論文誌:プログラミング Vol.49,No.SIG1(PRO35)

      Pages: 84-95

    • NAID

      110006594926

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] Validating Correctness of Compiler Optimizer Execution Using Temporal Logic2008

    • Author(s)
      Sassa, M., Sahara, S.
    • Journal Title

      Seventh International Workshop on Compiler Optimization meets Compiler Verification(COCV 2008) 7

      Pages: 1-17

    • NAID

      130004549095

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 要求駆動型部分無用コード除去2008

    • Author(s)
      滝本宗宏
    • Journal Title

      組込みシンポジウム2008論文集

      Pages: 107-114

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 静的単一代入形式上で通常形式部分冗長除去を実現する汎用的手法2008

    • Author(s)
      今橋孝典, 伊藤陽, 佐々政孝
    • Journal Title

      情報処理学会論文誌:プログラミング Vol.49, No. SIG1 (PRO 35)

      Pages: 84-95

    • NAID

      110006594926

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 時相論理を用いたコンパイラ最適化器の実行の正しさの検査2008

    • Author(s)
      佐原聡一郎, 佐々政孝
    • Journal Title

      コンピュータソフトウェア Vol.25, No.1

      Pages: 151-166

    • NAID

      130004549095

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 静的単一代入形式を用いた最適化(導入編)2008

    • Author(s)
      佐々政孝, 滝本宗宏
    • Journal Title

      コンピュータソフトウェア Vol.25, No.1

      Pages: 19-29

    • NAID

      110006572496

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Generating Java Compiler Optimizers Using Bidirectional CTL2007

    • Author(s)
      Fang, L., Sassa, M.
    • Journal Title

      Electronic Notes in Theoretical Computer Science Vol.190/4

      Pages: 49-63

    • NAID

      110006291058

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] 双方向CTLによるJava最適化器の生成2007

    • Author(s)
      方玲, 佐々政孝
    • Journal Title

      報処理学会論文誌:プログラミング Vol.48,No.SIG10(PRO33)

      Pages: 76-89

    • NAID

      110006291058

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] Generating Java Compiler Optimizers Using Bidirectional CTL2007

    • Author(s)
      Fang, L. and Sassa, M.
    • Journal Title

      Electronic Notes in Theoretical Computer Science 190/4

      Pages: 49-63

    • NAID

      110006291058

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Presentation] 時相論理CTL*を用いたJAVA最適化器の生成の試み2009

    • Author(s)
      藤原一貴, 佐々政孝
    • Organizer
      日本ソフトウェア科学会大会論文集, 第26回
    • Place of Presentation
      島根大学
    • Year and Date
      2009-09-17
    • Related Report
      2009 Final Research Report
  • [Presentation] レジスタプロモーションによるコード最適化の実装と評価2009

    • Author(s)
      及川宗明, 佐々政孝
    • Organizer
      日本ソフトウェア科学会大会
    • Place of Presentation
      松江市島根大学
    • Year and Date
      2009-09-17
    • Related Report
      2009 Annual Research Report
  • [Presentation] Verification of Compiler Optimization Using Temporal Logic by Checking Value Equality Difference2009

    • Author(s)
      Fang, L., Sassa, M.
    • Organizer
      Eighth International Workshop on Compiler Optimization meets Compiler Verification (COCV 2009)
    • Place of Presentation
      York, U.K.
    • Year and Date
      2009-03-22
    • Related Report
      2009 Final Research Report
  • [Presentation] 自動的等価性差分の抽出によるSSAコンパイラ最適化器の正しさの検証2009

    • Author(s)
      Fang Ling, 佐々政孝
    • Organizer
      情報処理学会プログラミング研究会
    • Place of Presentation
      東京大学駒場
    • Year and Date
      2009-03-17
    • Related Report
      2009 Final Research Report
  • [Presentation] 自動的等価性差分の抽出によるSSAコンパイラ最適化器の正しさの検証2009

    • Author(s)
      Fang Ling, 佐々政孝
    • Organizer
      情報処理学会プログラミング研究会
    • Place of Presentation
      東京大学
    • Year and Date
      2009-03-17
    • Related Report
      2008 Annual Research Report
  • [Presentation] COINSを用いた大域的データサイズ推論の実現2008

    • Author(s)
      太田眞敬, 滝本宗宏
    • Organizer
      日本ソフトウェア科学会大会論文集, 第25回
    • Place of Presentation
      筑波大学東京キャンパス
    • Year and Date
      2008-09-11
    • Related Report
      2009 Final Research Report
  • [Presentation] Validating Correctness of Compiler Optimizer Execution Using Temporal Logic2008

    • Author(s)
      Sassa, M., Sahara, S.
    • Organizer
      Seventh International Workshop on Compiler Optimization meets Compiler Verification (COCV 2008)
    • Place of Presentation
      Budapest, Hungary
    • Year and Date
      2008-04-05
    • Related Report
      2009 Final Research Report
  • [Presentation] 質問伝播に基づく要求駆動型大域値番号付け2008

    • Author(s)
      滝本宗宏, 佐々政孝
    • Organizer
      日本ソフトウェア科学会第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)
    • Place of Presentation
      仙台市.
    • Year and Date
      2008-03-07
    • Related Report
      2009 Final Research Report
  • [Presentation] Array SSAとそれを用いた最適化の実装と評価2008

    • Author(s)
      米倉翔一、佐々政孝
    • Organizer
      第169回計算機アーキテクチャ・第114回ハイパフォーマンスコンピューティング合同研究発表会(HOKKE-2008)
    • Place of Presentation
      北海道大学
    • Year and Date
      2008-03-05
    • Related Report
      2007 Annual Research Report
  • [Book] コンパイラの基盤技術と実践-コンパイラ・インフラストラクチヤCOINSを用いて2008

    • Author(s)
      中田育男, 渡辺坦, 佐々政孝, 滝本宗宏
    • Total Pages
      260
    • Publisher
      朝倉書店
    • Related Report
      2008 Annual Research Report
  • [Book] コンパイラの基盤技術と実践-コンパイラ・インフラストラクチャCOINSを用いて

    • Author(s)
      中田育男,渡辺坦,佐々政孝,滝本宗宏
    • Total Pages
      260
    • Publisher
      朝倉書店
    • Related Report
      2009 Final Research Report
  • [Remarks] 滝本宗宏,渡辺坦,中田育男,COINSがもたらすコンパイラ革命,UNIX MAGAZINE 2009年7月号.(ホームページ)

    • URL

      http://www.is.titech.ac.jp/~sassa/coins-www-ssa/japanese/index.html

    • Related Report
      2009 Final Research Report
  • [Remarks]

    • URL

      http://www.is.titech.ac.jp/~sassa/papers-written/index.html

    • Related Report
      2009 Annual Research Report
  • [Remarks]

    • URL

      http://www.is.titech.ac.jp/~sassa/papers-written/index.html

    • Related Report
      2008 Annual Research Report
  • [Remarks]

    • URL

      http://www.is.titech.ac.jp/~sassa/papers-written/index.html

    • Related Report
      2007 Annual Research Report

URL: 

Published: 2007-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi