This talk presents a methodology for the verified compilation of high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory synchronization and automatic (concurrent) memory management.  Ensuring the correctness of compilers for these languages is challenging because high-level actions are translated into sequences of non-atomic actions with compiler-injected snippets of potentially racy code; the behavior of this code depends not only the actions of other threads, but also on out-of-order reorderings performed by the processor.  A naïve correctness proof of the compiler would require reasoning over all possible thread interleavings that can arise during execution, an impractical and non-scalable exercise.

To address this challenge, we define a refinement-based proof methodology that precisely relates concurrent code expressed at different abstraction levels, cognizant throughout of the relaxed memory semantics of the underlying processor. Our technique allows the compiler writer to reason compositionally about the atomicity of low-level concurrent code used to implement managed services.  We validate the effectiveness of our approach by demonstrating the verified compilation of the non-trivial components comprising a realistic concurrent garbage collector, including racy write barriers and memory allocators.

This is joint work with David Pichardie, Vincent Laporte, Gustavo Petri, and Jan Vitek.