Лаборатория языковых инструментов
Семантика слабой модели памяти, основанная на структурах событий
Семантика модели памяти высокоуровневого языка программирования должна допускать поведения многопоточной программы, полученные в результате выполнения оптимизаций компилятора. Многие предложенные ранее способы задания семантики слабой модели памяти были либо слишком строгими, либо, наоборот, слишком слабыми. Последнее может привести к появлению так называемых "значений из воздуха", т.е. контр-интуитивных поведений программы, которые нельзя наблюдать на практике, но которые допускаются формальной семантикой.
Недавно Чакраборти и Вафеядис предложили семантику слабой модели памяти, которая решает проблему "значений из воздуха". Новая семантика основана на структурах событий и выгодно отличается от альтернативных решений своей декларативностью. В докладе будет представлена семантика, основанная на структурах событий. Мы сравним её с альтернативной "обещающей" операционной семантикой. Также будет рассмотрена схема доказательства корректности компиляции из модели структур событий в промежуточную модель памяти.
Материалы к докладу:
Soham Chakraborty and Viktor Vafeiadis. Grounding Thin-Air Reads with Event Structures \\ POPL'19
Anton Podkopaev, Ori Lahav, Viktor Vafeiadis. Bridging the Gap Between Programming Languages and Hardware Weak Memory Models \\ POPL'19
Докладчик: Евгений Моисеенко