Source-level debugging of compiled code only works when compilers generate the necessary metadata. Currently, that means it rarely works well, at least in optimising ahead-of-time compilers like LLVM and GCC. I'll give an overview of how compiler-generated metadata enables source-level debugging, the challenges of making it work for optimised code, and our recent work on doing better. Whereas compilers have so far taken a "best-effort" approach with no particular correctness criterion, I'll outline a correctness condition for local variable information that seems to balance the relevant trade-offs. I'll then describe a tool we've built that can use this to mechanically find valid LLVM bugs capturing avoidable losses or corruptions of debug info. A theme will be how the textbook framing of compiler optimisations as "eliminating" code or variables could be more constructively thought of as "residualising" them into debug info; I'll finish with some thoughts on what that could mean for how compilers are built. All this is joint work with J. Ryan Stinnett.

Bio: Stephen Kell does practical research on programming systems, with the the goal of making computers work for human beings and not vice-versa, and a focus on infrastructure software including operating systems and language runtimes. Some past and present research topics include: realistic formal and metaprogrammable specifications of operating systems' linking, loading and system call interfaces; reflective run-time services in Unix-like processes; using the latter to provide new kinds of dynamic checking in C and other 'unsafe' languages; and making debugging of optimized code more reliable. Currently he is a Lecturer (Assistant Professor) in Computer Science at King's College London. https://www.kcl.ac.uk/people/stephen-kell

Zoom: https://vuw.zoom.us/my/spgroom