arm

Title:
Téléchat: Testing Compiler Correctness with Memory Models

Speaker:
Luke Geeson

Abstract:
Open source compilers are broken, and that means your programs are broken too.
Compiler Correctness must account for the memory model in the source and target. This isn't simple however as we must account for interpretations of language standards, the effects of optimizations, and requirements of the architecture. We should not leave this work to interpretation, yet there is no tool that can automatically check correctness of C++ compilers with respect to memory models.

In this talk, we shall look at one way we test our compilers with respect to our formal memory models. We propose the Téléchat tool to check whether compiler translation preserves concurrent program semantics over the source and target memory models. On the way, you will learn about about the standards you should consider when writing code in either C, C++, or Arm assembly. You'll discover the kinds of behaviors you should expect from your concurrent C programs, and how that translates into Arm code.

Speaker's Bio:
Luke is a Compiler Engineer in the open source LLVM & Arm Compiler Team. He has worked in Arm Research on formal verifying processor specifications, and in the Arm Architecture team on formalizing relaxed memory. His interests are in all things programming languages, verification, and the use of functional programming to solve real problems. He previously graduated with an MSc in Computer Science from Oxford, and a BSc Computer Science from Nottingham.