Alastair F. Donaldson / Multicore Programming Group
Department of Computing, Imperial College London
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.
Frank Busse, Pritam Gharat, Cristian Cadar and I have had an experience paper accepted at ISSTA 2022 on various attempts to combine static analysis and dynamic symbolic execution.
The paper actually reports a couple of negative results: the static analysers we investigated are not able to find real-world bugs in the kinds of applications we were able to apply the KLEE tool to, and on a large set of synthetic bugs we found that equipping KLEE with information from candidate error traces reported by static analysers did not actually help much in accelerating KLEE’s progress towards the bug. I was pleased that the ISSTA reviewers were receptive to the idea of publishing these negative results, which we hope will provide inspiration for future work.
I took a bit of a break from PC service after serving as PC chair for ECOOP 2019 and general chair for PLDI 2020, and while I was only part time in academia. But now, it is my honour to have recently served on, or be due to serve on, some exciting program committees, including ECOOP 2022, CAV 2022, ASE 2022 and POPL 2023.
We have had two papers conditionally accepted at OOPSLA 2021, which I’m very much hoping to be able to attend in person in October.
“The semantics of shared memory in Intel CPU/FPGA systems” was led by
PhD student Dan Iorga, and is a collaboration with John Wickerson,
Tyler Sorensen and myself. In this paper we study the memory model of
a recent combined CPU/FPGA system from Intel, presenting operational
and axoimatic versions of the memory model, and show how formal
specification and tools can be used to reason about and generate
litmus tests. Check out John’s blog post about the paper!
“Specifying and testing GPU workgroup progress models” was led by Tyler Sorensen, and is a collaboration with former Princeton undergraduates Lucas Salvador and Harmit Raval, Hugues Evrard at Google, myself and John Wickerson at Imperial, and Margaret Martonosi at Princeton. Rather like the CPU/FPGA paper, we also apply formal specification and tooling, but this time to the domain of GPU execution models, allowing a variety of GPU schedulers to be described at a high level of abstraction using process algebra, using model checking to determine whether particular execution model litmus tests are guaranteed to terminate with respect to a given progress model, and using the Alloy tool to synthesise execution model conformance tests.
Drafts available after we make changes requested by the reviewers.
11 months ago
PLDI 2021 song (May 2021)
Check out this song, “Pure Implementation”, based on the music of “Pure Imagination” but with new lyrics by John Wickerson, arrangements and production by me, and contributions from many members of the PL community, to help promote the upcoming PLDI 2021 conference: