Optimization Verifying Compilers

本研究的目的是将“验证编译器”的理论应用于编译器优化，研究编译器优化的数学理论，拓宽验证的领域。验证编译器的概念最初是由Car Hoare提出的。今天，编译器优化已经变得复杂，而且由于它们的复杂性而容易出错。在本研究中，我们的目标是建立一个自动验证优化应用的编译器系统，并自动保证生成的代码的正确性。今年，我们研究了一个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.