Dear all, The next talk in the IARCS Verification Seminar Series will be given by Alastair Donaldson, a Professor and Director of Research in the Department of Computing at Imperial College London. The talk is scheduled on Tuesday, March 4, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=Nzd2Zmc1bnNvN3ViMGtrbDloM2E3NW5ka2MgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/), and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: Taking Back Control: Formally Modelling a Compiler Intermediate Representation for GPU Computing Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting 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. 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.