1 ноября в Санкт-Петербурге пройдёт открытая лекция Антона Подкопаева Weak memory models. Приглашаем в БЦ «Таймс» — ул. Кантемировская д. 2, начало в 19:00.

Пожалуйста, зарегистрируйтесь: https://comscicenter.timepad.ru/event/1098222/

Антон — кандидат физико-математических наук, руководитель группы слабых моделей памяти в лаборатории языковых инструментов JetBrains Research, доцент департамента информатики НИУ ВШЭ (СПб) и постдок в MPI-SWS (Германия). Научные интересы: формальная верификация, сертификационный и функциональный стили программирования, семантика языков программирования.

На лекции речь пойдёт о моделях памяти в целом. Лектор расскажет, почему и как обещающая модель памяти решает существующие проблемы моделей памяти языков программирования, и затронет доказательства корректности компиляции из обещающей модели в модели x86-TSO, Power и ARMv8.3 с использованием промежуточной модели памяти (IMM).

Современные компиляторы и процессоры являются оптимизирующими. Из-за этого поведение многопоточных программ не получится полностью описать моделью памяти последовательной консистентности, т.е. как поочередное исполнение потоков на одном процессоре или ядре.

Существуют модели памяти для процессорных архитектур (x86, Power, ARM) и для языков программирования C/C++11, Java. Модели памяти C/C++ и Java являются частью стандартов языков, и у них есть недостатки. Недавно представленная обещающая модель памяти должна решить эти проблемы. Чтобы эта модель могла стать заменой моделей памяти C/C++ и Java, нужно показать наличие эффективной схемы компиляции из обещающей модели в модели памяти целевых процессорных архитектур.