Title: Taking Back Control: Formally Modelling a Compiler Intermediate Representation for GPU Computing

Speaker: Alastair Donaldson    (bio) (bio)

Alastair Donaldson is a Professor in the Department of Computing at Imperial College London where he is Director of Research and leads the Multicore Programming Group, investigating novel techniques and tool support for programming, testing and reasoning about highly parallel systems and their programming languages. He was Founder and Director of GraphicsFuzz Ltd., a start-up company specialising in metamorphic testing of graphics drivers, which was acquired by Google in 2018, after which he spent time working with Google as a software engineer and then as a Visiting Researcher. He was the recipient of the 2017 BCS Roger Needham Award and an EPSRC Early Career Fellowship, and has published more than 100 articles in the fields of programming languages, formal verification, software testing and parallel programming. Alastair was previously a Visiting Researcher at Microsoft Research Redmond, an EPSRC Postdoctoral Research Fellow at the University of Oxford and a Research Engineer at Codeplay Software Ltd. He holds a PhD from the University of Glasgow, and is a Fellow of the British Computer Society.

When: Tuesday, 04 March 2025 at 1900 hrs (IST)  

Meeting Details: Zoom link, ID: 891 6409 4870, Passcode: 082194

Abstract:
We will present our POPL 2023 work on using formal modelling and analysis techniques to understand and fix fundamental problems in the design of SPIR-V, a compiler intermediate representation that is widely-used in GPU computing. An innovation of SPIR-V is that it features special instructions that allow information about high level control flow constructs to be documented in its otherwise-unstructured basic block-based representation. The idea is that compilers can exploit this information to generate efficient GPU-specific machine code. However, the original definitions of these instructions and the rules that govern them were fraught with ambiguities, preventing users of SPIR-V from understanding their purpose and hindering their use by compiler developers. We used the Alloy modelling language and analysis tool to build an initial best-effort formal model of SPIR-V control flow, after which we iteratively refined the model by cross-checking it against official documentation, test suites and validation tools, consulting with experts in industry to resolve differences. Along the way we fixed numerous deficiencies in these test suites and validation tools, and ended up with agreement between our revised formal model and these other sources of truth about SPIR-V. We then rewrote relevant parts of the English language formal specification based on our rigorous formal model, and our changes to the language have been incorporated in the latest version of the SPIR-V specification. As an added bonus, we devised a novel technique for automated testing of SPIR-V compilers that uses our formal model to generate unusual control flow graphs which are then fleshed out into self-checking SPIR-V test cases. This led to the discovery of numerous bugs affecting open source and commercial SPIR-V compilers.