Extending applicability of symbolic execution to uncover possible shared memory transactions in GPU programs

Abstract: General-purpose computing on the graphics processing unit has become popular since the cost-to-power ratio is lower for GPUs (compared to CPUs) and the programmability of the GPU has increased. CUDA is an extension of the C/C++ programming languages which enables software developers to more easily make use of the computational power of the GPUs. One of the main inefficiencies of GPU programs is shared memory bank conflicts. Recent work at Linköping University has proposed a symbolic execution tool, GBC, built on top of the already existing tool GKLEE, to systematically find inputs causing a certain number of shared memory transactions in programs written using CUDA. The aim of this thesis project was to extend the applicability of this tool. To accomplish this, a GPU implementation of breadth-first search was chosen to be analyzed with GBC. This program was chosen since graph algorithms are common in computer science and are an active area of research in the context of GPUs. The input to breadth-first search, the graph, had to be modeled symbolically. This symbolic model can be used to represent both directed and undirected graphs. The results of this thesis show that it is indeed possible to apply GBC to breadth-first search in conjunction with the symbolically modeled graphs. GBC discards states with graphs that do not conform to the constraints enforced by the model, and GBC can also find graphs that show different behaviors (the number of shared memory transactions) of the program. However, because of scalability issues with the underlying symbolic execution engine, GKLEE, the analysis has not been applied to inputs nearly as large as what is common in GPU applications.