Компиляция модели памяти OCaml в Power (Егор Намаконов, ISPRASOPEN-2019)

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

Докладчик: Егор Намаконов

В настоящее время для языков программирования и процессоров активно разрабатываются модели памяти, направленные на решение различных проблем многопоточного программирования.
Так, модель памяти языка OCaml (OCamlMM) позволяет избежать неопределённого поведения, вызванного гонками по данным.
Для применения этой модели на практике необходимо доказать корректность её компиляции в распространённые архитектуры процессоров. На данный момент это выполнено для моделей x86 и ARMv8, но не для Power.
Для того, чтобы упростить доказательство корректности компиляции OCamlMM в модель Power, предлагается построить схему компиляции OCamlMM в промежуточную модель памяти (IMM).
Для этой модели уже доказана корректность компиляции в модель Power и другие архитектуры, поэтому доказательство корректности компиляции OCamlMM в модель Power сводится к доказательству корректности компиляции OCamlMM в IMM.
В данной работе предложена схема компиляции OCamlMM в IMM и доказана её корректность. В этой схеме используются барьеры памяти и инструкции compare-and-swap, которые позволяют исключить поведение, допустимое IMM и запрещённое моделью OCaml.
Полученная схема компиляции даёт корректную схему компиляции OCamlMM в модель Power. Кроме того, при таком подходе доказать корректность компиляции OCamlMM в другую архитектуру можно, доказав корректность компиляции IMM в эту архитектуру.