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.

我们使用时态逻辑制作了一个编译器优化器生成器。这表明以前被认为不实用的生成优化器的效率接近手工制作的优化器。我们还开发并实现了一种使用时态逻辑验证编译器优化器正确性的方法。系统通过模型检查报告bug。另一方面，我们扩展了部分冗余消除，它可以删除仅在某些路径上执行的表达式，以便使用需求驱动的属性推测地将表达式提升到循环之外。我们进行了实验来评估我们的方法，因此我们表明它比以前的工作成本更低，并且生成更有效的代码。

项目成果

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

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

• 发表时间: 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
• 作者: 滝本宗宏;佐々政孝
• 通讯作者: 佐々政孝