SCP 2017

Journal of Science of Computer Programming 2017 – Software Track

ESBMC-GPU: A Context-Bounded Model Checking Tool to Verify CUDA Programs

Download Tools and Benchmarks

The chosen benchmark suite comprises 20 CUDA kernels from NVIDIA GPU Computing SDK v2.0, 20 CUDA kernels from Microsoft C++ AMP Sample Projects [1], and 114 CUDA-based programs that explore a wide range of CUDA functionalities [2]. In summary, the chosen suite contains 47.4% bug-free and 52.6% buggy benchmarks, which tackle data race, arithmetic operations, pointer assignment, __device__ function calls, general ANSI-C functions (e.g., memset), general CUDA functions (e.g., cudaMemcpy), general libraries in CUDA (e.g., curand.h), and the ability to work with variables, type modifiers (e.g., unsigned), pointers, type definitions, and intrinsic CUDA variables (e.g., uint4).

See Experimental Results

All these benchmarks were verified with 4 GPU verifiers (ESBMC-GPU v2.0, GKLEE  v2012, GPUVerify v1811, and CIVL v1.7.1), on an otherwise idle Intel Core i7-4790 CPU 3.60 GHz, with 16 GB of RAM, running Ubuntu 14.04 OS. It is worth notice that PUG verifier has been excluded from the experimental evaluation, once, its major components are being merged into GKLEE to address the syntax parsing problem and gain better performance [3]. Furthermore, all presented execution times are actually CPU times, (i.e., only the elapsed time periods spent in the allocated CPUs), which was measured with the times system call (POSIX system).

[1] Microsoft Corporation, C++ AMP sample projects for download (MSDN blog), 2012.
[2] Cheng, J., Grossman, M., and McKercher, T. Professional CUDA C Programming, John Wiley and Sons, Inc., 2014.
[3] University of Utah. PUG – Prover of User GPU programs, 2012.