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

使用时态逻辑和考虑别名的高级 SSA 形式优化来生成和验证编译器优化器

• 批准号: 19300006
• 负责人: SASSA Masataka
• 金额: $ 12.06万
• 依托单位: Tokyo Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2007
• 资助国家: 日本
• 起止时间: 2007 至 2009
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19300006/
• 关键词: コンパイラ; 最適化器; 検証; 時相論理; モデル検査; 投機的部分冗長除去; 無用コード; データフロー解析; 部分無用コード除去; 最適化; SSA形式

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.

我们使用时间逻辑制作了编译器优化器的生成器。这表明了生成的优化器的效率（以前被认为是不可行的）方法是手工制作的效率。我们还开发了一种使用时间逻辑来验证编译器优化器正确性的方法。该系统通过模型检查报告错误。另一方面，我们扩展了局部冗余消除，该冗余消除可以删除仅在某些路径上执行的表达式，以便使用需求驱动的属性从循环中提起表达式。我们进行了实验以评估我们的方法，以表明它的成本较低，并且比以前的工作产生更有效的代码。

项目成果

要求駆動型部分無用コード除去

请求驱动的部分无用代码消除

• 发表时间: 2008
• 期刊: 組込みシステムシンポジウム 2008
• 作者: Hiroto Tadano;Tetsuya Sakurai;滝本宗宏
• 通讯作者: 滝本宗宏

双方向CTLによるJava最適化器の生成

使用双向 CTL 生成 Java 优化器

• 发表时间: 2007
• 期刊: 報処理学会論文誌:プログラミング Vol.48,No.SIG10(PRO33)
• 作者: 方玲;佐々政孝
• 通讯作者: 佐々政孝

静的単一代入形式上で通常形式部分冗長除去を実現する汎用的手法

一种在静态单赋值形式上实现正则形式部分冗余去除的通用方法

• 发表时间: 2008
• 期刊: 情報処理学会論文誌:プログラミング Vol.49,No.SIG1(PRO35)
• 作者: 今橋孝典;伊藤陽;佐々政孝
• 通讯作者: 佐々政孝

時相論理CTL*を用いたJAVA最適化器の生成の試み

尝试使用时序逻辑 CTL* 生成 JAVA 优化器

• 发表时间: 2009
• 作者: 藤原一貴;佐々政孝
• 通讯作者: 佐々政孝

Generating Java Compiler Optimizers Using Bidirectional CTL

• DOI: 10.1016/j.entcs.2007.09.007
• 发表时间: 2007-11
• 作者: Ling-Kuang Fang;Masataka Sassa