A Sound and Complete Abstraction for Reasoning about Parallel Prefix Sums
This webpage accompanies our POPL'14 paper, which introduces a novel abstraction for scalable reasoning about parallel prefix sum implementations. We show that the correctness of a candidate implementation can be determined by (a) proving that the program is data-race free and (b) running a single test-case using our abstraction.
Downloads
We give code for our experimental evaluation, including 4 parallel prefix sum OpenCL implementations (Kogge-Stone, Sklansky, Brent-Kung and Blelloch) and scripts to build and reproduce the results in our paper. To run this code you will require an OpenCL device and GPUVerify. Instructions are given as a readme inside the tarball.