CARP: Correct and Efficient Accelerator Programming

News from the CARP project

December 2014

  • 19/20 December 2014: Polly/isl workshop in Zurich
    The CARP ENS team are involved in running a two day workshop which brings together CARP researchers and LLVM/Polly developers to learn about each other's work, to enable the transfer of CARP technology into the LLVM compiler infrastructure project.
  • 1 December 2014: Marieke Huisman is awarded the Prof. de Winter Prize
    Marieke Huisman, who leads the CARP team at the University of Twente, has been jointly awarded the Prof. de Winter Prize; see here for details (in Dutch)
  • November 2014

  • 29 November 2014: CARP work presented at INVEST workshop
    A recent workshop, INVEST, introducing verification and testing to early stage researchers, featured presentations on the GPUVerify project from CARP.
  • 27 November 2014: PollyComp Tutorial announced
    Sven Verdoolage and Tobias Grosser will give a tutorial on Polyhedral Compilation at the HiPEAC 2015 conference in Amsterdam, on 20 January 2015.
  • 21 November 2014: OpenCL verification paper from UT
    A paper on Specification and verification of GPGPU programs from the University of Twente team has appeared in Science of Computer Programming. Check it out!
  • 10 November 2014: PENCIL benchmark implementations published
    To demonstrate PENCIL in action, ARM have released PENCIL implementations of six SHOC and Rodinia benchmarks. They are available at
  • 6 November 2014: Five orders of magnitude speed-up for probabilistic counterexample generation
    The CARP team at RWTH Aachen and their collaborators presented, at ATVA'14 in Sydney, new technique based on MaxSat to obtain a minimal PRISM model that characterizes a counterexample for probabilistic models. This approach achieves a speed-up of about five orders of magnitude over competing techniques. Check out the paper.
  • October 2014

  • 30 October 2014: Nathan Chong successfully defends PhD thesis
    Nathan Chong has defended his PhD thesis, Scalable Verification Techniques for Data-Parallel Programs. Nathan was a key contributor to the GPUVerify project, which is part of CARP.
  • 21 October 2014: Tobias Grosser PhD defense, and Polyhedral Compilation for the Masses
    Congratulations to Tobias Grosser on defending his PhD thesis, on the topic of A Decoupled Approach to High-Level Loop Optimization. The code generation ideas discussed in his thesis form an important part of the PPCG optimizer.
    The defense coincided with a mini-workshop on Polyhedral Compilation for the Masses, bringing together researchers in parallelizing compilation, polyhedral algorithms, scientific computing on GPUs, and formal methods for signal-processing and control systems.
  • 20 October 2014: PENCIL paper at DSLDI
    The CARP project had a paper on the PENCIL language at the Domain-Specific Language Design and Implementation workshop at SPLASH.
  • September 2014

  • 4 September 2014: Verifying Gigantic Markov Models
    Joost-Pieter Katoen gave a keynote talk at the 12th International Conference on Software Engineering and Formal Methods (SEFM) on the application of model checking to gigantic Markov models.
  • August 2014

  • 11 August 2014: Realeyes C++ Grandmaster
    Robert David from the CARP Realeyes team has achieved the C++ Grand Master title: a software development proficiency challenge that only very few most rigorous, dedicated and brave engineers are able to attain. Among thousands accepting the challenge Robert David is one of only 24 who successfully completed it this year. Check out his certificate!
  • 1 August 2014: EmotionBooth on Android
    The CARP Realeyes team have completed engineering work to make EmotionBooth platform independent, allowing creation of the first Android version of emotion tracking software.
  • July 2014

  • 22-24 July 2014: CARP papers at ICGT
    Two CARP papers have been presented at ICGT, the main conference on graph transformation techniques: on the connection between separation logic and graph grammars, as well as an inter-procedural dataflow analysis to automatically derive procedure contracts.
  • June 2014

  • 30 June 2014: Nathan Chong wins UK ICT Pioneers award
    Imperial PhD student Nathan Chong won the Technology Everywhere category at the 2014 UK ICT Pioneers award, for his contributions to GPUVerify. Nathan was also selected as overall winner of the competition! See here for the full story.
  • 25 June 2014: Funding for research on automatic detection of concurrency exploits
    The Imperial team have been awarded funding from GCHQ for a PhD studentship on the topic of automatic detection of concurrency exploits in systems software. This is through their Academic Centres for Excellence in Cyber Security Research (ACEs CSR) programme.
  • 16-20 June 2014: Survey on Probabilistic Counterexample Generation
    An extensive survey paper from the RWTHA Aachen CARP team on Counterexample Generation for Discrete-Time Markov Models has been presented at the SFM Summer School in Bertinoro. Check it out.
  • 15 June 2014: Realeyes Emotion Mirror at Cannes Lions 2014
    Realeyes have started a new dissemination project called EmotionMirror, based on EmotionBooth, but modified to run in a huge 190x150 cm mirror. The idea of the mirror is to overlay emotion readings on to the reflection in the mirror. The mirror was presented at the Cannes Lions 2014 conference, the biggest annual event in the world of creative design, marketing and advertising.
  • 13 June 2014: CARP paper at LCTES
    The CARP ARM team presented a paper entitled VOBLA: A Vehicle for Optimized Basic Linear Algebra presented at the LCTES 2014 conference. The paper demonstrates the use of PENCIL as compilation target for the VOBLA linear algebra DSL.
  • May 2014

  • 30 May 2014: Realeyes validation OpenCL and PENCIL validation benchmarks complete
    Realeyes have completed the implementation of a key CARP validation benchmark in the OpenCL and PENCIL languages, an important milestone for CARP.
  • 8 May 2014: Termination analysis for GPU kernels
    Jeroen Ketema and Alastair Donaldson from the CARP Imperial team have had a paper on automatically proving termination of GPU kernels accepted at the Workshop on Termination, which will be co-located with CAV 2014 and the Vienna Summer of Logic.
  • April 2014

  • 18 April 2014: GPUVerify paper accepted at CAV
    A paper from the Imperial team on Engineering a Static Verification Tool for GPU Kernels, has been accepted at CAV'14, the main conference on Computer-Aided Verification.
  • 1 April 2014: Realeyes win I-COM Big Data Venture Challenge
    Realeyes are winners of the I-COM Big Data Venture Challenge, a global competition showcasing top startups offering data and measurement services in digital marketing industry, where Realeyes's emotion measurement solution has received highest marks both from the audience and the final jury. Check it out!
  • March 2014

  • 11 March 2014: Paper accepted at IWOCL
    Ethel Bardsley, John Wickerson and Alastair Donaldson" have had a paper accepted at the International Workshop on OpenCL on KernelInterceptor, an extension to the GPUVerify tool for automatically intercepting kernel invocations at runtime to allow static verification of race-freedom to be applied to each dynamic instance. The paper, KernelInterceptor: automating GPU kernel verification by intercepting and generalising kernel parameters will be presented by Ethel.
  • February 2014

  • 18 February 2014: Best Student Paper Award at PPoPP
    A paper from the Imperial CARP team, Concurrency Testing Using Schedule Bounding: an Empirical Study, received Best Student Paper Award at this year's PPoPP conference. The empirical study was led and presented by PhD student Paul Thomson. The work attempts to validate claims made in prior research on systematic concurrency testing using a large, publicly available set of benchmarks. The benchmark set, SCTBench, and the results of the study, are publicly available.
  • 14 February 2014: Year 2 review success in Brussels
    We presented the CARP project to the European Commission and reviewers in Brussels, demonstrating the VOBLA->PENCIL->OpenCL tool chain running on both AMD and ARM Mali GPUs (the latter using a Chromebook), showing GPUVerify in action on GPU kernels from ARM through the rise4fun interface, and presenting prototype results related to Codeplay's new RenderScript analysis technology. The project was given three green lights, for dissemination and use, technical progress, and management.
  • 10 February 2014: Open source PENCIL and VOBLA tools
    ARM have released their tool chains associated with the PENCIL intermediate language and the VOBLA linear algebra DSL publicly available as open source.
  • 7 February 2014: CAV submission with cool plots
    The Imperial team have submitted a tooling and engineering paper on GPUVerify to the CAV'14 conference. The paper features an experimental evaluation over more than 500 GPU kernels using both the Z3 and CVC4 constraint solvers, evaluating GPUVerify at five different optimisation levels. Due to the severe limitations of paper for presenting this sort of data, Nathan Chong has created an interactive web page plotting the results of our study. Check it out.
  • January 2014

  • 28 January 2014: CARP verification work at POPL 2014 in San Diego
    Nathan Chong, Jeroen Ketema and Ethel Bardsley from Imperial College London have busy presenting our verification activities at the POPL 2014 conference in San Diego:
  • 28 January 2014: CARP at HiPEAC 2014 in Vienna
    CARP was well represented at the HiPEAC 2014 conference last week:
  • 23-24 January 2014: Full project meeting in Twente
    We held a very successful 5th full CARP project meeting, hosted by Marieke Huisman at the University of Twente.
  • 20 January 2014: Sven Verdoolaege co-organizes IMPACT workshop
    Sven Verdoolaege co-organizes the fourth edition of the IMPACT 2014 workshop. 9 out of 12 submitted papers have been accepted.
  • 20 January 2014: CARP paper at IMPACT
    ENS had a paper titled Schedule Trees presented at IMPACT 2014. Schedule trees form a natural and convenient representation of the schedules constructed for transforming PENCIL code to CUDA or OpenCL code.
  • December 2013

  • 23 December 2013: Journal paper on semantics for probabilistic programs
    A journal version of the RWTH Aaachen team's paper Operational versus weakest pre-expectation semantics for the probabilistic guarded command language has been accepted for the journal Performance Evaluation
  • 20 December 2013: Welcoming new CARP partner, Codeplay Software Ltd.
    We are delighted to welcome a new partner, Codeplay Software Ltd., who are joining the consortium to work on techniques for analysis and optimization of RenderScript. Codeplay are internationally recognized experts in advanced optimizing technologies, compilers and programmable graphics, and have been providing acceleration solutions that optimize performance for graphics semiconductor designers and AAA game developers since 1999.
  • 20 December 2013: Presentation for LLVM FOSDEM devroom accepted
    Tobias Grosser will present Polly, our polyhedral compilation framework for LLVM in the LLVM devroom at FOSDEM 2014. Polly uses the same polyhedral infrastructure as our research prototype PPCG and will facilitate technology transfer both to industry but also into other open source projects (e.g. Julia)
  • 19 December 2013: GPUVerify tutorials at UKMAC, HiPEAC and POPL.
    Alastair Donaldson presented GPUVerify at the UKMAC 2013 conference in Oxford this week. In January, Nathan Chong and Jeroen Ketema are running a tutorial on verification and semantics for GPU kernels at POPL in San Diego, while John Wickerson and Dan Liew are running the Formal Analysis Techniques for GPU Kernels (FAT-GPU) tutorial at HiPEAC in Vienna.
  • 15 December 2013: Tobias Grosser co-organizes the European LLVM conference 2014
    Tobias Grosser co-organizes the European LLVM Conference 2014, taking place 7/8 April 2014 in Edinburgh, Scotland. We expect over 200 participantes, many using LLVM in their products and research. The LLVM compiler infrastructure is an important part of the CARP research prototypes and also in the products of our industry partners.
  • 11 December 2013: HiPEAC Technology Transfer Award.
    The CARP team at Imperial College London have received a HiPEAC technology transfer award in recognition of their ongoing tech transfer of GPUVerify to ARM, which is also supported by CARP.
  • 10 December 2013: CARP paper at HiStencils 2014
    ENS had a paper titled The relation between diamond tiling and hexagonal tiling has been accepted at the HiStencils 2014 workshop taking place 21 January 2014 in Viena, Austria.
  • 1 December 2013: CARP enters its third year.
    December 2013 marks the third and final year of the CARP project! We anticipate an exciting final year of work.
  • November 2013

  • 27 November 2013: Tobias Grosser co-organizes LLVM FOSDEM developer room
    Tobias Grosser co-organizes the LLVM FOSDEM devroom. The LLVM workshop at FOSDEM 2014 gives LLVM developers and the open source community a platform to interact and discuss.
  • 25-27 November 2013: CARP poster presentation at the Google PhD Student Summit 2013, Munich
    Tobias Grosser presented a poster titled "Hybrid Hexagonal/Classical Tiling for GPUs" at the Google PhD student summit, a meeting of over 50 PhD students working in the area of compilation. This poster presents our work on domain specific optimizations for stencil computations on accelerators.
  • 20 November 2013: Presentation at Supercomputing 2013 LLVM BOF
    Tobias Grosser has been invited to give a presentation of Polly at the LLVM BoF at Supercombuting 2013. The presentation was given by P. Sadayappan.
  • 18 November 2013: CARP presentation at Compiler, Architecture and Tools Conference
    Tobias Grosser gave a presentation titled "
  • 7 November 2013: CARP paper at CGO 2014
    Our work titled Hybrid Hexagonal/Classical Tiling for GPUs has been accepted at the International Symposium on Code Generation and Optimization in Orlando, Florida.
  • 7 November 2013: Tobias Grosser leads Polly BoF at LLVM conference 2013
    Tobias Grosser leads the BoF session on Polly, our polyhedral compiler for LLVM, at the LLVM conference 2013.
  • October 2013

  • 3 October 2013: Javed Absar presents CARP at PP4EE
    Javed Absar presented the CARP project at the Parallel Processing for Energy Efficiency (PP4EE) seminar at NNTU.
  • 1 October 2013: RWTH Aachen University selects Joost-Pieter Katoen as Distinguished Professor
    RWTH Aachen University have selected Joost-Pieter Katoen, leader of the CARP team at Aachen, as Distinguished Professor. This will boost the research activities on probabilistic programs as started during CARP.
  • 1 October 2013: CARP paper at POPL
    We have had a paper entitled "A Sound and Complete Abstraction for Reasoning About Parallel Prefix Sums" accepted at POPL 2014. In this work we show how to verify functional correctness of GPU kernel implementations of prefix sums by establishing data race-freedom (in our case using GPUVerify, but in principle using any capable tool) and then running a single test case using a novel abstract domain.
  • September 2013

  • 20 September 2013: ARM Arndale developer board
    These days we are doing some very hands-on work with the Mali GPU series, thanks to the gift of an Arndale developer board from ARM which Dan Liew has been having fun with:

    Arndale developer board Arndale developer board

  • 15 September 2013: Joost-Pieter Katoen elected as member of Academia Europaea
    Prof Joost-Pieter Katoen, leader of the RWTH Aachen team in CARP, has been elected as a member of Academia Europaea, the European Academy of Science.
  • 10 September 2013: GPUVerify on rise4fun
    Thanks to Dan Liew's efforts, you can now try out the GPUVerify tool through Microsoft Research's rise4fun service.
  • 1 September 2013: CARP partner Monoidics acquired by Facebook
    Our parnter Monoidics are leaving the consortium as their technology for verification of complex heap-manipulating programs has been acquired by Facebook. We wish the Monoidics team all the best in their new endeavour at Facebook in London!
  • August 2013

  • 26 August 2013: CARP work presented at QEST 2013 during Buenos Aires Dependability Week
    Friedrich Gretz presented his latest version of the PRINSYS tool at the QEST conference, and Joost-Pieter Katoen gave an invited talk at CONCUR about random effects in concurrency.
  • 7 August 2013: Dagstuhl Report online
    The report from our Dagstuhl seminar on Correct and Efficient Accelerator Programming is now available online. Many thanks to Jeroen Ketema for leading the collection of articles for this report.
  • 1 August 2013: Updated CARP Fact Sheet
    Check out our updated Fact Sheet for the CARP project. This gives an overview of CARP, and summarises a selection of mid-project results.
  • July 2013

  • 30 July 2013: CARP paper accepted at OOPSLA 2013
    The Imperial College CARP team, in collaboration with Shaz Qadeer at Microsoft Research, have had a paper accepted at the OOPSLA conference, part of SPLASH 2013. The paper is about barrier invariants, a shared state abstraction which makes it possible to reason about data-dependent GPU kernels. The GPUVerify tool underlying this work was also reviewed through the artifact evaluation process, new to OOPSLA this year, and gained their stamp of approval:

  • 26 July 2013: Public release of PPCG
    First public release of PPCG, a protoype polyhedral PENCIL compiler. This initial release only supports the generation of CUDA code. The next release will also support the generation of OpenCL code. PPCG is released under the MIT license.
  • 15 July 2013: Marieke Huisman receives Netherlands Prize for ICT Research
    Marieke Huisman, who is leading the CARP work going on at the University of Twente, is this year's recipient of the Netherlands Prize for ICT Research, in recognition of her and her team's work on reliability and correctness of concurrent software. Congratulations, Marieke!
  • June 2013

  • 24-25 June 2013: Full project meeting in Paris
    We held an exciting full project meeting at INRIA in Paris, hosted by Albert Cohen. This marks the mid-way point of the CARP project!
  • May 2013

  • 22 May 2013: GPU verification tutorial at LEAP conference
    Nathan Chong gave a tutorial about GPU kernel verification, demoing the GPUVerify tool, at the LEAP conference, which was very well received by both industral and academic attendees. See post by Simon McIntosh-Smith.
  • April 2013

  • 29-30 April 2013: ENS hosts the European LLVM conference 2013
    Tobias Grosser co-organized the European LLVM Conference 2013, a major open source conference with 180 participants many of them core contributors to LLVM. LLVM as a compiler infrastructure is widely used in industry and research. Most important for CARP, it is a core component of most industry OpenCL compilers and also an important infrastructure piece for the research prototypes we develop. The use of the same infrastructure components is essential to facilitate technology transfer.
  • 26 April 2013: Videos about GPUVerify
    Alastair Donaldson recently recorded some videos about GPUVerify, an analysis technique and tool for OpenCL and CUDA kernels being developed as part of CARP. Watch the videos on YouTube:

    Video 2: Verification method

    Video 3: Predicated execution and invariant inference

  • 1-5 April 2013: Dagstuhl seminar on Correct and Efficient Accelerator Programming
    This week we organised a seminar on Correct and Efficient Accelerator Programming at Dagstuhl, which featured presentations and discussions from world experts in this area, including several of the CARP partners. Here are the seminar participants (click on the image for a larger version):


  • March 2013

  • 27 March 2013: Paper accepted at ECRTS
    A paper on CARP work on worst case execution time analysis for GPU kernels has been accepted at the 25th Euromicro Conference on Real-Time Systems (ECRTS 2013). This work was led by Adam Betts at Imperial College London.
  • 17-23 March 2013: CARP work presented at ETAPS
    The week of this year's European Joint Conferences on Theory and Practice of Software (ETAPS 2013) featured two papers on CARP verification work: Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels at ESOP (led by Imperial), and Specification and Verification of GPGPU Programs Using Permission-based Separation Logic at BYTECODE (exciting new work from the University of Twente).
  • 16 March 2013: CARP work presented at GPGPU'13 workshop
    A CARP paper was presented at the 6th GPGPU workshop in Houston, Texas. The work introduces important adances in trapezoidal tiling for stencil codes and was led by Tobias Grosser from ENS.
  • February 2013

  • 1 February 2013: CARP First Review success
    We held our first annual review with the European Commission in Brussels, leading to the good news that the project should be allowed to continue without modifications.
  • January 2013

  • 30-31 January 2013: Project meeting in Aachen
    We had fun at our third full project meeting, hosted by Joost-Pieter Katoen's group at RWTH Aachen University, with talks from project partners on the latest CARP developments in compilation, verification and cost analysis techniques.
  • 28 January: CARP work presented at VMCAI 2013
    Christian Dehnert from the RWTH Aachen team presented his symbolic technique for reducing state spaces of probabilistic models at VMCAI 2013 in Rome, Italy.
  • 21 January 2013: CARP project at HiPEAC conference in Berlin
    During the HiPEAC conference this week, Coordinator Alastair Donaldson will give a tutorial, Formal Analysis for GPU Kernels, on the verification techniques being developed during CARP, and the team at ENS will present a poster on the PENCIL intermediate language during the HiPEAC EU projects day.
  • 14 January 2013: CARP work presented at Research School at ENS Lyon
    CARP Coordinator Alastair Donaldson is teaching at an École de Recherche on Semantics and Tools for Low-Level Concurrent Programming, at ENS Lyon, presenting techniques for analysing GPU kernels that have been developed during the project. The other speakers at the school are Francesco Zappa Nardelli (INRIA), Mark Batty (Univesity of Cambridge) and Martin Vechev (ETH Zurich).
  • December 2012

  • 5 December 2012: CARP overview presented
    Alexey Kravets (ARM) presented an overview of CARP activities at the 4th UK Many-core developer conference (UKMAC) in Bristol.
  • November 2012

  • 16 November 2012: Paper at WOLFHPC presented
    Riyadh Baghdadi presented a position paper on PENCIL, the Platform Neutral Compute Intermediate Language being developed as part of CARP at the WOLFHPC workshop. Check out the slides from his talk.
  • 15-16 November 2012: Verification work package meeting in the Netherlands
    CARP researchers from Imperial College London, Monoidics and RWTHA Aachen University joined collaborators at the University of Twente for a two day verification work package meeting, combined with a seminar on GPUVerify to the Formal Methods and Tools group.
  • October 2012

  • 23 October 2012: Paper at OOPSLA 2012 presented
    Alastair Donaldson presented a paper on GPUVerify, the verification and analysis tool for GPU kernels being developed as part of CARP, at the 2012 OOPSLA conference, part of SPLASH. Check out the paper.
  • 1 October 2012: Paper accepted at POPL 2013
    We're pleased to announce that "Sub-Polyhedral Scheduling Using (Unit-)Two-Variable-Per-Inequality Polyhedra" has been accepted for publication at the POPL 2013 conference to be held in Rome, Italy, in January.
  • August 2012

  • 2 August 2012: Paper accepted at RTSS 2012
    We're pleased to announce that "Reducing the Size of the Constraint Model in Implicit Path Enumeration using Super Blocks" has been accepted for publication at the RTSS 2012 conference to be held in San Juan, Puerto Rico, in December.
  • July 2012

  • 5-6 July 2012: Full project meeting in the UK
    July saw the CARP project's mid-year meeting, held at the offices of ARM in Cambridge. The two day event featured research presentations from project partners, and breakout sessions on intermediate languages, power modelling, polyhedral compilation, verification, cost analysis and applications.
  • 4 July 2012: Paper accepted at OOPSLA 2012
    We're pleased to announce that "GPUVerify: a Verifier for GPU Kernels" has been accepted for publication at the OOPSLA 2012 conference, which is part of the SPLASH symposium to be held in Tucson, Arizona, in October. The paper was led by Imperial College London (coordinators of CARP), and is joint with Shaz Qadeer at Microsoft Research, Redmond. The work also features collaboration among the CARP consortium, with ARM providing experimental results for the Mali architecture, and Rightware providing their Basemark CL benchmark for evaluation. Draft available soon from our publications page.
  • June 2012

  • 28 June 2012: CARP presentation in the Netherlands
    Marieke Huisman (University of Twente) will present the CARP project at the Platform Parallel Netherlands.
  • 12-13 June 2012: Verification work package meeting in London
    CARP researchers from Imperial College, University of Twente and Monoidics got together in London for a two day work package meeting on formal verification techniques for accelerator programming.
  • May 2012

  • 31 May 2012: CARP deliverable now available
    The first public CARP deliverable, a report surveying the state-of-the-art in accelerator programming, is now available from our dissemination page.
  • 29 May 2012: CARP project in the media
    The CARP project appears on HPCWire.
  • 16 May 2012: CARP project in the media
    CARP press release on ARM's website.
  • 10 May 2012: Prestigious award for CARP project member
    Dino Distefano (Monoidics) is the recipient of the 2012 Roger Needham award, for his contributions to the field of Software Verification.
  • January 2012

  • 25 January 2012: CARP presentation in France
    Imperial College London, ARM and ENS presented a poster on CARP at the HiPEAC 2012 conference in Paris.
  • December 2011

  • 8-9 December 2011: CARP begins
    Kick-off meeting at Imperial College, London, UK.

  • Project number 287767. Coordinator: Dr Alastair F. Donaldson,