(avec Viktor Vafeiadis, et Suresh Jagannathan, Jaroslav Sevcik, Peter Sewell)

A simple compiler optimisation for removing redundant memory fences in programs running on top of x86 multiprocessors turned out to be challenging to prove correct. In this talk, I will give a short overview of the challenges of the semantic design and verified compilation of high-level programming languages language above shared memory multiprocessors (focussing on x86 and Power/ARM), and will conclude by proving the fence optimisation correct by introducing a novel simulation technique.