CARP: Correct and Efficient Accelerator Programming

Christian Dehnert, Friedrich Gretz, Christina Jansen, Joost-Pieter Katoen

CARPMassively parallel accelerator processors, primarily graphics processing units (GPUs), have become widely available to end-users. Accelerators offer tremendous compute power at a low cost, and tasks such as media processing, medical imaging and eye-tracking can be accelerated to beat CPU performance by orders of magnitude, both in energy efficiency and execution speed. Despite these advantages, accelerators present a serious challenge for software development. Designing software for the diverse and growing range of platforms on the market is not feasible without better programming languages and tool support.

The aim of CARP is to design techniques and tools for correct and efficient accelerator programming:

  • Novel and attractive methods for constructing system-independent accelerator programs.
  • Advanced code generation techniques to produce highly optimised system-specific code from system-independent programs.
  • Scalable static techniques for analysing accelerator software both qualitatively and quantitatively.

These methods will provide a unified development flow for accelerated software, reducing cost and time-to-market quotas, increasing energy efficiency (and thus battery life in mobile devices) and improving reliability. With respect to key case studies, the CARP technology is anticipated to provide:

  • A performance increase of at least 4x when comparing optimised code with non-optimised code, on multiple platforms.
  • A reduction of at least 20% in energy consumption.
  • Automatic detection of at least 70% of known functional errors.
  • A reduction of several orders of magnitude in time taken to design an application to run efficiently across multiple accelerator platforms.

For further details, please see


DOIJonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Verifying Pointer Programs using Graph Grammars. Science of Computer Programming 97, pages 157–162, 2015.
DOIChristina Jansen, Thomas Noll. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs. Proc. 7th Int. Conf. on Graph Transformation (ICGT 2014), Volume 8571 of LNCS, pages 49–64, Springer, 2014.
DOIChristina Jansen, Florian Göbe, Thomas Noll. Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs. Proc. 7th Int. Conf. on Graph Transformation (ICGT 2014), Volume 8571 of LNCS, pages 65–80, Springer, 2014.
DownloadLinkChristian Dehnert, David Parker, Joost-Pieter Katoen. SMT-based Bisimulation Minimisation of Markov Models. 14th International Conference on Verification, Model Checking, and Abstract Interpretation, Volume 7737 of LNCS, pages 28–47, Springer, 2013.
LinkMarkus Bals, Christina Jansen, Thomas Noll. Incremental Construction of Greibach Normal Form for Context-Free Grammars. Proc. Int. Symp. on Theoretical Aspects of Software Engineering (TASE 2013), pages 165–168, IEEE Computer Society, 2013.