Detecting Data Races on OpenCL Kernels with Symbolic Execution
Monoidics Ltd
arXiv:1308.3203 [cs.PL], (14 Aug 2013)
@article{2013arXiv1308.3203D,
author={Distefano}, D. and {Dubreil}, J.},
title={"{Detecting Data Races on OpenCL Kernels with Symbolic Execution}"},
journal={ArXiv e-prints},
archivePrefix={"arXiv"},
eprint={1308.3203},
primaryClass={"cs.PL"},
keywords={Computer Science – Programming Languages},
year={2013},
month={aug},
adsurl={http://adsabs.harvard.edu/abs/2013arXiv1308.3203D},
adsnote={Provided by the SAO/NASA Astrophysics Data System}
}
We present an automatic analysis technique for checking data races on OpenCL kernels. Our method defines symbolic execution techniques based on separation logic with suitable abstractions to automatically detect non-benign racy behaviours on kernels.
August 15, 2013 by hgpu
