April 1 – 4 , 2013, Dagstuhl Seminar 13142

Correct and Efficient Accelerator Programming


Albert Cohen (ENS – Paris, FR)
Alastair F. Donaldson (Imperial College London, GB)
Marieke Huisman (University of Twente, NL)
Joost-Pieter Katoen (RWTH Aachen, DE)

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 3, Issue 4 Dagstuhl Report
Aims & Scope
List of Participants


In recent years, massively parallel accelerator processors, primarily GPUs, have become widely available to end-users. Accelerators offer tremendous compute power at a low cost, and tasks such as media processing, simulation and eye-tracking can be accelerated to beat CPU performance by orders of magnitude. Performance is gained in energy efficiency and execution speed, allowing intensive media processing software to run in low-power consumer devices. Accelerators present a serious challenge for software developers. A system may contain one or more of the plethora of accelerators on the market, with many more products anticipated in the immediate future. Applications must exhibit portable correctness, operating correctly on any configuration of accelerators, and portable performance, exploiting processing power and energy efficiency offered by a wide range of devices.

The seminar focussed on the following areas:

  • 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 system-independent and system-specific accelerator programs both qualitatively and quantitatively.

The seminar featured five tutorials providing an overview of the landscape of accelerator programming:

  • Architecture -- Anton Lokhmotov, ARM
  • Programming models -- Lee Howes, AMD
  • Compilation techniques -- Sebastian Hack, Saarland University
  • Verification - Ganesh Gopalakrishnan, University of Utah
  • Memory models -- Jade Alglave, University College London

In addition, there were short presentations from 12 participants describing recent results or work-in-progress in these areas, and two discussion sessions:

  • Domain specific languages for accelerators;
  • Verification techniques for GPU-accelerated software.

Due to the "correctness" aspect of this seminar, there was significant overlap of interest with a full week seminar on Formal Verification of Distributed Algorithms running in parallel. To take advantage of this overlap a joint session was organised, featuring a talk on verification of GPU kernels by Alastair Donaldson, Imperial College London (on behalf of the Correct and Efficient Accelerator Programming seminar) and a talk on GPU-accelerated runtime verification by Borzoo Bonakdarpour, University of Waterloo, on behalf of the Formal Verification of Distributed Algorithms seminar.

Summary text license
  Creative Commons BY 3.0 Unported license
  Albert Cohen, Alastair F. Donaldson, Marieke Huisman, and Joost-Pieter Katoen


  • Hardware
  • Programming Languages / Compiler
  • Semantics / Formal Methods


  • Intermediate languages
  • Multi-core programming
  • Polyhedral compilation
  • Portability
  • Formal verification
  • Correctness
  • Efficiency


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.