Optimization Verifying Compilers

优化验证编译器

• 批准号: 17500016
• 负责人: SATO Hiroyuki
• 金额: $ 2.39万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2005
• 资助国家: 日本
• 起止时间: 2005 至 2007
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17500016/
• 关键词: performance optimization; compiler; distributed environment; security; formalization; 分散スケジューリング; 検証; 自律分散性; 最適化; 最適化コンパイラ; 型システム; Itanium2; メモリモデル; XSLT

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.

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

项目成果

Performance comparison of vector calculations between Itanium2 and other processors

安腾2与其他处理器矢量计算性能对比

• 发表时间: 2006
• 期刊: Proceedings of International Workshop on Innovative Architecture
• 作者: Takeshi Nanri;Yoshitaka Watanabe and Hiroyuki Sato,
• 通讯作者: Yoshitaka Watanabe and Hiroyuki Sato,

Construction of Registration Authority for Server Certificates in the University of Tokyo

东京大学服务器证书注册机构建设

• 发表时间: 2008
• 期刊: IPSJ SIG Technical Reports 2008-DSM-48
• 作者: NISHIMURA;Takeshi and SATO;Hiroyuki
• 通讯作者: Hiroyuki

Etracting Tag Hierarchy from Folksonomy

从 Folksonomy 中提取标签层次结构

• 发表时间: 2007
• 期刊: Proceedings of Semantic Web and Web Services
• 作者: OGINOn and SATO;Hiroyuki
• 通讯作者: Hiroyuki

Static Optimization of XSLT stylesheets : template instantiation optimization and lazy XML parsing

XSLT 样式表的静态优化：模板实例化优化和惰性 XML 解析

• 发表时间: 2005
• 期刊: Proc.ACM Document Engineering 2005
• 作者: Manaka;K.;Sato;H.
• 通讯作者: H.

東京大学におけるサーバ証明書発行体制の構築と課題

东京大学服务器证书颁发系统的构建及问题

• 发表时间: 2008
• 期刊: 情報処理学会研究報告 DSM-48
• 作者: 西村健;佐藤周行
• 通讯作者: 佐藤周行