Paper Info
Title
Practical symbolic race checking of GPU programs
Abstract
Even the careful GPU programmer can inadvertently introduce data races while writing and optimizing code. Currently available GPU race checking methods fall short either in terms of their formal guarantees, ease of use, or practicality. Existing symbolic methods: (1) do not fully support existing CUDA kernels; (2) may require user-specified assertions or invariants; (3) often require users to guess which inputs may be safely made concrete; (4) tend to explode in complexity when the number of threads is increased; and (5) explode in the face of thread-ID based decisions, especially in a loop. We present SESA, a new tool combining Symbolic Execution and Static Analysis to analyze C++ CUDA programs that overcomes all these limitations. SESA also scales well to handle non-trivial benchmarks such as Parboil and Lonestar, and is the only tool of its class that handles such practical examples. This paper presents SESA's methodological innovations and practical results.
Year
DOI
Venue
2014
10.1109/SC.2014.20
SC
Keywords
Field
DocType
sesa,parallelism,gpu,symbolic execution,cuda,parboil,virtual machine,parallel architectures,graphics processing units,data flow analsis,thread-id based decision,symbolic race checking,lonestar,static analysis,gpu program,cuda kernel,program diagnostics,taint analysis,c++ cuda program,c++ language,formal verification
Programming language,Virtual machine,Programmer,Computer science,CUDA,Parallel computing,Static analysis,Thread (computing),Taint checking,Symbolic execution,Formal verification,Distributed computing
Conference
ISSN
Citations 
PageRank 
2167-4329
12
0.62
References 
Authors
16
3
Name
Order
Citations
PageRank
Peng Li11807.67
Guodong Li21546.18
Ganesh Gopalakrishnan31619130.11