Optimization Verifying Compilers

本研究的目的是将“验证编译器”理论应用于编译器优化，研究编译器优化的数学理论，拓宽验证的领域。验证编译器的概念最初是由CAR Hoare提出的。如今，编译器优化已经变得非常复杂，并且由于其复杂性而容易出错。在本研究中，我们旨在构建一个编译系统，在该编译系统中，优化的应用程序可以自动验证，并自动保证生成的代码的正确性。今年，我们研究了Web社区中优化知识的提取，Web社区已经迅速成为一个计算平台。具体来说，我们已经成功地提取了与编程相关的知识。我们已经看到，结果直观上是正确的。此外，我们还揭示了分布式环境中计算的形式化与安全描述密切相关，安全描述是正确性保证的邻居。具体地说，我们提出了一种形式化业务工作流并在文档中表示它的方法。此外，我们还研究了“超越编译器优化的性能调优”，其中我们扩大了优化候选的搜索空间。具体来说，我们将高阶程序变换应用到数值程序中，发现了更广阔的候选搜索空间。

The objective of this research is to apply the theory of "Verifying Compilers" to compiler optimization, and to investigate the mathematical theory of compiler optimizations, and to broaden the area of verifications. The concept of verifying compilers is originally proposed by CAR Hoare. Today, compiler optimization have become complicated, and error-prone because of their complexities. In this research, we aim at building a compiler system in which an application of an optimization is automatically verified, and the correctness of the generated codes is also automatically guaranteed.This year, we studied the extraction of knowledge of optimizations in a Web community, which has rapidly emerged as a computing platform. Concretely, we have succeeded in extracting knowledge related to programming. We have seen that the result is intuitively correct. Furthermore, we have revealed that the formalization of computing in a distributed environment is closely related to security description, which is a neighbor to correctness guarantee. Concretely, we have proposed a method of formalizing a business workflow, and of representing it in a document.Moreover, we have studied "performance tuning beyond compiler optimizations," in which we have broaden the search space of candidates of optimizations. Concretely we have applied higher order program transformations to numerical programs, and have found the wider space of candidate search.