Adding support for CUDA Cooperative Groups API

[cs17resch01003]

As a part of our work (@cs17resch01003 and @sbjoshi) on GPURepair (https://arxiv.org/abs/2011.08373), we have extended Bugle and GPUVerify to support the CUDA Cooperative Groups API (https://docs.nvidia.com/cuda/cuda-c-programming-guide/index.html#cooperative-groups). This pull request depends on https://github.com/mc-imperial/bugle/pull/8. There are two changes in this pull request:

1. We have changed the access modifiers of the GPUVerifyErrorReporter class and some methods in it so that it can be extended in GPURepair
2. To support grid-level synchronization, we have added code to GPUVerify such that the shared variables can be havoced without checking if the threads belong to the same group. We have included comments wherever we have made a code change, please take a look

We have tried to maintain the same code formatting as that of the existing code. Please let us know if any changes are needed or if there are any questions.

One thing we noticed is that the Travis build configuration checks out the code for libclc from version bac1578088e of https://git.llvm.org/git/libclc.git/ which doesn't exist anymore. For GPURepair, we are using https://github.com/llvm/llvm-project/tree/release/8.x/libclc which we believe is the closest to the checked-out version. With that change one of the test cases (OpenCL/pointeranalysistests/manyprocedures) is failing. GPUverify is able to identify null pointer accesses and write-write races for this kernel. This test case is failing even without our code changes. Attaching the output from GPUVerify. Please let us know if any further investigation is needed from our side.

[jeroenk]

Hi @cs17resch01003

Thanks for your merge request. We're committed from our side to get this merged, but both @afd and I are quite busy at the moment, so things might move a bit slowly. Our apologies for this in advance.

To start, two requests:

• Could the changes to the access modifiers be split off in a separate merge request? These changes have nothing to do with with cooperative groups, so we would like to look at them separately.
• Could you add some tests to the test suite? Some passing and failing tests similar to https://github.com/mc-imperial/gpuverify/blob/master/testsuite/CUDA/localarrayaccess/kernel.cu but with a global array probably make most sense. You will need to create a directory per test kernel and the kernel file needs to be named kernel.cu. These need to be located below https://github.com/mc-imperial/gpuverify/tree/master/testsuite/CUDA . If you need inspiration with regard to directory structure, have a look at the curand tests in https://github.com/mc-imperial/gpuverify/tree/master/testsuite/CUDA/curand_tests

Thanks,

Jeroen

[cs17resch01003]

Thank you for the reply. I will make the required changes and raise new pull requests. @sbjoshi