Ethel Bardsley of Imperial College London
[gview file=”/wp-content/uploads/iwocl-2014-tech-presentation-Ethel-Bardsley.pdf”]
GPUVerify is a tool for verifying that GPU kernels are free from data races and barrier divergence. It is intended as an automatic verification tool, but its usability is impaired by the fact that the user must explicitly supply kernel source code, the number of threads, and some kernel parameters. Extracting this information from nontrivial OpenCL programs is laborious and error-prone.
We describe an extension to GPUVerify, called KernelInterceptor, that automates the extraction of this information from a given OpenCL application. KernelInterceptor executes the application, detects each kernel launch, records the values of the various parameters, tries to generalise the values of these parameters across repeated kernel launches, and then runs GPUVerify using the parameters thus obtained. We explain how the interception mechanism works, and comment on the extent to which it improves the usability of GPUVerify.