核心概念
データフロープログラムの非同期性を考慮し、動的分数パーミッションを用いることで、命令型プログラムと等価なデータフロープログラムを検証する。
摘要
本論文は、コース粒度再構成可能アレイ(CGRA)アーキテクチャ向けのデータフロープログラムの翻訳検証手法を提案している。CGRAは命令レベルの並列性が高く、電力効率に優れているが、非同期性によりデータ競合などの新たな正誤問題が発生する。
提案手法WaveCertは2段階のアプローチを取る:
記号実行を用いて、命令型プログラムとデータフロープログラムの正準スケジュールにおける等価性を証明する。
動的分数パーミッションを用いて、データフロープログラムの収束性(confluence)を証明する。これにより、正準スケジュール以外のスケジュールでも等価性が成り立つことを示す。
WaveCertは、最先端のRipTideデータフロープログラムコンパイラを対象に実装され、8つのコンパイラバグを発見した。多くの検証結果が10秒以内に得られ、最長でも30秒程度であった。
統計資料
データフロープログラムの非同期性により、命令型プログラムと比べて指数的に多くの状態が生じる。
動的分数パーミッションを用いることで、オペレータ間のメモリアクセスの整合性を自動的に検証できる。
引述
"データフロープログラムは、その本質的な並列性ゆえに、新たな微妙な正誤問題を引き起こす。"
"過去の経験から、正式な検証を早期に組み込むべきであると主張する。CGRAアーキテクチャが意図通りに動作するためには、正しいデータフロープログラムが不可欠である。"