Description

Radix sort algorithm is a well-known sorting algorithm with many applications. Researchers have proposed different GPU-based implementations of this algorithm. Therefore, the correctness of this algorithm becomes an important issue. 

In this project, we would like to verify data race freedom and functional correctness of GPU-based radix sort algorithm. There is a tool develop in our group, named VerCors, to verify parallel programs. We need to formally define the specification of the algorithm and embed it into the language of the tool. Thereafter, we need to prove correctness of the algorithm against the specification using the tool.

TASKS:

1. Review GPU-based implementations of radix sort algorithm and capture the general parallel algorithm.

1. Formalize the parallel algorithm into the language of VerCors.

2. Verify data race freedom of the algorithm.

3. Verify functional correctness of the algorithm.

Note: Radix sort uses counting sort algorithm internally and counting sort uses prefix sum algorithm inside it. We have already verified a parallel prefix sum algorithm. Thus, verification of counting sort and thereafter radix sort will be on top of prefix sum algorithm.

Final paper: https://drive.google.com/file/d/1aiZ_TFNWIchbU9BjdkwFBKPSSVbW_WhD/view