Generation and verification of COINS compiler optimizers using temporal logic and high-level extensions of optimizers
| Project/Area Number |
22300007
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
SASSA Masataka 東京工業大学, 大学院・情報理工学研究科, 教授 (20016182)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TAKIMOTO Munehiro 東京理科大学, 理工学部, 准教授 (00318205)
|
|---|
| Project Period (FY) |
2010 – 2012
|
| Project Status |
Completed (Fiscal Year 2012)
|
| Budget Amount *help |
¥18,070,000 (Direct Cost: ¥13,900,000、Indirect Cost: ¥4,170,000)
Fiscal Year 2012: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2011: ¥5,980,000 (Direct Cost: ¥4,600,000、Indirect Cost: ¥1,380,000)
Fiscal Year 2010: ¥7,670,000 (Direct Cost: ¥5,900,000、Indirect Cost: ¥1,770,000)
|
|---|
| Keywords | コンパイラ / コード最適化 / 時相論理 / 静的単一代入形式 / 網羅型データフロー 解析 / 要求駆動型データフロー解析 / キャッシュ効率化 / 大域値番号付け / 最適化 / COINS / スカラー置換 / 部分冗長性除去 / 部分無用コード除去 / キャッシュ最適化 / 時相論理理 / CTL |
|---|
| Research Abstract |
We generated a C language compiler optimizers using the low-level intermediate form of the COINS compiler. We specify patterns and transformations of optimizers in CTL-FV, which is a bi-directional temporal logic, and performed model checking.On the other hand, a generic algorithm is made, which converts partial redundancy elimination (PRE) in the normal form into one in the static single assignment form. In addition to the generalization, we have improved the effectiveness and the efficiency of the PRE and the partial dead code elimination which is another code optimization technique similar to PRE. As a new code optimization, we also have proposed atechnique that increases cache-hit ratio.
|
Report
(4 results)
Research Products
(19 results)
