high performance computing on graphics processing units: hgpu.org

Computing general problems using the graphical processing unit (GPU) of a device is an emerging field. The parallel structure of the GPU allows for massive concurrency, when executing a program. Therefore, by executing (a part of) the code on the GPU, a previously unused resource can be used, to achieve a speed-up of an application. Previously, programming on GPUs was a tedious job, and the implementation was depending on the manufacturer – or even on the model of the GPU. With the arrival of OpenCL, an open and broad platform was offered, focussed to deliver General Purpose computing on the GPU, or GPGPU to a broader audience. Despite the sometimes simple appearance of OpenCL code, it is important to keep in mind that there can be thousands of threads running the code concurrently. All these concurrently executing threads that are potentially accessing the same memory locations, can easily lead to implementation errors. This research is focussed on verifying OpenCL code, using permission-based separation logic, to prevent those errors in an early stage. Moreover, we have investigated what are the consequences of optimizations of a OpenCL-program for the verification of that program. It is common practice to use optimization in GPGPU, since the code executed on the GPU is often "resource-hungry", either for memory, processing power, or both. Therefore, optimizing the GPGPU part of a program will often result in a significant speed-up. As a verification use-case, we have developed a simple implementation of Conway’s Game of Life, a well-known zero player game, based on a cellular automaton. We have verified this implementation using permission-based separation logic, enriched with some rules specifically for OpenCL. Therefore, we had to annotate the code in a similar way when using the VerCors tool-set. Furthermore, we developed three optimizations of this code using common optimization techniques. To verify each of the optimizations we have looked at the changes needed in the verification, in relation to the original verification. Our optimized versions, upon execution, are indeed faster than the original implementation. Moreover, we can show several patterns for changing our verification to fit our optimization. Using these patterns, one could possibly automatically optimize OpenCL code, whilst still guaranteeing the correctness of the program, given that the previous implementation was correct.