SMT‐based context‐bounded model checking for CUDA programs. (2nd August 2016)

• Record Type: Journal Article
• Authors: Pereira, Phillipe; Albuquerque, Higo; da Silva, Isabela; Marques, Hendrio; Monteiro, Felipe; Ferreira, Ricardo; Cordeiro, Lucas
• Other Names: Fox Geoffrey C. guestEditor.; Goldman Alfredo guestEditor.; Arantes Luciana guestEditor.; Moreno Edward guestEditor.
• Is Part Of: Concurrency and computation. Volume 29:Number 22(2017)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2016-08-02
• Subjects: model checking -- GPU -- CUDA programs -- formal verification; Parallel processing (Electronic computers) -- Periodicals; Parallel computers -- Periodicals; 004.35
• DOI: 10.1002/cpe.3934
• Languages: English
• ISSNs: 1532-0626

Abstract

Summary: 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. Copyright © 2016 John Wiley & Sons, Ltd.