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

点击翻译按钮获取中文摘要

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