Abstract
This paper presents a technique for repairing errors in GPU kernels written in CUDA or OpenCL due to data races and barrier divergence. Our novel extension to prior work can also remove barriers that are deemed unnecessary for correctness. We implement these ideas in our tool called GPURepair, which usesGPUVerify as the verification oracle for GPU kernels. We also extend GPUVerify to support CUDA Cooperative Groups, allowing GPURepair to suggest inter-block synchronization for repairing a CUDA kernel if deemed necessary. To the best of our knowledge, GPURepair is the only tool that can propose a fix for intrablockdata races and barrier divergence errors for both CUDA and OpenCL kernels. It is also the only tool that can propose fixes for inter-block data races in CUDA kernels. We perform extensive experiments on about 750 kernels and provide a comparison with prior work. We demonstrate the superiority of GPURepair through its capability to fix more kernels and its unique ability to remove redundant barriers and handle inter-block data races. We have also enhanced the initial version of GPURepair to support incremental solving during the repairprocess. This enhancement improves the performance of GPURepair by about 25% for the test suite that we have used.
Saurabh Joshi
Principal Researcher
My research interests include Blockchain, Distributed Systems, Constraint Programming, Formal Verification, Programming Languages and Program Analysis.