On compilation correctness for a subset of a promising memory model to the ARMv8.3 memory model

A 'promising' memory model is an auspicious solution to the problem of defining semantics for an imperative language with concurrency, such as C/C++ or Java. An essential requirement for such a memory model is the existence of an effective and correct compilation scheme from the language to its target platforms. There are compilation correctness proofs from the promising model to x86 and Power as well as to an operational model ARMv8 POP. This paper presents such proof for an axiomatic memory model for ARMv8.3. In the proof, we use a new method of execution traversal, which might be used in other compilation correctness proofs for the promising memory model.