Jump to:

• Software tools
• Videos
• Posters
• Deliverables and reports
• Publications

Software tools

GPUVerify: A Verifier for GPU Kernels

Try out GPUVerify now on rise4fun:

• GPUVerify for OpenCL
• GPUVerify for CUDA

Check out videos related to GPUVerify below.

PENCIL and VOBLA Tool Chain and Benchmarks

The PENCIL and VOBLA tool chains developed during CARP:

• PENCIL driver. This is what you need to compile PENCIL code; it includes the PENCIL header files.
• PENCIL-related tools:
  • PENCIL-to-PENCIL optimizer and linker.
  • PENCIL auto-tuner.
• VOBLA: VOBLA-to-PENCIL frontend and BLAS implementation in VOBLA.
• Benchmarks:
  • A set of PENCIL benchmarks covering image processing, the VOBLA DSL and NAS.
  • PENCIL linear algebra benchmarks.
• PENCIL compiler and benchmarks in the CK format.

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:

• PPCG, a parallel code generator
• Polly, an LLVM framework for high-level loop and data-locality optimizations; a developement version of Polly can use PPCG for automatic GPU code generation
• pet, a prototype PENCIL parser used by PPCG
• isl, a support library for polyhedral compilation
• barvinok, which contains iscc, an interactive environment for experimenting with polyhedral operations (in turn using isl and pet)

Videos

PENCIL and VOBLA

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.

Posters

Deliverables and reports

PENCIL Language Specification: Draft for Discussion (based on D3.2 and D3.5)

Project deliverables made available by the Consortium:

• D2.1: State-of-the-Art Survey
• D2.2A: Requirements Analysis
• D2.2B: Defect Survey
• D6.1: Verification of PENCIL
• D6.2: Static Verification of OpenCL
• D6.4: Update on verification of PENCIL, PENCIL-to-OpenCL transformations, and verification of OpenCL

Publications

• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU kernels. Peter Collingbourne, Alastair F. Donaldson, Jeroen Ketema, and Shaz Qadeer. In Proceedings of ESOP, to appear in March 2013.
• SMT-Based Bisimulation Minimisation of Markov Models. Christian Dehnert, Joost-Pieter Katoen, and David Parker. In Proceedings of VMCAI 2013, January 2013.
• Improved Loop Tiling Based on the Removal of Spurious False Dependences. Riyadh Baghdadi, Albert Cohen, Sven Verdoolaege, and Konrad Trifunovic. In Proceedings of HiPEAC, January 2013.
• Polyhedral Parallel Code Generation for CUDA. Sven Verdoolaege, Carlos Juega, Albert Cohen, Ignacio Gomez, Christian Tenllado, and Francky Catthoor. In Proceedings of HiPEAC, January 2013.
• Sub-polyhedral scheduling using (unit-)two-variable-per-inequality polyhedra. R. Upadrasta and A. Cohen. In Proceedings of POPL, January 2013.
• GPUVerify: a Verifier for GPU Kernels. Adam Betts, Nathan Chong, Alastair F. Donaldson, Shaz Qadeer, Paul Thomson. In Proceedings of OOPSLA 2012, October 2012.
• Operational Versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language. Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver. In QEST 2012, September 2012.
• Presentation of the CARP project. CARP consortium. HiPEAC 2012, Paris, January 2012