読者です 読者をやめる 読者になる 読者になる

はまやんはまやんはまやん

hamayanhamayan's blog

GPUプログラム検証まとめ

研究

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を使用。

論文

  • 2013年 Specification and verification of GPGPU programs using permission-based separation logic
  • 2014年 A Case Study for GPGPU Program Verification
  • 2015年 Specification and Verification of Atomic Operations in GPGPU Programs

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

論文

  • 2010年 GRace: A Low-Overhead Mechanism for Detecting Data Races in GPU Programs
  • 2012年 GMProf: A Low-Overhead, Fine-Grained Profiling Approach for GPU Programs(検証じゃない)
  • 2014年 GMRace: Detecting Data Races in GPU Programs via a Low-Overhead Scheme

東京工業大学、増原英彦研究室

Coqを使ったsoundnessの検証
http://prg.is.titech.ac.jp/ja/news/coqpl17/
http://prg.is.titech.ac.jp/ja/projects/gpucsl/
最近発見した。

論文

  • 2016年 Proof of Soundness of concurrent Separation Logic for GPGPU in Coq
  • 2017年 CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL

京都大学、計算機ソフトウェア分野

http://www.fos.kuis.kyoto-u.ac.jp
ホーア理論を使ってGPUを検証しているみたい。

論文

  • 2016年 Automated verification of functional correctness of race-free GPU programs
  • 2017年 A Hoare Logic for GPU kernels