Alastair F. Donaldson
NEW: I am recruiting two PhD students to work on device driver verification and synthesis.
NEW: Videos about GPUVerify
I'm currently on the PC for:
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:
- Video 1: Introduction and overview
- Video 2: Verification method
- Video 3: Predicated execution and invariant inference
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.
- November 2011-: Lecturer, Department of Computing, Imperial College London
- August-September 2011: Visiting Researcher, RiSE Group, Microsoft Research Redmond
- January 2010-August 2011: Research Fellow, Wolfson College Oxford
- May 2009-August 2011: EPSRC Postdoctoral Research Fellow, Department of Computer Science, University of Oxford, working in the Formal Verification Group, led by Daniel Kroening
- January 2007-May 2009: Research Engineer at Codeplay Software Ltd.
- July-September 2005: Summer intern, Graham Technology
- October 2003-June 2007: PhD in Computing Science, Department (now School) of Computing Science, University of Glasgow, supervised by Alice Miller
- June-September 2002: Summer intern, Reuters Plc.
- October 1999-July 2003: BSc (hons, First Class) in Computing Science and Mathematics (combined), University of Glasgow
The design of this website has been borrowed, with permission, from Daniel Kroening.