Alastair F. Donaldson

Lecturer?

 		     

Leader of the Multicore Programming Group
Department of Computing
Imperial College London
180 Queen's Gate
London SW7 2BZ 		      Imperial College London logo

Office: 422    Phone: +44 (0)20 7594 8266
Email: alastairZZZ.donaldson@imperial.ac.uk [no ZZZ]

NEW: Videos about GPUVerify


More videos

I'm currently on the PC for:

News

Paper at OOPSLA 2013 (July 2013) Nathan Chong, Jeroen Ketema, Paul Kelly, Shaz Qadeer and I 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.

This year, OOPSLA featured an artifact evaluation process, separate for paper review, in which authors were invited to submit their tools to be tried out in detail by a committee of researchers. I think this is a great idea, something that more conferences should consider doing. The artifact evaluation committee, chaired by Matthias Hauswirth and Steve Blackburn, clearly put a great deal of effort into trying out our software. I'm pleased to say that our implementation in GPUVerify gained their stamp of approval:

Welcoming UROP student Ethel Bardsley (July 2013) Ethel Bardsley has just completed her MEng degree at Imperial, and will join the Multicore Programming Group for a 10 week placement under the Undergraduate Research Opportunities Programme (UROP), to work on GPUVerify.

New PhD student, Pantazis Deligiannis (July 2013) I'm very pleased to welcome Pantazis Deligiannis, who has joined the Multicore Programming Group to take up a PhD studentship funded by a gift from Intel Corporation.

Student Academic Choice Awards (May 2013) I was surprised and delighted to win the award for Best Teaching for Undergraduates at Imperial College's 2013 Student Academic Choice awards. More about the awards.

Videos about GPUVerify (April 2013) I recently recorded some videos about GPUVerify, an analysis technique and tool for OpenCL and CUDA kernels being developed as part of the CARP project. Watch the videos on YouTube:

Dagstuhl seminar on Correct and Efficient Accelerator Programming (April 2013) I have just returned from a Dagstuhl seminar on techniques for improved accelerator programming which I co-organised with Albert Cohen, Marieke Huisman and Joost-Pieter Katoen. The seminar ran in parallel with a seminar on Formal Verification of Distributed Algorithms, and there were some good synergies between the seminars.

Paper at ECRTS (March 2013) Adam Betts and I have had a paper on worst case execution time analysis for GPU kernels accepted at the 25th Euromicro Conference on Real Time Systems. Draft available soon!

Two PhD opportunities on new research project, Automatic Synthesis of High-Assurance Device Drivers, funded by Intel Corporation (March 2013) The Multicore Programming Group are soon to embark on an exciting new research project in collaboration with Gernot Heiser at NICTA, Leonid Ryzhyk and Michael Stumm at University of Toronto, and Pavol Cerny at University of Colorado Boulder. The project is funded by a generous gift from Intel Corporation and will focus on verification and synthesis techniques to aid in the development of high-assurance device drivers. We have funding for two PhD students to work on this at Imperial, and are currently recruiting. Advert for these positions with more details.

CARP project at HiPEAC conference in Berlin (January 2013) During the HiPEAC conference, I am giving a half-day tutorial on Formal Analysis Techniques for GPU Kernels, on the verification techniques being developed during the CARP project. The CARP team at ENS Paris will also present a poster on our PENCIL intermediate language during the HiPEAC EU projects day.

École de Recherche, ENS Lyon (January 2013) I have been 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 CARP project. Also speaking at the school were Francesco Zappa Nardelli (INRIA), Mark Batty (Univesity of Cambridge) and Martin Vechev (ETH Zurich).

New PhD student Dan Liew (January 2013) Dan Liew has jointed the Multicore Programming and Software Reliability groups to undertake a PhD, co-supervised by me and Cristian Cadar. His studentship is partly supported by ARM.

Paper on semantics of GPU kernels accepted at ESOP (December 2012) We have had a paper on the relationship between interleaving and lock-step semantics for GPU kernels, and applications of this relationship to formal verification, accepted at the ESOP 2013 conference. This is joint work with Peter Collingbourne, Jeroen Ketema and Shaz Qadeer. Check it out.

EPSRC Research project: Scalable Automatic Verification of GPU Kernels (October 2012) EPSRC have agreed to fund a one-year project continuing my research group's work on formal verification techniques for GPU kernels. During this project we plan to collaborate with a number of partners, including Shaz Qadeer at Microsoft Research, Redmond, Ganesh Gopalakrishnan at the University of Utah, and Peter Sewell at the University of Cambridge. The project will also involve further collaboration with ARM and Rightware, who are partners on CARP.

Paper on verification of message-based device drivers accepted at SSV (October 2012) A paper co-authored with collaborators at NICTA, Australia (principally Sidney Amani and Leonid Ryzhyk) has been accepted to the Systems Software Verification conference, which will take place in Sydney, Australia, during November. Draft available soon!

Position paper on PENCIL at WOLFHPC (October 2012) A position paper, co-authored by many members of the CARP project, has been accepted for presentation at the WOLFHPC workshop. The paper outlines the preliminary design of PENCIL, a new intermediate language for accelerator programming that we are designing as part of CARP. Draft available soon!

Industrial CASE PhD studentship sponsored by ARM (September 2012) ARM and EPSRC have generously agreed to fund a PhD studentship at Imperial to investigate techniques for improving the reliability of GPU software. The student will be co-supervised by me and Cristian Cadar, as the studentship spans the interests of the Multicore Programming and Software Reliability groups.

New course: Software Reliability (August 2012) Starting in October I will be teaching a new course for final year undergraduates at Imperial, entitled Software Reliability.

FAT-GPU tutorial at HiPEAC 2013 (August 2012) I'll present a half day tutorial on Formal Analysis Techniques for GPU Kernels (codename FAT-GPU) at the HiPEAC 2013 conference, January 2013. This will describe recent developments in this area arising from the CARP project, as well as techniques from the group of Prof Ganesh Gopalakrishnan at the University of Utah.

Paper on GPU verification accepted at OOPSLA (July 2012) Our paper on GPUVerify, a technique and tool for verifying race- and divergence-freedom of GPU kernels, has been accepted at the OOPSLA 2012 conference! This is joint work with Adam Betts, Nathan Chong and Paul Thomson at Imperial, and Shaz Qadeer at Microsoft Research. Check it out!

Welcoming UROP students Cassie Epps and Egor Kyshtymov (July 2012) Cassie Epps and Egor Kyshtymov, both Imperial undergraduates, are joining the Multicore Programming group for the summer through the Undergraduate Research Opportunities (UROP) scheme.

Older News

Short Bio

Acknowledgement

The design of this website has been borrowed, with permission, from Daniel Kroening.