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

1.SSA形式反变换的评价及新的优化方法的发展(I)从SSA形式到范式的反变换的主要算法是Briggs等人的方法。和Sreedhar等人的研究，但到目前为止还没有研究对它们进行比较。我们实现了这两种算法，并对Briggs等人进行了改进。算法，并利用SPEC基准对三者进行了实验比较。结果表明，Sreedhar et al.的算法实际上是目前编译器技术水平下最好的。(Ii)SSA形式的优化方案多种多样，但仍有不足之处。例如，在部分冗余消除和代码移动算法中，很难跨SSA形式的Phi函数移动代码，并且无法优化的简单示例是已知的。在我们的研究中，我们开发并实现了一个算法来克服这个问题。并且可以使用Perform…来移动部分冗余代码2.编译器优化器的验证(I)作为一种测试编译器优化器的方法，我们开发并实现了一个系统，将优化前后的每个变量的值作为轨迹输出，然后对优化后的输出进行比较检查。这可以验证各种优化器的正确性。(Ii)我们实现了一个从时态逻辑中优化器的规格说明自动生成优化器的系统。我们设计了多种实现技术，与以往的工作相比，该系统具有在较小的实际时间内实现优化的特点。(Iii)提出了一种方法，用时序逻辑描述现有优化器要满足的条件，并在实际进行优化后，使用模型检测来检查指定条件的可满足性。它得到了实施和评估。通过这种方式，它可以验证现有的手写优化器。此外，它还可以在优化器中发现未知的错误。较少

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