|June 13, 2013||BSc Presentation: Formal Specification and Verification of OpenCL Kernel Optimizations|
|Room: Zi 5126||Jeroen Vonk|
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 execute (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 threads running the code can be executed concurrently with thousands of threads. All these threads concurrently executing, and 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 the consequences are 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.