OpenCL verification (Bachelor Project)

As part of my study Computer Science I have done the Bachelor Project. In this project I worked on verifying an OpenCL progam with Permission-Based Separation Logic. I have written a paper about the results of my research and presented this at the 23rd Twente Studen Conference on IT organised by the University of Twente. I received the Best Paper Award for my paper, which means it was chosen as the best paper in the track Formal Methods and Software Engineering (contained 7 papers in total). I received a mark of 9 out of 10 for the project (the process, the paper and the presentation combined).

logo

Abstract

The Prefix Sum is an algorithm used as a building block for various other algorithms, for example radix sort, quicksort and lexically comparing strings. Implementing the Prefix Sum algorithm on the CPU is trivial, but a parallel approach with OpenCL is more complicated. An implementation in OpenCL has been made, and optimized to minimize branch divergence by comparing two different storage solutions. These storage solutions have been benchmarked in order to show the difference in execution time. In addition to performance, verification of the algorithm is important. The two aspects that need to be verified are the absence of data races and functional correctness. This paper describes a specification that covers the absence of data races, by using Permission-Based Separation Logic. The first part of this specification (the up-sweep phase of the algorithm) has been verified using the VerCors tool.