Современные компиляторы и процессоры являются оптимизирующими. Из-за этого поведение многопоточных программ не может быть полностью описано моделью памяти последовательной консистентности [Lamport:TC79], т.е. как поочередное исполение потоков на одном процессоре (ядре). На данный момент существуют модели памяти как для процессорных архитектур (x86, Power, ARM), так и для языков программирования (C/C++11, Java). Тем не менее, известно, что у моделей памяти C/C++ [Batty-al:POPL11] и Java [Manson-al:POPL05], которые являются частью стандартов языков, есть существенные недостатки. Недавно представленная обещающая модель памяти [Kang-al:POPL17] является перспективным решением этих недостатков. Для того, чтобы эта модель могла стать заменой моделей памяти C/C++ и Java, необходимо показать наличие эффективной схемы компиляции из обещающей модели в модели памяти целевых процессорных архитектур.

В этом докладе мы рассмотрим модели памяти в целом, почему и как обещающая модель памяти решает существующие проблемы моделей памяти языков программирования, а также рассмотрим доказательства корректности компиляции из обещающей модели в модели x86-TSO [Owens-al:TPHOL09], Power [Alglave-al:TOPLAS14] и ARMv8 POP [Flur-al:POPL16].