University of Twente Student Theses
GPGPU Verification: Correctness of Odd-Even Transposition Sort Algorithm
Kumashev, Yernar (2020) GPGPU Verification: Correctness of Odd-Even Transposition Sort Algorithm.
|
PDF
372kB |
| Abstract: | 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. |
| Item Type: | Essay (Bachelor) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Business & IT BSc (56066) |
| Link to this item: | https://purl.utwente.nl/essays/80585 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page