Let’s sort this out: GPGPU Verification of Radix Sort
University of Twente, P.O. Box 217, 7500AE Enschede, The Netherlands
University of Twente, 2020
@misc{essay80589,
month={January},
title={Let’s sort this out: GPGPU Verification of Radix Sort},
author={D.H.M.A. van {Oorschot}},
year={2020},
url={http://essay.utwente.nl/80589/}
}
This paper shows how the VerCors verification toolset can be used to prove data race freedom and functional correctness of a parallel radix sort algorithm for GPUs. This is a widely used standard sorting implementation for GPGPU programming frameworks and therefore its correctness is of utmost importance. Additionally, it presents the usefulness of VerCors as well as its current limitations to the scientific community.
February 23, 2020 by hgpu
