Optimization Verifying Compilers
| Project/Area Number |
17500016
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
SATO Hiroyuki The University of Tokyo, Information Technology Center, Associate Professor (20225999)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SATO Hiroyuki The University of Tokyo, Information Technology Center, Associate Professor (20225999)
|
|---|
| Project Period (FY) |
2005 – 2007
|
| Project Status |
Completed (Fiscal Year 2007)
|
| Budget Amount *help |
¥3,740,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥240,000)
Fiscal Year 2007: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2006: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 2005: ¥1,400,000 (Direct Cost: ¥1,400,000)
|
|---|
| Keywords | performance optimization / compiler / distributed environment / security / formalization / 分散スケジューリング / 検証 / 自律分散性 / 最適化 / 最適化コンパイラ / 型システム / Itanium2 / メモリモデル / XSLT |
|---|
| Research Abstract |
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.
|
Report
(4 results)
Research Products
(18 results)
