13881

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

Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric
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}

}

Download Download (PDF)   View View   Source Source   

1719

views

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.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2024 hgpu.org

All rights belong to the respective authors

Contact us: