SMT-based context-bounded model checking for CUDA programs

作者：Pereira Phillipe; Albuquerque Higo; da Silva Isabela; Marques Hendrio; Monteiro Felipe; Ferreira Ricardo; Cordeiro Lucas^*

来源：Concurrency and Computation: Practice and Experience (CCPE) , 2017, 29(22): e3934.

DOI：10.1002/cpe.3934

• model checking
• GPU
• CUDA programs
• formal verification

We present ESBMC-GPU tool, an extension to the Efficient SMT-Based Context-Bounded Model Checker (ESBMC), which is aimed at verifying Graphics Processing Unit (GPU) programs written for the Compute Unified Device Architecture (CUDA) platform. ESBMC-GPU uses an operational model, that is, an abstract representation of the standard CUDA libraries, which conservatively approximates their semantics, in order to verify CUDA-based programs. It then explicitly explores the possible interleavings (up to the given context bound), while treats each interleaving itself symbolically. Additionally, ESBMC-GPU employs the monotonic partial order reduction and the two-thread analysis to prune the state space exploration. Experimental results show that ESBMC-GPU can successfully verify 82% of all benchmarks, while keeping lower rates of false results. Going further than previous attempts, ESBMC-GPU is able to detect more properties violations than other existing GPU verifiers due to its ability to verify errors of the program execution flow and to detect array out-of-bounds and data race violations.

• 出版日期2017-11-25