|title:||Breadth-First Search: Verifying GPGPU Programs|
|keywords:||GPU programming, GPGPU verification, Graph, OpenCL, Parallel algorithm|
Breadth-First Search (BFS) is a well-known problem in graph theory which has many applications. In this problem, we would like to find the minimum number of edges needed to reach a vertex ‘v’ from a source vertex ‘s’ in a graph ‘G’. The formal definition of the problem is:
- A graph G=(V, E) where V is the set of vertices and E the set of edges.
- A source vertex s in V.
- An array in size of V to indicate the minimum number of edges for each vertex.
This project consists of two parts. In the first part, you will design a parallel BFS algorithm and implement it to run on a GPU. The second part is to verify the correctness of the algorithm.
- Design and implement a parallel BFS algorithms on a GPU using OpenCL.
- Formulate the requirements in a formal specification language.
- Verify data race-freedom of the algorithm using VerCors tool.
- Verify functional Correctness of the algorithm using VerCors tool.