Alastair F. Donaldson (Ally) is a Professor in the Department of Computing at Imperial College London, where he leads the Multicore Programming Group. He is also a Visiting Researcher at Google. He was also Founder and Director of GraphicsFuzz, which was acquired by Google in 2018 (after which he spent some time as a Software Engineer in the Android Graphics Team at Google.) Read more.
Our paper, Randomised Testing of the Compiler for a Verification-Aware Programming Language, won Best Paper at the Industry track of ICST 2024! This is a collaboration between me and two outstanding MEng students, Dilan Sheth and Alex Usher at Imperial, and Jean-Baptiste Tristan at Amazon, and was supported by an Amazon Research Award.
Our paper, Validating Database System Isolation Level Implementations with Version Certificate Recovery, led by Jack Clark, won a Best Paper award at EuroSys 2024 in Athens!
I am delighted to be selected as one of the recipients of an Amazon Research Award on Validating Compilers for the Dafny Verified Programming Language, following on last year’s Amazon Research Award on DafnyDefender: automated testing for the Dafny ecosystem.
We will be presenting three papers at the upcoming ISSTA conference in Seattle!
GrayC: Greybox Fuzzing of Compilers and Analysers for C is about a new technique and tool for finding (crash) bugs in compilers and analysers for the C programming language, by performing coverage-guided fuzzing using custom mutators tailored specially for C. It is joint with Karine Even-Mendoza (former Imperial postdoc, now faculty at King’s College London), Arindam Sharma (Imperial PhD student) and Cristian Cadar.
RustSmith: Random Differential Compiler Testing for Rust is a
tool demonstration paper about the first (to our knowledge) tool aimed
at differential testing of Rust compilers. It seems that the official
Rust compiler, rustc, is pretty reliable: RustSmith did not find any
new bugs, though the tool was able to find a number of (new to us)
historical bugs, and provide some coverage improvements. This is based
on the excellent MEng thesis work of Mayank Sharma, and is also a
collaboration with Imperial PhD student Pingshi Yu.
Grammar Mutation for Testing Input Parsers presents a new technique for grammar-based fuzzing that involve mutating the grammar itself to generate weird - but not too weird - inputs. It is a “registered report”, which means that it sets out a plan for a large experimental campaign (yet to be run) to evaluate the idea. This idea and plan will be presented at the FUZZING workshop. The work is led by Bachir Bendrissou (Imperial PhD student) and is joint with Cristian Cadar.
Delighted that a new paper, Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs, will appear at PLDI 2023. This is joint work with former masters students Bastien Lecoeur and Hasan Mohsin. I’m very fortunate to get to work with such talented students at Imperial!
The paper focuses on the problem of what to do about programming language undefined behaviour when deploying random differential testing and test case reduction to find compiler bugs.
This paper is close to my heart and has been a bit of a labour of love - rejected from PLDI 2022 and FSE 2022 (but with very useful reviewer feedback). I hope people find it interesting.
Happy New Year everybody! Having not posted any news for a while, here is a summary of some of the exciting things that have been happening since June!
New PhD students: Bachir Bendrissou and Pingshi Yu joined the group as PhD students (with Bachir being co-supervised by Cristian Cadar)
New postdoc: Chengsong Tan has joined the group as a postdoc on the IRIS project, working under my and John Wickerson‘s guidance
Dan Iorga passed his viva: Dan Iorga (co-supervised with John Wickerson) successfully defended his PhD thesis, “Memory Models for Heterogeneous Systems”, in November - congratulations Dan!
Inaugural Lecture: I gave my Inaugural Lecture, “My Plan B” - check it out on YouTube!
Most Influential Paper award: Our paper on GPUVerify from 2012 won the Most Influential Paper award at OOPSLA 2022! At time of writing the only evidence for this claim comes from Twitter, but the announcement should make it here in due course.
Paper at POPL 2023: We have had a paper, “Taking Back Control in an Intermediate Language for GPU Computing”, accepted at POPL 2023 - check it out! The paper is about using formal modelling techniques to improve the SPIR-V programming language - see this tweet summary. Joint work with Vasileios Klimis, Jack Clark and John Wickerson at Imperial, and our collaborators Alan Baker and David Neto at Google.
Paper at ICST 2023 Industry Track: During 2021 and 2022 I spent time as a Visiting Researcher at Google working on compiler testing techniques for the WebGPU and SPIR-V shading languages. We have had a paper, “Industrial Deployment of Compiler Fuzzing Techniques for Two GPU Shading Languages”, describing this experience accepted at the industry track of the ICST 2023 conference. The work features contributions from two excellent former Imperial undergraduates, Hasan Mohsin and Hana Watson, as well as Vasyl Teliman, an independent contributor based in Ukraine, and Ben Clayton, Ryan Harrison and David Neto at Google. Draft available soon!
Paper at CC 2023: George Mitenkov, formerly an undergrad at Imperial, did an excellent BEng project jointly with members of the Blue Brain team at EPFL, on generating efficient vector and GPU code from the NMODL domain specific language using LLVM IR. We have just had a paper on this work, entitled “MOD2IR: High-Performance Code Generation for a Biophysically Detailed Neuronal Simulation DSL”, accepted at the CC 2023 conference - this is joint work with George Mitenkov, Ioannis Magkanaris, Omar Awile, Pramod Kumbhar and Felix Schürmann. Draft available soon!
Looking forward to an exciting year ahead!
It’s wonderful to be back at an in-person conference - PLDI’22 in San Diego. Dan Iorga will present last year’s OOPSLA paper on CPU/FPGA memory models. I enjoyed participating in the Student Research Competition as a judge, and am looking forward to the Steering Committee meeting.
Who checks the checkers? Automatically finding bugs in C-to-RTL formal equivalence checkers
Michalis Pardalos, Alastair F. Donaldson, Emiliano Morini, Laura Pozzi, John Wickerson
Proceedings of Design and Verification Conference Europe (DVCon Europe 2024)
Randomised Testing of the Compiler for a Verification-Aware Programming Language
Alastair F. Donaldson, Dilan Sheth, Jean-Baptiste Tristan, Alex Usher
IEEE International Conference on Software Testing, Verification and Validation (ICST'24)
Validating Database System Isolation Level Implementations with Version Certificate Recovery
Jack Clark, Alastair F. Donaldson, John Wickerson, Manuel Rigger
Proceedings of the 19th European Conference on Computer Systems (EuroSys'24)
Challenges in Empirically Testing Memory Persistency Models
Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis, John Wickerson, Azalea Raad
Proceedings of the 2024 ACM/IEEE 44th International Conference on Software Engineering: New Ideas and Emerging Results
Synchronisation in Language-level Symmetry Reduction for Probabilistic Model Checking
Ivaylo Valkov, Alastair F. Donaldson, Alice Miller
30th International Symposium on Model Checking of Software (SPIN'23)