CARP: Correct and Efficient Accelerator Programming

Jump to:

Software tools

GPUVerify: A Verifier for GPU Kernels

Try out GPUVerify now on rise4fun:

Check out videos related to GPUVerify below.

PENCIL and VOBLA Tool Chain and Benchmarks

The PENCIL and VOBLA tool chains developed during CARP:

Polyhedral Compilation Targeting GPUs

É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:

Videos about GPUVerify

Alastair Donaldson has recorded three videos about the GPUVerify part of the CARP work to disseminate the project to a broad industrial audience.

GPUVerify: Introduction and overview

This first video gives an overview of GPUVerify, including a demonstration of the tool in action on some practical examples.

GPUVerify: Verification method

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.

GPUVerify: Predicated execution and invariant inference

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.


HiPEAC 2012

HiPEAC 2013


POPL 2014

HiPEAC 2014

UKMAC 2013 and HiPEAC 2014

Deliverables and reports

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,