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

Семантика модели памяти высокоуровневого языка программирования должна допускать поведения многопоточной программы, полученные в результате выполнения оптимизаций компилятора. Многие предложенные ранее способы задания семантики слабой модели памяти были либо слишком строгими, либо, наоборот, слишком слабыми. Последнее может привести к появлению так называемых "значений из воздуха", т.е. контр-интуитивных поведений программы, которые нельзя наблюдать на практике, но которые допускаются формальной семантикой.

Недавно Чакраборти и Вафеядис предложили семантику слабой модели памяти, которая решает проблему "значений из воздуха". Новая семантика основана на структурах событий и выгодно отличается от альтернативных решений своей декларативностью. В докладе будет представлена семантика, основанная на структурах событий. Мы сравним её с альтернативной "обещающей" операционной семантикой. Также будет рассмотрена схема доказательства корректности компиляции из модели структур событий в промежуточную модель памяти.

Материалы к докладу:

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

Докладчик: Евгений Моисеенко