title: Breadth-First Search: Verifying GPGPU Programs
keywords: GPU programming, GPGPU verification, Graph, OpenCL, Parallel algorithm
topics: Other
committee: Mohsen Safari ,
Marieke Huisman

Description

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:

 

Input:

-       A graph G=(V, E) where V is the set of vertices and E the set of edges.

-       A source vertex s in V.

Output:

-       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.

 

Task:

  1. Design and implement a parallel BFS algorithms on a GPU using OpenCL.
  2. Formulate the requirements in a formal specification language.
  3. Verify data race-freedom of the algorithm using VerCors tool.
  4. Verify functional Correctness of the algorithm using VerCors tool.