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

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