Try out GPUVerify now on rise4fun:
The PENCIL and VOBLA tool chains developed during CARP:
École normale supérieure has developed several tools supporting polyhedral compilation of applications, generating GPU kernels. These tools are being used and extended during CARP by various partners. The tools include:
Javed Absar gives an overview of the CARP project, and presents details of PENCIL and VOBLA:
Alastair Donaldson has recorded three videos about the GPUVerify part of the CARP work to disseminate the project to a broad industrial audience.
This first video gives an overview of GPUVerify, including a demonstration of the tool in action on some practical examples.
This second video explains how the verification techniques of GPUVerify works under the hood, showing how data race analysis for a massively parallel kernel can be reduced to analysis of a sequential program.
In the final video Alastair covers two advanced topics: the lock-step predicated execution technique that the tool uses to handle conditional and looping code, and the manner by which loop invariants are automatically inferred using the Houdini algorithm.
PENCIL Language Specification: Draft for Discussion (based on D3.2 and D3.5)
Project deliverables made available by the Consortium:
Project number 287767. Coordinator: Dr Alastair F. Donaldson, firstname.lastname@example.org