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等人的算法实际上是可行的。这(ii)对于SSA形式的优化存在各种建议，但仍然存在不足之处，例如在部分冗余消除和代码移动算法中，很难跨网络移动代码。 SSA 形式的函数和无法优化的简单示例是已知的。在我们的研究中，我们开发并实现了一种克服此问题的算法，该算法可以通过执行值编号来移动部分冗余代码。2.编译器的验证。 Optimizers(i)作为测试编译器优化器的方法，我们开发并实现了一个系统，该系统输出优化前后每个变量的值作为跟踪，然后在优化后对这些输出进行比较检查。验证各种优化器的正确性。(ii)我们制作了一个根据时序逻辑中的优化器规范自动生成优化器的系统。我们在实现中设计了各种技术，该系统的一个特点是可以实现小型优化。实际时间与之前相比(iii)我们开发了一种方法，其中在时间逻辑中指定现有优化器要满足的条件，并在实际进行优化后，使用模型检查来检查指定条件的可满足性，并对其进行实现和评估。通过这种方式，它可以验证现有的手写优化器，此外，它还可以发现优化器中的未知错误。