Description

By emerging GPUs, many sequential programs migrate into GPUs to gain more performance, but verifying the correctness of GPU programs is still challenging. There is a tool, VerCors, developed in our group to verify concurrent programs. It accepts input languages (Java, OpenMP, OpenCL, PVL) a long with annotations and verifies data race freedom and functional correctness of the programs. In the case of GPU programs, the annotations are as  pre/postconditions in the kernels and barriers. Barriers are mechanisms in GPU programs to synchronize the execution of threads in one block. 

There is a another tool, GPUVerify, developed at Imperial College London, to verify only data race freedom of GPU programs. The advantage of this tool, rather than VerCors is that they can generate annotations automatically. Since they generate annotations for barriers, we would like to investigate how we can use it to generate annotations for barriers in VerCors.

TASK:

1. Understanding how VerCors and GPUVerify works.

2. Understanding how annotations are generated for barriers in GPUVerify.

3. Discovering how VerCors can benefit from step 2 to generate annotations for barriers.

4. Implementing step 3 in the VerCors toolset.