Tweets by@bcs_apsg
Please disable the ad-blocker in your browser to view the APSG Twitter newsfeed.
Date & Time | : | Thursday 10 May 2018, 6.00pm - 9.30pm |
Venue | : | BCS, 1st Floor, The Davidson Building, 5 Southampton Street, London, WC2E 7HA (View on Google Maps) |
Speaker | : | Dr Alastair Donaldson |
Compilers are among the infrastructure on which we most critically depend, yet production compilers are beyond the scope of formal verification. Testing compilers is hindered by the lack of a reliable "test oracle": for well defined yet complex languages it is possible in principle to have a golden reference compiler against which other compilers could be compared, but such a reference compiler rarely exists in practice. Furthermore, many programming languages are under-specified, permitting a high degree of implementation flexibility meaning that a reference compiler to be used as a test oracle cannot exist even in theory.
We have been investigating methods for testing compilers for the OpenGL shading language, GLSL, a language that exhibits a high degree of under-specification with regard to floating-point operations, making the oracle problem particularly hard. Our approach to testing GLSL compilers is to use "metamorphic testing", whereby a compiler is cross-checked against itself using families of semantically equivalent graphics shader programs. For each shader in a family, an OpenGL implementation should render a very similar image, such that outlier images (as judged by an appropriate image differencing metric) highlight compiler bugs.
I will give an overview of this approach, with examples of some of the functional and security-critical bugs that our approach has shed light on. I will also speculate on the potential for metamorphic testing to aid in analysing other systems that are fundamentally hard to test, arising in machine learning and computer vision, for example.
Alastair Donaldson is a Reader and EPSRC Early Career Fellow in the Department of Computing, Imperial College London, where he leads the Multicore Programming Group. He is the recipient of the 2017 BCS Roger Needham Award for his research into many-core programming. He has published more than 70 peer-reviewed papers on programming languages, formal verification, software testing and parallel programming, and leads the GPUVerify project on automatic verification of GPU kernels - a collaboration with Microsoft Research - and the GLFuzz project on automated testing for graphics shader compilers. Alastair coordinated the FP7 project CARP: Correct and Efficient Accelerator Programming, which completed successfully in 2015. Before joining Imperial, Alastair was 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.