GPUプログラム検証？
プログラム検証という研究分野がある。
検証の意味合いについては色々あるが、GPUプログラム上での検証は主にデータ競合の検知が重要となる。
そのデータ競合の検知についての最近の研究についてまとめていく。
最近の事情の俯瞰には、書籍「Advances in GPU Research and Practice」の「Formal Analysis Techniques for Reliable GPU programming: Current Solutions and Call to Action」が詳しいです。
Utah大学 (GKLEE)
http://www.parallel.utah.edu
LLVMの記号実行環境KLEEの拡張としてGPUの検証機能をもたせたGKLEEを開発。
GPUと銘打った論文は2010年から。しかしそれ以前にもMPIプログラムの検証とかをしている。
以前はPUGを開発していたが、そちらは終了して、今はGKLEEがメイン。
GKLEEで使用するSESAという静的解析ツールも作成している。
中心人物: Peng Li, Guodong Li, Ganesh Gopalakrishnan
論文
- 2010年 A Symbolic Verifier for Cuda Programs
- ☆2010年 PUG: A Symbolic Verifier of GPU Programs
- 2010年 Scalable SMT-Based Verification of GPU Kernel Functions
- ☆2012年 GKLEE: Concolic Verification and Test Generation for GPUs
- 2012年 Parametrized Verification of GPU Kernels
- ☆2012年 Parametric Flows: Automated Behavior Equivalencing for Symbolic Analysis of Races in CUDA Programs
- 2013年 Formal Analysis of GPU Programs with Atomics via Conflict-Detected Delay-Bounding
- ☆2014年 Practical Symbolic Checking of GPU Programs
インペリアル・カレッジ・ロンドン (GPUVerify)
http://multicore.doc.ic.ac.uk
検証用の言語Boogieを使って検証するGPUVerifyを開発。
中心人物: Alastair F. Donaldson
論文
- 2011年 Symbolic Testing of OpenCL Code
- ☆2012年 GPUVerify: a Verifier for GPU Kernels
- 2013年 Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
- ☆2013年 Barrier Invariants: a Shared State Abstraction for the Analysis of Data-Dependent GPU Kernels
- 2014年 KernelInterceptor: Automating GPU Kernel Verification by Intercepting Kernels and their Parameters
- ☆2015年 The Design and Implementation of a Verification Technique for GPU Kernels
Twente大学 (VerCors)
http://fmt.cs.utwente.nl
検証プラットフォームVerCorsにOpenCLも検証できるようにした感じ。
Permission-Based Separation Logicを使用。
Linkoping University
論文
- 2011年 Software Model Checking for GPGPU Programs Towards a Verification Tool
- 2014年 Automated Software Testing of Memory Performance in Embedded GPUs
オハイオ州立大学（GRaceなど）
研究室のサイトは更新が止まっているようなので、筆者のサイトを追うと良い
http://web.cse.ohio-state.edu/~qin/publication.htm
http://web.cse.ohio-state.edu/~agrawal/
中心人物: Feng Qin, Gagan Agrawal
東京工業大学、増原英彦研究室
Coqを使ったsoundnessの検証
http://prg.is.titech.ac.jp/ja/news/coqpl17/
http://prg.is.titech.ac.jp/ja/projects/gpucsl/
最近発見した。
京都大学、計算機ソフトウェア分野
http://www.fos.kuis.kyoto-u.ac.jp
ホーア理論を使ってGPUを検証しているみたい。
