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

Семинар по обещающей компиляции в ARMv8.3

Поведение многопоточных программ не может быть промоделировано попеременным последовательным исполнением различных потоков на одном вычислительном узле. На данный момент полное и корректное описание поведения многопоточных программ является открытой теоретической проблемой. Одним из перспективных решений этой проблемы является „обещающая“ модель памяти [Kang et al. POPL’17]. Для того, чтобы некоторая модель могла быть использована в стандарте некоторого промышленного языка программирования, должна быть доказана корректность компиляции из этой модели в модель памяти целевой процессорной архитектуры. В докладе мы рассмотрим доказательство корректности компиляции из подмножества обещающей модели в модель памяти процессора ARMv8.3 [Pulte et al. POPL’18]. Главной идеей доказательства является введение промежуточного операционного варианта модели ARMv8.3, поведение которого может быть симулировано обещающей моделью.

Доклад базируется на данной статье (полная версия доказательства тут).

Докладчик --- Антон Подкопаев

20.11.2017, 17:15.

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