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

Материал из 0x1.tv

(перенаправлено с «20191205AI»)
Докладчик
Егор Намаконов.jpg
Егор Намаконов

В настоящее время для языков программирования и процессоров активно разрабатываются модели памяти, направленные на решение различных проблем многопоточного программирования.

Так, модель памяти языка 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 в эту архитектуру.

Видео

on youtube

Посмотрели доклад? Понравился? Напишите комментарий! Не согласны? Тем более напишите.

Презентация

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

Примечания и ссылки


Plays:87   Comments:1