Alastair DonaldsonHome

I am a Senior Lecturer? (roughly equivalent to US Associate Professor) in Computing at Imperial College London.  More about me.

Current and recent service

Please consider submitting your work to these venues.


S-REPLS (May 2015) I attended and gave a talk at S-REPLS, the first South of England Regional Programming Languages Seminar, in Cambridge.  It was a really cool event, based on the successful Scottish Programming Languages Seminar series.  If you do PL research in the South of England, please consider S-REPLS mailing list.

PLDI artifact evaluation (April 2015)  The tools associated with our PLDI papers were accepted by the PLDI Artifact Evaluation Committee.  Check out the camera-ready versions of our Many-Core Compiler Fuzzing paper and our paper on Asynchronous Programming, Analysis and Testing with State Machines.

Intensive research project funded by GCHQ (February 2015) The Multicore Programming Group has been awarded a £36,000 grant from GCHQ to fund a seven week intensive project entitled Detecting Vulnerabilities in Compilers for a Massively Parallel Language, which will allow me and two members of my group to extend the OpenCL compiler testing work associated with our upcoming PLDI paper.

Two papers at PLDI (February 2015)  We are excited to have had two papers accepted at the 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI).

One paper, entitled Many-Core Compiler Fuzzing, is joint work with Christopher Lidbury, Andrei Lascu and Nathan Chong (current/former members of my research group) and is about the application of random differential testing and equivalence modulo inputs testing to find defects in OpenCL compilers.  We found a lot of compiler defects during this project.  Check out our CLsmith tool for generation of random OpenCL kernels.

The other paper, entitled Asynchronous Programming, Analysis and Testing with State Machines, is a collaboration with Pantazis Deligiannis, Jeroen Ketema and Paul Thomson at Imperial, and with Akash Lal at Microsoft Research.  The paper describes a new language, P#, for asynchronous programming, together with static and dynamic analysis techniques that leverage features of the new language for scalability.

Drafts of both available soon!

HiPEDS PhD studentship available, supported by Imagination Technologies (January 2015)  Imagination Technologies are sponsoring a PhD studentship at Imperial as part of the HiPEDS Centre for Doctoral Training.  The studentship will be supervised jointly by me (in the Department of Computing) and Prof George Constantinides (in the Department of Electrical and Electronic Engineering), and is on Hardware/Software Co-Optimisation of Concurrent Numerical SoftwareSee this description for details of the project and how to apply.

Paper at ASPLOS (January 2015) We just submitted the camera-ready version of a paper entitled GPU Concurrency: Weak Behaviours and Programming Assumptions which has been accepted at ASPLOS.  This is a collaboration with Jade Alglave at UCL/Microsoft Research, Tyler Sorensen at UCL (and previously at Utah), Daniel Poetzl at Oxford, Mark Batty at Cambridge, Ganesh Gopalakrishnan at Utah, and Jeroen Ketema and John Wickerson at Imperial.  A main contribution of the work is to empirically study the memory consistency of GPUs from Nvidia and AMD, showing that weak behaviours can be observed, and illustrating that these can make it difficult to correctly implement software that exploits fine-grained concurrency on GPUs.

Invited talk at JFLA (January 2015) I am excited to be on my way to The Vosges to gives an invited talk at Les vingt-sixièmes Journées Francophones des Langages Applicatifs. Unfortunately (or perhaps fortunately for the audience) I will not be delivering my talk in French!

CAV and POPL programme committees (December 2014) I’m honoured to have been invited to serve on the Programme Committees for CAV 2015 and POPL 2016.

INVEST workshop (November 2014) Cristian Cadar, Philippa Gardner and I ran a workshop, INVEST, on an introduction to verification and testing research, at Imperial.  The workshop was targeted at late stage undergrad/MSc students and early stage PhD students.

Nathan Chong gets his PhD (October 2014)  Congratulations to Nathan Chong, who successfully defended his PhD thesis at the end of October.  He was supervised jointly with Paul KellyGanesh Gopalakrishnan made the journey to Utah to act as external examiner, and George Constantinides from our neighbouring EEE department was internal examiner.  Well done Nathan!

Welcoming new research group members, Christopher Lidbury and Andrei Lascu (October 2014)  I am delighted that Christopher Lidbury has joined the Multicore Programming Group as a PhD student, and that Andrei Lascu will work with us over the coming months as a Research Assistant.  Chris and Andrei spent the summer working with our group under the Imperial Undergraduate Research Opportunities Programme (UROP).

Invited talk at AVoCS and tutorial article on GPUVerify (September 2014) I gave an invited talk at the AVoCS workshop, which was held at the University of Twente. For the proceedings, I wrote a tutorial overview of the GPUVerify method which you can check out here.

