Verifying Parallel Odd–Even Sorting

title:Verifying Parallel Odd–Even Sorting
keywords:verification, logics, algorithms, GPU, parallel
topics:Case studies and Applications, Logics and semantics
contact:W.H.M. Oortwijn MSc & prof.dr. M. Huisman


Description

Odd-even sort is a relatively simple sorting algorithm that can elegantly be implemented on parallel platforms, like GPU kernels. A description of the algorithm can be found at [1]. Moreover, one of the challenges of the verification competition VerifyThis2017 [2] was to verify a parallel implementation of this algorithm. On the university of Twente we are developing the VerCors verification toolset [3], which is capable of verifying the correctness of such algorithms. In this research project you will demonstrate this.

Concretely, in this project you will use the VerCors verifier to prove correctness of the parallel odd-even sorting algorithm (implemented as a GPU kernel). With proving correctness we mean proving the following: (1) the output array is sorted; (2) the output array is a permutation of the input array; and (3) the algorithm terminates. The VerCors toolset can be found at [3], together with a large collection of verification examples (including GPU kernels and other sorting algorithms).

References

  1. Odd-even sort (Digital version available here)
  2. VerifyThis2017 (Digital version available here)
  3. VerCors source code (Digital version available here)