Исследовательская группа

Лаборатория языковых инструментов

Компиляция модели памяти OCaml в Power

25 ноября 2019

Одной из проблем слабых моделей памяти (к которым относятся модели Java, C++ и других современных языков) является то, что они дают слабые гарантии на поведение программ, содержащих гонки по данным. Для решения этой проблемы была предложена модель памяти OCaml, которая гарантирует последовательно согласованное исполнение всех участков программы, не содержащих гонок.

Для применения модели OCaml на практике необходимо построить для неё корректные схемы компиляции в распространённые архитектуры процессоров. Схема является корректной, если любой возможный результат исполнения скомпилированной программы допускается моделью памяти для исходной программы.

В докладе мы обсудим построение таких схем с помощью промежуточной модели памяти. Для этого мы рассмотрим, как можно представить исполнения программ в виде графов и выразить условие корректности компиляции через предикаты на этих графах.

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

Дополнительно