Compiling OCaml memory model for Power (Egor Namakonov, ISPRASOPEN-2019)

Короткая ссылка: 20191205AI-

Speaker: Егор Намаконов

Currently, memory models are actively being developed for programming languages and processors aimed at solving various problems of multi-threaded programming.
Thus, the OCaml memory model (OCamlMM) allows to avoid undefined behavior caused by data races.
For application of this model in practice it is necessary to prove correctness of its compilation into widespread processor architectures. At the moment it is done for x86 and ARMv8 models, but not for Power.
In order to simplify the proof of OCamlMM compilation into Power model, it is suggested to build OCamlMM compilation scheme into Intermediate Memory Model (IMM).
This model has already been proven to compile correctly into the Power model and other architectures, so the proof of OCamlMM compiling correctly into the Power model comes down to the proof of OCamlMM compiling correctly into IMM.
This paper suggests the OCamlMM compilation scheme in IMM and proves it correctly. In this scheme memory barriers and compare-and-swap instructions are used, which allow to exclude the behavior allowed by IMM and prohibited by OCaml model.
The resulting Compilation Scheme gives the correct OCamlMM Compilation Scheme for the Power model. In addition, with this approach, you can prove that OCamlMM was compiled correctly to another architecture by proving that IMM was compiled correctly to that architecture.
Translation of http://0x1.tv/20191205AI