Compilation of OCaml memory model into Power

The development of memory models aimed at solving various concurrency problems is an active research topic. One such model is the OCaml memory model (OCamlMM), which allows to mitigate undefined behavior caused by data races. To use this model in practice one has to prove the correctness of its compilation into mainstream CPU architectures. At the moment, it is done for x86 and ARM but not for Power.One way to prove the correctness of compilation of OCamlMM into the Power model is to develop a compilation scheme from OCamlMM into the Intermediate Memory Model (IMM). It would be sufficient since there already exists a compilation scheme from IMM to the Power model. In this paper, the compilation scheme from OCamlMM into IMM is presented and proved to be correct. Memory fences and compare-and-swap instructions are used to permit only behavior allowed by OCamlMM. The resulting compilation scheme gives a correct compilation scheme from OCamlMM to the Power model. Moreover, when a compilation scheme from IMM into another CPU architecture will be developed, such an approach would immediately give a correct scheme of compilation of OCamlMM into that architecture.