权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

New methods for translation and optimization using SSA form in compilers and their validation systems

在编译器及其验证系统中使用 SSA 形式进行翻译和优化的新方法

基本信息

批准号：
16500016
负责人：
SASSA Masataka
金额：
$ 2.24万
依托单位：
Tokyo Institute of Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2004
资助国家：
日本
起止时间：
2004 至 2006
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-16500016/
关键词：
Compiler Optimization Static single assignment form Validation モデル検査時相論理

项目摘要

1.Evaluation of back translation and development of new optimization method in SSA form(i)Major algorithms for the back translation from SSA form to normal form are the method by Briggs et al. and that by Sreedhar et al., but so far there have been no research which compares them. We implemented these two algorithms and an improvement of Briggs et al. 's algorithm, and made experiments to compare the three using the SPEC benchmark. The result shows that Sreedhar et al. 's algorithm is actually the best under the current technical level of compilers.(ii)Various proposals exist for optimization in SSA form, but there are still insufficient points. For example, in partial redundancy elimination and code motion algorithms, it is difficult to move code across the phi-functions of the SSA form and simple examples that cannot be optimized are known. In our research, we developed and implemented an algorithm which overcomes this problem. and which can move partially redundant code with perform … More ing value numbering.2.Validation of compiler optimizers(i)As a method to test the compiler optimizer, we developed and implemented a system, which outputs the values of each variable before and after optimization as a trace, and then performs the comparison checking of these outputs after the optimization. This can validate the correctness of various optimizers.(ii)We made a system that automatically generates the optimizer from the specification of the optimizer in temporal logic. We devised various techniques in implementation, and the system has a characteristic feature that it can realize optimization in small practical time compared to previous work.(iii)We developed a method in which the condition to be satisfied by the existing optimizer is specified in temporal logic, and after actually doing the optimization, the satisfiability of the specified condition is checked using model checking. It is implemented and evaluated. By this, it can validate the existing hand-written optimizers. Furthermore, it could find an unknown bug in an optimizer. Less

1. SSA形式的反翻译评价和新的优化方法的发展（i）从SSA形式到规范形式的反翻译的主要算法是Briggs等人的方法和Sreedhar等人的方法，但迄今为止还没有研究对它们进行比较。我们实现了这两种算法和Briggs等人的改进算法，并使用SPEC基准测试程序进行了实验比较。结果表明，Sreedhar等人的算法实际上是目前编译器技术水平下的最佳算法。（二）关于特别服务协定形式的优化，有各种建议，但仍有不足之处。例如，在部分冗余消除和代码移动算法中，难以跨SSA形式的phi函数移动代码，并且已知无法优化的简单示例。在我们的研究中，我们开发并实现了一个算法，克服了这个问题。并且可以随着执行而移动部分冗余代码 ...更多信息 2.编译器优化器的验证（i）作为测试编译器优化器的方法，我们开发并实现了一个系统，该系统输出优化前后每个变量的值作为跟踪，然后在优化后对这些输出进行比较检查。这可以验证各种优化器的正确性。（ii）我们做了一个系统，它可以从时序逻辑中的优化器规范自动生成优化器。我们设计了各种技术在实施中，该系统具有一个特点，它可以实现在小的实际时间相比，以前的工作优化。（iii）我们开发了一种方法，其中现有优化器要满足的条件在时态逻辑中指定，并且在实际进行优化之后，使用模型检查来检查指定条件的可满足性。它被执行和评估。从而验证了现有的手写优化器的有效性。此外，它还可以在优化器中找到未知的bug。少