Abstract

GPU based computing has made significant strides in recent years. Unfortunately, GPU program optimizations can introduce subtle concurrency errors, and so incisive formal bug-hunting methods are essential. This paper presents a new formal bug-hunting method for GPU programs that combine barriers and atomics. We present an algorithm called Conflict-directed Delay-bounded scheduling algorithm (CD) that exploits the occurrence of conflicts among atomic synchronization commands to trigger the generation of alternate schedules; these alternate schedules are executed in a delay-bounded manner. We formally describe CD, and present two correctness checking methods, one based on final state comparison, and the other on user assertions. We evaluate our implementation on realistic GPU benchmarks, with encouraging results.

Citation

Wei-Fan Chiang, Ganesh Gopalakrishnan, Guodong Li, Zvonimir Rakamaric
Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding
Proceedings of the 5th NASA Formal Methods Symposium (NFM), 7871: 213--228, doi:10.1007/978-3-642-38088-4_15, 2013.

BibTeX

@inproceedings{2013_nfm_cglr,
  title = {Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding},
  author = {Wei-Fan Chiang and Ganesh Gopalakrishnan and Guodong Li and Zvonimir Rakamaric},
  booktitle = {Proceedings of the 5th NASA Formal Methods Symposium (NFM)},
  series = {Lecture Notes in Computer Science},
  volume = {7871},
  publisher = {Springer},
  editor = {Guillaume Brat and Neha Rungta and Arnaud Venet},
  pages = {213--228},
  doi = {10.1007/978-3-642-38088-4_15},
  year = {2013}
}

Acknowledgements

Supported by NSF CCF 1255776, OCI 1148127, and the Microsoft SEIF Award.

Abstract

Citation

BibTeX

Acknowledgements

Resources