JetBrains Research — наука, меняющая мир

Семинар: Компиляция модели памяти OCaml в Power

Семинар: Компиляция модели памяти OCaml в Power

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

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

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

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

25.11.2019, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 2