| Item type |
Trans(1) |
| 公開日 |
2018-09-20 |
| タイトル |
|
|
タイトル |
Verified Translation Validation Technique for OSCAR Automatically Parallelizing Compiler |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Verified Translation Validation Technique for OSCAR Automatically Parallelizing Compiler |
| 言語 |
|
|
言語 |
eng |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
[発表概要] |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_6501 |
|
資源タイプ |
journal article |
| 著者所属 |
|
|
|
Waseda University |
| 著者所属 |
|
|
|
The French National Institute for computer science and applied mathematics |
| 著者所属 |
|
|
|
The Univesity of Arizona |
| 著者所属 |
|
|
|
University of Illinois at Urbana-Champaign |
| 著者所属 |
|
|
|
Waseda University |
| 著者所属 |
|
|
|
Waseda University |
| 著者所属(英) |
|
|
|
en |
|
|
Waseda University |
| 著者所属(英) |
|
|
|
en |
|
|
The French National Institute for computer science and applied mathematics |
| 著者所属(英) |
|
|
|
en |
|
|
The Univesity of Arizona |
| 著者所属(英) |
|
|
|
en |
|
|
University of Illinois at Urbana-Champaign |
| 著者所属(英) |
|
|
|
en |
|
|
Waseda University |
| 著者所属(英) |
|
|
|
en |
|
|
Waseda University |
| 著者名 |
Jixin, Han
Tomofumi, Yuuki
Michelle, Strout
David, Padua
Hironori, Kasahara
Keiji, Kimura
|
| 著者名(英) |
Jixin, Han
Tomofumi, Yuuki
Michelle, Strout
David, Padua
Hironori, Kasahara
Keiji, Kimura
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
A parallelizing compiler transforms a source program aggressively to obtain a highly parallelized program. The parallelized program must preserve the semantics of the source program. However, an aggressive transformation might violate the semantics due to involuntary embedded bugs in a compiler. These compiler bugs are hard to investigate because of the complexity of a parallelizing compiler. In this presentation, we propose a verified transformation validation technique for OSCAR parallelizing compiler. The proposed technique can validate the correctness of a program transformation by comparing the semantics of a source program with that of a transformed program. We use a partial order relationship between tasks in a program as a program semantics. The compiler first decomposes a source program into multiple tasks hierarchically. Before and after each program transformation in the compiler, it analyses the earliest executable conditions, which represent both data and control dependences among tasks. Then, partial order relationships among tasks are obtained from the earliest executable conditions, and finally the validator compares them obtained from before and after the transformation to check the correctness of it. We also verify the validator mechanically by Coq. We define the theorems for Coq to prove the correctness of the proposed validator. |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
A parallelizing compiler transforms a source program aggressively to obtain a highly parallelized program. The parallelized program must preserve the semantics of the source program. However, an aggressive transformation might violate the semantics due to involuntary embedded bugs in a compiler. These compiler bugs are hard to investigate because of the complexity of a parallelizing compiler. In this presentation, we propose a verified transformation validation technique for OSCAR parallelizing compiler. The proposed technique can validate the correctness of a program transformation by comparing the semantics of a source program with that of a transformed program. We use a partial order relationship between tasks in a program as a program semantics. The compiler first decomposes a source program into multiple tasks hierarchically. Before and after each program transformation in the compiler, it analyses the earliest executable conditions, which represent both data and control dependences among tasks. Then, partial order relationships among tasks are obtained from the earliest executable conditions, and finally the validator compares them obtained from before and after the transformation to check the correctness of it. We also verify the validator mechanically by Coq. We define the theorems for Coq to prove the correctness of the proposed validator. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AA11464814 |
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO）
巻 11,
号 3,
p. 31-31,
発行日 2018-09-20
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
1882-7802 |
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-TPRO1103012.pdf (31.8 kB)
