Unsafe Floating-point to Unsigned Integer Casting Check for GPU Programs

Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric. 8th International Workshop on Numerical Software Verification (NSV 2015), Seattle, WA, USA.
[pdf] [bib]

Abstract: Numerical programs usually include type-casting instructions which convert data among different types. Identifying unsafe type-casting is important for preventing undefined program behaviors which cause serious problems such as security vulnerabilities and result non-reproducibility. While many tools had been proposed for handling sequential programs, to our best knowledge, there isn’t a tool geared toward GPUs. In this paper, we propose a static analysis based method which points out all potentially unsafe type-casting instructions in a program. To reduce false alarms (which are commonly raised by static analysis), we employ two techniques, manual hints and predefined function contracts, and we empirically show that these techniques are effective in practice. We evaluated our method with artificial programs and samples from CUDA SDK. Our implementation is currently being integrated into a GPU program analysis framework called GKLEE. We plan to integrate dynamic unsafe type-casting checks also in our future work.

Bibtex:

@inproceedings{nsv2015-cgr,
  author = {Wei-Fan Chiang and Ganesh Gopalakrishnan and Zvonimir Rakamari\'c},
  title = {Unsafe Floating-point to Unsigned Integer Casting Check for {GPU} Programs},
  booktitle = {Proceedings of the 8th International Workshop on
    Numerical Software Verification (NSV)},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = {317},
  publisher = {Elsevier},
  year = {2015},
  pages = {33--45},
}