Nathan Chong wins UK ICT Pioneers award (June 2014)  My PhD student Nathan Chong won the Technology Everywhere category at the 2014 UK ICT Pioneers award, sponsored by EPSRC, for his contributions to GPUVerify.  Nathan was also selected as overall winner of the competition!  See here for the full story.

PhD studentship funded by GCHQ (June 2014)  I 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.  I’m looking for excellent candidates for this position.  As the project will involve spending some time on site at GCHQ, candidates must be British citizens, and will have to go through some level of security clearance.  Contact me if you fit the bill and are interested!

Paper on termination analysis for GPU kernels (May 2014) Jeroen Ketema and I 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.  Draft available soon!

Nathan Chong reaches finals of UK ICT Pioneers competition (May 2014)  My PhD student Nathan Chong, whom I co-supervise with Prof Paul Kelly, has reached the finals of the UK ICT Pioneers competitionSee here for our Departmental news item on this.   To get through to the final, Nathan made this popular science video about his work on GPUVerify.

Paper accepted at CAV (April 2014) Our paper, Engineering a Static Verification Tool for GPU Kernels, has been accepted at CAV’14.

Shortlisted for Best Innovation in Teaching award (April 2014) I am delighted to have been shortlisted for the Best Innovation category in the Imperial College Union Student Academic Choice Awards 2014.

Paper accepted at IWOCL (March 2014)  Ethel Bardsley, John Wickerson and I 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.

Best Student Paper Award at PPoPP (February 2014) Our paper, 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 my PhD student Paul Thomson, and co-authored with Adam Betts.  In the work we attempted to validate claims made in prior work on systematic concurrency testing using a large, publicly available set of benchmarks.  The benchmark set, SCTBench, and the results of our study, are publicly available.

GPUVerify tooling and engineering paper submitted to CAV (February 2014) We have submitted a paper to CAV’14 describing the engineering experience we’ve gained over the last 2.5 years working on GPUVerify.  In the paper we report experiments for a set of more than 500 GPU kernels, with two different SMT solvers and various optimisation levels.  A paper is so limiting in the data one can show, thus Nathan Chong knocked up what I think is a very cool web page that allows you to plot our data in various ways to answer questions that are not addressed in the paper itself.  Check out the draft paper and plots.

Paper accepted at NASA Formal Methods (January 2014) Ethel Bardsley and I have had a paper on our efforts to extend GPUVerify with support for reasoning about warps and atomics accepted to the NFM’14 conference.  The paper is entitled Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU Kernels.  This is the culmination of Ethel’s MEng project at Imperial and follow-up UROP placement with my group.

Invited speaker at AVoCS 2014 (December 2013) I’m delighted to have been asked to be one of the invited speakers at the 14th International Workshop on Automated Verification of Critical Systems (AVoCS’14).  For me this is very cool as one of my very first papers, 10 years ago, was at AVoCS’04.

Tutorials on GPU verification (December 2013 – January 2014) I 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.

HiPEAC Technology Transfer Award (December 2013) We were delighted to hear that we have received a HiPEAC technology transfer award in recognition of our ongoing tech transfer of GPUVerify to ARM, which is also supported by the CARP project.

SCTBench (December 2013) Paul Thomson has made available the benchmarks he painstakingly gathered and adapted for systematic concurrency testing as part of our PPoPP empirical study.  Check them out: SCTBench.  We hope they will be useful to other researchers interested in concurrency analysis.

Paper at PPoPP 2014 (November 2013) My PhD student Paul Thomson, in collaboration with me and Adam Betts, has had a paper entitled “Concurrency Testing Using Schedule Bounding: an Empirical Study” accepted at PPoPP 2014. In this work we used the Maple concurrency testing tool as a framework on which to empirically study techniques for systematic concurrency testing where schedule bounding is used to reduce schedule explosion. We collected a large set of concurrent program benchmarks and used these to empirically study two well-known schedule bounding techniques: preemption bounding and delay bounding. The paper reports on our experimental method and findings.

Intel Early Career Faculty Honor Program Award (October 2013) I was delighted to be selected as one of this year’s recipients of an Early Career Award from Intel Corporation, which I received at the Intel European Research and Innovation Conference in Nice (which was nice).

Paper at POPL 2014 (October 2013) Nathan Chong, Jeroen Ketema and I 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.

ARM Arndale developer board (September 2013) 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

GPUVerify on rise4fun (September 2013) Thanks to Dan Liew‘s efforts, you can now try out the GPUVerify tool through Microsoft Research’s rise4fun service.

PLDI 2014 External Review Committee (August 2013) I am honoured to have been invited to serve on the ERC for PLDI 2014.

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:

Older news



Delicious Twitter Digg this StumbleUpon Facebook