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.
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 https://github.com/carpproject/benchmarks.
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.
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.
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.
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.
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.
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.
Anton also gave a talk at the 2nd Workshop on Transfer to Industry and Start-ups, highlighting how open-sourcing of research software under permissive licenses facilitates transfer to industry, exemplified by the CARP work on GPUVerify and polyhedral libraries
John also presented a poster about GPU memory models, a collaboration with UCL, Cambridge, and the University of Utah
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.
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.
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: 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.
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:
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.
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.
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:
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):
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, alastair.donaldson@imperial.ac.uk
