ubstantial research efforts have been devoted to tools for reasoning about -and proving properties of- programs. A related concern is making sure that compilers preserve the soundness of programs, that is making sure that the compiled code respects the behavior of the source program (see for instance the CompCert C compiler). This talk is about an attempt at proving the soundness of some basic low-level transformations for concurrent C programs. We will see some elements of the official semantics of concurrency in C, and I will relate how the focus of this work shifted from proving the soundness of program transformations to patching the official semantics.