| 講演名 | 2007/3/9 C言語プログラムにおけるループ最適化に対するループ展開を伴わない等価性検証手法(検証,組込技術とネットワークに関するワークショップETNET2007) 松本 剛史, 瀬戸 謙修, 藤田 昌宏, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 組込みシステムのように設計制約の厳しいシステムの設計では、設計者の手による高度なループ最適化は重要な技術の一つである.本稿では、ループ最適化を対象とした等価性検証手法を提案する。従来の記号シミュレーションによる検証では、ループを展開するため、等価性は展開された回数までしか証明されず、また、展開回数が多い場合に検証時間が長期化するという問題点があった。そこで、提案手法では、比較するべき出力変数の記号式を記号シミュレーションによって求める前に、あらかじめプログラムを解析し、必要な文とそれが実行されるときのイテレータの記号値を求める。記号シミュレーションを選択された文に対してのみ行うことにより、ループ展開を行うことなく、等価性検証を行う。実際のループ最適化に対する実験を通して、提案手法が十分短い検証時間で、等価性を検証することができることを示す。 |
| 抄録(英) | In designing systems such as embedded systems, where many restrictions must be satisfied, loop optimization plays an improtant role. In this paper, an equivalence checking of loop optimization is proposed. In the previous methods based on symbolic simulation, loops must be unrolled before verification. This results in that the equivalence is proved just for the unrolled programs and verification takes much time when the number of unrolling is large. In the proposed method, first, statements and the corresponding symbolic values of the iterators that are required to compute the output variables are identified. Then, symbolic simulation is applied only to the statements. Therefore, the equivalence can be checked without unrolling loops. The experimental results show that the proposed method can verify the real loop optimizations in short time. |
| キーワード(和) | 等価性検証 / ループ最適化 / データ依存グラフ / 記号シミュレーション |
| キーワード(英) | Equivalence checking / Loop optimization / Data dependence graph / Symbolic simulation |
| 資料番号 | CPSY2006-94,DC2006-108 |
| 発行日 |
| 研究会情報 | |
| 研究会 | DC |
|---|---|
| 開催期間 | 2007/3/9(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Dependable Computing (DC) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | C言語プログラムにおけるループ最適化に対するループ展開を伴わない等価性検証手法(検証,組込技術とネットワークに関するワークショップETNET2007) |
| サブタイトル（和） | |
| タイトル（英） | Equivalence Checking of Loop Optimizations in C Programs without Loop Unrolling |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 等価性検証 / Equivalence checking |
| キーワード(2)（和/英） | ループ最適化 / Loop optimization |
| キーワード(3)（和/英） | データ依存グラフ / Data dependence graph |
| キーワード(4)（和/英） | 記号シミュレーション / Symbolic simulation |
| 第 1 著者 氏名（和/英） | 松本 剛史 / Takeshi MATSUMOTO |
| 第 1 著者 所属（和/英） | 東京大学大学院工学系研究科電子工学専攻 Dept. of Electronics Engineering, University of Tokyo |
| 第 2 著者 氏名（和/英） | 瀬戸 謙修 / Kenshu SETO |
| 第 2 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター VLSI Design and Education Center, University of Tokyo |
| 第 3 著者 氏名（和/英） | 藤田 昌宏 / Masahiro FUJITA |
| 第 3 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター VLSI Design and Education Center, University of Tokyo |
| 発表年月日 | 2007/3/9 |
| 資料番号 | CPSY2006-94,DC2006-108 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 604 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |