Detecting Bank Conflict of GPU Programs Using Symbolic Execution—Case Study
- 1 Graduate School of Natural Science and Technology, Kanazawa University, Kanazawa, Japan
- 2 Graduate School of Natural Science and Technology, Kanazawa University, Kanazawa, Japan
Abstract
GPU (Graphics Processing Unit) is used in various areas. Therefore, the demand for the verification of GPU programs is increasing. In this paper, we suggest the method to detect bank conflict by using symbolic execution. Bank conflict is one of the bugs happening in GPU and it leads the performance of programs lower. Bank conflict happens when some processing units in GPU access the same shared memory. Symbolic execution is the method to analysis programs with symbolic values. By using it, we can detect bank conflict on GPU programs which use many threads. We implement a prototype of the detector for bank conflict and evaluate it with some GPU programs. The result states that we can detect bank conflict on the programs with no loop regardless of the number of threads.
- Owens, J.D., Houston, M., Luebke, D., Green, S., Stone, J.E. and Phillips, J.C. (2008) GPU Computing. Proceedings of the IEEE, 96, 879-899. https://doi.org/10.1109/JPROC.2008.917757
- Li, P., Li, G. and Gopalakrishnan, G. (2014) Practical Symbolic Race Checking of GPU Programs. Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, New Orleans, 16-21 November 2014, 179-190. https://doi.org/10.1109/SC.2014.20
- Betts, A., et al. (2015) The Design and Implementation of a Verification Technique for GPU Kernels. ACM TOPLAS, 37, Article No. 10.
- Barnett, M., Evan Chang, B.-Y., DeLine, R., Jacobs, B. and Leino, K.R.M. (2005) Boogie: A Modular Reusable Verifier for Object-Oriented Programs. Vol. 4111, Springer, Berlin Heidelberg, 364-387.
- Huisman, M. and Matej, M. (2013) Specification and Verification of GPGPU Programs Using Permission-Based Separation Logic.
- De Moura, L. and Nikolaj, B. (2008) Z3: An Efficient SMT Solver. Vol. 4963, Springer, Berlin Heidelberg, 337-340. https://doi.org/10.1007/978-3-540-78800-3_24
- Sarfraz, K., Psreanu, C.S. and Visser, W. (2003) Generalized Symbolic Execution for Model Checking and Testing. Vol. 2619, Springer, Berlin Heidelberg, 553-568.
- Psreanu, C.S. and Willem, V. (2009) A Survey of New Trends in Symbolic Execution for Software Testing and Analysis. International Journal on Software Tools for Technology Transfer, 11, 339-353. https://doi.org/10.1007/s10009-009-0118-1
- Cadar, C. and Koushik, S. (2013) Symbolic Execution for Software Testing: Three Decades Later. Communications of the ACM, 56, 82-90. https://doi.org/10.1145/2408776.2408795
- Geof23/GkleeTests. https://github.com/Geof23/GkleeTests
- Beyer, D., et al. (2007) The Software Model Checker BLAST. International Journal on Software Tools for Technology Transfer, 9, 505-525.