|title:||GPGPU Verification: Correctness of Odd-Even Transposition sort algorithm|
|keywords:||GPGPU Verification: Correctness of Odd-Even Transposition Sort Algorithm|
|topics:||Case studies and Applications|
With the increasing popularity of concurrent programming, many parallel algorithms have been proposed, that are not yet verified. The use of unverified parallel programs in production can result in wrong outputs from the programs leading to undesired situations. This paper discusses the verification of data race freedom and functional correctness of one of the parallel algorithms, the Odd-Even Transposition Sort algorithm, that was not yet verified to the best of our knowledge. The first step is to use Permission-Based Separation Logic supported by verification tool VerCors, to verify that the algorithm is data-race free. The Permission-Based Separation Logic is an extension of Hoare logic and Separation Logic that helps to reason about computer program correctness with the use of pre/post conditions. The next step is to verify the functional correctness of the algorithm, meaning that it outputs the sorted input array. The verification of functional correctness is achieved by adding more annotations to the Permission-Based Separation Logic annotations used to prove data-race freedom.