Note: Talk will be at https://umd.zoom.us/my/mhicks2

Previously, researchers established some frameworks, such as Morpheus, to specify a compiler translation in a small language and prove the semantic preservation property of the translation in the language under the assumption of sequential consistency. Based on the Morpheus specification language, we extend the verification framework to prove the compiler translation semantic preservation property in a large real-world programming language with a real-world weak concurrency model. We named the framework as Morpheus+.

In this talk, we focus on a special part of the framework: K-LLVM, which is the complete semantics of LLVM IR. To the best of our knowledge, K-LLVM is the most complete formal LLVM IR semantics to date, including all LLVM IR instructions, intrinsic functions in the LLVM documentation and Standard-C library functions that are necessary to execute many LLVM IR programs. Additionally, K-LLVM formulates an abstract machine that executes all LLVM IR instructions. The machine allows to describe our formal semantics in terms of simulating a conceptual virtual machine that runs LLVM IR programs, including non-deterministic programs.

Besides, we will see how a compiler verification step can be done on top of K-LLVM by our Per-Location Simulation (PLS) framework. PLS is simple and suitable for proving that a compiled program semantically preserves its original program under a CFG-based language with a real-world, C/C++ like, weak memory model. To the best of our knowledge, PLS is the first simulation framework weaker than the CompCert/CompCertTSO one that is used for proving compiler correctness. With a combination of PLS, the compiler proof-framework Morpheus, and a language semantics with a weak memory model, we are able to prove that programs are semantically preserved through a transformation.