Formal Analysis Techniques for GPU Kernels

Tutorial at HiPEAC 2014, Berlin
21 January 2014

FAT-GPU 2014 is supported by the FP7 project CARP: Correct and Efficient Accelerator Programming

The tutorial is also supported by the HiPEAC Network of Excellence, through which the HiPEAC conference is organised.

Bibliography

The tutorial will not assume that the audience has read any background material on formal analysis techniques for GPU kernels. Nevertheless, some advance preparation is likely to make the tutorial material easier to follow.

The tutorial will, in part, cover material from the following paper:

• A. Betts, N. Chong, A.F. Donaldson, S. Qadeer, P. Thomson. GPUVerify: a verifier for GPU kernels. OOPSLA 2012.

Other relevant recent works on verification and semantics for GPU kernels include:

• G. Li, P. Li, G. Sawaya, G. Gopalakrishnan, I. Ghosh, and S.P. Rajan. GKLEE: concolic verification and test generation for GPUs. In PPOPP 2012.
• G. Li, G. Gopalakrishnan. Scalable SMT-based verification of GPU kernel functions. In FSE 2010.
• P. Collingbourne, C. Cadar, P.H.J. Kelly. Symbolic testing of OpenCL code. In HVC 2011.
• A. Leung, M. Gupta, Y. Agarwal, R. Gupta, R. Jhala, S. Lerner. Verifying GPU kernels by test amplification. PLDI 2012.
• A. Habermaier, A. Knapp. On the correctness of the SIMT execution model of GPUs. In ESOP 2012.