11123

Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU Kernels

Ethel Bardsley, Alastair F. Donaldson
Imperial College London
Imperial College London, 2013

@article{bardsley2013warps,

   title={Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU Kernels},

   author={Bardsley, Ethel and Donaldson, Alastair F},

   year={2013}

}

Download Download (PDF)   View View   Source Source   Source codes Source codes

Package:

4550

views

We describe the design and implementation of methods to support reasoning about data races in GPU kernels where constructs other than the standard barrier primitive are used for synchronization. At one extreme we consider kernels that exploit implicit, coarse-grained synchronization between threads in the same warp, a feature provided by many architectures. At the other extreme we consider kernels that reduce or avoid barrier synchronization through the use of atomic operations. We discuss design decisions associated with providing support for warps and atomics in GPUVerify, a formal verification tool for OpenCL and CUDA kernels. We evaluate the practical impact of these design decisions using a large set of benchmarks, showing that warps can be supported in a scalable manner, that a coarse abstraction suffices for efficient reasoning about most practical uses of atomic operations, and that a novel, refined abstraction captures an important design pattern where atomic operations are used to compute unique array indices. Our evaluation revealed two previously unknown bugs in publicly available benchmark suites.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2024 hgpu.org

All rights belong to the respective authors

Contact us: