This page intentionally left blank. Verifying Compiler Transformations for Concurrent Programs

Compilers transform programs, either to optimize performance or to translate language-level constructs into hardware primitives. For concurrent programs, ensuring that a transformation preserves the semantics of the input program can be challenging. In particu-lar, the emitted code must correctly emulate the semantics of the language-level memory model when running on hardware with a relaxed memory model. In this paper, we present a novel proof methodology for prov-ing the soundness of compiler transformations for concurrent pro-grams. Our methodology is based on a new formalization of mem-ory models as dynamic rewrite rules on event streams. We imple-ment our proof methodology in a first-of-its-kind semi-automated tool called Traver to verify or falsify compiler transformations. Us-ing Traver, we prove or refute the soundness of several commonly used compiler transformations for various memory models. In this process, we find subtle bugs in the CLR JIT compiler and in the JSR-133 Java JIT compiler recommendations