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 优化器

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

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

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

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

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

使用双向 CTL 生成 Java 优化器

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

時相論理を用いたコンパイラ最適化器の実行の正しさの検査

使用时态逻辑验证编译器优化器执行的正确性

• 发表时间: 2008
• 期刊: コンピュータソフトウェア Vol.25, No.1
• 作者: 佐原聡一郎;佐々政孝
• 通讯作者: 佐々政孝