Unsafe Floating-point to Unsigned Integer Casting Check for GPU Programs
School of Computing, University of Utah, Salt Lake City, UT, USA
8th International Workshop on Numerical Software Verification (NSV), 2015
@inproceedings{nsv15-fp-hol-light,
author={Jacobsen, Charles and Solovyev, Alexey and Gopalakrishnan, Ganesh},
title={A Parameterized Floating-Point Formalization in {HOL} Light},
booktitle={NSV 2015: 8th International Workshop on Numerical Software Verification 2015},
url={http://www.cs.utah.edu/fv/papers/nsv15-fp-hol-light.pdf},
note={Seattle, url{http://nsv2015.informatik.uni-freiburg.de/}},
month={apr},
year={2015}
}
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 pre-defined 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.
April 17, 2015 by hgpu