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

The paper


We got confirmation the ParBoil bugs (mentioned in ยง5, p13) are genuine bugs!

How to Build

  1. Download the above sources
  2. Build as per for regular GPUVerify (http://multicore.doc.ic.ac.uk/tools/GPUVerify/)

How to Use

Intra-warp synchronization

There are 3 additional flags for warps:


Atomic support, with the refined atomic abstraction, is enabled by default. To turn of the refined abstraction and force adversarial abstraction, use --no-refined-atomics


Ethel Bardsley and Alastair Donaldson