2009 Fiscal Year Final Research Report
Generation and verification of compiler optimizers using temporal logic and high-level SSA form optimization considering aliases
| Project/Area Number |
19300006
|
|---|
| 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 Tokyo Institute of Technology, 大学院・情報理工学研究科, 教授 (20016182)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TAKIMOTO Munehiro 東京理科大学, 理工学部, 講師 (00318205)
|
|---|
| Project Period (FY) |
2007 – 2009
|
| Keywords | コンパイラ / 最適化器 / 検証 / 時相論理 / モデル検査 / 投機的部分冗長除去 |
|---|
| 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.
|
